Commit 7346a433 authored by Glen Mével's avatar Glen Mével
Browse files

definition of logically atomic triples

parent 3393863e
......@@ -101,3 +101,5 @@
\end{figure}
% JH : TODO : serait-ce pertinent de mentionner ici la timelessness et l'objectivité de isQueue et la persistence de queueInv? Cela fait partie de la spec, à mon sens.
% GLEN: la persistance oui, la timelessness c’est peut-être trop technique ?
% TODO: a-t-on dit quelque part que tous ces triplets atomiques ont implicitement \queueInv en hypothèse ?
......@@ -483,5 +483,117 @@ the proof of the specification: for example, \reftail and \refhead are
strictly monotonic, and statuses are non-negative.
\subsection{Proof of \tryenqueue}
\label{sec:queue:proof:tryenqueue}
We now outline the proof that \tryenqueue satisfies its specification
from~\fref{fig:queue:spec:weak}.
%
The proof for \trydequeue is similar; those for \enqueue and \dequeue are
deduced from the two previous by an obvious induction; and the proof of \make is
simply a matter of initializing the ghost state.
%
Being absolutely formal is not a goal of this text. The interested reader may
find these proofs, conducted in the Coq proof assistant, in~\cite{TODO}.
\subsubsection{Logical atomicity}
\label{sec:queue:proof:la}
The specification to prove is a logically atomic Hoare triple.
The definition of such a triple has been given in~\citep[\S7]{iris-15} and
further refined in~\citep{jung-slides-2019}. We do not attempt to replicate
their explanation and full definition. A simplified definition that suffices for
capturing the essence of logical atomicity, and following our proof, is:
%
\newcommand{\laabort}[2]{\mathrm{Abort}\;{#1}\;{#2}}%
\newcommand{\lacommit}[2]{\mathrm{Commit}\;{#1}\;{#2}}%
%
\[\begin{array}{rcl}%
\lahoare<x>{P}{e}{\varphi}
&\eqdef&
\delimiterfactor = 1200
\Forall \Phi,
\left[ \mu U.\spac \pvs \Exists x.
P \isep (\laabort P U \land \lacommit \varphi \Phi)
\right]
\wand
\wpre e \Phi
\\
\laabort P U
&\eqdef&
\hphantom{\Forall v.} P \hphantom{\;v} \wand\pvs U
\\
\lacommit \varphi \Phi
&\eqdef&
\Forall v. \varphi\;v \wand\pvs \Phi\;v
\end{array}\]%
In this formula,
the variables~$P$ and $U$ are Cosmo assertion (of type $\typeVProp$);
the variables~$\varphi$ and~$\Phi$ are predicates on values (of type $\typeVal \ra \typeVProp$);
$P$ and $\varphi$ may refer to the name~$x$.
%
The assertion $\wpre e \Phi$ is the weakest precondition for program~$e$ and
postcondition~$\Phi$
(in Iris, Hoare triples are syntactic sugar around weakest preconditions).
%
The notation $\mu U.\spac F(U)$ designates a fixpoint of $F$, i.e.\ an
assertion~$U$ which is equivalent to its unrolling~$F(U)$.
To prove the logically atomic triple about program~$e$, with precondition~$P$
and postcondition~$\varphi$ (maybe referring to a bound name~$x$), we have to
prove, for any postcondition~$\Phi$, the weakest precondition of~$e$ and~$\Phi$,
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 \varphi \Phi$, 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~$\varphi$ to obtain $\Phi$ after an update step.
Recall that $P$ and $\varphi$ 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 $\varphi$ just after.
%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).
\subsubsection{...}
Recalling here the specification, we ought to prove the following assertion:
\[\begin{array}{@{}l@{}}
\infer{%
\queueInv
}{\;\;\;%
\lahoareV
{\begin{array}{@{}l@{}}
\lahoarebinder{\tview, \hview, \nbelems, \elemViewList*[]}
\\ \hspace{2.9em}
\isQueue \tview {\hphantom(\hview\hphantom{{}\viewjoin\view)}} \elemViewList
\hphantom{, \pair\elem\view}
\isep \seen\view
\end{array}}
{\tryenqueue~\queue~\elem}
{\Lam \boolval.
\matchwithnobinder{\boolval}
{\False}{\isQueue \tview {\hphantom(\hview\hphantom{{}\viewjoin\view)}} \elemViewList}
{\True }{%
\isQueue \tview {(\hview \sqcup \view)} {\elemListSnoc \elemViewList {\pair\elem\view}}
\isep \seen\hview
}
}
\;\;\;}
\end{array}\]
% …
\hfill\pagebreak
......@@ -59,7 +59,7 @@ The idea of logical atomicity~\cite[\S7]{jung-slides-2019,iris-15} aims at addre
When using this concept, instead of using ordinary Hoare triples, we use \emph{logically atomic triples}.
This kind of triples are like Hoare triples: they specify a program fragment, have a precondition and a postcondition.
The core difference is that they allow opening invariants around the triple: in a sense, when a function is specified using logically atomic triples, one states that said function behaves just like if it were atomic.
The definition of logically atomic triples is further discussed in
The definition of logically atomic triples is further discussed in~\sref{sec:queue:proof:la}
% TODO : référencer la section
and given with detail in previous work~\cite[\S7]{jung-slides-2019,iris-15}.
In order to get a good intuition, let us consider an approximated definition of 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.
......@@ -67,13 +67,13 @@ This linearization point being atomic, it allows the opening of invariants just
%
\begin{mathpar}
%
\infer{%
\infer[LAHoare]{% using the rule names from \cite{iris-15}
\lahoare <x> {P} {e} {Q}
}{%
\Forall x. \hoare {P} {e} {Q}
}
\infer{%
\infer[LAInv]{% using the rule names from \cite{iris-15}
\lahoare <x> {\later I \isep P} {e} {\later I \isep Q}
}{%
\knowInv{}{I} \vdash \lahoare <x> {P} {e} {Q}
......
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