Commit 8fbb02d3 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Changes in the proof section.

parent 6a5b8e3e
......@@ -11,17 +11,17 @@
We now turn on proving that the implementation shown in \sref{sec:queue:impl}
satisfies the functional specification of \sref{sec:queue:spec:weak} and
\fref{fig:queue:spec:weak}. The internal invariant $\queueInv$, as well as other
assertions that are useful in the proof, are shown in
\fref{fig:queue:inv}. It features several pieces of ghost state.
In the Iris methodology, which \hlog{} is based on, concurrent protocols are established thanks to \emph{ghost state} and \emph{invariants}.
Ghost state in Iris takes values from algebraic structures called CMRAs.
For the purpose of this paper, it is enough to think of a CMRA as a set
equipped with a binary composition operation $(\mtimes)$ that is partial,
associative and commutative.%
associative and commutative. %
%% \footnote{%
%% CMRAs are also step-indexed, but this is out of the scope of this paper.
%% }
% JH : j'ai viré ça. Je ne pense pas que ça apporte une quelconque information
Ghost state values are assigned to ghost variables.
The separation logic assertion~$\ownGhost\gname{a}$, where $a$ is an element of
some CMRA, intuitively means that we own a fragment of the ghost variable
......@@ -35,6 +35,10 @@ operation of the CMRA:
In \hlog, ghost state is objective (as it is independent from the physical state
of the memory).
Ghost state can be coupled with invariants such as the ones presented in \sref{sec:queue:spec:sc} to describe protocols that threads have to follow to access shared resources.
In \fref{fig:queue:inv}, we can see how this methodology is used for describing the internal protocol of the queue: the persistent predicate $\queueInv$ is in fact an invariant, the exclusive representation predicate $\isQueue\tview\hview\elemViewList$ is defined using ghost state, and several other internal resources are defined using ghost variables.
We detail these definitions in the following sections.
% TODO: ghost state updates
% useful RA constructions:
......@@ -59,11 +63,12 @@ involved CMRA uses two standard Iris constructions.
For a given set~$S$,%
In fact, $S$ must be an OFE, which in Iris is the step-indexed analog of
a set.
For a given set~$S$, %% %
%% \footnote{%
%% In fact, $S$ must be an OFE, which in Iris is the step-indexed analog of
%% a set.
%% }
% JH : je vire cette footnote : en réalité, ce n'est même pas faux de parler d'ensemble ici, puisque la notion d'ensemble dans la logique step-indicée coincide avec la notion d'OFE lorsqu'on regarde le modèle.
the \emph{exclusive CMRA}, $\exm(S)$, is a trivial CMRA whose carrier set is
$S$ and whose composition is defined nowhere.
It allows for ghost state whose value is drawn from an arbitrary set and
......@@ -91,9 +96,9 @@ involved CMRA uses two standard Iris constructions.
% \authfrag b \mtimes \authfrag b' &\eqdef \authfrag (b \mtimes b')
allows for a ghost state where a value~$a$ drawn from~$M$ is known from two sides.
allows for a ghost state where an authority knows the composition of the ghost states owned by a collection of clients.
On the one side, the authoritative element~$\authfull a$ asserts full
knowledge of that value; the authority is exclusive, it cannot be split.
knowledge of the global composition; the authority 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
......@@ -118,7 +123,7 @@ we provide the user with the persistent assertion $\queueInv$. It contains the
internal invariant governing the queue~$\queue$, whose public state is exposed
via the ghost variable~$\gqueue$. In addition to the public state, there are
two more ghost variables, named $\gmonos$ and $\gtokens$, which are hidden
to the user but which are needed by the queue operations. Thus they are
to the user but needed by the queue operations. Thus they are
existentially quantified in this persistent assertion. We will explain the
purpose and meaning of these ghost variables in a moment. For now, we look at
the internal invariant, $\queueInvInner$.
Supports Markdown
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