queue-spec-sc.tex

\subsection{Specification under sequential consistency}
\label{sec:queue:spec:sc}

We now consider the situation where several threads can access the queue concurrently.
Let us assume for now that the memory model is sequentially consistent~\cite{lamport-79}.
%
\citet{ohearn-07} devises \CSL, an extension of \SL that enables to reason
about programs where several threads can access the same piece of memory,
through the use of ``conditional critical regions''.
This logic spawned a variety of descendants; in this work, we use
Iris~\cite{iris}, a modular framework for building separation logics.

In a derivative of \CSL, we may retain the exact same specification as is presented
in~\fref{fig:queue:specseq}, recalling that $\isQueueSEQ\elemList$ is an
exclusive assertion:
a thread that has this assertion could safely assume to be the only one allowed
to operate on the queue.
%
The assertion would be transferable between threads via some means of
synchronization: for instance, we may use a lock to guard all operations on the
shared queue, following the approach of \CSL.
%
However this coarse grain concurrency has a run-time penalty,
and it also creates some contention on the use of the queue.
%
These costs are often unnecessary, as many data~structures are designed
specifically to support concurrent accesses. In this paper, as stated, we wish
to prove the correctness of a MRMW~queue implementation, which should thus
ensure, by itself, thread safety.
%
Hence we can achieve finer-grain concurrency, where operating on a queue does
not require its exclusive ownership. In this context, it is important that the
ownership of the queue can be shared among several threads.

One option to address this constraint in our specification is to provide the client
with a persistent assertion, instead of an exclusive representation predicate.
A challenge is then to describe the public state of the queue tightly enough so
that any client application can reason about it.
It is impossible for a thread to know exactly the current list of items, as any
thread can change it any moment.

For example, a possible but rather weak specification would only guarantee that
all of the elements stored in the queue satisfy some predicate~$\Phi$. This is
not satisfactory in the general case, as we lose most structural properties of
a queue: the same specification could also describe a stack or a bag.
%
\begin{mathpar}
%
  %\infer{}{%
  %  \persistent{\isQueuePers\Phi}
  %}
  %
  \infer{%
    \isQueuePers\Phi
  }{%
    \hoare
      {\Phi\,\elem}
      {\enqueue~\queue~\elem}
      {\Lam \Unit. \TRUE}
  }

  \infer{%
    \isQueuePers\Phi
  }{%
    \hoare
      {\TRUE}
      {\dequeue~\queue}
      {\Lam \elem. \Phi\,\elem}
  }
%
\end{mathpar}

% GLEN: j’ai reformulé les paragraphes présentant ces deux options, j’espère ne
% pas les avoir dénaturés. Si j’ai bien compris ce dont tu voulais parler,
% l’invariant dont on parle dans la 2e option n’est pas l’invariant interne de
% la structure de données (\queueInv), donc j’insiste ici sur le fait qu’on
% parle du côté client.
% Il me semble que dans cette présentation, la 2e option, avant qu’on parle de
% remplacer les triplets normaux par des triplets logiquement atomiques,
% consiste à garder la spec séquentielle telle quelle; c’est un peu étrange
% comme progression du discours, on a déjà dit au début de la sous-section qu’on
% pouvait le faire mais que ça n’était pas utilisable tel quel (il faudrait par
% exemple protéger la structure de données par un verrou) et qu’on voulait faire
% mieux. Du coup, la 1re option vient un peu comme une digression.
% Parler de la 1re option est-il nécessaire ?
% On pourrait dire quelque chose comme:
%     la queue est représentée par une ressource exclusive (qui confère sa
%     possession). Pour autoriser plusieurs participants, soit on transfère la
%     ressource d’un thread à l’autre via des synchros (physiques, telles qu’un
%     verrou), soit on la partage entre tous les threads via un invariant
%     (opération purement logique).
%     La 2e méthode n’est pas toujours applicable car, dans un cadre concurrent,
%     un invariant ne peut être ouvert qu’autour d’un fragment de programme
%     "atomique" dans un certain sens. Pour les invariants standards d’Iris, la
%     définition des programmes "atomiques" est trop restreinte (syntaxique
%     / opérationnelle) et ne s’applique pas ici.
%     Pourtant notre queue est thread-safe, enqueue et dequeue réalisent une
%     certaine forme empirique d’atomicité (de façon comparable à une section
%     critique protégée par un verrou). On introduit donc des triplets
%     logiquement atomiques, qui permettent d’ouvrir des invariants autour de
%     tels programmes.
% JH : Oui, je ne tiens pas à garder la première option. En fait, à vrai dire, je l'avais laissée parce que je pensais que tu y tenais. Ce que tu propose me semble très bien.
% => TODO : déplacer ceci en tant qu'exemple à la fin de la spec SC

Another option is to keep exposing a specification akin to that of~\fref{fig:queue:specseq}, that relies on an exclusive representation predicate allowing for the most exact description of the public state, and let clients share it themselves by applying a technique commonly used in Iris-like logics%
%to keep a precise description of the state that is stable in the face of interference by other threads
: one would typically place the exclusive ownership of the queue in an \emph{invariant}.
An invariant is an assertion which is agreed upon by all threads, and is owned by anyone; it remains true forever.
In this invariant, the client would also express which properties about the public state their particular application needs.
Then, when one of the threads needs to access the shared resource, it can \emph{open} the invariant, perform the shared state operations it needs, reestablish the invariant, and finally close it.
However, in order to be sound in the face of concurrency, the use of invariants in Iris needs to obey a strict constraint: they can remain open during at most a single step of execution.
Unfortunately, $\enqueue$ and $\dequeue$ perform complex operations that take more than one step of execution.

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 triples are like Hoare triples: they specify a program fragment, have a precondition and a postcondition.
The core difference is that they allow to open 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 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.
This linearization point being atomic, it allows the opening of invariants just like atomic instructions.
%
\begin{mathpar}
%
  \infer{%
    \lahoare <x> {P} {e} {Q}
  }{%
    \Forall x. \hoare {P} {e} {Q}
  }

  \infer{%
    \lahoare <x> {\later I \isep P} {e} {\later I \isep Q}
  }{%
    \knowInv{}{I} \vdash \lahoare <x> {P} {e} {Q}
  }
%
\end{mathpar}

% TODO: faire référence aux règles ci-dessus dans le texte.
% mentionner qu’un triplet log. atomique implique le triplet usuel ? (1re règle)
% I doit pouvoir parler de x, il me semble ?
% peut-être enlever le binder à cet endroit.

% TODO : expliquer la syntaxe des invariants, dire que \later est une technicité d'Iris

% JH : le mieux, c'est peut-être de mettre ces règles dasn une figure, et de s'y référer à plusieurs endroits:
% 1- regardez, on peut ouvrir des invariants autour d'un triplet logiquement atomique (oubliez le binder pour l'instant)
% 2- maintenant que je vous ai expliqué ce que c'est ce binder, vous voyez, il apparaît dans la syntax
% 3- tout à la fin de 2.2.2, on peut parler de transformer un triplet logiquement atomique en triplet de Hoare au moment où on parle de déduire la spec à base de \Phi.
% 3bis- Si on décide de ne pas parler de la spec à base de \Phi au début du paragraphe, soit on en parle à la fn de 2.2.2, parce que ça fait un bon exemple

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 ($\lahoarebinder{\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 \sref{sec:queue:proof}.
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$ is persistent and therefore freely duplicated and shared among threads.
% TODO : pour après la soumission : expliquer pourquoi QueueInv n'est pas caché dans isQueeu (footnote pour les experts d'Iris : ça rendrait isQueue non timeless, et on aurait une étape "abort" au début de enqueue/dequeue => pas impossible, mais plus compliqué)

The use of such a specification in a concrete example will be detailed in \sref{sec:pipeline:proof}.
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, one would simply define $\isQueuePers\Phi$ as the conjuction of $\queueInv$ and of the following Iris invariant:
\[
  \knowInv{}{\Exists \nbelems, \elemList*[]. \isQueueSC\elemList \isep \Phi\,\nthElem{0} \isep \cdots \isep \Phi\,\nthElem{\nbelems-1}}
\]
This is trivial to produce at the creation of the queue, when \make hands us the assertions $\queueInv$ and $\isQueueSC{[]}$.
Then, for proving the weaker specification of $\enqueue$ and $\dequeue$, one would open the invariant around the associated logically atomic triples.

%% 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
%%   %% \isep \displaystyle\Sep_{0 \leq i < \nbelems} \Phi %% \nthElem\idx
%%   $