Commit 46380512 by Glen Mével

 %\begin{figure} $\begin{array}{@{}l@{}} \begin{mathpar} % \infer{\queueInv}{\;\;\;% \lahoareV {\Forall \nbelems, \elemList*[]. \isQueueSC \elemList} {\enqueue~\queue~\elem} {\Lam \Unit. \isQueueSC {\elemListSnoc \elemList \elem}} \;\;\;} \quad \infer{\queueInv}{\;\;\;% \lahoareV {\Forall \nbelems, \elemList*[]. \isQueueSC \elemList} {\dequeue~\queue} {\Lam \elem. 1 \leq \nbelems \isep \elem = \elem_0 \isep \isQueueSC {\elemList<1>*}} \;\;\;} \\\\ \end{array}$ % \end{mathpar} \Description{A specification of the queue'' data structure under sequential consistency.} \caption{A specification of the queue'' data structure under sequential consistency} \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 ?
 %\begin{figure} $\begin{array}{@{}l@{}} \begin{mathpar} % \hoareV {\isQueueSEQ \elemList} {\enqueue~\queue~\elem} {\Lam \Unit. \isQueueSEQ {\elemListSnoc \elemList \elem}} \qquad \hoareV {\isQueueSEQ \elemList} {\dequeue~\queue} {\Lam \elem. 1 \leq \nbelems \isep \elem = \elem_0 \isep \isQueueSEQ {\elemList<1>*}} \end{array}$ % \end{mathpar} \Description{A specification of the queue'' data structure in a sequential setting.} \caption{A specification of the queue'' data structure in a sequential setting} \label{fig:queue:specseq} ... ...
 ... ... @@ -9,10 +9,7 @@ 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 representation predicate: % FP suggestion d'anglais: on n'utilise jamais le futur ("will") % dans un article scientifique, et on écrit tout au présent. % C'est vraiment rare qu'on ait absolument besoin du futur. is represented in separation logic with a predicate: % $\isQueueSEQ \elemList ... ... @@ -29,16 +26,18 @@ give us back the ownership of~\queue, where \elem has been appended at the h 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 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. % (by some other thread). % FP peut-être pourrais-tu noter aussi que cette spec peut décrire une % queue de capacité bornée; dans ce cas il faut aussi que enqueue % boucle quand la capacité est atteinte. 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} ... ... @@ -54,10 +53,7 @@ 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. % %Even though this resource would be transferable via other means (such as %a lock), this will be of little use as the goal is to share the queue among %several threads. % 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. ... ... @@ -68,18 +64,14 @@ shared queue. % FP noter que c'est l'approche de la logique de séparation concurrente % traditionnelle, pioneered by \citet{ohearn-07} % FP as-tu annoncé plus tôt à quelle implémentation tu t'intéresses? % sinon, tu pourrais écrire, de façon plus abstraite, que "some % implementations of concurrent queues are thread-safe by design, % so that they do not need to be protected by a lock". However the implementation that we wish to prove correct is already thread-safe. Both \enqueue and \dequeue have a linearization point. %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 data structure can be shared among several threads. 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 ... ... @@ -96,49 +88,82 @@ ownership of the queue data structure can be shared among several threads. %% queue~\queue with a logical-level variable~\gqueue, which will be used to %% describe the state of the queue (ghost state). One possibility to address this constraint is to use persistent assertions in order to replace the representation predicate \isQueueSEQ\elemList of the queue. With this choice, an issue is then how to describe the state of the queue. Since any thread can change it at any moment, no thread can know the current state to be some list \elemList. 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. % We may give a weaker specification by guaranteeing only that all of the elements stored in the queue satisfy some predicate~\Phi. \begin{mathpar} % \[\begin{array}{lcr} \hoareV {\isQueueSEQ \Phi \isep \Phi\,\elem} {\enqueue~\queue~\elem} {\Lam \Unit. \isQueueSEQ \Phi} \qquad \hoareV {\isQueueSEQ \Phi} {\dequeue~\queue} {\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 or a bag. %% or even (if $\Phi$ is %% duplicable) a single memory cell always returning the same value. % 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. There is a common technique 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 state in an invariant which is agreed upon by all the threads. %\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, the use of invariants in Iris need 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). 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. % FP "resists" c'est pas mal, mais on pourrait écrire aussi % "that is stable in the face of interference by other threads", % ça évoquerait une terminologie standard. 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. ... ... @@ -148,6 +173,28 @@ The definition of logically atomic triples is further discussed in 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 {\Forall x. P} {e} {Q} }{% \Forall x. \hoare {P} {e} {Q} } \infer{% \lahoare {\Forall x. I \isep P} {e} {I \isep Q} }{% \knowInv{}{I} \vdash \lahoare {\Forall 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}. ... ... @@ -155,29 +202,36 @@ 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. % TODO: in Iris literature the binder is simply denoted as "x." with no ∀ symbol. 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$. 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. 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. % 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 \Phi % 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, 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 their logically atomic triples. 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 ... ...