@@ -106,30 +106,30 @@ the queue. Since any thread can change it at any moment, no thread can

know the current state to be some list $\elemList$.

%

We may give a weaker specification by guaranteeing only that all of the

elements stored in the queue satisfy some predicate~$P$.

elements stored in the queue satisfy some predicate~$\Phi$.

%

\[\begin{array}{lcr}

\hoareV

{\queueInv\isep\isQueueSC P\isepP\,\elem}

{\isQueueSEQ\Phi\isep\Phi\,\elem}

{\enqueue~\queue~\elem}

{\Lam\Unit. \isQueueSC P}

{\Lam\Unit. \isQueueSEQ\Phi}

\qquad

\hoareV

{\queueInv\isep\isQueueSC P}

{\isQueueSEQ\Phi}

{\dequeue~\queue}

{\Lam\elem. \isQueueSC P\isepP\,\elem}

{\Lam\elem. \isQueueSEQ\Phi\isep\Phi\,\elem}

\end{array}\]

This is not satisfactory, as we lose most structural properties of a queue: the

same specification could also describe a stack, a bag.

%% or even (if $P$ is

%% or even (if $\Phi$ is

%% duplicable) a single memory cell always returning the same value.

% FP la remarque sur P duplicable est un peu étrange, car a priori

% la file est polymorphe en P donc ne peut pas avoir ce comportement.

% FP la remarque sur \Phi duplicable est un peu étrange, car a priori

% la file est polymorphe en \Phi donc ne peut pas avoir ce comportement.

% de plus une cellule mémoire unique = une file de capacité 1,

% donc ce n'est pas vraiment un exemple différent des précédents.

...

...

@@ -143,35 +143,49 @@ Unfortunately, $\enqueue$ and $\dequeue$ perform complex operations and are not

% "that is stable in the face of interference by other threads",

% ça évoquerait une terminologie standard.

% TODO: explain logical atomicity

% \cite[\S7]{iris-15}

% \cite{jung-slides-2019}

The idea of logical atomicity~\cite[\S7]{jung-slides-2019,iris-15} aims at addressing that difficulty.

When using this concept, instead of using ordinary Hoare triples, we use \emph{logically atomic triples}.

This kind of triple are like Hoare triples: they specify a program fragment, have a precondition and a postcondition.

The core difference being that they allow the opening of invariants around the triple

allows to write the specification shown

in~\fref{fig:queue:specsc}. It closely resembles that of the sequential setting

(\fref{fig:queue:specseq}). Differences are that the assertion describing the

state of the queue ($\isQueueSC\elemList$) now talks about the ghost

name~$\gqueue$, that the invariant of the queue ($\queueInv$) is an additional

precondition of both operations (repeating it in the postcondition is unneeded,

as it is persistent) and that \emph{atomic} Hoare triples are used.

%

The universal quantifier ($\forall\nbelems, \elemList*[]{.}$) is part of the

syntax of an atomic triple: it binds the following variables in the precondition as

well as in the postcondition.

% FP on peut se demander ce que signifie intuitivement cette spec,

% et surtout comment elle peut être exploitée utilement par un

% client.

The core difference being that they allow the opening of 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

% TODO : référencer la section

and given with more all details in previous work~\cite[\S7]{jung-slides-2019,iris-15}.

In order to get a good intuition, let's 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.

This linearization point being atomic, it allows the opening of invariants just like atomic instructions.

Using logically atomic triples, the specification can be written as shown

in~\fref{fig:queue:specsc}.

It closely resembles that of the sequential setting (\fref{fig:queue:specseq}).

The first difference that can be seen is the use of angle brackets $\anglebracket{\ldots}$ denoting logically atomic triples instead of curly brackets $\curlybracket{\ldots}$ for ordinary Hoare triples.

Another difference is the presence of embedded universal quantifiers ($\forall\nbelems, \elemList*[]{.}$) in the syntax of logically atomic triples.

These additional bindings address a subtlety of logical atomicity: indeed, recall that the precondition and the postcondition are to be interpreted at the linearization point.

However, the state of the shared queue is not known in advance by the client when calling the functions $\enqueue$ and $\dequeue$: instead, both the preconditions and the postconditions need to be parameterized by said shared state.

Said otherwise, since we do not know in advance when executing a program fragment the state of the shared resource at the linearization point, a logically atomic triple provides a \emph{familly} of pre/postcondition pairs covering all the possible shared states at the linearization point.

The last difference of the sequentially consistent concurrent specification is the splitting of the representation predicate into the two parts $\isQueueSC\elemList$ and $\queueInv$, linked by the ghost name $\gqueue$.

That splitting is an artifact of our correctness proof techniques which we detail in

% TODO : section de la preuve de la queue.

.

Note that this does not complicate the use of the queue by the client: both parts of the representation predicate are produced at the same time when creating the queue, and the part $\queueInv$, which cannot be shared using an invariant (since it is mentioned as a general premise rather than in the pre/postconditions of the logically atomic triples) is persistent and therefore freely duplicated and shared among threads.

% FP il serait sans doute bon d'affirmer (et d'expliquer) que

% que cette spec avec des triplets logiquement atomiques

% permet de retrouver la spec faible où tous les éléments

% satisfont un prédicat P

% satisfont un prédicat \Phi

The use of such a specification in a concrete example will be detailed in

% TODO : référence Section pipeline

.

For now, note that it is easy to deduce from this specification a weaker specification such as the one described above where each element of the queue should satisfy a predicate $\Phi$.

Indeed, after creating the queue (and getting the assertions $\isQueueSC{[]}$ and $\queueInv$), one simply has to create the new Iris invariant $\knowInv{}{\Exists\nbelems, \elemList*[]. \isQueueSC\elemList\isep\Phi\,\nthElem{0}\isep\cdots\isep\Phi\,\nthElem{\nbelems-1}}$, which is trivial to initialize when holding $\isQueueSC{[]}$.

Then, for proving the weaker specification of $\enqueue$ and $\dequeue$, one simply has to open the invariant around the logically atomic triple.

% TODO : faut-il en dire plus, ou est-ce compréhensible tel quel?

%% Indeed, after creating the queue (and getting the assertions $\isQueueSC{[]}$ and $\queueInv$), one simply has to create the new Iris invariant $\knowInv{}{\Exists \nbelems, \elemList*. A%% \isQueueSC\elemList