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

split queue-spec.tex, label subsections

parent 2bd78763
\subsubsection{Specification under sequential consistency}
\label{sec:queue:spec:sc}
We now consider the case where several threads access the queue concurrently. Let’s assume for now that
the memory model is sequentially consistent. % FP ajouter une référence?
%
We may retain the exact same specification as is presented
in~\fref{fig:queue:specseq}, recalling that $\isQueueSEQ\elemList$ is an
\emph{exclusive} resource.
% TODO: vérifier qu’on l’a bien dit précédemment, sinon ce n’est pas un rappel…
%
A thread that has this resource could safely assume to be the only one allowed
to operate on the queue.
%
The resource would be transferable between threads via some mean of
synchronization: for instance, we may use a lock to guard all operations on the
shared queue.
% FP noter que c'est l'approche de la logique de séparation concurrente
% traditionnelle, pioneered by \citet{ohearn-07}
However the implementation that we wish to prove correct is already thread-safe.
%Both $\enqueue$ and $\dequeue$ have a linearization point.
% FP Je ne sais pas forcément ce que signifie "linearization point",
% surtout que l'on parle d'une structure qui n'est pas (forcément)
% linéarisable, me semble-t-il. Supprimer cette ligne?
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.
%% the queue data~structure
%% will be described by an \emph{invariant}. It is a persistent assertion, that can
%% be freely duplicated and holds true for all threads.
%% % FP il me semble que "invariant" et "ghost state" sont des outils techniques
%% % qui participent à la preuve, mais ici on est en train de discuter la spec.
%% % Au niveau de la spec, il faut surtout pointer d'abord qu'on va avoir besoin
%% % de partager l'accès à la queue, donc 1- isQueue ne peut plus être exclusif;
%% % il doit être partagé d'une façon ou d'une autre (il pourrait être
%% % fractionnel ou persistant, par exemple) et 2- un participant ne peut
%% % plus espérer connaître avec certitude le contenu actuel de la queue.
%% %
%% We will denote our invariant as $\queueInv$; it connects the physical
%% queue~$\queue$ with a logical-level variable~$\gqueue$, which will be used to
%% describe the state of the queue (ghost state).
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.
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 invariant which is agreed upon by all the threads.
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 follow a strict constraint: they can only stay opened for an \emph{atomic} duration (i.e., during an atomic instruction, or be closed immediately after being opened).
Unfortunately, $\enqueue$ and $\dequeue$ perform complex operations and are not atomic.
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 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.
%
\begin{mathpar}
%
\infer{%
\lahoare <x> {P} {e} {Q}
}{%
\Forall x. \hoare {P} {e} {Q}
}
\infer{%
\lahoare <x> {I \isep P} {e} {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)
% later devant I ?
% I doit pouvoir parler de x, il me semble ?
% peut-être enlever le binder à cet endroit.
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
% 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 the client cannot share 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.
% GLEN: "which the client cannot share using an invariant" --> confusant ?
% il "peut", mais alors il ne sera pas en mesure d’utiliser les triplets
% logiquement atomiques qu’on lui fournit.
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, 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{[]}$
% TODO: ça laisse penser qu’il faut ajouter la spec de make en SC (et en
% séquentiel, pour la symétrie).
Then, for proving the weaker specification of $\enqueue$ and $\dequeue$, one would open the invariant around the associated logically atomic triples.
% TODO : faut-il en dire plus, ou est-ce compréhensible tel quel?
% GLEN: ça me semble suffisant (j’ai ajouté qu’il faut garder l’invariant
% interne, \queueInv, à côté).
%% 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
%% $
\subsubsection{Specification in a sequential setting}
\label{sec:queue:spec:seq}
A queue holding $\nbelems$ items \(\elemList*\), where the left extremity
of the list is the tail and the right extremity is the head,
is represented in separation logic with a predicate:
%
\[
\isQueueSEQ \elemList
\]
In a sequential setting, we can give a simple specification to the operations of
the queue, as presented in~\fref{fig:queue:specseq}. We use the standard Hoare
triple notation, with a partial correctness meaning.
%
If we own a queue~$\queue$, then we can $\enqueue$ some item~$\elem$
into~$\queue$; if this operation ever returns, then it must return the unit value~$\Unit$ and
give us back the ownership of~$\queue$, where $\elem$ has been appended at the head.
%
Conversely, if we own a queue~$\queue$, then we can $\dequeue$ from~$\queue$; if
this operation ever returns, then it must return the first item~$\elem_0$ found at
the tail of~$\queue$, and it gives us back the ownership of~$\queue$, where that
first item has been removed.
This specification implies that $\dequeue$ cannot possibly return when the queue is empty
($\nbelems = 0$); in this case, it must loop forever.
This is pointless in a sequential setting, but becomes meaningful
in the presence of concurrency,
where it makes sense for $\dequeue$ to wait until an item is
enqueued.
%
This specification also applies to bounded queues, where (somewhat analogously)
\enqueue loops when the capacity is reached ($\nbelems = \capacity$), waiting
until room becomes available.
\begin{figure}
\input{figure-queue-spec-seq}
\input{figure-queue-spec-sc}
\end{figure}
\subsubsection{Specification under weak memory}
\label{sec:queue:spec:weak}
\input{figure-queue-spec}
Up to now, we ignored the weakly consistent behavior of the semantics of \mocaml{}.
In this section, we lift this restriction, and propose a more precise specification for our concurrent queue implementation, which takes into account this aspect.
We will use the separation logic Cosmo~\citecosmo:
this framework has been designed on top of Iris in order to provide a powerful proof framework for the weak memory model of \mocaml{}.
Because Cosmo is based on Iris, logically atomic triples can also be defined in this logic.
In fact, the specification shown in~\fref{fig:queue:specsc} still applies.
However, as such, this specification is of little value in a weakly consistent context.
Indeed, as we explained in~\sref{sec:queue:spec:sc}, that specification is designed so that the representation predicate $\isQueueSC\elemList$ should be shared among threads by using an invariant.
But, in Cosmo, invariants are restricted to a special class of assertions, called \emph{objective} assertions.
As a result, the specification shown in~\fref{fig:queue:specsc} is useful in a weakly consistent context only if the representation predicate $\isQueueSC\elemList$ is objective.
Hence, the first addition in our specification to take into account weakly consistent behaviors is the objectiveness of $\isQueueSC\elemList$.
This correspond to asserting that the use of atomic accesses in the concurrent queue library is sufficient to maintain its linearizability.
In a weakly consistent context, the concurent queue library is not only linearizable: calls to the concurrent queue library also provides guarantees for memory accesses \emph{outside} of the queue.
In particular, our library guarantees \emph{happens-before} relationships between some function calls:
\begin{enumerate}%
\item from an enqueuer to the dequeuer that obtains the corresponding item;
\item from an enqueuer to the following enqueuers;
\item from a dequeuer to the following dequeuers.
\end{enumerate}%
These happens-before relationships are important to use the queue in practice.
For example, imagine that thread~$A$ enqueues a complex data structure in the queue (say, a hash table).
Then, when thread~$B$ dequeues the corresponding item, one naturally expects that thread~$B$ is able to access the data structure as if it were its unique owner (provided, of course, that thread~$A$ did not access the data structure once enqueued).
In a weakly consistent memory model, this is only possible if there is a happens-before relationship between enqueuing and dequeuing: otherwise, nothing guarantees that thread~$B$ has seen all the changes made by thread~$A$ to the data structure.
% TODO : il faut expliquer quelque part comment les relations happens-before s'expriment par des transferts de vues
We are able to express and prove these relationships within \hlog{} as transfers
of views. As seen later with the example of the pipeline, % FP pointeur?
this can be used for
transferring subjective resources from a sender to a receiver.
% FP as-tu expliqué l'idée de subjective resource? la notion de vue?
% et comment transférer une vue permet de transférer une ressource?
To reflect this,
the representation predicate now takes more parameters:
%
\[
\isQueue \tview \hview \elemViewList
\]
\begin{enumerate}%
\item For each item~$\elem_\idx$ in the queue, we now have a corresponding
view~$\eview_\idx$. This view represents the flow of memory information
from the thread which enqueued this item, to the one that will dequeue it.
\item The \textit{head} view~$\hview$ represents memory information
accumulated by successive enqueuers.
\item The \textit{tail} view~$\tview$ represents memory information
accumulated by successive dequeuers.
\end{enumerate}%
The queue, however, does not guarantee any happens-before relationship from
a dequeuer to an enqueuer.%
%
\footnote{%
This is not entirely true: the implementation that we study does create
a happens-before relationship from the dequeuer of rank~$\idx$ to the enqueuer of
rank~$\idx+\capacity$ (hence also to all enqueuers of subsequent ranks).
We choose to not reveal this in the specification.
}
%
Hence, by contrast with a sequential queue that would
be guarded by a lock, the concurrent queue is not linearizable, even though it
retains an interesting behavior that should suffice for many use cases.
% FP ce serait bien de donner un exemple de scénario où le comportement
% de la queue est conforme à la spec et néanmoins non linéarisable;
% sinon ça reste vague, je trouve
% FP "that should suffice for many use cases" n'est pas très convaincant.
% a-t-on une idée plus claire, un argument plus convaincant? quel
% serait le type de situation où cette queue ne convient pas et on
% a absolument besoin d'une queue linéarisable?
The full specification under weak memory is shown in~\fref{fig:queue:spec}.
It extends the previous specification (\fref{fig:queue:specsc}) with views as
just presented, capturing the mentioned happens-before relationships as follows.
\begin{enumerate}%
\item When a thread with a local view at least~$\view$ (in other words, with
$\seen\view$ as a precondition) $\enqueue$s an item~$\elem$, it pairs it
with the view~$\view$.
% FP il faudra ré-expliquer les notations Cosmo, et peut-être le principe
% de certaines règles de preuve, en particulier le fait que les lectures
% et écritures dans une case atomique transfèrent une vue
%
Afterwards, when another thread $\dequeue$s that same item~$\elem_0$, it
merges the view~$\eview_0$ that was paired with it into its own local view
(in other words, it obtains $\seen\eview_0$ as a postcondition).
\item When a thread $\enqueue$s an item, it also obtains the head~view~$\hview$
left by the previous enqueuer (in other words, it obtains $\seen\hview$ as
a postcondition), and it adds its own view~$\view$ to the head~view (which
becomes $\hview \viewjoin \view$).
\item When a thread $\dequeue$s an item, it also obtains the tail~view~$\tview$
left by the previous dequeuer (in other words, it obtains $\seen\tview$ as
a postcondition), and it adds its own view~$\view$ to the tail~view (which
becomes $\tview \viewjoin \view$).
\end{enumerate}%
This diff is collapsed.
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