@@ -6,11 +6,11 @@ The model of Iris lives in the category of \emph{Complete Ordered Families of Eq
This definition varies slightly from the original one in~\cite{catlogic}.
\begin{defn}[Chain]
Given some set $\cofe$ and an indexed family $({\nequiv{n}}\subseteq\cofe\times\cofe)_{n \in\mathbb{N}}$ of equivalence relations, a \emph{chain} is a function $c : \mathbb{N}\to\cofe$ such that $\All n, m. n \leq m \Ra c (m)\nequiv{n} c (n)$.
Given some set $\cofe$ and an indexed family $({\nequiv{n}}\subseteq\cofe\times\cofe)_{n \in\nat}$ of equivalence relations, a \emph{chain} is a function $c : \nat\to\cofe$ such that $\All n, m. n \leq m \Ra c (m)\nequiv{n} c (n)$.
\end{defn}
\begin{defn}
A \emph{complete ordered family of equivalences} (COFE) is a tuple $(\cofe, ({\nequiv{n}}\subseteq\cofe\times\cofe)_{n \in\mathbb{N}}, \lim : \chain(\cofe)\to\cofe)$ satisfying
A \emph{complete ordered family of equivalences} (COFE) is a tuple $(\cofe, ({\nequiv{n}}\subseteq\cofe\times\cofe)_{n \in\nat}, \lim : \chain(\cofe)\to\cofe)$ satisfying
\begin{align*}
\All n. (\nequiv{n}) ~&\text{is an equivalence relation}\tagH{cofe-equiv}\\
\All n, m.& n \geq m \Ra (\nequiv{n}) \subseteq (\nequiv{m}) \tagH{cofe-mono}\\
...
...
@@ -115,7 +115,7 @@ Since Iris ensures that the global ghost state is valid, this means that we can
\subsection{CMRA}
\begin{defn}
A \emph{CMRA} is a tuple $(\monoid : \COFEs, (\mval_n \subseteq\monoid)_{n \in\mathbb{N}},\\\mcore{{-}}: \monoid\nfn\maybe\monoid, (\mtimes) : \monoid\times\monoid\nfn\monoid)$ satisfying:
A \emph{CMRA} is a tuple $(\monoid : \COFEs, (\mval_n \subseteq\monoid)_{n \in\nat},\\\mcore{{-}}: \monoid\nfn\maybe\monoid, (\mtimes) : \monoid\times\monoid\nfn\monoid)$ satisfying:
\begin{align*}
\All n, \melt, \meltB.&\melt\nequiv{n}\meltB\land\melt\in\mval_n \Ra\meltB\in\mval_n \tagH{cmra-valid-ne}\\
\All n, m.& n \geq m \Ra\mval_n \subseteq\mval_m \tagH{cmra-valid-mono}\\
...
...
@@ -136,7 +136,7 @@ Since Iris ensures that the global ghost state is valid, this means that we can
This is a natural generalization of RAs over COFEs.
All operations have to be non-expansive, and the validity predicate $\mval$ can now also depend on the step-index.
We define the plain $\mval$ as the ``limit'' of the $\mval_n$:
\All n. n \in\melt.V \Ra\melt.c(n) \nequiv{n}\meltB.c(n) \\
% \All n \in {\melt.V}.\, \melt.x \nequiv{n} \meltB.x \\
...
...
@@ -131,11 +131,11 @@ You can think of the $c$ as a \emph{chain} of elements of $\cofe$ that has to co
The reason we store a chain, rather than a single element, is that $\agm(\cofe)$ needs to be a COFE itself, so we need to be able to give a limit for every chain of $\agm(\cofe)$.
However, given such a chain, we cannot constructively define its limit: Clearly, the $V$ of the limit is the limit of the $V$ of the chain.
But what to pick for the actual data, for the element of $\cofe$?
Only if $V =\mathbb{N}$ we have a chain of $\cofe$ that we can take a limit of; if the $V$ is smaller, the chain ``cancels'', \ie stops converging as we reach indices $n \notin V$.
Only if $V =\nat$ we have a chain of $\cofe$ that we can take a limit of; if the $V$ is smaller, the chain ``cancels'', \ie stops converging as we reach indices $n \notin V$.
To mitigate this, we apply the usual construction to close a set; we go from elements of $\cofe$ to chains of $\cofe$.
We define an injection $\aginj$ into $\agm(\cofe)$ as follows:
\[\aginj(x)\eqdef\record{\mathrm c \eqdef\Lam\any. x, \mathrm V \eqdef\mathbb{N}}\]
\[\aginj(x)\eqdef\record{\mathrm c \eqdef\Lam\any. x, \mathrm V \eqdef\nat}\]
There are no interesting frame-preserving updates for $\agm(\cofe)$, but we can show the following:
The last two are the tokens used for managing invariants, $\textmon{Inv}$ is the monoid used to manage the invariants themselves.
Finally, $\textmon{State}$ is used to provide the program with a view of the physical state of the machine.
...
...
@@ -28,7 +28,7 @@ Furthermore, we assume that instances named $\gname_{\textmon{State}}$, $\gname_
\paragraph{World Satisfaction.}
We can now define the assertion $W$ (\emph{world satisfaction}) which ensures that the enabled invariants are actually maintained:
\begin{align*}
W \eqdef{}&\Exists I : \mathbb N\fpfn\Prop.
W \eqdef{}&\Exists I : \nat\fpfn\Prop.
\begin{array}{@{} l}
\ownGhost{\gname_{\textmon{Inv}}}{\authfull
\mapsingletonComp{\iname}
...
...
@@ -47,7 +47,7 @@ The following assertion states that an invariant with name $\iname$ exists and m
Next, we define \emph{view updates}, which are essentially the same as the resource updates of the base logic ($\Sref{sec:base-logic}$), except that they also have access to world satisfaction and can enable and disable invariants:
\[\pvs[\mask_1][\mask_2]\prop\eqdef W *\ownGhost{\gname_{\textmon{En}}}{\mask_1}\wand\upd\diamond(W *\ownGhost{\gname_{\textmon{En}}}{\mask_2}*\prop)\]
Here, $\mask_1$ and $\mask_2$ are the \emph{masks} of the view update, defining which invariants have to be (at least!) available before and after the update.
We use $\top$ as symbol for the largest possible mask, $\mathbb N$, and $\bot$ for the smallest possible mask $\emptyset$.
We use $\top$ as symbol for the largest possible mask, $\nat$, and $\bot$ for the smallest possible mask $\emptyset$.
We will write $\pvs[\mask]\prop$ for $\pvs[\mask][\mask]\prop$.
%
View updates satisfy the following basic proof rules:
...
...
@@ -369,14 +369,14 @@ Furthermore, we will often know that namespaces are \emph{disjoint} just by look
The namespaces $\namesp.\texttt{iris}$ and $\namesp.\texttt{gps}$ are disjoint no matter the choice of $\namesp$.
As a result, there is often no need to track disjointness of namespaces, we just have to pick the namespaces that we allocate our invariants in accordingly.
Formally speaking, let $\namesp\in\textlog{InvNamesp}\eqdef\List(\mathbb N)$ be the type of \emph{invariant namespaces}.
Formally speaking, let $\namesp\in\textlog{InvNamesp}\eqdef\List(\nat)$ be the type of \emph{invariant namespaces}.
We use the notation $\namesp.\iname$ for the namespace $[\iname]\dplus\namesp$.
(In other words, the list is ``backwards''. This is because cons-ing to the list, like the dot does above, is easier to deal with in Coq than appending at the end.)
The elements of a namespaces are \emph{structured invariant names} (think: Java fully qualified class name).
They, too, are lists of $\mathbb N$, the same type as namespaces.
In order to connect this up to the definitions of \Sref{sec:invariants}, we need a way to map structued invariant names to $\mathbb N$, the type of ``plain'' invariant names.
Any injective mapping $\textlog{namesp\_inj}$ will do; and such a mapping has to exist because $\List(\mathbb N)$ is countable.
They, too, are lists of $\nat$, the same type as namespaces.
In order to connect this up to the definitions of \Sref{sec:invariants}, we need a way to map structued invariant names to $\nat$, the type of ``plain'' invariant names.
Any injective mapping $\textlog{namesp\_inj}$ will do; and such a mapping has to exist because $\List(\nat)$ is countable.
Whenever needed, we (usually implicitly) coerce $\namesp$ to its encoded suffix-closure, \ie to the set of encoded structured invariant names contained in the namespace: \[\namecl\namesp\eqdef\setComp{\iname}{\Exists\namesp'. \iname=\textlog{namesp\_inj}(\namesp' \dplus\namesp)}\]
We will overload the notation for invariant assertions for using namespaces instead of names: