Commit 5cebdd9e authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Gagner de la place pour éviter le gros blanc de la page 18.

parent 7e41ef3c
......@@ -68,15 +68,16 @@ ghost state, stored in a ghost variable~$\gqueue$.
%
More precisely, the public state is kept in sync with the values which appear in an authoritative assertion $\ownGhost\gqueue{\authfull \tuple{\tview, \hview, \elemViewList}}$, the latter being owned by the internal invariant.
Formally, the two assertions satisfy the properties shown in~\fref{fig:queue:axioms:isqueue}.
The two assertions satisfy the properties shown in~\fref{fig:queue:axioms:isqueue}.
%
Rule~\ruleIsQueueAg asserts that the state known to the invariant (first premise) is identical to that known to the representation predicate (second premise).
%
Rule~\ruleIsQueueUpd asserts that, whenever we own both the representation predicate and its authoritative counterpart, we can update the public state to any other value by taking a \emph{ghost update} step. The symbol~$\upd$ is an Iris modality which represents such a ghost update.
Rule~\ruleIsQueueUpd asserts that, whenever we own both the representation predicate and its authoritative counterpart, we can update the public state to any other value by taking a \emph{ghost update} step.
Such a ghost update is allowed by the Iris modality denoted $\upd$.
We achieve these properties by using an adequate CMRA for the values of the ghost variable~$\gqueue$.
We build this CMRA by composing several classical Iris constructs; namely, the exclusive CMRA $\exm(S)$ where $S$ is a set, and the authoritative CMRA $\authm(M)$ where $M$ is a CMRA\@.
We do not explain the construction in more detail; the interested reader may refer to the documentation of Iris~\cite{iris}.
This CMRA is built by composing several classical Iris constructs: the exclusive CMRA $\exm(S)$, and the authoritative CMRA $\authm(M)$.
We do not explain the construction in more detail; we refer the interested reader to the documentation of Iris~\cite{iris}.
It is worth remarking that this construction makes the representation predicate exclusive: it is absurd to own simultaneously two assertions of the form $\isQueue - - -$.
......@@ -115,7 +116,7 @@ $\nthpointstoAT\reftail0{\mkval\tail\tview}$.
Apart from this physical state, the invariant also stores ghost state. It owns
the authority on all three ghost variables, $\gqueue$, $\gmonos$ and $\gtokens$.
%
The authority of $\gqueue$ is simple: it simply ties internal values to the
The authority of $\gqueue$ is simple: it ties internal values to the
public state of the queue, as explained earlier.
We now explain the other two pieces of ghost state.
......@@ -149,7 +150,7 @@ connected via a ghost variable~$\gmonos$.
Relevant definitions appear in~\fref{fig:queue:inv:witness}.
%
The first assertion, owned by the invariant of the queue is connected by the invariant to the value-view pair stored in the status cell.
In addition, it is exclusive: for any offset~$\offset$, two assertions
It is exclusive: for any offset~$\offset$, two assertions
of the form $\ownGhost \gmonos {\mapsingleton\offset{\authfull -}}$ cannot hold simultaneously.
%
The second assertion $\monoWitness \offset {\pair\status\sview}$ means that the value-view pair stored in the status cell is at least $\pair\status\sview$.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment