queue-spec-sc.tex 9.44 KB
Newer Older
1
\subsection{Specification under sequential consistency}
2
3
\label{sec:queue:spec:sc}

Glen Mével's avatar
Glen Mével committed
4
We now consider a situation where several threads can access the queue concurrently.
Glen Mével's avatar
Glen Mével committed
5
Let us assume for now that the memory model is sequentially consistent~\cite{lamport-79}.
6
%
Glen Mével's avatar
Glen Mével committed
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's avatar
Glen Mével committed
14
15

In a derivative of \CSL, we may retain the exact same specification as is presented
16
in~\fref{fig:queue:spec:seq}, recalling that $\isQueueSEQ\elemList$ is an
Glen Mével's avatar
Glen Mével committed
17
exclusive assertion:
18
a thread that has this assertion can safely assume to be the only one allowed
19
20
to operate on the queue.
%
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's avatar
Glen Mével committed
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.
%
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
30
to prove the correctness of a MPMC~queue implementation, which should thus
31
32
ensure, by itself, thread safety.
%
Glen Mével's avatar
Glen Mével committed
33
Hence we can achieve finer-grain concurrency, where operating on a queue does
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.
42
%
Glen Mével's avatar
Glen Mével committed
43
% GLEN: digression (on introduit le vocabulaire "public state" ici):
44
45
46
47
As the public state of the queue---the list $\elemList$ of currently stored
items---would only be known from that invariant, the client would also express
in there the properties about this state that their particular application
needs.
48
%
49
50
51
Then, when one of the threads needs to access the shared resource, it can
\emph{open} the invariant, get the assertions it contains, perform the desired
operation on the shared state, reestablish the invariant, and finally close it.
52
%
53
54
55
However, to ensure soundness in the face of concurrency, the use of invariants
in Iris obeys a strict constraint: they can remain open during at most a single
step of execution. Unfortunately, $\enqueue$ and $\dequeue$ are complex
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
56
operations which, \emph{a~priori}, take more than one step of execution. Hence a client
57
58
59
would be unable to open their invariant around the triples shown
in~\fref{fig:queue:spec:seq}.
Yet these operations are ``atomic'' in some empirical sense.
60

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
61
The concept of logical atomicity~\cite[\S7]{jacobs2011expressive,jung-slides-2019,iris-15} aims at addressing that difficulty.
Glen Mével's avatar
Glen Mével committed
62
63
64
65
To use it, we substitute ordinary Hoare triples with \emph{logically atomic triples}.
Just like ordinary triples, they specify a program fragment with a precondition and a postcondition.
The core difference is that invariants can be opened around a logically atomic triple, regardless of the number of execution steps of the program fragment: in a sense, when a function is specified using a logically atomic triple, one states that said function behaves as if it were atomic.
%
66
The definition of logically atomic triples is further discussed in~\sref{sec:queue:proof:la}
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
67
and given with detail in previous work~\cite[\S7]{jung-slides-2019,iris-15}.
Glen Mével's avatar
Glen Mével committed
68
We now try to give an intuition on that concept:
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
69
70
a logically atomic triple $\lahoare{P}{e}{Q}$ states, roughly, that the expression $e$ contains a commit point which has $P$ as a precondition and $Q$ as a postcondition.
The triple then allows the opening of invariants around that commit point
Glen Mével's avatar
Glen Mével committed
71
because it is an atomic instruction.
72
73
74
%
\begin{mathpar}
%
75
  \infer[LAHoare]{% using the rule names from \cite{iris-15}
76
77
78
79
    \lahoare <x> {P} {e} {Q}
  }{%
    \Forall x. \hoare {P} {e} {Q}
  }
Glen Mével's avatar
Glen Mével committed
80
\and
81
  \infer[LAInv]{% using the rule names from \cite{iris-15}
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
82
    \lahoare <x> {\later I \isep P} {e} {\later I \isep Q}
83
  }{%
84
    \knowInv{}{I} \vdash \lahoare <x> {P} {e} {Q}
85
86
87
88
89
  }
%
\end{mathpar}

% TODO: faire référence aux règles ci-dessus dans le texte.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
90
% => JH
91
92
% mentionner qu’un triplet log. atomique implique le triplet usuel ? (1re règle)
% peut-être enlever le binder à cet endroit.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
93
94
% TODO : expliquer la syntaxe des invariants, dire que \later est une technicité d'Iris

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
95
96
97
98
% JH : le mieux, c'est peut-être de mettre ces règles dasn une figure, et de s'y référer à plusieurs endroits:
% 1- regardez, on peut ouvrir des invariants autour d'un triplet logiquement atomique (oubliez le binder pour l'instant)
% 2- maintenant que je vous ai expliqué ce que c'est ce binder, vous voyez, il apparaît dans la syntax
% 3- tout à la fin de 2.2.2, on peut parler de transformer un triplet logiquement atomique en triplet de Hoare au moment où on parle de déduire la spec à base de \Phi.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
99
% 3bis- Si on décide de ne pas parler de la spec à base de \Phi au début du paragraphe, soit on en parle à la fn de 2.2.2, parce que ça fait un bon exemple
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
100

101
Using logically atomic triples, the specification can be written as shown
102
103
in~\fref{fig:queue:spec:sc}.
It closely resembles that of the sequential setting (\fref{fig:queue:spec:seq}).
Glen Mével's avatar
Glen Mével committed
104
105
106
107
108
109
110
111
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's avatar
Jacques-Henri Jourdan committed
112
the state of the queue at the commit point,
Glen Mével's avatar
Glen Mével committed
113
114
115
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's avatar
Jacques-Henri Jourdan committed
116
covering every possible shared state at the commit point.
Glen Mével's avatar
Glen Mével committed
117
118
119
120
121
122
123

The last departure from the sequential specification
is that the representation predicate is split into two parts:
a persistent assertion~$\queueInv$ and an exclusive assertion $\isQueueSC\elemList$,
connected by a ghost name~$\gqueue$.
That splitting is an artifact of our correctness proof technique,
which we detail in~\sref{sec:queue:proof}.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
124
% TODO : GLEN: 1re fois qu’on parle d’assertions persistantes , définir le terme ici.
Glen Mével's avatar
Glen Mével committed
125
126
127
128
129
130
%
Note that this does not complicate the use of the queue by the client:
both assertions are produced when creating the queue,
and while the exclusive component can be put in an invariant as before,
the persistent component can be directly duplicated and distributed to all threads.
% TODO : pour après la soumission : expliquer pourquoi QueueInv n'est pas caché dans IsQueue (footnote pour les experts d'Iris : ça rendrait IsQueue non timeless, et on aurait une étape "abort" au début de enqueue/dequeue => pas impossible, mais plus compliqué)
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
131

132
133
134
135
136
137
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's avatar
Jacques-Henri Jourdan committed
138
\label{sec:queue:spec:sc:persistent}
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179

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:
%
180
\[
181
182
  \isQueuePers\Phi
  \;\eqdef\;
Glen Mével's avatar
Glen Mével committed
183
  \Exists\gqueue. \isepV{%
184
      \queueInv
Glen Mével's avatar
Glen Mével committed
185
  \\  \knowInv{}{\Exists \nbelems, \elemList*[]. \isQueueSC\elemList \ISEP \Phi\,\nthElem{0} \ISEP \cdots \ISEP \Phi\,\nthElem{\nbelems-1}}
186
  }
187
188
\]

189
190
191
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's avatar
Glen Mével committed
192
one opens the invariant around the associated logically atomic triples.