Commit 036451a2 authored by Glen Mével's avatar Glen Mével
Browse files

ICFP21 paper: higher-level presentation of ghost state of queue (WIP)

parent 360187b3
......@@ -52,7 +52,9 @@ their views.
It is tied to the internal state of the queue via the use of an authoritative
ghost state, stored in a ghost variable~$\gqueue$.
%
It satisfies the following properties:
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.
%
In other words, the two assertions satisfy the following properties:
%
\begin{mathpar}
%
......@@ -62,11 +64,6 @@ It satisfies the following properties:
}{%
\tview = \tview'
\land \hview = \hview'
%\land \val_0 = \val'_0
%\land \eview_0 = \eview'_0
%\land ...
%\land \val_{\nbelems-1} = \val'_{\nbelems-1}
%\land \eview_{\nbelems-1} = \eview'_{\nbelems-1}
\land \Forall i. \val_i = \val'_i
\land \eview_i = \eview'_i
}
......@@ -84,62 +81,13 @@ It satisfies the following properties:
%
The first property asserts that the state known to the invariant (first premise) is identical to that known to the representation predicate (second premise).
%
The second property asserts that, whenever we own both the representation predicate and its counterpart which is usually stored in the invariant, 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.
To achieve these properties,
the value of the ghost variable~$\gqueue$ ranges over a CMRA whose
definition involves two standard Iris constructions:
%
\begin{itemize}%
The second property 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.
\item
For a given set~$S$,
the \emph{exclusive CMRA}, $\exm(S)$, is a trivial CMRA whose carrier set is
$S$ and whose composition is everywhere undefined.
It allows for ghost state whose value is drawn from an arbitrary set and
cannot be fragmented.
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}.
%\newcommand{\authboth}[2]{\authfull\!\!\authfrag (#1, #2)}
\item
For a given CMRA~$M$,%
\footnote{%
It is also required that $M$ possess an unit element, but we can
always add such an element artificially, so we omit this technical detail
for the sake of clarity.
}
the \emph{authoritative CMRA}, $\authm(M)$,
%is a CMRA whose elements are built from three constructors:
%$\authfull a$ for any element~$a$ of~$M$,
%$\authfrag b$ for any element~$b$ of~$M$, and combination thereof
%$\authboth{a}{b}$ for any $a$ and $b$ such that $b$ is included in $a$
%(by which we mean that there exists some $c$ such that $a = b \mtimes c$).
%Only the following compositions are defined:
%\begin{align*}%
% \authboth{a}{b} \mtimes \authfrag b' &\eqdef \authboth{a}{b \mtimes b'} &\text{if $b \mtimes b'$ is included in $a$} \\
% \authfull a \mtimes \authfrag b\hphantom' &\eqdef \authboth{a}{b} &\text{if $b$ is included in $a$} \\
% \authfrag b \mtimes \authfrag b' &\eqdef \authfrag (b \mtimes b')
%\end{align*}%
%It
allows for a ghost state where an authority knows the entirety of a ghost value whose ownership is split among a collection of clients.
On one side, the authoritative element~$\authfull a$ asserts full
knowledge of the global composition. This element is exclusive: it cannot be split.
On the other side, fragmentary elements~$\authfrag b$ assert knowledge of
fragments~$b$ of that same value; fragments can be split and combined.
Owning both an authority~$\authfull a$ and a fragment~$\authfrag b$ implies
that $b$ is included in $a$ (noted $b \mincl a$), by which we mean that
there exists some~$c$ such that $a = b \mtimes c$.
\end{itemize}%
%
Here, we use an authoritative CMRA to equate the public state
$\tuple{\tview, \hview, \elemViewList}$ provided by the representation predicate, to
the one that is known internally by the queue. The queue itself possesses the
authority in its internal invariant. Moreover, since we want the representation
predicate to provide the full public state, and not a partial fragment of it
(whatever that could mean), we compose the authoritative CMRA with the exclusive
CMRA: $\authm(\exm(-))$. In this way, there cannot be more than one fragment
(so, in fact, the authority and the fragment play symmetric roles).
This makes the representation predicate exclusive.
It is worth remarking that this construction makes the representation predicate exclusive: it is absurd to own simultaneously two assertions of the form $\isQueue - - -$.
\subsection{Internal invariant}
......@@ -166,7 +114,7 @@ Recall that in \hlog, $\nthpointstoAT\refstatuses\offset{\mkval{\status_\offset}
is the pointsto assertion for the atomic cell at index~\offset\ of
location~\refstatuses: it asserts the unique ownership of that cell, and states
that it currently contains the value $\status_\offset$ and the view
$\sview_\offset$ (or a better view).
$\sview_\offset$ (or a larger view).
%
Since we encode references as arrays of length~one,
$\pointstoAT\reftail{\mkval\tail\tview}$ is a shorthand for
......@@ -180,69 +128,86 @@ the authority on all three ghost variables, $\gqueue$, $\gmonos$ and $\gtokens$.
%
The authority of $\gqueue$ is simple: it simply ties internal values to the
public state of the queue, as explained earlier.
We now explain the other two pieces of ghost state.
\subsection{Monotonicity of statuses}
The purpose of the ghost variable~$\gmonos$ is to reflect the fact that statuses
are monotonic.
%
As we need this for every buffer offset, we use a map from offsets to an
adequate CMRA\@. For a given CMRA~$M$, \mbox{$\smash{\finmapm{\Z}{M}}$} is the CMRA
whose elements are finite partial functions from~$\Z$ to~$M$, and whose
composition is the pointwise composition. The invariant owns~$\gmonos$,
the value of which is
a map whose domain is the range $[0, \capacity)$.
%
Then, for a given offset~\offset, to reflect just the monotonicity of its status,
we would take for~$M$ the authoritative CMRA $\authm((\Z, \max))$.
% over the CMRA of
% integers where the composition of two integers is their maximum.
Indeed,
inclusion order~$(\mincl_\Z)$ for the CMRA $(\Z, \max)$ coincides with the usual order on
integers, so, from the joint ownership of $\mapsingleton\offset{\authfrag \status}$ and
$\mapsingleton\offset{\authfull \status'}$, we would deduce that
$\status \leq \status'$. Furthermore, by reading the status and observing its value
to be $\status$, we would obtain $\mapsingleton\offset{\authfrag \status}$,
which would act as a reminder that the status of slot~\offset\ cannot become
less than~$\status$.
In fact, because we are dealing with weak memory, it turns out that we need a stronger
property: statuses are \emph{strictly} monotonic.
% FP: il faudrait expliquer le lien entre la mémoire faible
% et le besoin de monotonie stricte. On n'aurait pas besoin
% de cela en SC?
As a consequence, as long as
the value of some status cell has not increased, we know that no write happened to
it. In particular, the view that this atomic cell contains has not augmented
either. This fact will be used in the proof.
%
Hence, we seek for~$M$ a CMRA structure on pairs of a status and a view,
%such that the inclusion order $\pair\status\sview \mincl_M \pair{\status'}{\sview'}$
%implies both the inequality $\status \leq \status'$ and the fact that,
%if $\status = \status'$, then $\sview \viewgeq \sview'$.
such that the inclusion order~$(\mincl_M)$ has the following implication:
More precisely, they are \emph{strictly} monotonic: every write to a status cell necessarily increases its value. As a consequence, as long as the value of a status cell has not increased, we know that no write happened to it and, in particular, that the view that it stores has not augmented either.
%
In other words, we have the monotonicity of the value-view pair stored in a status cell, for the lexicographic order where the order on views is reversed:
%
\[
\pair{\status_1}{\sview_1}
\sqsubseteq
\pair{\status_2}{\sview_2}
\mathlop{\Longleftrightarrow}
\status_1 < \status_2 \lor \left( \status_1 = \status_2 \land \sview_1 \viewgeq \sview_2 \right)
\]
%
This stronger monotonicity property will be used in the proof---specifically, when verifying \trydequeue---and specifying it is thus an additional requirement of working with a weak memory model.
To reflect monotonicity of the status of offset~$\offset$,
we use two assertions,
$\ownGhost \gmonos {\mapsingleton\offset{\authfull \pair\status\sview}}$
and $\monoWitness \offset {\pair\status\sview}$,
connected via a ghost variable~$\gmonos$.
%
The first assertion, owned by the invariant of the queue, implies that the value-view pair stored in the status cell is exactly $\pair\status\sview$.
In addition, it is exclusive: for any offset~$\offset$, not two assertions
of the form $\ownGhost \gmonos {\mapsingleton\offset{\authfull -}}$ can hold simultaneously.
%
The second assertion means that the value-view pair stored in the status cell is at least $\pair\status\sview$.
Importantly, a witness assertion is persistent: once it has been established, it remains true forever.
We thus have the following properties:
%
\begin{mathpar}
%
\infer{~}{\persistent{\monoWitness \offset {\pair\status\sview}}}
\infer{%
\pair\status\sview \mincl_M \pair{\status'}{\sview'}
\ownGhost \gmonos {\mapsingleton\offset{\authfull \pair\status\sview}}
\ISEP \monoWitness \offset {\pair{\status'}{\sview'}}
}{%
\status \leq \status' \LAND (\status = \status' \IMPLIES \sview \viewgeq \sview')
\pair{\status'}{\sview'} \sqsubseteq \pair\status\sview
}
\infer{%
\ownGhost \gmonos {\mapsingleton\offset{\authfull \pair\status\sview}}
\ISEP \pair\status\sview \sqsubseteq \pair{\status'}{\sview'}
}{%
\upd
\ownGhost \gmonos {\mapsingleton\offset{\authfull \pair{\status'}{\sview'}}}
\ISEP \monoWitness \offset {\pair{\status'}{\sview'}}
}
%
\end{mathpar}
%
In other words, the inclusion order is the lexicographic order where the order
on views is reversed.
The first property is the persistency just mentioned. The second property is the fact that a witness gives a lower bound on what the status cell currently stores.
%
The last property asserts that we can update a status cell to any larger or equal contents, and obtain a witness for that contents.
We achieve these properties by constructing an adequate CMRA for the values taken by the ghost variable~$\gmonos$. Again, we will not explain standard Iris constructs here, except for one point.
%
The construction involves building a CMRA
whose carrier set is $\Z \times \typeView$, the set of status-view pairs,
and whose inclusion order%
\footnote{%
For two elements $a$ and $b$ of a CMRA~$M$,
we say that $b$ is included in $a$
if there exists some~$c$ such that $a = b \mtimes c$.
}
coincides with the desired order $\sqsubseteq$.
%
A general recipe for deriving a CMRA structure with a given inclusion order, if
that order admits binary joins, consists in taking the join operation as the
composition of the CMRA\@~\cite{timany2021monotonicity}.
In this case, we equip the product set \(\Z \times \typeView\) with
the following join-semilattice structure:
%
% GLEN: recall here that views form a lattice, so they also have a meet.
%
\[\begin{array}{@{}rcl@{}}%
\statusViewLat
&\eqdef&
......@@ -269,39 +234,6 @@ the following join-semilattice structure:
\end{cases}%
\end{array}\]%
To sum up, the ghost variable~$\gmonos$ takes its values from the CMRA
$\finmapm{\Z}{\authm(\statusViewLat)}$ and, with the assertion
$\monoWitness\offset{\pair\status\sview}$ defined as in \fref{fig:queue:inv},
we get the following:
%
\begin{mathpar}
%
\infer{%
\monoWitness{\offset}{\pair\status\sview}
\ISEP \ownGhost\gmonos{\mapsingleton \offset {\authfull \pair{\status'}{\sview'}}}
}{%
\status \leq \status' \LAND (\status = \status' \IMPLIES \sview \viewgeq \sview')
}
%
\end{mathpar}
%
Thus the assertion $\monoWitness\offset{\pair\status\sview}$ acts as a reminder that, at some point, the status of slot~\offset\ stored the value~$\status$ and the view~$\sview$.
%
We also get the following rule for updating this piece of ghost state to a larger value, according to the desired order:
%
\begin{mathpar}
%
\infer{%
\ownGhost\gmonos{\mapsingleton \offset {\authfull \pair{\status}{\sview}}}
\ISEP \pair{\status}{\sview} \sqsubseteq \pair{\status'}{\sview'}
}{%
\upd
\ownGhost\gmonos{\mapsingleton \offset {\authfull \pair{\status'}{\sview'}}}
\ISEP \monoWitness{\offset}{\pair{\status'}{\sview'}}
}
%
\end{mathpar}
\subsection{Description of slots}
The last two lines of the invariant describe the state of each slot.
......
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