atomic.tex 16.8 KB
Newer Older
Zhen Zhang's avatar
Zhen Zhang committed
1
\documentclass[11pt]{article}
Zhen Zhang's avatar
Zhen Zhang committed
2
3
4
5
6
7
\usepackage{lmodern}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage{fontspec}
\setmonofont{Source Code Pro}

Zhen Zhang's avatar
Zhen Zhang committed
8

Zhen Zhang's avatar
Zhen Zhang committed
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
\newif\ifslow\slowfalse %\slowtrue
\ifslow
  \usepackage[english]{babel}
  \usepackage[babel=true]{microtype}
\fi
\usepackage[top=1in, bottom=1in, left=1.25in, right=1.25in]{geometry}

\usepackage[backend=biber]{biblatex}
\bibliography{bib}

\newcommand{\bdia}{\blacklozenge}
\newcommand{\dia}{\Diamond}
\newcommand{\injR}{\texttt{injR}}
\newcommand{\injL}{\texttt{injL}}

\input{setup}

\begin{document}

\title{\bfseries iris-atomic}
\author{Zhen Zhang}
\maketitle

Zhen Zhang's avatar
Zhen Zhang committed
32
33
34
35
36
37
38
39
\section{Overview}

\begin{figure}[hb]
  \centering
  \includegraphics[width=0.5\textwidth]{ispace}
  \caption
   {Two dimensions of atomicity verification in Iris}
\end{figure}
Zhen Zhang's avatar
Zhen Zhang committed
40

Zhen Zhang's avatar
Zhen Zhang committed
41
42
43
\section{Generic syncer spec}

\begin{align*}
Zhen Zhang's avatar
Zhen Zhang committed
44
45
46
47
  \text{synced}(R, f', f) \eqdef
  \All P, Q, x.
    &\hoare{ R * P(x)}{f(x)}{ v.\,R * Q(x,v) } \ra \\
    &\hoare{ P(x)}{f'(x)}{ v.\,Q(x,v) }
Zhen Zhang's avatar
Zhen Zhang committed
48
\end{align*}
Zhen Zhang's avatar
Zhen Zhang committed
49

Zhen Zhang's avatar
Zhen Zhang committed
50
\[ \text{syncer}(R, s) \eqdef \All f. \wpre{s(f)}{ f'.\, \text{synced}(R, f', f)} \]
Zhen Zhang's avatar
Zhen Zhang committed
51
52


Zhen Zhang's avatar
Zhen Zhang committed
53
\[\text{mkSyncer}(f) \eqdef \All R. \hoare{R}{f()}{ s.\,\always \text{syncer}(R, s)} \]
Zhen Zhang's avatar
Zhen Zhang committed
54

Zhen Zhang's avatar
Zhen Zhang committed
55
This \textbf{generic syncer spec} is inspired by CaReSL. In CaReSL, fine-grained syncer (e.g. flat combiner) is proven to be contextual refinement of coarse-grained \texttt{mkSync} (See section \ref{mksync}). However, there is no program refinement yet in Iris, so I made this generalization and prove that flat combiner satisfies this \emph{directly}.
Zhen Zhang's avatar
Zhen Zhang committed
56

Zhen Zhang's avatar
Zhen Zhang committed
57
In fact, any sensible syncer is expected to satisfy this generic spec.
Zhen Zhang's avatar
Zhen Zhang committed
58

Zhen Zhang's avatar
Zhen Zhang committed
59
Besides generalization, I also split original spec into two parts, corresponding to two calls that happen at different times. More generally speaking, this problem is caused by a special case of curried function (e.g. $\lambda x_1.\, \lambda x_2.\,...$): Is it possible to go from \[\All x_1, x_2. \hoare{P(x_1, x_2)}{f(x_1, x_2)}{Q(x_1, x_2)}\] to \[\All x_1. \hoare{\top}{f(x_1)}{f_1.\, \All x_2. \hoare{P(x_1, x_2)}{f_1(x_2)}{Q(x_1, x_2)}}\], assuming that \(f \eqdef \lambda x_1, x_2.\, e\).
Zhen Zhang's avatar
Zhen Zhang committed
60

Zhen Zhang's avatar
Zhen Zhang committed
61
Finally, I'd like to point out that pre- and post-conditions $P, Q$ are universally qualified per application, that is to say, $P, Q$ are arbitrary depending on the context.
Zhen Zhang's avatar
Zhen Zhang committed
62

Zhen Zhang's avatar
Zhen Zhang committed
63
And similarly, $f$ is universally qualified per synchronization, which means that syncer is only parameterized by the shared resource $R$, it can work with any operation that needs to access this $R$.
Zhen Zhang's avatar
Zhen Zhang committed
64

Zhen Zhang's avatar
Zhen Zhang committed
65
\section{Logically atomic triple (LAT)}
Zhen Zhang's avatar
Zhen Zhang committed
66

Zhen Zhang's avatar
Zhen Zhang committed
67
68
69
\begin{align*}
    &\lahoare{g.\, \alpha(g)}{e}{v.\, \beta(g, v)}[E_i][E_o] \eqdef\\
    &\All P, Q.
Zhen Zhang's avatar
Zhen Zhang committed
70
71
72
    \begin{aligned}
          &P \vs[Eo][Ei] \Exists g, \alpha(g) * (\alpha(g) \vsW[Ei][Eo] P \land \All v. \beta(g, v) \vsW[Ei][Eo] Q(g, v)) \wand \\
          &\hoare{P}{e}{v.\, \Exists g. Q(g, v)}
Zhen Zhang's avatar
Zhen Zhang committed
73
74
    \end{aligned}
\end{align*}
Zhen Zhang's avatar
Zhen Zhang committed
75

Zhen Zhang's avatar
Zhen Zhang committed
76
Note again, the $P, Q$ are arbitrary depending on the context.
Zhen Zhang's avatar
Zhen Zhang committed
77

Zhen Zhang's avatar
Zhen Zhang committed
78
And also, note the separation product of two linear view shifts: First one represents \textbf{abandon} direction, while the second one represents \textbf{commit} direction. Using linear view shifts enables us to frame alongside the transition some non-persistent resource.
Zhen Zhang's avatar
Zhen Zhang committed
79

Zhen Zhang's avatar
Zhen Zhang committed
80
81
82
83
84
85
\begin{figure}[hb]
  \centering
  \includegraphics[width=0.5\textwidth]{lat}
  \caption
   {Sketch of how library function specified with LAT will be used}
\end{figure}
Zhen Zhang's avatar
Zhen Zhang committed
86

Zhen Zhang's avatar
Zhen Zhang committed
87
\section{Coarse-grained syncer}\label{mksync}
Zhen Zhang's avatar
Zhen Zhang committed
88

Zhen Zhang's avatar
Zhen Zhang committed
89
First, we give the CaReSL's \texttt{mkSync} written in heap-lang (which is basically the same as in Coq, despite a few cosmetics).
Zhen Zhang's avatar
Zhen Zhang committed
90
91
92
93
94
95
96
97
98
99
100
101

\begin{verbatim}
mk_sync :=
    λ: <>,
       let l := newlock() in
       λ: f x,
          acquire l;
          let ret := f x in
          release l;
          ret.
\end{verbatim}

Zhen Zhang's avatar
Zhen Zhang committed
102
Okay, now the question is: can we give a LAT spec for \texttt{mk\_sync}? Actually, we can! and we can do this in a general way (i.e. for any syncer satisfying the generic syncer spec). We will briefly discuss about it in the next section.
Zhen Zhang's avatar
Zhen Zhang committed
103

Zhen Zhang's avatar
Zhen Zhang committed
104
\section{Encoding generic syncer spec as a LAT-style spec}
Zhen Zhang's avatar
Zhen Zhang committed
105

Zhen Zhang's avatar
Zhen Zhang committed
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
The first question is: \textbf{Why do we want to do so?}

First, they both talk about atomicity, so we will naturally want to know what is the possible relationship between them. And second, the generic syncer spec is not canonical -- it doesn't tell explicitly what effects that operation has. When use the generic syncer spec as a client, you have to prove something about $e$ every time. But LAT, on the contrary, gives you the exact specification of the operation itself, which means that you only need to prove the viewshifts (in some sense similar to weakening/strengthening rules). And most importantly, this exact specification, should look exactly like the sequential specification! Just consider the following illustrative comparison of a sequential/concurrent stack \texttt{push} spec:

\begin{align*}
  \All xs.\hoare{stack(s, xs)}{\texttt{push}(x, s)}{\_.\, stack(s, x::xs)}\\
  \lahoare{xs.\, stack'(s, xs)}{\texttt{push'}(x, s)}{\_.\, stack'(s, x::xs)}
\end{align*}

The second question is: \textbf{Is it possible to do so?}

Intuitively, what syncer spec says is that the $e$'s sequential effects are \emph{compressed} to a single point. Consider the coarse-grained implementation of generic syncer spec, \texttt{mk\_sync}, it guards the resource $R$ by putting it inside a lock, thus every operation will exclusively own $R$ for a certain period, which makes the whole operation look atomic, when observed from outside in terms of resource accessing.

The last question is: \textbf{How to do it?}

First, consider what LAT's client can provide to the library: abandoning and committing viewshifts. And these two actions must happen instantly. So, naturally, we will try to commit at the time of finishing the operation and give back the $R$ to lock. But what about abandoning? What role will it have in the syncer spec?

Remember that there is a canonical pre-condition $\alpha$ in LAT, which should coincide with the sequential spec. But the sequential code, when executed between the lock/unlock, is still non-atomic. So after we exchange $P$ for $\alpha$, we must retain $\alpha$ for a long time, while we also have to close the LAT viewshifts in an instant. We can't close by abandoning, since we need to give back the $\alpha$; and we can't close by committing, since we haven't started the action yet!

But wait, why we \emph{must} give back $\alpha$ while losing it? What if we require that $\alpha$ is duplicable? Then problem solved! We just need to abandon in the beginning to get a duplicated $\alpha$ out, then committing with $P$ when finishing off.

Now, with a sketch in mind, I will introduce you to the detailed construction: First, here is the specialized logically atomic triple for such purpose:
Zhen Zhang's avatar
Zhen Zhang committed
128
129
130
131
132

\[ \lahoare{g.\, \ownGhost{\gname}{g^{1/2}} * \always \alpha(g)}
           {f(x)}
           {v.\, \Exists g'. \ownGhost{\gname}{g'^{1/2}} * \beta(x, g, g', v)}[E_i][E_o]\]

Zhen Zhang's avatar
Zhen Zhang committed
133
134
135
136
137
138
139
140
141
142
143
144
145
Here, $g$ represents \textbf{ghost state}. $g$ can be of any proper type. $\ownGhost{\gname}{g'^{1/2}}$ is a snapshot of $g$, i.e. local knowledge about the physical configuration. (Why it is written in such way? Well, this is the implementation detail related to the monoid used to encode this).

Here, the persistent (thus duplicable) $\alpha(g)$ is some extra condition. And in the post condition, we say there exists an updated ghost state $g'$, which satisfy $\beta$, a relation over input, previous state, current state, and output.

Let's take concurrent \texttt{push} again as an example. If $s$ is a stack pointer, \[R_s \eqdef \Exists xs. stack(s, xs) * \ownGhost{\gname}{xs^{1/2}}\] is the physical configuration plus global snapshot, then $\text{synced}(stack(s, xs), \texttt{push'}, \texttt{push}(s))$ should expand like this:

\begin{align*}
  \All P, Q, x.
    &\hoare{ R_s * P(x)}{\texttt{push}(s)(x)}{ v.\,R_s * Q(x,v) } \ra \\
    &\hoare{ P(x)}{\texttt{push'}(x)}{ v.\,Q(x,v) }
\end{align*}

And the LAT we can get from it looks like this:
Zhen Zhang's avatar
Zhen Zhang committed
146

Zhen Zhang's avatar
Zhen Zhang committed
147
\[\lahoare{xs.\, \ownGhost{\gname}{xs^{1/2}}}{\texttt{push'}(x)}{\_.\, \Exists xs'. \ownGhost{\gname}{xs'^{1/2}} * (xs' = x::xs)} \]
Zhen Zhang's avatar
Zhen Zhang committed
148

Zhen Zhang's avatar
Zhen Zhang committed
149
Here, note that in this case $\always \alpha(g)$ is selected as $\top$ (thus we can imagine that in most cases persistent restriction is not much of a problem); also, $s$ is entirely hidden somewhere in some global place, i.e., using $\ownGhost{\gname}{xs^{1/2}}$, you can also atomically access $\Exists s. stack(s, xs)$, even though such accessing is not specified as a LAT.
Zhen Zhang's avatar
Zhen Zhang committed
150

Zhen Zhang's avatar
Zhen Zhang committed
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
\begin{verbatim}
sync(mk_syncer) :=
  λ: f_seq l,
     let s := mk_syncer() in
     s (f_seq l).
\end{verbatim}

\[seq\_spec(f, \phi, \alpha, \beta, E) \eqdef
      \All l.
         \hoare{\top}{f(l)}{f'.\,
            \begin{aligned}
            \pure &\All x, \Phi, g.\\
                &\phi (l, g) * \always \alpha(x) *\\
                &(\All v, g'. \phi(l, g') \wand \beta(x, g, g', v) \wand \pvs[E][E] \Phi(v))\\
                &\proves \wpre{f'(x)}[E]{ \Phi }
              \end{aligned}
        }\]
Zhen Zhang's avatar
Zhen Zhang committed
168
169
170
171

Here is the sequential spec. pre-condition is the persistent alpha and exclusive ownership of shared state, and when it returns, we got the updated physical state g’, as well as beta.

Funny thing is again that I have to apply f to l first ... because of currying and call site problem.
Zhen Zhang's avatar
Zhen Zhang committed
172
173
174
175
176
177
178
179
180
181
182
183
184
  
\[\begin{aligned}
      &\text{atomic\_spec}(mk\_syncer, f\_seq, l, \phi, \alpha, \beta, E_i) \eqdef\\
      &\All g_0.
        seq\_spec(f\_seq, \phi, \alpha, \beta, \top) \ra
        mk\_syncer\_spec(mk\_syncer) \ra\\
        &\phi(l, g_0)
        \proves \wpre{sync(mk\_syncer, f\_seq, l)}{ f.\,
          \Exists \gname. \ownGhost{\gname}{g_0^{1/2}} *
          \All x. \always \lahoare{g.\, \ownGhost{\gname}{g^{1/2}} * \always \alpha(g)}{f(x)}
                                  {v.\, \Exists g'. \ownGhost{\gname}{g'^{1/2}} * \beta(x, g, g', v)}[E_i][\top]}
      \end{aligned} \]

Zhen Zhang's avatar
Zhen Zhang committed
185
186
187
188
189
190
So, here is the theorem that states such derivation. Inside the blue box is the triple defined earlier, it is returned in the post-condition.

The meta procedure “sync” is parameterised in Coq with any kind of syncer constructor you want to prove about. Its heap-lang parameters are sequential code closure and the location to internal state. As you can see from its definition, it partially applies \texttt{f\_seq} with l, i.e., binding operation with shared state pointer, and return a concurrent operation synchronized by newly-created syncer.

Now let’s observe its two pure conditions: first, sequential code must have a spec; second, \texttt{mk\_syncer} satisfies the syncer constructor spec [review]

Zhen Zhang's avatar
Zhen Zhang committed
191
192
\[ (\Exists g. \phi(l, g') * \ownGhost{\gname}{g^{1/2}} * P x \]

Zhen Zhang's avatar
Zhen Zhang committed
193
194
\includegraphics[width=0.5\textwidth]{atomic_sync}

Zhen Zhang's avatar
Zhen Zhang committed
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
\section{treiber.v}

\begin{verbatim}
push s x :=
  let hd := !s in
  let s' := ref SOME (x, hd) in
  if CAS s hd s'
    then ()
    else push s x.

pop s :=
  let hd := !s in
  match !hd with
  | SOME (x, hd') =>
    if: CAS s hd hd'
      then SOME x
      else pop s
  | NONE => NONE
  end.

iter hd f :=
  match !hd with
  | NONE => ()
  | SOME (x, hd') => f x ; iter hd' f
  end.

\end{verbatim}

Zhen Zhang's avatar
Zhen Zhang committed
223
224
225
226
227
228
Finally, it is time to talk about flat combiner …. oh no, not yet. We need to talk about treiber’s stack first.

These push and pop are all standard lock-free implementation.

We will give LAT spec for these two operations first

Zhen Zhang's avatar
Zhen Zhang committed
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
Logiall atomic spec (version 1):

\[ \lahoare{xs.\, stack(s, xs)}{push(s, x)}{stack(s, x::xs)}[heapN][\top]\]
\[ \lahoare{xs.\, stack(s, xs)}{pop(s)}{v. \begin{split} (&\Exists x, xs'. v = SOME(x) * stack(s, xs')) \lor\\
                                            (&v = NONE * xs = \emptyset * stack(s, \emptyset)) \end{split}}[heapN][\top]\]


Logiall atomic spec (version 2):

\[ \lahoare{hd, xs.\, s \mapsto hd * list(hd, xs)}{push(s, x)}{\Exists hd'. s \mapsto hd' * hd' \mapsto SOME(x, hd) * list(hd, xs)}[heapN][\top]\]
\[ \lahoare{hd, xs.\, s \mapsto hd * list(hd, xs)}{pop(s)}{v.
    \begin{split}
      (&\Exists x, xs', hd'. v = SOME(x) * hd \mapsto SOME(x, hd') * s \mapsto hd' * list(hd', xs')) \lor\\
      (&v = NONE * xs = \emptyset * hd \mapsto NONE)
    \end{split}
  }[heapN][\top]
  \]

Zhen Zhang's avatar
Zhen Zhang committed
247
248
249
250
251
For these two operations, we usually will give a more abstract spec, like the one above, which talks about s and elements in it, but no more.

However, we can also give one that exposes how stack is implemented (here, as a linked list). Actually, if we want to prove push spec in per-item-invariant style, we must expose enough details.

Why? The intuition is that, when push some element in a per-item setting, we need to open, modify where s points to, and then close the invariant. But how can we make sure that the rest of the stack is always satisfying the per-item invariants? If we want such evidence, we need to expose something physical, such as the head pointer in this case.
Zhen Zhang's avatar
Zhen Zhang committed
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270

\section{peritem.v}

A crappy but working spec:

\[f\_spec (\gname, xs, s, f, Rf, RI) \eqdef
    \All x.
      \hoare{x \in xs * \knowInv\iname{\Exists xs. stack'(\gname, xs, s) * RI} * Rf}{f(x)}{ v.\, v = () }.\]

\[\begin{split}
  iter\_spec(\gname, s, Rf, RI) \eqdef
    &\All xs, hd, f.\\
      &f\_spec(xs, s, f', Rf, RI) \ra\\
      &\hoare{\knowInv\iname{\Exists xs. stack'(xs, s) * RI} * list'(\gname, hd, xs) * Rf}{iter(hd, f)}{ v.\, v = () * Rf}
  \end{split}\]

\[push\_spec (\gname, s, x, RI) \eqdef
  \hoare{R(x) * \knowInv\iname{\Exists xs. stack'(xs, s) * RI}}{push(s, x)}{v.\, v = () * (\Exists hd. ev(\gname, hd, x))}\]

Zhen Zhang's avatar
Zhen Zhang committed
271
272
273
274
275
276
277
278
Okay, but in per-item spec, why do you need to make sure that the stack is growth-only, and governed by a global invariant?

Answer: because we need to iterate thought it non-atomically. I mean, the process of iteration is not atomic. The single operation f still needs to atomically access any resource related x.

So, having already talked a lot about per-item spec… here is how it looks like in my implementation. Well, I agree with you that this is a bit messy. 

note that global inv of stack is parametrised by per-item predicate R

Zhen Zhang's avatar
Zhen Zhang committed
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
\section{flat.v}

\begin{verbatim}
doOp :=
  λ: p,
     match !p with
     | InjL (f, x) => p <- InjR (f x)
     | InjR _ => ()
     end.

try_srv :=
  λ: lk s,
    if try_acquire lk
      then let hd := !s in
           iter hd doOp;
           release lk
      else ().

loop p s lk :=
    match !p with
    | InjL _ =>
        try_srv lk s;
        loop p s lk
    | InjR r => r
    end.

install :=
  λ: f x s,
     let p := ref (InjL (f, x)) in
     push s p;
     p.

mk_flat :=
  λ: <>,
   let lk := newlock() in
   let s := new_stack() in
   λ: f x,
      let p := install f x s in
      let r := loop p s lk in
      r.
\end{verbatim}

Zhen Zhang's avatar
Zhen Zhang committed
321
322
323
324
325
326
327
328
329
330
331

Let’s go to my flat combiner code now.

Compared to CaReSL, here are several notable differences:

I break them down into five procedures, instead of nesting them inside the constructor. It is easier to specify.
CaReSL’s flat constructor takes f; this doesn’t, which makes it more flexible.
CaReSL’s install utilize TLS to avoid blowup of space use. I push in a new slot every time, which is terrible in practice, but follows the same spec.

Also, another problem that exist both in my, CaReSL, and FCSL’s example code, is that we never recycle the slots.

Zhen Zhang's avatar
Zhen Zhang committed
332
333
334
335
336
337
\[p \mapsto \injR(-)\]
\[p \mapsto \texttt{injL}(f, x)\]
\[p \mapsto \injR(y)\]
\[\circ_i, \bullet_i, \dia_i, \bdia, \dia_i \circ_i, \dia_i \bullet_i, \bdia \bullet_i\]


Zhen Zhang's avatar
Zhen Zhang committed
338
339
340
341
342
343
344
345
346
347
\includegraphics[width=0.5\textwidth]{helping}

This is the protocol of helping … 

The black diamond is a token owned by server lock.
The other three kinds of token are all tagged with i, which should be similar to thread id in CaReSL’s reasoning, but in my case, it is the slot address (Is it more flexible than using tid to index?). And the indexing is essentially done through a ghost map in invariant. 

Note that this graph is heavily simplified to reflect how I encode protocol with bare exclusive monoids. Next slide gives the detailed invariant construction


Zhen Zhang's avatar
Zhen Zhang committed
348
349
350
351
352
353
354
355
\begin{align*}
     &\Exists y.          &&p \fmapsto[1/2] \injR(-) * \dia_i * \circ_i\\
\lor &\Exists f, x, P, Q. &&p \fmapsto[1/2] \injL(f, x) * \ownGhost{\gname}{x^{1/2}} *
                           P(x) * (\hoare{R * P(x)}{f(x)}{v.\,R * Q(x, v)}) * \gamma \mapstoprop Q(x) * \dia_i * \bullet_i\\
\lor &\Exists x.          &&p \fmapsto[1/2] \injL(-, x) * \ownGhost{\gname}{x^{1/4}} * \bdia * \bullet_i\\
\lor &\Exists x, y.       &&p \fmapsto[1/2] \injR(y) * \ownGhost{\gname}{x^{1/2}} * \gamma \mapstoprop Q(x) * Q(x, y) * \dia_i * \bullet_i
\end{align*}

Zhen Zhang's avatar
Zhen Zhang committed
356
357
358
359
360
361
Here is the per-item (i.e. request slot) invariant, which have four branches.

Note how f x P Q are all hidden under existential qualification, while (Q x) is saved under some name. It means that only post-condition matter to waiting client.

This is basically the core of flat combiner proofs. There are just a couple of critical points, the rest are all boilerplates like open/close invariant. A nicer per-item spec could improve it I guess.

Zhen Zhang's avatar
Zhen Zhang committed
362
363
364
365
366
\[\alpha = \alpha_a * \alpha_o, \alpha = \alpha_a' * \alpha_o\]
\[\alpha = \alpha_o * \alpha_a, \alpha_a' * \alpha_o = \beta\]
\[\alpha = \alpha_a * \alpha_o, \alpha = \alpha_a' * \alpha_o\]

\end{document}