@@ -254,126 +253,41 @@ We obtain the following frame-preserving update:
% \end{proof}
% %\subsection{Disposable monoid}
% %
% %Given a monoid $M$, we construct a monoid where, having full ownership of an element $\melt$ of $M$, one can throw it away, transitioning to a dead element.
% %Let \dispm{M} be the monoid with carrier $\mcarp{M} \uplus \{ \disposed \}$ and multiplication
% %% The previous unit must remain the unit of the new monoid, as is is always duplicable and hence we could not transition to \disposed if it were not composable with \disposed
% % {a \in \mcarp{M} \setminus \{\munit_M\} \and \All b \in \mcarp{M}. a \sep b \Ra b = \munit_M}
% % {a \mupd \disposed}
% %\end{mathpar}
% %
% %\begin{proof}[Proof of \ruleref{DispUpd}]
% %Assume a frame $f$. If $f = \disposed$, then $a = \munit_M$, which is a contradiction.
% %Thus $f \in \mcarp{M}$ and we can use $a \mupd_M B$.
% %\end{proof}
% %
% %\begin{proof}[Proof of \ruleref{Dispose}]
% %The second premiss says that $a$ has no non-trivial frame in $M$. To show the update, assume a frame $f$ in $\dispm{M}$. Like above, we get $f \in \mcarp{M}$, and thus $f = \munit_M$. But $\disposed \sep \munit_M$ is trivial, so we are done.
% Given a monoid $M$, we construct a monoid modeling someone owning an \emph{authoritative} element $x$ of $M$, and others potentially owning fragments $\melt \le_M x$ of $x$.
% (If $M$ is an exclusive monoid, the construction is very similar to a half-ownership monoid with two asymmetric halves.)
% (x \mtimes y, \melt \mtimes \meltB) \quad \mbox{if } x \sep y \land \melt \sep \meltB \land (x \mtimes y = \munit_{\exm{\mcarp{M}}} \lor \melt \mtimes \meltB \leq_M x \mtimes y)
% \]
% Note that $(\munit_{\exm{\mcarp{M}}}, \munit_M)$ is the unit and asserts no ownership whatsoever, but $(\munit_{M}, \munit_M)$ asserts that the authoritative element is $\munit_M$.
% Let $x, \melt \in \mcarp M$.
% We write $\authfull x$ for full ownership $(x, \munit_M):\auth{M}$ and $\authfrag \melt$ for fragmental ownership $(\munit_{\exm{\mcarp{M}}}, \melt)$ and $\authfull x , \authfrag \melt$ for combined ownership $(x, \melt)$.
% If $x$ or $a$ is $\mzero_{M}$, then the sugar denotes $\mzero_{\auth{M}}$.
% \ralf{This needs syncing with the Coq development.}
% The frame-preserving update involves a rather unwieldy side-condition:
Given a CMRA $M$, we construct $\authm(M)$ modeling someone owning an \emph{authoritative} element $\melt$ of $M$, and others potentially owning fragments $\meltB\mincl\melt$ of $\melt$.
We assume that $M$ has a unit $\munit$, and hence its core is total.
(If $M$ is an exclusive monoid, the construction is very similar to a half-ownership monoid with two asymmetric halves.)
Note that $(\mnocore, \munit)$ is the unit and asserts no ownership whatsoever, but $(\exinj(\munit), \munit)$ asserts that the authoritative element is $\munit$.
% \subsection{Fractional heap monoid}
% \label{sec:fheapm}
Let $\melt, \meltB\in M$.
We write $\authfull\melt$ for full ownership $(\exinj(\melt), \munit)$ and $\authfrag\meltB$ for fragmental ownership $(\mnocore, \meltB)$ and $\authfull\melt , \authfrag\meltB$ for combined ownership $(\exinj(\melt), \meltB)$.
% By combining the fractional, finite partial function, and authoritative monoids, we construct two flavors of heaps with fractional permissions and mention their important frame-preserving updates.
% Hereinafter, we assume the set $\textdom{Val}$ of values is countable.
The frame-preserving update involves the notion of a \emph{local update}:
\newcommand\lupd{\stackrel{\mathrm l}{\mupd}}
\begin{defn}
It is possible to do a \emph{local update} from $\melt_1$ and $\meltB_1$ to $\melt_2$ and $\meltB_2$, written $(\melt_1, \meltB_1)\lupd(\melt_2, \meltB_2)$, if
\[\All n, \maybe{\melt_\f}. x_1\in\mval_n \land\melt_1\nequiv{n}\meltB_1\mtimes\maybe{\melt_\f}\Ra\melt_2\in\mval_n \land\melt_2\nequiv{n}\meltB_2\mtimes\maybe{\melt_\f}\]
\end{defn}
In other words, the idea is that for every possible frame $\maybe{\melt_\f}$ completing $\meltB_1$ to $\melt_1$, the same frame also completes $\meltB_2$ to $\melt_2$.
% Given a set $Y$, define $\FHeap(Y) \eqdef \textdom{Val} \fpfn \fracm(Y)$ representing a fractional heap with codomain $Y$.
% From \S\S\ref{sec:fracm} and~\ref{sec:fpfunm} we obtain the following frame-preserving updates as well as the fact that $\FHeap(Y)$ is cancellative.
% We will write $qh$ with $h : \textsort{Val} \fpfn Y$ for the function in $\FHeap(Y)$ mapping every $x \in \dom(h)$ to $(q, h(x))$, and everything else to $\munit$.
% Define $\AFHeap(Y) \eqdef \auth{\FHeap(Y)}$ representing an authoritative fractional heap with codomain $Y$.
% We easily obtain the following frame-preserving updates.
Given a state-transition system~(STS, \ie a directed graph) $(\STSS, {\stsstep}\subseteq\STSS\times\STSS)$, a set of tokens $\STST$, and a labeling $\STSL: \STSS\ra\wp(\STST)$ of \emph{protocol-owned} tokens for each state, we construct an RA modeling an authoritative current state and permitting transitions given a \emph{bound} on the current state and a set of \emph{locally-owned} tokens.
@@ -96,7 +96,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$.
We use $\top$ as symbol for the largest possible mask, $\mathbb N$, 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:
...
...
@@ -230,10 +230,10 @@ The following rules can all be derived inside the DC logic:
@@ -409,7 +409,7 @@ All we need to know is that this name is \emph{different} from the names of othe
Keeping track of the $n^2$ mutual inequalities that arise with $n$ invariants quickly gets in the way of the actual proof.
To solve this issue, instead of remembering the exact name picked for an invariant, we will keep track of the \emph{namespace} the invariant was allocated in.
Namesapces are sets of invariants, following a tree-like structure:
Namespaces are sets of invariants, following a tree-like structure:
Think of the name of an invariant as a sequence of identifiers, much like a fully qualified Java class name.
A \emph{namespace}$\namesp$ then is like a Java package: it is a sequence of identifiers that we think of as \emph{containing} all invariant names that begin with this sequence. For example, \texttt{org.mpi-sws.iris} is a namespace containing the invariant name \texttt{org.mpi-sws.iris.heap}.
...
...
@@ -434,7 +434,7 @@ We can now derive the following rules (this involves unfolding the definition of
