queue-spec-sc.tex 11.6 KB
 Glen Mével committed Mar 02, 2021 1 \subsection{Specification under sequential consistency}  Glen Mével committed Feb 27, 2021 2 3 \label{sec:queue:spec:sc}  Glen Mével committed Feb 28, 2021 4 5 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}.  Glen Mével committed Feb 27, 2021 6 %  Glen Mével committed Feb 28, 2021 7 8 9 \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''.  Glen Mével committed Mar 02, 2021 10 This logic spawned a variety of descendants; in this work, we use  Glen Mével committed Feb 28, 2021 11 12 13 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  Glen Mével committed Feb 27, 2021 14 in~\fref{fig:queue:specseq}, recalling that $\isQueueSEQ\elemList$ is an  Glen Mével committed Feb 28, 2021 15 16 exclusive assertion: a thread that has this assertion could safely assume to be the only one allowed  Glen Mével committed Feb 27, 2021 17 18 to operate on the queue. %  Glen Mével committed Feb 28, 2021 19 The assertion would be transferable between threads via some means of  Glen Mével committed Feb 27, 2021 20 synchronization: for instance, we may use a lock to guard all operations on the  Glen Mével committed Feb 28, 2021 21 22 23 24 25 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. %  Glen Mével committed Mar 02, 2021 26 27 28 29 30 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. %  Glen Mével committed Feb 28, 2021 31 32 33 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.  Glen Mével committed Feb 27, 2021 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101  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.  Jacques-Henri Jourdan committed Mar 01, 2021 102 % 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.  Jacques-Henri Jourdan committed Mar 01, 2021 103 % => TODO : déplacer ceci en tant qu'exemple à la fin de la spec SC  Glen Mével committed Feb 27, 2021 104 105 106  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  Glen Mével committed Feb 28, 2021 107 108 : 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.  Glen Mével committed Feb 27, 2021 109 110 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.  Jacques-Henri Jourdan committed Mar 01, 2021 111 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.  Glen Mével committed Mar 02, 2021 112 Unfortunately, $\enqueue$ and $\dequeue$ perform complex operations that take more than one step of execution.  Glen Mével committed Feb 27, 2021 113 114 115 116 117 118 119  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  Jacques-Henri Jourdan committed Mar 01, 2021 120 and given with detail in previous work~\cite[\S7]{jung-slides-2019,iris-15}.  Glen Mével committed Feb 28, 2021 121 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.  Glen Mével committed Feb 27, 2021 122 123 124 125 126 127 128 129 130 131 132 This linearization point being atomic, it allows the opening of invariants just like atomic instructions. % \begin{mathpar} % \infer{% \lahoare {P} {e} {Q} }{% \Forall x. \hoare {P} {e} {Q} } \infer{%  Jacques-Henri Jourdan committed Mar 01, 2021 133  \lahoare {\later I \isep P} {e} {\later I \isep Q}  Glen Mével committed Feb 27, 2021 134 135 136 137 138 139 140 141 142 143 144  }{% \knowInv{}{I} \vdash \lahoare {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.  Jacques-Henri Jourdan committed Mar 01, 2021 145 146 % TODO : expliquer la syntaxe des invariants, dire que \later est une technicité d'Iris  Jacques-Henri Jourdan committed Mar 01, 2021 147 148 149 150 % 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.  Jacques-Henri Jourdan committed Mar 01, 2021 151 % 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  Jacques-Henri Jourdan committed Mar 01, 2021 152   Glen Mével committed Feb 27, 2021 153 154 155 156 157 158 159 160 161 162 163 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$.  Jacques-Henri Jourdan committed Mar 01, 2021 164 165 166 167 168 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}.  Glen Mével committed Feb 27, 2021 169 170 171 172 173 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}}$  Glen Mével committed Feb 28, 2021 174 This is trivial to produce at the creation of the queue, when \make hands us the assertions $\queueInv$ and $\isQueueSC{[]}$.  Glen Mével committed Feb 27, 2021 175 176 177 178 179 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 %%$