MAJ terminée. Nous sommes passés en version 14.6.2 . Pour consulter les "releases notes" associées c'est ici :

queue-spec-sc.tex 9.02 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 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 02, 2021 43 44 45 46 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 47 %  Glen Mével committed Mar 02, 2021 48 49 50 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 51 %  Glen Mével committed Mar 02, 2021 52 However, to ensure soundness in the face of concurrency, the use of invariants  Glen Mével committed Jun 03, 2021 53 in Iris obeys a strict constraint: they can remain open during at most one  Glen Mével committed Mar 02, 2021 54 step of execution. Unfortunately, $\enqueue$ and $\dequeue$ are complex  Glen Mével committed Jun 03, 2021 55 operations which, \emph{a~priori}, take several steps. Hence a client  Glen Mével committed Mar 02, 2021 56 57 58 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 59   Jacques-Henri Jourdan committed Jun 02, 2021 60 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 61 To use it, we substitute ordinary Hoare triples with \emph{logically atomic triples}.  Glen Mével committed Jun 06, 2021 62 Two important reasoning rules for logically atomic triples are given in \fref{fig:hlog:latriples}.%  Glen Mével committed Jun 03, 2021 63 64 65  \footnote{% Following Iris notations, $\knowInv{}{I}$ is an invariant whose content is the assertion~$I$, and $\later$ is a step-indexing modality, a technicality of Iris that we can ignore in this paper. }  Glen Mével committed Jun 03, 2021 66 67 A logically atomic triple is denoted with angle brackets~$\anglebracket{\ldots}$. Just like an ordinary triple, it specifies a program fragment with a precondition and a postcondition.  Glen Mével committed Jun 06, 2021 68 69 In fact, as witnessed by rule \rulelahoare, one can deduce an ordinary Hoare triple from a logically atomic triple. The core difference is that, thanks to rule \rulelainv, 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 05, 2021 70 %  Glen Mével committed Mar 03, 2021 71 The definition of logically atomic triples is further discussed in~\sref{sec:queue:proof:la}  Jacques-Henri Jourdan committed Mar 01, 2021 72 and given with detail in previous work~\cite[\S7]{jung-slides-2019,iris-15}.  Glen Mével committed Jun 03, 2021 73 We now try to give an intuition of that concept:  Glen Mével committed Jun 06, 2021 74 a logically atomic triple $\lahoare{P}{e}{Q}$ states, roughly, that the expression~$e$ contains an atomic instruction, called the \emph{commit point}, which has $P$ as a precondition and $Q$ as a postcondition.  Glen Mével committed Jun 03, 2021 75 Because it is atomic, invariants can be opened around that commit point.  Glen Mével committed Jun 06, 2021 76 77  \input{figure-hlog-latriples}  Glen Mével committed Feb 27, 2021 78 79  Using logically atomic triples, the specification can be written as shown  Glen Mével committed Mar 02, 2021 80 81 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 82 83 84 85 86 87 88 89 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 90 the state of the queue at the commit point,  Glen Mével committed Mar 05, 2021 91 92 93 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 94 covering every possible shared state at the commit point.  Glen Mével committed Mar 05, 2021 95 96 97  The last departure from the sequential specification is that the representation predicate is split into two parts:  Glen Mével committed Jun 03, 2021 98 99 100 101 102 103 104 105 106 107 108 a persistent% \footnote{% In Iris terms, \emph{persistent} qualifies an assertion that is duplicable. Once established, such an assertion holds forever. } assertion~$\queueInv$ and an exclusive assertion $\isQueueSC\elemList$, connected by a ghost name% \footnote{% Ghost names in Iris are identifiers for pieces of ghost state. We say more on this in~\sref{sec:queue:proof}. }% ~$\gqueue$.  Glen Mével committed Mar 05, 2021 109 110 111 112 113 114 That splitting is an artifact of our correctness proof technique, which we detail in~\sref{sec:queue:proof}. % 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,  Glen Mével committed Jun 03, 2021 115 116 117 118 119 the persistent component can be directly duplicated and distributed to all threads.% \footnote{% An Iris expert may want to conceal the queue invariant, $\queueInv$, inside $\isQueueSC\elemList$. However, we need to access this invariant at various places other than the commit point. This is feasible with a more elaborate definition of logically atomic triples than the one given in this paper, so that they support \emph{aborting}~\cite{jung-slides-2019}. Another drawback is that we would lose the timelessness of the representation predicate. }  Jacques-Henri Jourdan committed Mar 01, 2021 120   Glen Mével committed Mar 02, 2021 121 122 123 124 125 126 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 127 \label{sec:queue:spec:sc:persistent}  Glen Mével committed Mar 02, 2021 128 129 130 131 132 133 134 135 136 137 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  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 169 $ Glen Mével committed Mar 02, 2021 170 171  \isQueuePers\Phi \;\eqdef\;  Glen Mével committed Mar 08, 2021 172  \Exists\gqueue. \isepV{%  Glen Mével committed Mar 02, 2021 173  \queueInv  Glen Mével committed Mar 08, 2021 174  \\ \knowInv{}{\Exists \nbelems, \elemList*[]. \isQueueSC\elemList \ISEP \Phi\,\nthElem{0} \ISEP \cdots \ISEP \Phi\,\nthElem{\nbelems-1}}  Glen Mével committed Mar 02, 2021 175  }  Glen Mével committed Feb 27, 2021 176 177 $  Glen Mével committed Mar 02, 2021 178 179 180 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 181 one opens the invariant around the associated logically atomic triples.