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

queue-proof.tex 33.2 KB
 Glen Mével committed Feb 23, 2021 1 2 3 4 % ------------------------------------------------------------------------------ % Proof of the bounded queue.  Glen Mével committed Mar 02, 2021 5 \section{Proof of the Specification for the Ring Buffer}  Glen Mével committed Feb 23, 2021 6 7 \label{sec:queue:proof}  Glen Mével committed Mar 02, 2021 8 \input{figure-queue-inv}  Glen Mével committed Feb 23, 2021 9   Glen Mével committed May 19, 2021 10 11 12 We now turn to proving the following. \begin{theorem}%  POTTIER Francois committed May 31, 2021 13  The implementation shown in \fref{fig:queue:impl} (\sref{sec:queue:impl})  Glen Mével committed May 19, 2021 14 15 16  satisfies the functional specification appearing in \fref{fig:queue:spec:weak} (\sref{sec:queue:spec:weak}). \end{theorem}%  Glen Mével committed Feb 27, 2021 17   Jacques-Henri Jourdan committed Mar 02, 2021 18 In the Iris methodology, which \hlog{} is based on, concurrent protocols are established thanks to \emph{ghost state} and \emph{invariants}.  Glen Mével committed May 31, 2021 19 20 21 Ghost state in Iris is a flexible tool for defining custom resources. It takes values from algebraic structures called CMRAs; for the purpose of this paper, it is enough to think of a CMRA as a set  Glen Mével committed Feb 27, 2021 22 equipped with a binary composition operation $(\mtimes)$ that is partial,  Glen Mével committed May 31, 2021 23 associative and commutative.  Glen Mével committed Feb 27, 2021 24 25 26 27 Ghost state values are assigned to ghost variables. The separation logic assertion~$\ownGhost\gname{a}$, where $a$ is an element of some CMRA, intuitively means that we own a fragment of the ghost variable $\gname$ and that this fragment has value~$a$.  POTTIER Francois committed Mar 03, 2021 28 Unlike what happens with a traditional pointsto assertion, the ownership \emph{and value} of  Glen Mével committed Feb 27, 2021 29 30 31 32 33 a ghost variable can be split into fragments according to the composition operation of the CMRA: $$\ownGhost\gname{a \mtimes b} \iequiv \ownGhost\gname{a} \isep \ownGhost\gname{b}$$.  Glen Mével committed May 31, 2021 34 35 In \hlog, ghost state is objective, as it is independent from the physical state of the memory.%  Jacques-Henri Jourdan committed Jun 04, 2021 36 37 38  %% \footnote{% %% In fact, the physical memory is itself encoded as a piece of ghost state. %% }  Glen Mével committed May 31, 2021 39   Glen Mével committed Feb 27, 2021 40   POTTIER Francois committed Mar 03, 2021 41 42 Ghost state can be coupled with invariants such as the ones presented in \sref{sec:queue:spec:sc} to describe protocols that threads must follow to access shared resources. In \fref{fig:queue:inv}, one can see how this methodology is used for describing the internal protocol of the queue: the persistent predicate $\queueInv$ is in fact an invariant; the exclusive representation predicate $\isQueue\tview\hview\elemViewList$ is defined using ghost state, as are several internal resources.  Jacques-Henri Jourdan committed Mar 02, 2021 43 44 We detail these definitions in the following sections.  Glen Mével committed Jun 06, 2021 45 46 47 48 49 50 51 52 53 54 55 \begin{figure} \input{figure-queue-axioms-isqueue} \mbox{}\vfil\mbox{} \input{figure-queue-axioms-witness} \mbox{}\vfil\mbox{} \input{figure-queue-axioms-token} \Description{Axiomatic description the ghost state of the queue.} \caption{Axiomatic description of the ghost state of the queue} \label{fig:queue:axioms} \end{figure}  Glen Mével committed Mar 02, 2021 56 \subsection{Public state}  Glen Mével committed Feb 28, 2021 57   Glen Mével committed Jun 06, 2021 58 59 60 %\input{figure-queue-ghost-isqueue} The assertion $\isQueue\tview\hview\elemViewList$, defined in~\fref{fig:queue:inv:isqueue}, exposes to the user the public  Glen Mével committed Feb 27, 2021 61 state of the queue. This public state, as motivated in \sref{sec:queue:spec:weak},  Glen Mével committed May 31, 2021 62 is composed of the tail view, the head view, and the list of current items with  POTTIER Francois committed Mar 03, 2021 63 their views.  Glen Mével committed Feb 27, 2021 64 65 % It is tied to the internal state of the queue via the use of an authoritative  Glen Mével committed May 31, 2021 66 67 ghost state, stored in a ghost variable~$\gqueue$. %  Glen Mével committed Jun 03, 2021 68 More precisely, the public state is kept in sync with the values which appear in an authoritative assertion $\ownGhost\gqueue{\authfull \tuple{\tview, \hview, \elemViewList}}$, the latter being owned by the internal invariant.  Glen Mével committed May 31, 2021 69   Glen Mével committed Jun 06, 2021 70 Formally, the two assertions satisfy the properties shown in~\fref{fig:queue:axioms:isqueue}.  Glen Mével committed May 31, 2021 71 %  Glen Mével committed Jun 05, 2021 72 Rule~\ruleIsQueueAg asserts that the state known to the invariant (first premise) is identical to that known to the representation predicate (second premise).  Glen Mével committed May 31, 2021 73 %  Glen Mével committed Jun 05, 2021 74 Rule~\ruleIsQueueUpd asserts that, whenever we own both the representation predicate and its authoritative counterpart, we can update the public state to any other value by taking a \emph{ghost update} step. The symbol~$\upd$ is an Iris modality which represents such a ghost update.  Glen Mével committed Feb 27, 2021 75   Glen Mével committed Jun 03, 2021 76 77 78 We achieve these properties by using an adequate CMRA for the values of the ghost variable~$\gqueue$. We build this CMRA by composing several classical Iris constructs; namely, the exclusive CMRA $\exm(S)$ where $S$ is a set, and the authoritative CMRA $\authm(M)$ where $M$ is a CMRA\@. We do not explain the construction in more detail; the interested reader may refer to the documentation of Iris~\cite{iris}.  Glen Mével committed Feb 27, 2021 79   Glen Mével committed Jun 03, 2021 80 It is worth remarking that this construction makes the representation predicate exclusive: it is absurd to own simultaneously two assertions of the form $\isQueue - - -$.  Glen Mével committed Feb 27, 2021 81   Glen Mével committed Mar 02, 2021 82 \subsection{Internal invariant}  Glen Mével committed Feb 28, 2021 83   Glen Mével committed Feb 27, 2021 84 Along with the exclusive representation predicate $\isQueue\tview\hview\elemViewList$,  Glen Mével committed Jun 06, 2021 85 we provide the user with a persistent assertion $\queueInv$ defined in~\fref{fig:queue:inv:inv}. It contains the  Glen Mével committed Feb 27, 2021 86 87 88 internal invariant governing the queue~$\queue$, whose public state is exposed via the ghost variable~$\gqueue$. In addition to the public state, there are two more ghost variables, named $\gmonos$ and $\gtokens$, which are hidden  Glen Mével committed Jun 04, 2021 89 to the user of the queue but needed internally. Thus they are  Glen Mével committed Feb 27, 2021 90 91 92 existentially quantified in this persistent assertion. We will explain the purpose and meaning of these ghost variables in a moment. For now, we look at the internal invariant, $\queueInvInner$.  Glen Mével committed Feb 27, 2021 93   POTTIER Francois committed Mar 03, 2021 94 95 This invariant owns most of the physical locations of the queue: \reftail, \refhead, \refstatuses, and some parts of the array \refelements.  Glen Mével committed Jun 04, 2021 96 Recall that pointsto assertions for atomic cells are objective and can be placed inside an invariant.  Glen Mével committed Feb 27, 2021 97 98 % The array-pointsto assertion $\arraypointstoAT\refstatuses\statusViewList$ is  POTTIER Francois committed Mar 03, 2021 99 a shorthand for the following iterated conjunction:  Glen Mével committed Feb 27, 2021 100 101 102 103 $\Sep_{0 \leq \offset < \capacity} \nthpointstoAT\refstatuses\offset{\mkval{\status_\offset}{\sview_\offset}}$ %  Glen Mével committed Jun 04, 2021 104 105 106 107 108 %Recall that in \hlog, $\nthpointstoAT\refstatuses\offset{\mkval{\status_\offset}{\sview_\offset}}$ %is the pointsto assertion for the atomic cell at index~\offset\ of %location~\refstatuses: it asserts the unique ownership of that cell, and states %that it currently contains the value $\status_\offset$ and the view %$\sview_\offset$ (or a larger view).  Glen Mével committed Feb 27, 2021 109 %  Glen Mével committed Jun 04, 2021 110 111 Also, since we encode references as arrays of length~one, we write $\pointstoAT\reftail{\mkval\tail\tview}$ as a shorthand for  Glen Mével committed Feb 27, 2021 112 113 $\nthpointstoAT\reftail0{\mkval\tail\tview}$.  Glen Mével committed Feb 27, 2021 114 115 116 117 118 Apart from this physical state, the invariant also stores ghost state. It owns the authority on all three ghost variables, $\gqueue$, $\gmonos$ and $\gtokens$. % The authority of $\gqueue$ is simple: it simply ties internal values to the public state of the queue, as explained earlier.  Glen Mével committed Jun 03, 2021 119 We now explain the other two pieces of ghost state.  Glen Mével committed Feb 27, 2021 120   Glen Mével committed Mar 02, 2021 121 \subsection{Monotonicity of statuses}  Glen Mével committed Feb 28, 2021 122   Glen Mével committed Jun 06, 2021 123 124 125 %\input{figure-queue-ghost-witness} %\input{figure-queue-cmra-statlat}  Glen Mével committed Feb 27, 2021 126 127 128 The purpose of the ghost variable~$\gmonos$ is to reflect the fact that statuses are monotonic. %  POTTIER Francois committed Jun 03, 2021 129 More precisely, they are \emph{strictly} monotonic: every write to a status cell necessarily increases its value. As a consequence, as long as the value of a status cell has not increased, we know that no write happened to it and, in particular, that the view that it stores has not increased either.  Glen Mével committed Feb 27, 2021 130 %  Glen Mével committed Jun 03, 2021 131 132 133 134 135 136 137 138 139 In other words, we have the monotonicity of the value-view pair stored in a status cell, for the lexicographic order where the order on views is reversed: % $\pair{\status_1}{\sview_1} \sqsubseteq \pair{\status_2}{\sview_2} \mathlop{\Longleftrightarrow} \status_1 < \status_2 \lor \left( \status_1 = \status_2 \land \sview_1 \viewgeq \sview_2 \right)$  Glen Mével committed Feb 27, 2021 140 %  Glen Mével committed Jun 03, 2021 141 142 143 144 145 146 147 This stronger monotonicity property will be used in the proof---specifically, when verifying \trydequeue---and specifying it is thus an additional requirement of working with a weak memory model. To reflect monotonicity of the status of offset~$\offset$, we use two assertions, $\ownGhost \gmonos {\mapsingleton\offset{\authfull \pair\status\sview}}$ and $\monoWitness \offset {\pair\status\sview}$, connected via a ghost variable~$\gmonos$.  Glen Mével committed Jun 06, 2021 148 Relevant definitions appear in~\fref{fig:queue:inv:witness}.  Glen Mével committed Jun 03, 2021 149 %  Jacques-Henri Jourdan committed Jun 04, 2021 150 The first assertion, owned by the invariant of the queue is connected by the invariant to the value-view pair stored in the status cell.  POTTIER Francois committed Jun 03, 2021 151 152 In addition, it is exclusive: for any offset~$\offset$, two assertions of the form $\ownGhost \gmonos {\mapsingleton\offset{\authfull -}}$ cannot hold simultaneously.  Glen Mével committed Jun 03, 2021 153 %  Jacques-Henri Jourdan committed Jun 04, 2021 154 155 The second assertion $\monoWitness \offset {\pair\status\sview}$ means that the value-view pair stored in the status cell is at least $\pair\status\sview$. Importantly, a witness assertion is persistent: once it has been established, it remains true forever and can be duplicated at will.  Glen Mével committed Jun 03, 2021 156   Glen Mével committed Jun 06, 2021 157 We thus have the properties summarized in~\fref{fig:queue:axioms:witness}.  Glen Mével committed Feb 27, 2021 158 %  Glen Mével committed Jun 06, 2021 159 Rule~\ruleWitnessPers is the persistency just mentioned.  Glen Mével committed Feb 28, 2021 160 %  Glen Mével committed Jun 06, 2021 161 Rule~\ruleWitnessOrder asserts that a witness gives a lower bound on what the status cell currently stores.  Glen Mével committed Jun 03, 2021 162 %  Glen Mével committed Jun 05, 2021 163 Rule~\ruleWitnessUpd asserts that we can update a status cell to any larger or equal content, and obtain a witness for that content.  Glen Mével committed Feb 27, 2021 164   Glen Mével committed Jun 03, 2021 165 166 167 168 169 170 171 172 173 174 175 176 We achieve these properties by constructing an adequate CMRA for the values taken by the ghost variable~$\gmonos$. Again, we will not explain standard Iris constructs here, except for one point. % The construction involves building a CMRA whose carrier set is $\Z \times \typeView$, the set of status-view pairs, and whose inclusion order% \footnote{% For two elements $a$ and $b$ of a CMRA~$M$, we say that $b$ is included in $a$ if there exists some~$c$ such that $a = b \mtimes c$. } coincides with the desired order $\sqsubseteq$. %  Glen Mével committed Feb 28, 2021 177 178 A general recipe for deriving a CMRA structure with a given inclusion order, if that order admits binary joins, consists in taking the join operation as the  Glen Mével committed May 31, 2021 179 composition of the CMRA\@~\cite{timany2021monotonicity}.  Glen Mével committed Feb 28, 2021 180 In this case, we equip the product set $$\Z \times \typeView$$ with  Glen Mével committed Jun 06, 2021 181 the join-semilattice structure whose definition appears in~\fref{fig:queue:cmra:statlat}.  Glen Mével committed Feb 23, 2021 182   Glen Mével committed Jun 04, 2021 183 \subsection{Available and occupied slots}  Glen Mével committed Mar 01, 2021 184   Glen Mével committed Jun 06, 2021 185 In~\fref{fig:queue:inv:inv}, the last two lines of the invariant describe the state of each slot.  Glen Mével committed Mar 01, 2021 186 187 188 189 190 191 192 193 194 195 196 197 198 For clarity, we introduce two abbreviations: % the assertion $\emptyCell \idx {\pair\status\sview}$ represents slot~$\modcap\idx$ being available for a future item of rank~$\idx+\capacity$; % the assertion $\fullCell \idx {\pair\status\sview} {\pair\elem\eview}$ represents slot~$\modcap\idx$ being occupied by the item of rank~$\idx$, whose value is $\elem$ with the associated view $\eview$. % In these two abbreviations, the status field of the slot has value~$\status$ and stores view~$\sview$.  Glen Mével committed Jun 04, 2021 199 200 % These abbreviations are also where we keep the ownership of the \emph{nonatomic} cell $\refelements[\modcap\idx]$, via a pointsto assertion.  Glen Mével committed Mar 01, 2021 201 202  %In both cases, we must own the memory cell.  Glen Mével committed Jun 04, 2021 203 204 205 206 207 208 %Recall that in \hlog, $\nthpointstoNA\refelements{\modcap\idx}\elem$ %is the pointsto assertion for the \emph{nonatomic} cell at index~$\modcap\idx$ %of location~\refelements: it asserts the unique ownership of that cell, and %states that we have observed its latest write event, which wrote the value~$\elem$. % Recall that, in \hlog, unlike an atomic pointsto assertion, a nonatomic pointsto assertion is \emph{subjective}: its truth  POTTIER Francois committed Mar 03, 2021 209 depends on the view of the subject thread. As a consequence, it cannot be placed in  Glen Mével committed Mar 01, 2021 210 211 an invariant as is. %  POTTIER Francois committed Mar 03, 2021 212 213 In order to share this assertion, we must explicitly indicate at which view it holds.  Glen Mével committed Jun 03, 2021 214 This is the purpose of the $\opat$ connective.  Glen Mével committed Mar 01, 2021 215 216  At which view can we own a nonatomic memory cell?  Glen Mével committed Jun 04, 2021 217 218 At a view which contains the latest write event to that cell. %; for instance, the view of the last writer thread when that write occurred.  Glen Mével committed Mar 01, 2021 219 %  Glen Mével committed Mar 05, 2021 220 Fortunately, in our case, any thread---enqueuer or dequeuer---which writes to the  Glen Mével committed Mar 01, 2021 221 nonatomic cell $\refelements[\modcap\idx]$ then writes to the atomic cell  Glen Mével committed Jun 04, 2021 222 $\refstatuses[\modcap\idx]$. Thus it adds its knowledge, including its own  Glen Mével committed Mar 01, 2021 223 224 write to the item field, to the view~$\sview$ stored by the status field.  Glen Mével committed May 31, 2021 225 With all this said, a first attempt at representing the buffer might look as follows:  Glen Mével committed Mar 01, 2021 226 227 228 229 230 231 % $\begin{array}{rcl} % invariant (inner) (wrong): \queueInvInner & \tryeqdef  Glen Mével committed Mar 08, 2021 232  & \isepV{\begin{array}{c@{}l}  Glen Mével committed Mar 01, 2021 233 234 235 236 237 238 239 240 241 242 243 244 245 246  \vdots \\ \\ \displaystyle\Sep_{\head-\capacity \leq \idx < \tail}& \emptyCell \idx {\nthStatusView{\modcap\idx}} \\ \displaystyle\Sep_{\tail \leq \idx < \head}& \fullCell \idx {\nthStatusView{\modcap\idx}} {\nthElemView\idx} \end{array}} \\ % predicate for available cells (wrong): \emptyCell \idx {\pair\status\sview} & \tryeqdef & \status = 2(\idx + \capacity)  Glen Mével committed Mar 08, 2021 247  \ISEP (\nthpointstoNA\refelements{\modcap\idx}-) \opat \sview  Glen Mével committed Mar 01, 2021 248 249 250 251 252 253 254  \\ % predicate for occupied cells (wrong): \fullCell \idx {\pair\status\sview} {\pair\elem\eview} & \tryeqdef & \status = 2\idx + 1 \hphantom{()\,}  Glen Mével committed Mar 08, 2021 255 256  \ISEP (\nthpointstoNA\refelements{\modcap\idx}{\elem}) \opat \sview \ISEP \eview \viewleq \sview  Glen Mével committed Mar 01, 2021 257 258 259  \end{array}$  Glen Mével committed Mar 01, 2021 260 261 % GLEN: à partir d’ici, on omet "included / excluded" dans les intervalles… That is, we describe the $\capacity$~slots by ranging from~$\head-\capacity$ to~$\head$.  POTTIER Francois committed Mar 03, 2021 262 263 The indices from~$\head-\capacity$ to~$\tail$ correspond to available slots, while indices from~$\tail$ to~$\head$ correspond to slots occupied by the items of the queue.  Glen Mével committed May 31, 2021 264 In both cases, we own the item field at the view~$\sview$ which is stored in the corresponding status field.  Glen Mével committed Mar 01, 2021 265 266 267 268 269 270 271 The item field of an available slot stores an arbitrary value, while for an occupied slot it stores the item~$\elem$. An occupied slot should also carry the view~$\eview$ which the queue is supposed to transfer from the enqueuer to the dequeuer alongside item~$\elem$. This again relies on the view~$\sview$: the enqueuer adds $\eview$ to $\sview$ when updating the status, and the dequeuer adds~$\sview$ into its own view when  Glen Mével committed May 31, 2021 272 reading the status; so, to retrieve $\eview$, it is enough to state the inclusion  Glen Mével committed Mar 01, 2021 273 274 $\eview \viewleq \sview$.  Glen Mével committed Mar 02, 2021 275 276 277 278 279 The tentative invariant stated above, however, is not correct: while an invariant has to hold at any point of the execution, the assertion above is temporarily invalidated when a thread enqueues or dequeues. Specifically, the thread breaks the assertion when it increments \refhead or \reftail, thus commiting to enqueuing or dequeuing, until it updates the status  POTTIER Francois committed Mar 03, 2021 280 of the corresponding slot. It is thus necessary to represent slots which are in  Glen Mével committed Jun 06, 2021 281 a temporary state. In the actual invariant shown in~\fref{fig:queue:inv:inv},  Glen Mével committed Mar 02, 2021 282 283 284 285 286 287 288 slots from~$\head-\capacity$ to~$\tail$ are either available or in a temporary state where they appear as occupied ($\status_{\modcap\idx} = 2\idx + 1$), until a dequeuer finishes emptying them; slots from~$\tail$ to~$\head$ are either occupied or in a temporary state where they appear as available ($\status_{\modcap\idx} = 2\idx$), until an enqueuer finishes filling them.  Glen Mével committed Mar 02, 2021 289 290 291 292 293 When an enqueuer or dequeuer moves a slot into a temporary state, it takes ownership of its item field, so that it can write to it. Hence the invariant does not have the corresponding pointsto assertion. The thread must give it back when updating the status.  Glen Mével committed Jun 04, 2021 294 295 \subsection{Slot tokens}  Glen Mével committed Jun 06, 2021 296 297 %\input{figure-queue-ghost-token}  Glen Mével committed May 31, 2021 298 This time frame is also when the last piece of ghost state, stored in the ghost  POTTIER Francois committed Mar 03, 2021 299 variable~$\gtokens$, intervenes.  Glen Mével committed Mar 02, 2021 300 301 Other threads can make the queue progress between the moment when an enqueuer is attributed rank~$\idx$, and the moment when it returns the updated slot to the  Glen Mével committed Jun 04, 2021 302 303 invariant. An enqueuer needs the assurance that the queue has not gotten too far and attributed the slot on which it was working to a dequeuer, or  POTTIER Francois committed Mar 03, 2021 304 to another enqueuer in a subsequent cycle.  Glen Mével committed Mar 02, 2021 305 306 307 308 309 310 311 312 313 314  To this effect, we start by stating how advances of the \refhead and \reftail are limited with respect to one another; indeed, we prove these inequalities as part of the invariant: % $% 0 \leq \tail \leq \head \leq \tail+\capacity$% We also maintain in existence one token for each rank from~$\head-\capacity$  Glen Mével committed Jun 04, 2021 315 to~$\head$. These tokens are exclusive assertions, and there cannot exist two tokens  Glen Mével committed Mar 02, 2021 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 whose ranks are congruent modulo~$\capacity$. Hence the token of rank~$\idx$ is enough to grant unique write access to slot~$\modcap\idx$. % We use it as follows. % \begin{enumerate}% \item \label{item:token1} When an enqueuer is attributed rank~$\idx$, it borrows a newly created token of the same rank. \item \label{item:token2} When returning the updated slot to the invariant, the enqueuer also returns the token; from that moment the token is thus kept in the assertion $\fullCell \idx {\pair\status\sview} {\pair\elem\eview}$. \item \label{item:token3} When a dequeuer is attributed rank~$\idx$, it claims that assertion and borrows the token. \item \label{item:token4} When returning the updated slot to the invariant, the dequeuer also returns the token; from that moment the token is thus kept in the assertion $\emptyCell \idx {\pair\status\sview}$. \end{enumerate}% In step~\ref{item:token1}, the token is created while destructing the token of rank~$\idx-\capacity$ taken from the assertion $\emptyCell {(\idx-\capacity)} -$, which represents the available cell that the thread claims for enqueuing. To be able to distinguish between the two temporary states (enqueuing and dequeuing), we give the token a flavor: from steps~\ref{item:token1} to~\ref{item:token2} it is a \emph{write~token}; from steps~\ref{item:token3} to~\ref{item:token4} it is a \emph{read~token}. At any moment, there are read~tokens from rank~$\head-\capacity$ to~$\tail$, and write~tokens from~$\tail$ to~$\head$. We have a last requirement: when an enqueuer is attributed rank~$\idx$, the new item is added to the public state immediately---the CAS operation on \refhead  Jacques-Henri Jourdan committed May 31, 2021 351 is the commit point of enqueuing---even though the enqueuer has not  Glen Mével committed Mar 02, 2021 352 353 354 355 356 357 358 359 actually written the item yet. When it finally returns the updated slot, the enqueuer has lost track of the public state, which may have continued to progress in the meantime. At that moment, it thus needs a reminder that the item it just wrote is indeed the one it was expected to write. % We implement this by adding the value~$\elem$---and view~$\eview$---of the item as a payload to the write~token.  Glen Mével committed Jun 04, 2021 360 361 362 363 364 The read~token of rank~$\idx$ is denoted by $\tokenR\idx$, while the write~token of rank~$\idx$ with payload $\elem$ and $\eview$ is denoted by $\tokenW\idx{\pair\elem\eview}$. Their authoritative counterpart, owned by the invariant, is an assertion of the form $\ownGhost \gtokens {\authfull m}$ where $m$ is a finite map. Its domain is the range~$[\head-\capacity, \head)$ of ranks which have a token, and its images are the payload (considering that read~tokens bear a payload of $\Unit$). In the invariant, the value of the map is connected to that of the public state.  Glen Mével committed Jun 06, 2021 365 The assertions are defined in~\fref{fig:queue:inv:token} and satisfy the properties in~\fref{fig:queue:axioms:token}.  Glen Mével committed Jun 04, 2021 366 367 368 369 370 % The first three properties say that tokens are exclusive. % The next two say that tokens agree with the authoritative counterpart, hence with the public state. %  Glen Mével committed Jun 05, 2021 371 Rule~\ruleTokenUpdRW corresponds to step~\ref{item:token1} in the list above, where we create a write~token of rank~$\idx$ by destructing a read~token of rank~$\idx-\capacity$.  Glen Mével committed Jun 04, 2021 372 %  Glen Mével committed Jun 05, 2021 373 Likewise, rule~\ruleTokenUpdWR corresponds to step~\ref{item:token3}, where we turn a write~token into a read~token of the same rank.  Glen Mével committed Jun 04, 2021 374   Glen Mével committed Jun 06, 2021 375 In addition to these rules, the finite map described in the internal invariant is such that,  Glen Mével committed Jun 04, 2021 376 whenever we own a read~token (respectively a write~token), the rank of this token necessarily lies in the range~$[\head-\capacity, \tail)$ (respectively $[\tail, \head)$), where $\tail$ and $\head$ are the values of $\reftail$ and $\refhead$ which are existentially quantified in the invariant.  Glen Mével committed Jun 04, 2021 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 Thanks to that property, at step~\ref{item:token4} (respectively~\ref{item:token2}), when a dequeuer (respectively an enqueuer) returns the token, it knows that the rank it has been operating on is still in the right range---in other words, that the queue has not advanced too far while the thread was working. %To implement a token in ghost state, we again use an authority over an exclusive %value. %%The authority states the existence of the token. %The authority represents the duplicate of the token. %As we want one token for each rank in some range, we again use a finite partial %function; however, this time its domain $[\head-\capacity, \head)$ is not fixed, %so we apply the authority on the function itself. Hence, the CMRA of~$\gtokens$ %is $\authm\left(\finmapm{\Z}{\exm(M)}\right)$, %where $M$ is a CMRA for the payload of the tokens. %The token of rank~$\idx$, bearing the payload~$x \in M$, is %$\ownGhost\gtokens{\authfrag \mapsingleton\idx x}$. % %To achieve the distinction between read~tokens and write~tokens, $M$ is %a disjoint sum $M\sub{read} + M\sub{write}$. %Read~tokens do not carry a payload, % so we take for~$M\sub{read}$ the singleton set, $\typeUnit$. %Write~tokens carry as their payload an item, that is, a value and a view, % so we take for~$M\sub{write}$ the product set $\typeVal\times\typeView$. %Read~tokens and write~tokens are then defined as shown in~\fref{fig:queue:inv}.  Glen Mével committed Mar 02, 2021 398   Glen Mével committed Mar 02, 2021 399 400 % ------------------------------------------------------------------------------  Glen Mével committed Jun 04, 2021 401 402 There are more properties that are invariants of the queue, and thus could be stated and verified. However, they are not needed to  POTTIER Francois committed Mar 03, 2021 403 404 prove that the code satisfies its specification. For example, the fact that \reftail and \refhead are strictly monotonic, and the fact that statuses are non-negative, are not explicitly used.  Glen Mével committed Mar 02, 2021 405   Glen Mével committed Mar 03, 2021 406 \subsection{Logical atomicity}  Glen Mével committed Mar 03, 2021 407 408 \label{sec:queue:proof:la}  POTTIER Francois committed Mar 03, 2021 409 The specification that we wish to prove is a logically atomic Hoare triple.  Jacques-Henri Jourdan committed May 31, 2021 410 The definition of such triples is given by~\citet[\S7]{iris-15} and  POTTIER Francois committed Mar 03, 2021 411 412 413 further refined by~\citet{jung-slides-2019}. We do not attempt to replicate their explanation and full definition. An approximate definition that suffices to capture the essence of logical atomicity, and to understand our proof, is:  Glen Mével committed Mar 03, 2021 414 415 % $\begin{array}{rcl}%  416  \lahoare{P}{e}{\pred}  Glen Mével committed Mar 03, 2021 417  &\eqdef&  418  \Forall \predB,  Jacques-Henri Jourdan committed May 31, 2021 419 420  \left[ \pvs[\top][\emptyset] \Exists x. P \ISEP \left(\Forall v. \pred\;v \WAND\pvs[\emptyset][\top] \predB\;v\right)  Glen Mével committed Mar 03, 2021 421  \right]  Glen Mével committed Mar 08, 2021 422  \WAND  423  \wpre e \predB  Glen Mével committed Mar 03, 2021 424 425 426 \end{array}$% In this formula,  Jacques-Henri Jourdan committed May 31, 2021 427 the variable~$P$ is a Cosmo assertion (of type $\typeVProp$);  428 429 the variables~$\pred$ and~$\predB$ are predicates on values (of type $\typeVal \ra \typeVProp$); $P$ and $\pred$ may refer to the name~$x$.  Glen Mével committed Mar 03, 2021 430 %  431 432 The assertion $\wpre e \predB$ is the weakest precondition for program~$e$ and postcondition~$\predB$  POTTIER Francois committed Mar 03, 2021 433 (in Iris, Hoare triples are syntactic sugar for weakest preconditions).  Jacques-Henri Jourdan committed May 31, 2021 434   Glen Mével committed Jun 03, 2021 435 436 437 438 439 The purpose of a logically atomic triple is to give a specification to a non-atomic program $e$ \emph{as if it were atomic}. In practice, we require that the proof of $e$ accesses the precondition and turns it into the postcondition in \emph{one atomic step} only, which we call the commit point of this logically atomic program. That is, if $e$ satisfies the triple $\lahoare{P}{e}{\pred}$, then it can perform several steps of computation but, as soon as it accesses the resource~$P$, it must return the resource~$\pred$ in the same step of computation.\footnote{The full definition of logically atomic triples allows to access the precondition atomically before the commit point, hence without turning it into the postcondition. This is called \emph{aborting}; it is not needed in our proof, and out of the scope of this paper.} Once it has done so, $e$ can perform further computation steps but $P$ is not available anymore. As explained in \sref{sec:queue:spec:sc}, thanks to this constraint, the client of this specification can open invariants around $e$ as if $e$ were atomic.  Jacques-Henri Jourdan committed May 31, 2021 440   Glen Mével committed Jun 03, 2021 441 To capture this atomicity requirement, we ask the proof of the logically atomic triple for $e$ to be valid for any postcondition $\predB$ chosen by the client.  POTTIER Francois committed Jun 02, 2021 442 443 444 Given that $\predB$ is arbitrary, the only means of establishing this postcondition is to use the premise $\pvs[\top][\emptyset] \Exists x. P \ISEP (\Forall v. \pred\;v \WAND\pvs[\emptyset][\top] \predB\;v)$, which is known as an \emph{atomic update}. When desired, this atomic update gives access to the precondition~$P$ for some value of $x$, and, in exchange for the postcondition $\pred$ of the logically atomic triple, it returns the resource $\predB$, which can then be used to finish the proof. Crucially, the \emph{masks} $\emptyset$ and $\top$ annotating the \emph{fancy updates} $\pvs[\top][\emptyset]$ and $\pvs[\emptyset][\top]$ require that the atomic update be used during one atomic step only, as required.  Jacques-Henri Jourdan committed May 31, 2021 445 446  Using the invariant rules of Iris~\cite{iris}, it is easy to show that atomic updates can be used to open and close invariants.  Glen Mével committed Jun 06, 2021 447 Rule~\rulelainv follows as a corollary, rule~\rulelahoare is immediate.  Jacques-Henri Jourdan committed May 31, 2021 448   Glen Mével committed Mar 03, 2021 449   Glen Mével committed Mar 03, 2021 450 451 452 453 454 455 456 \subsection{Proof of \tryenqueue} \label{sec:queue:proof:tryenqueue} We now outline the proof that \tryenqueue satisfies its specification from~\fref{fig:queue:spec:weak}. % The proof for \trydequeue is similar; those for \enqueue and \dequeue are  POTTIER Francois committed Mar 03, 2021 457 deduced from the previous two by an obvious induction; and the proof of \make is  Glen Mével committed Mar 03, 2021 458 459 simply a matter of initializing the ghost state. %  POTTIER Francois committed Mar 03, 2021 460 The interested reader may  Glen Mével committed May 31, 2021 461 find these proofs, conducted in the Coq proof assistant, in our repository~\citep{repo}.  Glen Mével committed Mar 03, 2021 462   Glen Mével committed Mar 03, 2021 463 464 465 Recalling here the specification in~\fref{fig:queue:spec:weak}, and unfolding the definition of $\queueInv$, we ought to prove the following assertion: %  Glen Mével committed Mar 03, 2021 466 467 $\begin{array}{@{}l@{}} \infer{%  Glen Mével committed Mar 03, 2021 468 469  %\queueInv \knowInv{}{\queueInvInner}  Glen Mével committed Mar 08, 2021 470  }{%  Glen Mével committed Mar 03, 2021 471 472 473 474 475 476  \lahoareV {\begin{array}{@{}l@{}} \lahoarebinder{\tview, \hview, \nbelems, \elemViewList*[]} \\ \hspace{2.9em} \isQueue \tview {\hphantom(\hview\hphantom{{}\viewjoin\view)}} \elemViewList \hphantom{, \pair\elem\view}  Glen Mével committed Mar 08, 2021 477  \ISEP \seen\view  Glen Mével committed Mar 03, 2021 478 479 480 481 482 483 484  \end{array}} {\tryenqueue~\queue~\elem} {\Lam \boolval. \matchwithnobinder{\boolval} {\False}{\isQueue \tview {\hphantom(\hview\hphantom{{}\viewjoin\view)}} \elemViewList} {\True }{% \isQueue \tview {(\hview \sqcup \view)} {\elemListSnoc \elemViewList {\pair\elem\view}}  Glen Mével committed Mar 08, 2021 485  \ISEP \seen\hview  Glen Mével committed Mar 03, 2021 486 487  } }  Glen Mével committed Mar 08, 2021 488  }  Glen Mével committed Mar 03, 2021 489 \end{array}$  Glen Mével committed Mar 02, 2021 490   Glen Mével committed Mar 03, 2021 491 After unfolding the logically atomic triple, we must prove  492 $\wpre {(\tryenqueue\;\queue\;\elem)} \predB$ for any~$\predB$,  Glen Mével committed Mar 03, 2021 493 494 495 496 497 when in the proof context we have the internal invariant of the queue (with ghost variables~$\gqueue, \gmonos, \gtokens$) as well as the atomic update whose precondition and postconditions are that of the triple above. We then step through the program using usual weakest-precondition calculus.  POTTIER Francois committed Mar 03, 2021 498 The first interesting step is the atomic read of \refhead. The ownership of that  Glen Mével committed Mar 03, 2021 499 500 501 502 reference is shared in the invariant of the queue. Hence, to access it, we must open the invariant; then we get the pointsto assertion, we can step through the read operation, return the pointsto assertion and close the invariant again. After we have done so, and thus forgotten all the quantities which are  POTTIER Francois committed Mar 03, 2021 503 504 505 existentially quantified inside that invariant, we learn little about the value that has just been read, excepted that it is a nonnegative integer, say~$\idx$.  Glen Mével committed Mar 03, 2021 506   Glen Mével committed Mar 03, 2021 507 The second interesting step is the atomic read at index~$\modcap\idx$  POTTIER Francois committed Mar 03, 2021 508 509 of the array~\refstatuses. Again the invariant owns this cell, so we open it around the read instruction. This read yields some value~$\status^1$ and,  Glen Mével committed Mar 03, 2021 510 since it is atomic, it also augments our current (thread) view with the  POTTIER Francois committed Mar 03, 2021 511 512 513 514 515 view~$\sview^1$ which, at this moment, is stored in this cell. In other words, we gain the (persistent) assertion $\seen\sview^1$. % (previously, the read to \refhead also augmented our current view, but we chose % to ignore that fact as it is not useful in the proof). We can remember more information before closing the invariant:  Glen Mével committed Mar 03, 2021 516 517 indeed, from the authority of~$\gmonos$ found in the invariant, we derive a witness for the strict monotonicity of the status that we just read:  Glen Mével committed Mar 03, 2021 518 $\monoWitness {\modcap\idx} {\pair{\status^1}{\sview^1}}$.  Glen Mével committed Mar 03, 2021 519   Glen Mével committed Mar 03, 2021 520 Next, the program tests whether $\status^1 = 2\idx$. If the test fails, then  Glen Mével committed Mar 03, 2021 521 522 523 the program returns $\False$. In this case, we have to provide as postcondition of the logically atomic triple the untouched representation predicate that is in its precondition ($\isQueue \tview \hview \elemViewList$). We do this by  Glen Mével committed Mar 03, 2021 524 committing the atomic update in a trivial way, then conclude the proof.  Glen Mével committed Mar 03, 2021 525   Glen Mével committed Mar 03, 2021 526 527 If $\status^1 = 2\idx$, the program proceeds to performing $\CAS \refhead \idx {(\idx+1)}$.  Glen Mével committed Mar 03, 2021 528 529 To access \refhead, we open the invariant again. If that operation fails, the program also returns $\False$ and, after closing  Jacques-Henri Jourdan committed Jun 03, 2021 530 the invariant without having updated ghost state, we conclude as before.  Glen Mével committed Mar 03, 2021 531 532  If the CAS succeeds, then a number of things happen logically.  Glen Mével committed Mar 03, 2021 533 First, if $\head$ and $\tail$ are the values of \refhead and \reftail at the  Glen Mével committed Mar 03, 2021 534 moment of the CAS, then $\head = \idx$.  Glen Mével committed Mar 03, 2021 535 536 537 Second, we deduce that the buffer is not full, i.e.\ $\head < \tail+\capacity$. Indeed, the invariant directly gives us $\head \leq \tail+\capacity$; if we had $\head = \tail+\capacity$, then in particular,  Glen Mével committed Mar 03, 2021 538 539 $\tail \leq \idx-\capacity < \head$, so the invariant would own the following for slot~$\modcap{\idx-\capacity}$:  Glen Mével committed Mar 03, 2021 540 541 % $%  Glen Mével committed Mar 03, 2021 542  \fullCell {(\idx-\capacity)} {\nthStatusView{\modcap{\idx-\capacity}}} {\nthElemView{\idx-\capacity}}  Glen Mével committed Jun 05, 2021 543  \LOR  Glen Mével committed Mar 03, 2021 544  \status_{\modcap{\idx-\capacity}} = 2(\idx-\capacity)  Glen Mével committed Mar 03, 2021 545 546 $% %  Glen Mével committed Mar 03, 2021 547 Because $\modcap{\idx-\capacity} = \modcap\idx$, this implies:  Glen Mével committed Mar 03, 2021 548 549 % $%  Glen Mével committed Mar 03, 2021 550  \status_{\modcap\idx} = 2(\idx-\capacity) + 1  Glen Mével committed Jun 05, 2021 551  \LOR  Glen Mével committed Mar 03, 2021 552  \status_{\modcap\idx} = 2(\idx-\capacity)  Glen Mével committed Mar 03, 2021 553 554 $% %  Glen Mével committed Mar 03, 2021 555 In either case, we get $\status_{\modcap\idx} < 2\idx = \status^1$,  Glen Mével committed Mar 03, 2021 556 557 which contradicts the monotonicity of the status of that slot. We derive the contradiction by combining the assertion  Glen Mével committed Mar 03, 2021 558 $\monoWitness {\modcap\idx} {\pair{\status^1}{\sview^1}}$  Glen Mével committed Mar 03, 2021 559 560 that we had since we read the status, and the authority  Glen Mével committed Mar 03, 2021 561 $\ownGhost \gmonos {\authfull \nthStatusView{\modcap\idx}}$  POTTIER Francois committed Mar 03, 2021 562 that is found in the invariant.  Glen Mével committed Mar 03, 2021 563   Glen Mével committed Mar 03, 2021 564 Third, we thus know that $\head-\capacity \leq \idx-\capacity < \tail$, so  Glen Mével committed Mar 03, 2021 565 566 567 that the invariant gives us: % $%  Glen Mével committed Mar 03, 2021 568  \emptyCell {(\idx-\capacity)} {\nthStatusView{\modcap{\idx-\capacity}}}  Glen Mével committed Jun 05, 2021 569  \LOR  Glen Mével committed Mar 03, 2021 570  \status_{\modcap{\idx-\capacity}} = 2(\idx-\capacity)+1  Glen Mével committed Mar 03, 2021 571 572 $% %  Jacques-Henri Jourdan committed Jun 04, 2021 573 Again the second disjunct is absurd because the status is monotonic. Hence the slot we are claiming is available indeed.  Glen Mével committed Mar 03, 2021 574 575 % From this  Glen Mével committed Mar 03, 2021 576 %$\emptyCell {(\idx-\capacity)} {\nthStatusView{\modcap\idx}}$,  Glen Mével committed Mar 03, 2021 577 we get  Glen Mével committed Mar 03, 2021 578 579 580 $\status_{\modcap\idx} = 2\idx = \status^1$, the pointsto assertion $(\nthpointstoNA\refelements{\modcap\idx}-) \opat \sview_{\modcap\idx}$ and the read~token of rank~$\idx-\capacity$.  Glen Mével committed Mar 03, 2021 581 The sets of read~tokens and write~tokens depend on the value of \reftail and  Glen Mével committed Mar 03, 2021 582 583 584 585 586 587 588 589 590 591 592 \refhead, and we have just incremented the latter, to $\idx+1$, so we destruct the read~token of rank~$\idx-\capacity$ and create a write~token of rank~$\idx$ instead, giving it as payload the item~$\pair\elem\eview$ that we are trying to enqueue. This is also when the \emph{strict} monotonicity of the status comes into play: because $\status_\idx = \status^1$, it gives us $\sview_\idx \viewleq \sview^1$. But we have $\seen\sview^1$ in our proof context, so we obtain the pointsto assertion as a subjective assertion: $\nthpointstoNA\refelements{\modcap\idx}-$.  Jacques-Henri Jourdan committed May 31, 2021 593 We commit the atomic update now. Indeed the successful CAS is the commit  Glen Mével committed Mar 03, 2021 594 595 596 597 point of \tryenqueue. We know that the program will return $\True$, so we must provide the corresponding postcondition of the logically atomic triple, where our item~$\pair\elem\eview$ has been appended to the public state of the queue. Thus we take a ghost step to update this public state.  POTTIER Francois committed Mar 03, 2021 598 599 600 By committing, we finally obtain the assertion $\predB\;\True$ that will serve at the end of the proof, since $\True$ is the return value of the operation.  Glen Mével committed Mar 03, 2021 601 602 603 604 605 Along the way, we also collect the persistent assertion $\seen\eview$ from the precondition of the logically atomic triple. Finally, we keep on our side the write~token, the nonatomic pointsto assertion $\nthpointstoNA\refelements{\modcap\idx}-$,  POTTIER Francois committed Mar 03, 2021 606 we reconstruct the invariant, updated for the new value of \refhead, and we close it.  Glen Mével committed Mar 03, 2021 607 608 609 610 611  The next step of the program writes the value~$\elem$ to the nonatomic item field, which is easy since we have the pointsto assertion at hand. This assertion then becomes $\nthpointstoNA\refelements{\modcap\idx}\elem$. We turn it back to an objective assertion, which gives us a view~$\viewB$ and  POTTIER Francois committed Mar 03, 2021 612 two assertions $\seen\viewB$ and  Glen Mével committed Mar 03, 2021 613 614 615 616 617 618 619 620 621 622 623 $(\nthpointstoNA\refelements{\modcap\idx}\elem) \opat \viewB$. The last step of the program is to update the (atomic) status of the slot. Once more we open the invariant. If we again note $\head$ and $\tail$ the current values of \refhead and \reftail (potentially different from the last time we opened the invariant), then owning a write~token for rank~$\idx$ teaches us that $\tail \leq \idx < \head$. The invariant then gives us for slot~$\modcap\idx$: % $% \fullCell \idx {\nthStatusView{\modcap\idx}} {\nthElemView\idx}  Glen Mével committed Jun 05, 2021 624  \LOR  Glen Mével committed Mar 03, 2021 625 626 627  \status_{\modcap\idx} = 2\idx$% %  Jacques-Henri Jourdan committed Jun 04, 2021 628 629 The left disjunct would own our write~token, but we already have it and it is exclusive; hence we are in the right disjunct, $\status_{\modcap\idx} = 2\idx = s^1$.  Glen Mével committed Mar 03, 2021 630 631 632 633 634 We perform the atomic write with value~$\status^2 \eqdef 2\idx+1$ (strict monotonicity is respected), and since we have both $\seen\eview$ and $\seen\viewB$ in context, we can push the view~$\sview^2 = \eview \viewjoin \viewB$ to this atomic location while writing.  Jacques-Henri Jourdan committed Jun 04, 2021 635 We then switch to the left disjunct, by constituting the assertion:  Glen Mével committed Mar 03, 2021 636 637 638 % $% \fullCell \idx {\pair{\status^2}{\sview^2}} {\pair\elem\eview}  Glen Mével committed Jun 05, 2021 639  \;\iequiv\;  Glen Mével committed Mar 08, 2021 640  \isepV{%  Glen Mével committed Mar 03, 2021 641 642 643 644 645 646 647 648 649  \status^2 = 2\idx + 1 \cr (\nthpointstoNA\refelements{\modcap\idx}{\elem}) \opat \sview^2 \cr \tokenW\idx{\pair\elem\eview} \cr \eview \viewleq \sview^2 }$% % Hence we return the nonatomic pointsto assertion and the write~token to the invariant before closing it.  Glen Mével committed Mar 03, 2021 650   POTTIER Francois committed Mar 03, 2021 651 652 653 % FP: ça me paraît bien, tout ça. % Il faudra sans doute numéroter les lignes du code % et faire référence à des numéros précis dans le texte.