Commit 1547bc25 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Logicall atomicity

parent caebf38d
......@@ -505,7 +505,7 @@ write~tokens from~$\tail$ to~$\head$.
We have a last requirement: when an enqueuer is attributed rank~$\idx$, the new
item is added to the public state immediately---the CAS operation on \refhead
is the linearization point of enqueuing---even though the enqueuer has not
is the commit point of enqueuing---even though the enqueuer has not
actually written the item yet. When it finally returns the updated slot, the
enqueuer has lost track of the public state, which may have continued to
progress in the meantime. At that moment, it thus needs a reminder that the item
......@@ -556,81 +556,47 @@ strictly monotonic, and the fact that statuses are non-negative, are not explici
\subsection{Logical atomicity}
% GLEN: j’ai écrit une def des triplets LA car je crois qu’on en avait parlé
% mais la partie Abort ne nous sert à rien (et je n’ai pas vraiment écrit sa
% motivation).
The specification that we wish to prove is a logically atomic Hoare triple.
The definition of such a triple is given by~\citet[\S7]{iris-15} and
The definition of such triples is given by~\citet[\S7]{iris-15} and
further refined by~\citet{jung-slides-2019}. We do not attempt to replicate
their explanation and full definition. An approximate definition that suffices to
capture the essence of logical atomicity, and to understand our proof, is:
\delimiterfactor = 1200
\Forall \predB,
\left[ \mu U.\spac \pvs \Exists x.
P \ISEP (\laabort P U \LAND \lacommit \pred \predB)
\left[ \pvs[\top][\emptyset] \Exists x.
P \ISEP \left(\Forall v. \pred\;v \WAND\pvs[\emptyset][\top] \predB\;v\right)
\wpre e \predB
\laabort P U
\hphantom{\Forall v.} P \hphantom{\;v} \WAND\pvs U
\lacommit \pred \predB
\Forall v. \pred\;v \WAND\pvs \predB\;v
% JH : cette définition est incorrecte pour un "détail" important : comme elle ne mentionne pas les masques, on ne voit pas que le commit/abort doit avoir lieu de manière atomique. C'est important, parcqu'on a beaucoup dit plus haut que ça permettait d'ouvrir des invariants.
% Pas le temps de corriger ça pour la soumission, mais je laisse ce TODO pour la version finale.
In this formula,
the variables~$P$ and $U$ are Cosmo assertions (of type $\typeVProp$);
the variable~$P$ is a Cosmo assertion (of type $\typeVProp$);
the variables~$\pred$ and~$\predB$ are predicates on values (of type $\typeVal \ra \typeVProp$);
$P$ and $\pred$ may refer to the name~$x$.
The assertion $\wpre e \predB$ is the weakest precondition for program~$e$ and
(in Iris, Hoare triples are syntactic sugar for weakest preconditions).
The notation $\mu U.\spac F(U)$ designates a fixpoint of $F$, i.e.\ an
assertion~$U$ that is equivalent to its unrolling~$F(U)$.
To prove a logically atomic triple about program~$e$ with precondition~$P$
and postcondition~$\pred$ (possibly referring to a bound name~$x$), we have to
prove, for any postcondition~$\predB$, the weakest precondition of~$e$ and~$\predB$,
assuming the assertion between brackets.
This assertion~$U$ represents an \emph{atomic update}; it means that we can
perform a ghost update step ($\pvs$ is Iris’ update modality) to obtain $P$ and
\emph{either} $\laabort P U$ \emph{or} $\lacommit \pred \predB$, but not both,
at our convenience (since these two assertions are combined with a standard
conjunction instead of a separating conjunction).
In other words, we can consume $U$ to access the precondition~$P$, after which
we have two options for continuing the proof:
either we \emph{abort} the atomic update,
by returning the precondition $P$ intact to get~$U$ back (hence the fixpoint) after an update step;
or we \emph{commit} to it,
by providing the postcondition~$\pred$ to obtain $\predB$ after an update step.
Recall that $P$ and $\pred$ are to be understood as the precondition and
postcondition of the linearization point of~$e$.
We commit the atomic update during the execution of that atomic instruction:
we get~$P$ just before executing the instruction,
and must produce $\pred$ immediately afterwards.
%We do not otherwise have $P$ at hand.
However, we may need to access $P$ before the linearization point.
Aborting allows us to do so, as long as we return $P$ intact with no delay.
On the other side, committing consumes $U$, so after the linearization point
we cannot get $P$ anymore (nor commit again the same atomic update).
The goal of a logically atomic triple is to give the specification of a non-atomic term $e$ \emph{as if it were atomic}.
In practice, this means that we ask the proof of $e$ to access the precondition and turn it into the postcondition in \emph{one atomic step} only\footnote{In the full definition of logically atomic triples, it is actually possible to atomically access the precondition without turning it into the postcondition before the final commit. This is not needed for our proof, and out of the scope of this paper.}, which actually corresponds to the commit point of this logically atomic operation.
That is, if $e$ satisfies the triple $\lahoare<x>{P}{e}{\pred}$, then it can perform several steps of computations, but as soon as it accesses the resource $P$, it has to return the resource $\pred$ in the same step of computation.
Once it has returned $\pred$, then $e$ can proceed in executing further computation steps without accessing either $P$ or $\pred$.
As explained in \sref{sec:queue:spec:sc}, thanks to this constraint, the client of this specification is allowed to open an invariant around $e$, as if $e$ were atomic.
In order to capture this atomicity requirement, we ask the proof of the logically atomic triple for $e$ to be valid for any postcondition $\predB$ chosen by the client.
Given that $\predB$ is arbitrary, the only mean to establish this postcondition is by using the premise $\pvs[\top][\emptyset] \Exists x. P \ISEP (\Forall v. \pred\;v \WAND\pvs[\emptyset][\top] \predB\;v)$, called the \emph{atomic update}.
On demand, that atomic update gives access to the precondition $P$ for some value of $x$, and, in exchange to the postcondition $\pred$ of the logically atomic triple, it returns the resource $\predB$ which can then be used to finish the proof.
Crucially, the \emph{masks} $\emptyset$ and $\top$ annotating the \emph{fancy updates} $\pvs[\top][\emptyset]$ and $\pvs[\emptyset][\top]$ require that the atomic update is used during one atomic step only, as required.
Using the invariant rules of Iris~\cite{iris}, it is easy to show that atomic updates can be used to open and close invariants.
The rule \RULE{LAInv} follows as a corollary, and \RULE{LAHoare} is immediate.
\subsection{Proof of \tryenqueue}
......@@ -777,7 +743,7 @@ $\sview_\idx \viewleq \sview^1$. But we have $\seen\sview^1$ in our proof
context, so we obtain the pointsto assertion as a subjective assertion:
We commit the atomic update now. Indeed the successful CAS is the linearization
We commit the atomic update now. Indeed the successful CAS is the commit
point of \tryenqueue. We know that the program will return $\True$, so we must
provide the corresponding postcondition of the logically atomic triple, where
our item~$\pair\elem\eview$ has been appended to the public state of the queue.
......@@ -66,8 +66,8 @@ The core difference is that invariants can be opened around a logically atomic t
The definition of logically atomic triples is further discussed in~\sref{sec:queue:proof:la}
and given with detail in previous work~\cite[\S7]{jung-slides-2019,iris-15}.
We now try to give an intuition on that concept:
a logically atomic triple $\lahoare{P}{e}{Q}$ states, roughly, that the expression $e$ contains a linearization point which has $P$ as a precondition and $Q$ as a postcondition.
The triple then allows the opening of invariants around that linearization point
a logically atomic triple $\lahoare{P}{e}{Q}$ states, roughly, that the expression $e$ contains a commit point which has $P$ as a precondition and $Q$ as a postcondition.
The triple then allows the opening of invariants around that commit point
because it is an atomic instruction.
......@@ -108,11 +108,11 @@ Another difference is the presence, in the syntax of logically atomic triples,
of an explicit binder for some variables ($\nbelems, \elemList*[]$).
This binder addresses a subtlety of logical atomicity:
a client calling \enqueue or \dequeue does not know in advance
the state of the queue at the linearization point,
the state of the queue at the commit point,
which is when the precondition and postcondition are to be interpreted.
Hence, both formulas have to be parameterized by said shared state.
Said otherwise, a logically atomic triple provides a \emph{family} of pre/postcondition pairs
covering every possible shared state at the linearization point.
covering every possible shared state at the commit point.
The last departure from the sequential specification
is that the representation predicate is split into two parts:
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