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

https://about.gitlab.com/releases/2022/01/11/security-release-gitlab-14-6-2-released/
https://about.gitlab.com/releases/2022/01/04/gitlab-14-6-1-released/

queue-proof.tex 33.2 KB
Newer Older
1
2
3
4
% ------------------------------------------------------------------------------

% Proof of the bounded queue.

5
\section{Proof of the Specification for the Ring Buffer}
6
7
\label{sec:queue:proof}

Glen Mével's avatar
Glen Mével committed
8
\input{figure-queue-inv}
9

Glen Mével's avatar
Glen Mével committed
10
11
12
We now turn to proving the following.

\begin{theorem}%
POTTIER Francois's avatar
POTTIER Francois committed
13
  The implementation shown in \fref{fig:queue:impl} (\sref{sec:queue:impl})
Glen Mével's avatar
Glen Mével committed
14
15
16
  satisfies the functional specification appearing in \fref{fig:queue:spec:weak}
  (\sref{sec:queue:spec:weak}).
\end{theorem}%
17

18
In the Iris methodology, which \hlog{} is based on, concurrent protocols are established thanks to \emph{ghost state} and \emph{invariants}.
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
22
equipped with a binary composition operation $(\mtimes)$ that is partial,
23
associative and commutative.
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$.
28
Unlike what happens with a traditional pointsto assertion, the ownership \emph{and value} of
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}
\).
34
35
In \hlog, ghost state is objective, as it is independent from the physical state
of the memory.%
36
37
38
  %% \footnote{%
  %%   In fact, the physical memory is itself encoded as a piece of ghost state.
  %% }
39

40

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.
43
44
We detail these definitions in the following sections.

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}

56
\subsection{Public state}
57

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
61
state of the queue. This public state, as motivated in \sref{sec:queue:spec:weak},
62
is composed of the tail view, the head view, and the list of current items with
63
their views.
64
65
%
It is tied to the internal state of the queue via the use of an authoritative
66
67
ghost state, stored in a ghost variable~$\gqueue$.
%
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.
69

70
Formally, the two assertions satisfy the properties shown in~\fref{fig:queue:axioms:isqueue}.
71
%
72
Rule~\ruleIsQueueAg asserts that the state known to the invariant (first premise) is identical to that known to the representation predicate (second premise).
73
%
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.
75

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}.
79

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 - - -$.
81

82
\subsection{Internal invariant}
83

84
Along with the exclusive representation predicate $\isQueue\tview\hview\elemViewList$,
85
we provide the user with a persistent assertion $\queueInv$ defined in~\fref{fig:queue:inv:inv}. It contains the
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
89
to the user of the queue but needed internally. Thus they are
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$.
93

94
95
This invariant owns most of the physical locations of the queue: \reftail,
\refhead, \refstatuses, and some parts of the array \refelements.
96
Recall that pointsto assertions for atomic cells are objective and can be placed inside an invariant.
97
98
%
The array-pointsto assertion $\arraypointstoAT\refstatuses\statusViewList$ is
99
a shorthand for the following iterated conjunction:
100
101
102
103
\[
  \Sep_{0 \leq \offset < \capacity} \nthpointstoAT\refstatuses\offset{\mkval{\status_\offset}{\sview_\offset}}
\]
%
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).
109
%
110
111
Also, since we encode references as arrays of length~one,
we write $\pointstoAT\reftail{\mkval\tail\tview}$ as a shorthand for
112
113
$\nthpointstoAT\reftail0{\mkval\tail\tview}$.

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.
119
We now explain the other two pieces of ghost state.
120

121
\subsection{Monotonicity of statuses}
122

123
124
125
%\input{figure-queue-ghost-witness}
%\input{figure-queue-cmra-statlat}

126
127
128
The purpose of the ghost variable~$\gmonos$ is to reflect the fact that statuses
are monotonic.
%
POTTIER Francois's avatar
POTTIER Francois committed
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.
130
%
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)
\]
140
%
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$.
148
Relevant definitions appear in~\fref{fig:queue:inv:witness}.
149
%
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's avatar
POTTIER Francois committed
151
152
In addition, it is exclusive: for any offset~$\offset$, two assertions
of the form $\ownGhost \gmonos {\mapsingleton\offset{\authfull -}}$ cannot hold simultaneously.
153
%
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.
156

157
We thus have the properties summarized in~\fref{fig:queue:axioms:witness}.
158
%
159
Rule~\ruleWitnessPers is the persistency just mentioned.
160
%
161
Rule~\ruleWitnessOrder asserts that a witness gives a lower bound on what the status cell currently stores.
162
%
163
Rule~\ruleWitnessUpd asserts that we can update a status cell to any larger or equal content, and obtain a witness for that content.
164

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's avatar
Glen Mével committed
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's avatar
Glen Mével committed
179
composition of the CMRA\@~\cite{timany2021monotonicity}.
Glen Mével's avatar
Glen Mével committed
180
In this case, we equip the product set \(\Z \times \typeView\) with
181
the join-semilattice structure whose definition appears in~\fref{fig:queue:cmra:statlat}.
182

183
\subsection{Available and occupied slots}
184

185
In~\fref{fig:queue:inv:inv}, the last two lines of the invariant describe the state of each slot.
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$.
199
200
%
These abbreviations are also where we keep the ownership of the \emph{nonatomic} cell $\refelements[\modcap\idx]$, via a pointsto assertion.
201
202

%In both cases, we must own the memory cell.
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
209
depends on the view of the subject thread. As a consequence, it cannot be placed in
210
211
an invariant as is.
%
212
213
In order to share this assertion,
we must explicitly indicate at which view it holds.
214
This is the purpose of the $\opat$ connective.
215
216

At which view can we own a nonatomic memory cell?
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.
219
%
Glen Mével's avatar
Glen Mével committed
220
Fortunately, in our case, any thread---enqueuer or dequeuer---which writes to the
221
nonatomic cell $\refelements[\modcap\idx]$ then writes to the atomic cell
222
$\refstatuses[\modcap\idx]$. Thus it adds its knowledge, including its own
223
224
write to the item field, to the view~$\sview$ stored by the status field.

225
With all this said, a first attempt at representing the buffer might look as follows:
226
227
228
229
230
231
%
\[\begin{array}{rcl}

  % invariant (inner) (wrong):
    \queueInvInner
  & \tryeqdef
Glen Mével's avatar
Glen Mével committed
232
  & \isepV{\begin{array}{c@{}l}
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's avatar
Glen Mével committed
247
      \ISEP (\nthpointstoNA\refelements{\modcap\idx}-) \opat \sview
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's avatar
Glen Mével committed
255
256
      \ISEP (\nthpointstoNA\refelements{\modcap\idx}{\elem}) \opat \sview
      \ISEP \eview \viewleq \sview
257
258
259

\end{array}\]

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$.
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.
264
In both cases, we own the item field at the view~$\sview$ which is stored in the corresponding status field.
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
272
reading the status; so, to retrieve $\eview$, it is enough to state the inclusion
273
274
$\eview \viewleq \sview$.

Glen Mével's avatar
Glen Mével committed
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
280
of the corresponding slot. It is thus necessary to represent slots which are in
281
a temporary state. In the actual invariant shown in~\fref{fig:queue:inv:inv},
Glen Mével's avatar
Glen Mével committed
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's avatar
Glen Mével committed
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.

294
295
\subsection{Slot tokens}

296
297
%\input{figure-queue-ghost-token}

298
This time frame is also when the last piece of ghost state, stored in the ghost
299
variable~$\gtokens$, intervenes.
Glen Mével's avatar
Glen Mével committed
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
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
304
to another enqueuer in a subsequent cycle.
Glen Mével's avatar
Glen Mével committed
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$
315
to~$\head$. These tokens are exclusive assertions, and there cannot exist two tokens
Glen Mével's avatar
Glen Mével committed
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's avatar
Jacques-Henri Jourdan committed
351
is the commit point of enqueuing---even though the enqueuer has not
Glen Mével's avatar
Glen Mével committed
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.

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.

365
The assertions are defined in~\fref{fig:queue:inv:token} and satisfy the properties in~\fref{fig:queue:axioms:token}.
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.
%
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$.
372
%
373
Likewise, rule~\ruleTokenUpdWR corresponds to step~\ref{item:token3}, where we turn a write~token into a read~token of the same rank.
374

375
In addition to these rules, the finite map described in the internal invariant is such that,
Glen Mével's avatar
Glen Mével committed
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.
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's avatar
Glen Mével committed
398

Glen Mével's avatar
Glen Mével committed
399
400
% ------------------------------------------------------------------------------

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
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's avatar
Glen Mével committed
405

406
\subsection{Logical atomicity}
407
408
\label{sec:queue:proof:la}

409
The specification that we wish to prove is a logically atomic Hoare triple.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
410
The definition of such triples is given by~\citet[\S7]{iris-15} and
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:
414
415
%
\[\begin{array}{rcl}%
416
    \lahoare<x>{P}{e}{\pred}
417
    &\eqdef&
418
    \Forall \predB,
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
419
420
      \left[ \pvs[\top][\emptyset] \Exists x.
        P \ISEP \left(\Forall v. \pred\;v \WAND\pvs[\emptyset][\top] \predB\;v\right)
421
      \right]
Glen Mével's avatar
Glen Mével committed
422
      \WAND
423
      \wpre e \predB
424
425
426
\end{array}\]%

In this formula,
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
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$.
430
%
431
432
The assertion $\wpre e \predB$ is the weakest precondition for program~$e$ and
postcondition~$\predB$
433
(in Iris, Hoare triples are syntactic sugar for weakest preconditions).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
434

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<x>{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's avatar
Jacques-Henri Jourdan committed
440

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's avatar
POTTIER Francois committed
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's avatar
Jacques-Henri Jourdan committed
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.
447
Rule~\rulelainv follows as a corollary, rule~\rulelahoare is immediate.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
448

449

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
457
deduced from the previous two by an obvious induction; and the proof of \make is
458
459
simply a matter of initializing the ghost state.
%
460
The interested reader may
Glen Mével's avatar
Glen Mével committed
461
find these proofs, conducted in the Coq proof assistant, in our repository~\citep{repo}.
462

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:
%
466
467
\[\begin{array}{@{}l@{}}
  \infer{%
468
469
    %\queueInv
    \knowInv{}{\queueInvInner}
470
  }{%
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's avatar
Glen Mével committed
477
        \ISEP \seen\view
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's avatar
Glen Mével committed
485
            \ISEP \seen\hview
486
487
          }
      }
488
  }
489
\end{array}\]
Glen Mével's avatar
Glen Mével committed
490

491
After unfolding the logically atomic triple, we must prove
492
$\wpre {(\tryenqueue\;\queue\;\elem)} \predB$ for any~$\predB$,
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.

498
The first interesting step is the atomic read of \refhead. The ownership of that
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
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$.
506

Glen Mével's avatar
Glen Mével committed
507
The second interesting step is the atomic read at index~$\modcap\idx$
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,
510
since it is atomic, it also augments our current (thread) view with the
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:
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's avatar
Glen Mével committed
518
$\monoWitness {\modcap\idx} {\pair{\status^1}{\sview^1}}$.
519

Glen Mével's avatar
Glen Mével committed
520
Next, the program tests whether $\status^1 = 2\idx$. If the test fails, then
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's avatar
Glen Mével committed
524
committing the atomic update in a trivial way, then conclude the proof.
525

Glen Mével's avatar
Glen Mével committed
526
527
If $\status^1 = 2\idx$, the program proceeds to performing
$\CAS \refhead \idx {(\idx+1)}$.
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's avatar
Jacques-Henri Jourdan committed
530
the invariant without having updated ghost state, we conclude as before.
531
532

If the CAS succeeds, then a number of things happen logically.
533
First, if $\head$ and $\tail$ are the values of \refhead and \reftail at the
Glen Mével's avatar
Glen Mével committed
534
moment of the CAS, then $\head = \idx$.
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's avatar
Glen Mével committed
538
539
$\tail \leq \idx-\capacity < \head$, so the invariant would own the following
for slot~$\modcap{\idx-\capacity}$:
540
541
%
\[%
Glen Mével's avatar
Glen Mével committed
542
  \fullCell {(\idx-\capacity)} {\nthStatusView{\modcap{\idx-\capacity}}} {\nthElemView{\idx-\capacity}}
543
  \LOR
Glen Mével's avatar
Glen Mével committed
544
  \status_{\modcap{\idx-\capacity}} = 2(\idx-\capacity)
545
546
\]%
%
Glen Mével's avatar
Glen Mével committed
547
Because $\modcap{\idx-\capacity} = \modcap\idx$, this implies:
548
549
%
\[%
Glen Mével's avatar
Glen Mével committed
550
  \status_{\modcap\idx} = 2(\idx-\capacity) + 1
551
  \LOR
Glen Mével's avatar
Glen Mével committed
552
  \status_{\modcap\idx} = 2(\idx-\capacity)
553
554
\]%
%
Glen Mével's avatar
Glen Mével committed
555
In either case, we get $\status_{\modcap\idx} < 2\idx = \status^1$,
556
557
which contradicts the monotonicity of the status of that slot. We derive the
contradiction by combining the assertion
Glen Mével's avatar
Glen Mével committed
558
$\monoWitness {\modcap\idx} {\pair{\status^1}{\sview^1}}$
559
560
that we had since we read the status,
and the authority
Glen Mével's avatar
Glen Mével committed
561
$\ownGhost \gmonos {\authfull \nthStatusView{\modcap\idx}}$
562
that is found in the invariant.
563

Glen Mével's avatar
Glen Mével committed
564
Third, we thus know that $\head-\capacity \leq \idx-\capacity < \tail$, so
565
566
567
that the invariant gives us:
%
\[%
Glen Mével's avatar
Glen Mével committed
568
  \emptyCell {(\idx-\capacity)} {\nthStatusView{\modcap{\idx-\capacity}}}
569
  \LOR
Glen Mével's avatar
Glen Mével committed
570
  \status_{\modcap{\idx-\capacity}} = 2(\idx-\capacity)+1
571
572
\]%
%
573
Again the second disjunct is absurd because the status is monotonic. Hence the slot we are claiming is available indeed.
574
575
%
From this
Glen Mével's avatar
Glen Mével committed
576
%$\emptyCell {(\idx-\capacity)} {\nthStatusView{\modcap\idx}}$,
577
we get
Glen Mével's avatar
Glen Mével committed
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$.
581
The sets of read~tokens and write~tokens depend on the value of \reftail and
Glen Mével's avatar
Glen Mével committed
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's avatar
Jacques-Henri Jourdan committed
593
We commit the atomic update now. Indeed the successful CAS is the commit
Glen Mével's avatar
Glen Mével committed
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.
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's avatar
Glen Mével committed
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}-$,
606
we reconstruct the invariant, updated for the new value of \refhead, and we close it.
Glen Mével's avatar
Glen Mével committed
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
612
two assertions $\seen\viewB$ and
Glen Mével's avatar
Glen Mével committed
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}
624
  \LOR
Glen Mével's avatar
Glen Mével committed
625
626
627
  \status_{\modcap\idx} = 2\idx
\]%
%
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's avatar
Glen Mével committed
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.
635
We then switch to the left disjunct, by constituting the assertion:
Glen Mével's avatar
Glen Mével committed
636
637
638
%
\[%
  \fullCell \idx {\pair{\status^2}{\sview^2}} {\pair\elem\eview}
639
  \;\iequiv\;
Glen Mével's avatar
Glen Mével committed
640
  \isepV{%
Glen Mével's avatar
Glen Mével committed
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.
650

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.