Commit 5f517054 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Réunion.

parent 3dfe52a6
......@@ -53,11 +53,11 @@
\mid \ArrayReadAT\expr\expr
\mid \ArrayWriteAT\expr\expr\expr
\mid \ArrayCAS\expr\expr\expr\expr
& \text{--- operations on atomic cells}
\end{array}\]
\[\begin{array}{r@{\;}r@{\;}ll}%
& \text{--- operations on atomic cells} \\
%% \end{array}\]
%% \[\begin{array}{r@{\;}r@{\;}ll}%
\expr & ::= & \ldots
& \text{--- derived syntax:} \\
& \text{--- syntactic sugar:} \\
% additional programming language features:
&\mid &
\LetRecIn\var{\var,\ldots,\var}\expr\expr
......
......@@ -77,7 +77,7 @@
}
\end{array}\]
\Description{Internal invariant of the pipeline.}
\caption{Internal invariant of the pipeline}
\Description{Internal invariants of the pipeline.}
\caption{Internal invariants of the pipeline}
\label{fig:pipeline:invariant}
\end{figure}
%\begin{figure}
\begin{mathpar}
%
\infer{~}{\persistent{\queueInv}}
\qquad
\hoareV
{\TRUE}
{\make~\Unit}
{\Lam \queue. \queueInv \isep \isQueueSC {[]} \isep \persistent{\queueInv}}
{\Lam \queue. \queueInv \isep \isQueueSC {[]}}
\\
\infer{\queueInv}{\;\;\;%
\lahoareV
......@@ -23,12 +25,7 @@
\;\;\;}
%
\end{mathpar}
\Description{A specification of the ``queue'' data structure under sequential consistency.}
\caption{A specification of the ``queue'' data structure under sequential consistency}
\Description{A specification of the ``queue'' data structure in a sequentially consistent model.}
\caption{A specification of the ``queue'' data structure in a sequentially consistent memory model}
\label{fig:queue:specsc}
%\end{figure}
% JH : TODO : serait-ce pertinent de mentionner ici la timelessness 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 ?
% GLEN: je fais figurer la persistance en post-condition de make, ce n’est pas
% idéal mais c’est le mieux que je trouve pour la présentation (plutôt que
% d’avoir des mots "persistent(queueInv)" qui flottent au milieu de la page).
......@@ -40,11 +40,3 @@ There is syntactic sugar for single-cell locations, or ``references'':
$\AllocANY\val$ allocates a location of length~one, $\ReadANY\loc$ reads at
offset~zero, $\WriteANY\loc\val$ writes at offset~zero and
$\CAS\loc{\val_1}{\val_2}$ performs compare-and-set at offset~zero.
% JH : TODO :
% - ne serait-il pas pertinent de mettre un at aussi pour le CAS des tableaux ?
% GLEN: le problème est qu’on ne peut pas faire l’analogue pour CAS sur une
% référence, "CAS e_at e e" ou "CAS !at e e e" sont trop bizarres.
% par contre on pourrait écrire "CAS_at e e e"…
% - Il y a une ambiguïté dans la syntaxe des CAS pour les tableaux "CAS a[b] c d" peut à la fois parler du CAS dans un tableau mais aussi du CAS d'une référence stockée dans un tableau
% GLEN: cette ambiguïté existe seulement si CAS a une annotation "at". :-)
% For double-blind review submission:
% \documentclass[acmsmall,review,anonymous]{acmart}
\documentclass[acmsmall,review,anonymous]{acmart}
% \settopmatter{printfolios=true}
% For single-blind review submission:
% \documentclass[acmsmall,review]{acmart}
% \settopmatter{printfolios=true}
% For final camera-ready submission:
\documentclass[acmsmall,screen]{acmart}
%\documentclass[acmsmall,screen]{acmart}
\settopmatter{}
% Packages.
......@@ -59,11 +59,9 @@
\setlength{\pdfpagewidth}{\paperwidth}
\newcommand{\nl}{\texorpdfstring{\\}{}}
\title
{Formal Verification of a Concurrent Bounded Queue in a Weak Memory Model}
% FP: choix du titre:
% pour moi "With a Ring Buffer" n'apporte pas grand-chose
% par contre il manque l'aspect mémoire faible: "in the Multicore OCaml Weak Memory Model"?
\title{Formal Verification of a Concurrent Bounded Queue in a Weak Memory Model}
% TODO : nouvelles affiliations LMF
\author{Glen Mével}
\affiliation{%
......
......@@ -34,7 +34,7 @@ Similarly, \reftail stores the number of items that have been dequeued since
the creation of the queue.
In other words, it is the rank of the next item to be dequeued.
% GLEN: j’écris "each offset" et non "each cell" car on a en fait deux tableaux,
% J’écris "each offset" et non "each cell" car on a en fait deux tableaux,
% donc deux "cells" au sens du langage de programmation.
% Je prends soin de distinguer ces termes:
% - "offset" (indice d’un "slot", relatif au buffer, donc entre 0 et \capacity);
......@@ -52,8 +52,6 @@ In addition, for the concurrent queue operations to work properly, we must
remember for which rank each slot was last used.%
%
\footnote{%
% FP je pense qu'on peut supprimer cette remarque technique?
% Glen: je la passe en footnote.
Actually, we need not remember the full rank~\idx:
only the cycle, $\idx \div \capacity$, is needed.
}
......@@ -113,11 +111,6 @@ This is implied by, but is weaker than, the equation $\head = \tail$.%
$\tail$ but the slot would still appear as available.
}
% FP ces remarques techniques entre parenthèses sont intéressantes
% mais un peu difficiles à absorber en première lecture. Elles
% seraient mieux en footnote?
% GLEN: c’est fait, et j’en ai encore ajouté deux autres, mais ce serait
% peut-être mieux d’enlever toutes ces remarques superflues qui s’accumulent…
% GLEN: la terminologie "buffer vide/plein" est impropre: on dit que le buffer
% est "plein" quand la prochaine case où ajouter n’est pas encore vidée, mais
......@@ -140,10 +133,7 @@ attributes rank~\tail\ to the candidate dequeuer. Only then it is allowed to
write into slot~$\modcap\tail$.
The status of a given slot is strictly monotonic too. Indeed, there are two
places where it is updated:
either a successful enqueuer makes it odd after having read that it was even,
or a successful dequeuer makes it even after having read that it was odd.
%
places where it is updated.
As an enqueuer, when we write $2\head+1$, no other enqueuer updated the status
since we read it to be $2\head$, because only us have been attributed
rank~\head. In particular, it remained even, so no dequeuer tried to obtain
......@@ -153,8 +143,6 @@ still $2\head$ when we overwrite it with $2\head+1$.
Symmetrically, the status is still $2\tail+1$ when a dequeuer overwrites it with
$2(\tail+\capacity)$.
% GLEN: difficile d’expliquer un invariant comme ça, c’est forcément cyclique…
\subsubsection{Explanation of the code}
The function~\enqueue repeatedly calls \tryenqueue until it succeeds;
......@@ -236,12 +224,11 @@ and can fail either because the buffer is empty or because of a competing dequeu
% GLEN: un meilleur texte, j’espère (peut-être inutile et trop long):
A noteworthy feature of this implementation is that it avoids competition
between enqueuers and dequeuers. They operate on separate references: enqueuers
never access \reftail and dequeuers never access \refhead.
A noteworthy feature of this implementation is that it avoids competition between enqueuers and dequeuers, as long as there is enough lag between enqueuers and dequeuers of the same slot.
They operate on separate references: enqueuers never access \reftail and dequeuers never access \refhead.
%
It can happen that an enqueuer and a dequeuer operate concurrently on a same
slot, but arguably they are not ``competing''. % ``interfering''
slot.
Possible situations are:
\begin{itemize}%
......@@ -250,21 +237,15 @@ Possible situations are:
to be dequeued from slot~$\modcap\tail$ while the corresponding enqueuer is
not done yet;
%
%in that case the candidate dequeuer does not interfere with the enqueuer,
in that case the enqueuer continues unaffected,
%and the candidate dequeuer fails because of the enqueuer being too slow,
and the candidate dequeuer fails because the buffer is empty
(it would fail just as well if there was no enqueuer at all);
and the candidate dequeuer fails because the buffer is empty;
\item symmetrically, a candidate enqueuer checking whether slot~$\modcap\head$
is available for storing an item of rank~\head\ while a dequeuer is still in
the process of dequeuing the item of rank~$\head-\capacity$;
%
%in that case the candidate enqueuer does not interfere with the dequeuer,
in that case the dequeuer continues unaffected,
%and the candidate enqueuer fails because of the dequeuer being too slow,
and the candidate enqueuer fails because the buffer is full
(it would fail just as well if there was no dequeuer at all);
and the candidate enqueuer fails because the buffer is full;
\item a dequeuer dequeuing the item of rank~$\idx + r\capacity$
(with $r \geq 0$) while a candidate enqueuer is still checking whether
......@@ -284,16 +265,16 @@ Possible situations are:
the candidate dequeuer fails, but the existence of a enqueuer for a rank at
least $\idx+\capacity$ implies that another dequeuer has been attributed
rank~\idx\ before the candidate dequeuer, hence we can connect its failure
to competition with that other dequeuer;
to competition with that other dequeuer.
\end{itemize}%
Hence competition happens only between enqueuers, or between dequeuers.
A weakness of this implementation, however, is that it is blocking:
A weakness of this implementation, however, is that it is not non-blocking:
if an enqueuer or a dequeuer halts after it has been attributed a rank but before
it updates the corresponding slot, then after some time, any other thread trying
to enqueue or dequeue fails.
% TODO : citer la thèse de Keir Fraser
%
%Specifically, if an enqueuer halts after it has been attributed a rank~\idx\ but
%before it updates the corresponding slot, then no dequeuer will be able to
......
......@@ -173,7 +173,7 @@ integers, so from owning both $\mapsingleton\offset{\authfrag \status}$ and
$\mapsingleton\offset{\authfull \status'}$ we would learn that
$\status \leq \status'$; hence, when reading the status and observing its value
to be $\status$, we would also obtain $\mapsingleton\offset{\authfrag \status}$
which would act as a remainder that the status of slot~\offset\ cannot become
which would act as a reminder that the status of slot~\offset\ cannot become
less than~$\status$.
In fact, when dealing with the weak memory, it turns out that we need a stronger
......@@ -272,7 +272,7 @@ we get the following:
%
\end{mathpar}
%
Thus this assertion acts as a remainder that, at some point, the status of
Thus this assertion acts as a reminder that, at some point, the status of
slot~\offset\ stored the value~$\status$ and the view~$\sview$.
\subsubsection{Description of slots}
......
......@@ -9,7 +9,6 @@ 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 extensions; in this work, we use
Iris~\cite{iris}, a modular framework for building separation logics.
% TODO: say a few words about Iris here? motivation for using it?
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
......@@ -29,26 +28,6 @@ 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.
%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?
%% 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
......@@ -117,6 +96,7 @@ a queue: the same specification could also describe a stack or a bag.
% 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
......@@ -124,9 +104,8 @@ Another option is to keep exposing a specification akin to that of~\fref{fig:que
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 only stay opened for an \emph{atomic} duration (i.e.~they must be closed immediately or after the execution of an atomic instruction).
% TODO: define (informally) what is an "atomic instruction" ?
Unfortunately, $\enqueue$ and $\dequeue$ perform complex operations and are not atomic.
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 a 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}.
......@@ -134,7 +113,7 @@ This kind of triples are like Hoare triples: they specify a program fragment, ha
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}.
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.
%
......@@ -147,7 +126,7 @@ This linearization point being atomic, it allows the opening of invariants just
}
\infer{%
\lahoare <x> {I \isep P} {e} {I \isep Q}
\lahoare <x> {\later I \isep P} {e} {\later I \isep Q}
}{%
\knowInv{}{I} \vdash \lahoare <x> {P} {e} {Q}
}
......@@ -156,15 +135,16 @@ This linearization point being atomic, it allows the opening of invariants just
% 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.
% 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, soit on en parle pas du tout, et il faut parler de la trasformation d'un triplet log. atom. en triplet de Hoare en agitant les mains.
% 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}.
......@@ -177,14 +157,11 @@ However, the state of the shared queue is not known in advance by the client whe
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 is not adapted to sharing 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.
The use of such a specification in a concrete example will be detailed in
% TODO : référence Section pipeline
.
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:
\[
......
......@@ -21,9 +21,7 @@ predicate cannot be duplicated; we say that it is \emph{exclusive}.
The operations of the queue admit a simple sequential specification which is
presented in~\fref{fig:queue:specseq}. We use the standard Hoare
triple notation, with a partial correctness meaning.
% TODO: ref for Hoare triples?
The asterisk~$(\ast)$ is the separating conjunction.
% GLEN: in fact we do not really need the separating conjunction at that point.
\begin{itemize}
\item
......
......@@ -32,7 +32,7 @@ For example, imagine that thread~$A$ enqueues a pointer to a complex data struct
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.
In \hlog{}, happens-before relationship can be expressed as \emph{transpher of views}.
In \hlog{}, happens-before relationships can be expressed as \emph{transfer of views}.
In this logic, views (noted in this paper using calligraphic capital letters, such as $\mathcal{T,H,V,S}$) are abstract values denoting the knowledge of a thread of the current state of the global shared memory.
They are equipped with a lattice structure: larger views correspond to more recent knowledge.
In \hlog{}, when $\view$ is a view, the persistent assertion $\seen\view$ denotes that the current thread has the knowledge contained in $\view$.
......@@ -74,29 +74,22 @@ a dequeuer to an enqueuer.%
%
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.
retains an interesting behavior that suffices 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?
% JH : Je ne suis pas sûr de l'usage précis dans la littérature, mais, dans ce paragraphe, on commence par dire que c'est linéarisable, puis on finit par dire que cela ne l'est pas.
% Ce que je propose (mais je ne sais pas si c'est standard) : dire que /linéarisable/, c'est qu'il existe un ordre total sur les accès, et que ces accès respectent cet ordre (i.e., agissent uniquement sur l'état courant dans cet ordre). Donc notre queue est linéarisable. Par contre, elle n'est pas /séquentiellement consistente/, puisqu'elle ne garantit pas tout ce qu'elle pourrait en terme d'happens-before
% TODO : comprendre/prendre une décision sur le mot linearizable
Interestingly, \hlog{} is able to express this subtle difference between the behavior of our library and that of lock-based implementation: the full specification under weak memory is shown in~\fref{fig:queue:spec}.
It extends the previous specification (\fref{fig:queue:specsc}) with views, 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
\item When a thread with a local view~$\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).
......
......@@ -12,16 +12,14 @@ operate the queue safely. The answer depends on the implementation.
Possible restrictions include allowing only one thread to enqueue
(single~writer), or allowing only one thread to dequeue (single~reader),
or both.
% digression:
Despite not being fully general, such implementations have use cases:
work~stealing, for example, is commonly achieved using multiple-reader,
single-writer queues.
%% % digression:
%% Despite not being fully general, such implementations have use cases:
%% work~stealing, for example, is commonly achieved using multiple-reader,
%% single-writer queues.
In this paper we study an implementation of a \emph{multiple-reader, multiple-writer}
(MRMW) queue, that is, a queue in which any number of threads are allowed to
enqueue and dequeue.
% TODO: motivation for MRMW queues?
%
In addition, this queue is \emph{bounded}, that is, it occupies no more than a
fixed memory size. A motivation for that trait is that items may be enqueued
more frequently than they are dequeued; in this situation, a bounded queue has no risk of
......
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