queue-spec-sc.tex 9.43 KB
Newer Older
 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 Mar 05, 2021 4 We now consider a situation where several threads can access the queue concurrently. Glen Mével committed Feb 28, 2021 5 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 Mar 05, 2021 7 8 9 10 11 12 13 In a seminal work, \citet{brookes-04} and \citet{ohearn-07} devised \CSL, an extension of \SL which enables to reason about programs where several threads can access a same piece of memory. Though the original logic achieves sharing through hard-wired conditional critical regions'', it has spawned a variety of descendants lifting this limitation and pushing further the applicability of such separation logics. % applicability / expressiveness / generality In this work, we use Iris~\cite{iris}, a modular framework for building separation logics. Glen Mével committed Feb 28, 2021 14 15 In a derivative of \CSL, we may retain the exact same specification as is presented Glen Mével committed Mar 02, 2021 16 in~\fref{fig:queue:spec:seq}, recalling that $\isQueueSEQ\elemList$ is an Glen Mével committed Feb 28, 2021 17 exclusive assertion: Glen Mével committed Mar 02, 2021 18 a thread that has this assertion can safely assume to be the only one allowed Glen Mével committed Feb 27, 2021 19 20 to operate on the queue. % Glen Mével committed Mar 02, 2021 21 22 A client application can transfer this assertion between threads via some means of synchronization: for instance, it may use a lock to guard all operations on the Glen Mével committed Feb 28, 2021 23 24 25 26 27 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 28 29 These costs are often unnecessary, as many data~structures are designed specifically to support concurrent accesses. In this paper, as stated, we wish Glen Mével committed May 31, 2021 30 to prove the correctness of a MPMC~queue implementation, which should thus Glen Mével committed Mar 02, 2021 31 32 ensure, by itself, thread safety. % Glen Mével committed Feb 28, 2021 33 Hence we can achieve finer-grain concurrency, where operating on a queue does Glen Mével committed Mar 02, 2021 34 35 36 37 38 39 40 41 not require its exclusive ownership. In this context, another option is for the client to share this ownership among several threads, logically. In an Iris-like logic, one would typically place the exclusive ownership in an \emph{invariant}. %---alongside the properties about the public state which are needed by the particular application. 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 42 % Glen Mével committed Mar 05, 2021 43 % GLEN: digression (on introduit le vocabulaire "public state" ici): Glen Mével committed Mar 02, 2021 44 45 46 47 As the public state of the queue---the list $\elemList$ of currently stored items---would only be known from that invariant, the client would also express in there the properties about this state that their particular application needs. Glen Mével committed Feb 27, 2021 48 % Glen Mével committed Mar 02, 2021 49 50 51 Then, when one of the threads needs to access the shared resource, it can \emph{open} the invariant, get the assertions it contains, perform the desired operation on the shared state, reestablish the invariant, and finally close it. Glen Mével committed Feb 27, 2021 52 % Glen Mével committed Mar 02, 2021 53 54 55 However, to ensure soundness in the face of concurrency, the use of invariants in Iris obeys a strict constraint: they can remain open during at most a single step of execution. Unfortunately, $\enqueue$ and $\dequeue$ are complex Jacques-Henri Jourdan committed Mar 02, 2021 56 operations which, \emph{a~priori}, take more than one step of execution. Hence a client Glen Mével committed Mar 02, 2021 57 58 59 would be unable to open their invariant around the triples shown in~\fref{fig:queue:spec:seq}. Yet these operations are atomic'' in some empirical sense. Glen Mével committed Feb 27, 2021 60 Jacques-Henri Jourdan committed Jun 02, 2021 61 The concept of logical atomicity~\cite[\S7]{jacobs2011expressive,jung-slides-2019,iris-15} aims at addressing that difficulty. Glen Mével committed Mar 05, 2021 62 63 64 65 To use it, we substitute ordinary Hoare triples with \emph{logically atomic triples}. Just like ordinary triples, they specify a program fragment with a precondition and a postcondition. The core difference is that invariants can be opened around a logically atomic triple, regardless of the number of execution steps of the program fragment: in a sense, when a function is specified using a logically atomic triple, one states that said function behaves as if it were atomic. % Glen Mével committed Mar 03, 2021 66 The definition of logically atomic triples is further discussed in~\sref{sec:queue:proof:la} Jacques-Henri Jourdan committed Mar 01, 2021 67 and given with detail in previous work~\cite[\S7]{jung-slides-2019,iris-15}. Glen Mével committed Mar 05, 2021 68 We now try to give an intuition on that concept: Jacques-Henri Jourdan committed May 31, 2021 69 70 a logically atomic triple $\lahoare{P}{e}{Q}$ states, roughly, that the expression $e$ contains a commit point which has $P$ as a precondition and $Q$ as a postcondition. The triple then allows the opening of invariants around that commit point Glen Mével committed Mar 05, 2021 71 because it is an atomic instruction. Glen Mével committed Feb 27, 2021 72 73 74 % \begin{mathpar} % Glen Mével committed Mar 03, 2021 75 \infer[LAHoare]{% using the rule names from \cite{iris-15} Glen Mével committed Feb 27, 2021 76 77 78 79 \lahoare {P} {e} {Q} }{% \Forall x. \hoare {P} {e} {Q} } Glen Mével committed Mar 08, 2021 80 \and Glen Mével committed Mar 03, 2021 81 \infer[LAInv]{% using the rule names from \cite{iris-15} Jacques-Henri Jourdan committed Mar 01, 2021 82 \lahoare {\later I \isep P} {e} {\later I \isep Q} Glen Mével committed Feb 27, 2021 83 }{% 84 \knowInv{}{I} \vdash \lahoare {P} {e} {Q} Glen Mével committed Feb 27, 2021 85 86 87 88 89 90 91 } % \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) % peut-être enlever le binder à cet endroit. Jacques-Henri Jourdan committed Mar 01, 2021 92 93 % TODO : expliquer la syntaxe des invariants, dire que \later est une technicité d'Iris Jacques-Henri Jourdan committed Mar 01, 2021 94 95 96 97 % 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 98 % 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 99 Glen Mével committed Feb 27, 2021 100 Using logically atomic triples, the specification can be written as shown Glen Mével committed Mar 02, 2021 101 102 in~\fref{fig:queue:spec:sc}. It closely resembles that of the sequential setting (\fref{fig:queue:spec:seq}). Glen Mével committed Mar 05, 2021 103 104 105 106 107 108 109 110 The first noticeable difference 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, in the syntax of logically atomic triples, of an explicit binder for some variables ($\nbelems, \elemList*[]$). This binder addresses a subtlety of logical atomicity: a client calling \enqueue or \dequeue does not know in advance Jacques-Henri Jourdan committed May 31, 2021 111 the state of the queue at the commit point, Glen Mével committed Mar 05, 2021 112 113 114 which is when the precondition and postcondition are to be interpreted. Hence, both formulas have to be parameterized by said shared state. Said otherwise, a logically atomic triple provides a \emph{family} of pre/postcondition pairs Jacques-Henri Jourdan committed May 31, 2021 115 covering every possible shared state at the commit point. Glen Mével committed Mar 05, 2021 116 117 118 119 120 121 122 123 124 125 126 127 128 129 The last departure from the sequential specification is that the representation predicate is split into two parts: a persistent assertion~$\queueInv$ and an exclusive assertion $\isQueueSC\elemList$, connected by a ghost name~$\gqueue$. That splitting is an artifact of our correctness proof technique, which we detail in~\sref{sec:queue:proof}. % GLEN: 1re fois qu’on parle d’assertions persistantes , définir le terme ici. % Note that this does not complicate the use of the queue by the client: both assertions are produced when creating the queue, and while the exclusive component can be put in an invariant as before, the persistent component can be directly duplicated and distributed to all threads. % TODO : pour après la soumission : expliquer pourquoi QueueInv n'est pas caché dans IsQueue (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é) Jacques-Henri Jourdan committed Mar 01, 2021 130 Glen Mével committed Mar 02, 2021 131 132 133 134 135 136 The use of such a specification in a concrete example will be detailed in~\sref{sec:pipeline:proof}. For now, we illustrate how a weaker specification can be easily deduced from this one. % ------------------------------------------------------------------------------ \subsubsection{A Persistent Specification} Jacques-Henri Jourdan committed Mar 03, 2021 137 \label{sec:queue:spec:sc:persistent} Glen Mével committed Mar 02, 2021 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 If it were not for logical atomicity, and we still wanted to share the ownership of the queue, we would have little choice left than renouncing to an exclusive representation predicate. Only a persistent assertion would be provided, because the description of the public state has to be stable in the face of interference by other threads. The resulting specification would be much weaker. % For example, we may merely specify that all of the elements stored in the queue satisfy some predicate~$\Phi$. In doing so, 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} } \quad \infer{% \isQueuePers\Phi }{% \hoare {\Phi\,\elem} {\enqueue~\queue~\elem} {\Lam \Unit. \TRUE} } \quad \infer{% \isQueuePers\Phi }{% \hoare {\TRUE} {\dequeue~\queue} {\Lam \elem. \Phi\,\elem} } % \end{mathpar} To derive these Hoare triples from the ones of~\fref{fig:queue:spec:sc}, one simply defines the persistent assertion as follows, where the boxed assertion is an Iris invariant: % Glen Mével committed Feb 27, 2021 179 $Glen Mével committed Mar 02, 2021 180 181 \isQueuePers\Phi \;\eqdef\; Glen Mével committed Mar 08, 2021 182 \Exists\gqueue. \isepV{% Glen Mével committed Mar 02, 2021 183 \queueInv Glen Mével committed Mar 08, 2021 184 \\ \knowInv{}{\Exists \nbelems, \elemList*[]. \isQueueSC\elemList \ISEP \Phi\,\nthElem{0} \ISEP \cdots \ISEP \Phi\,\nthElem{\nbelems-1}} Glen Mével committed Mar 02, 2021 185 } Glen Mével committed Feb 27, 2021 186 187$ Glen Mével committed Mar 02, 2021 188 189 190 This assertion 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$, Glen Mével committed Mar 05, 2021 191 one opens the invariant around the associated logically atomic triples.