concurrent_stack4.v 16.1 KB
Newer Older
1
2
3
From iris.program_logic Require Export weakestpre hoare.
From iris.heap_lang Require Export lang proofmode notation.
From iris.algebra Require Import excl.
Daniel Gratzer's avatar
Daniel Gratzer committed
4
From iris_examples.concurrent_stacks Require Import specs.
5

Daniel Gratzer's avatar
Daniel Gratzer committed
6
7
(** Stack 4: Helping, CAP spec. *)

8
9
10
11
12
13
14
Definition mk_offer : val :=
  λ: "v", ("v", ref #0).
Definition revoke_offer : val :=
  λ: "v", if: CAS (Snd "v") #0 #2 then SOME (Fst "v") else NONE.
Definition take_offer : val :=
  λ: "v", if: CAS (Snd "v") #0 #1 then SOME (Fst "v") else NONE.

15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
Definition mk_mailbox : val := λ: "_", ref NONEV.
Definition put : val :=
  λ: "r" "v",
    let: "off" := mk_offer "v" in
    "r" <- SOME "off";;
    revoke_offer "off".
Definition get : val :=
  λ: "r",
    let: "offopt" := !"r" in
    match: "offopt" with
      NONE => NONE
    | SOME "x" => take_offer "x"
    end.

Definition mk_stack : val := λ: "_", (mk_mailbox #(), ref NONEV).
Definition push : val :=
  rec: "push" "p" "v" :=
    let: "mailbox" := Fst "p" in
    let: "s" := Snd "p" in
    match: put "mailbox" "v" with
      NONE => #()
    | SOME "v'" =>
      let: "tail" := ! "s" in
      let: "new" := SOME (ref ("v'", "tail")) in
      if: CAS "s" "tail" "new" then #() else "push" "p" "v'"
    end.
Definition pop : val :=
  rec: "pop" "p" :=
    let: "mailbox" := Fst "p" in
    let: "s" := Snd "p" in
    match: get "mailbox" with
      NONE =>
      match: !"s" with
        NONE => NONEV
      | SOME "l" =>
        let: "pair" := !"l" in
        if: CAS "s" (SOME "l") (Snd "pair")
        then SOME (Fst "pair")
        else "pop" "p"
      end
    | SOME "x" => SOME "x"
    end.
57
58

Definition channelR := exclR unitR.
59
Class channelG Σ := {channel_inG :> inG Σ channelR}.
60

61
Section proofs.
62
63
64
65
  Context `{!heapG Σ, !channelG Σ} (N : namespace).

  Implicit Types l : loc.

66
67
68
  Definition Nside_channel := N .@ "side_channel".
  Definition Nstack := N .@ "stack".
  Definition Nmailbox := N .@ "mailbox".
69

70
  Definition inner_mask : coPset :=   Nside_channel  Nstack.
71

72
73
74
  Lemma inner_mask_includes :
        N  inner_mask.
  Proof. solve_ndisj. Qed.
75

Daniel Gratzer's avatar
Daniel Gratzer committed
76
77
78
79
80
81
82
83
84
85
  Lemma inner_mask_promote (P Q : iProp Σ) :
     (P ={   N}= Q) - (P ={inner_mask}= Q).
  Proof.
    iIntros "Himp P".
    iMod (fupd_intro_mask' inner_mask (   N)) as "H"; first by apply inner_mask_includes.
    iDestruct ("Himp" with "P") as "HQ".
    iMod "HQ".
    by iMod "H".
  Qed.

86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
  Definition revoke_tok γ := own γ (Excl ()).
  Definition can_push P Q v : iProp Σ :=
    ( (xs : list val), P xs ={inner_mask}= P (v :: xs)  Q #())%I.
  Definition access_inv (P : list val  iProp Σ) : iProp Σ :=
    (|={  Nside_channel, inner_mask}=>  vs, ( P vs) 
      (( P vs) ={inner_mask,   Nside_channel}= True))%I.

  Definition stages γ P Q l (v : val) :=
    ((l  #0  can_push P Q v)  
     (l  #1  Q #()) 
     (l  #1  revoke_tok γ) 
     (l  #2  revoke_tok γ))%I.

  Definition is_offer γ P Q (v : val) : iProp Σ :=
    ( v' l, v = (v', #l)%V  inv Nside_channel (stages γ P Q l v'))%I.

  Lemma mk_offer_works P Q v :
    {{{ can_push P Q v }}}
      mk_offer v
    {{{ o γ, RET o; is_offer γ P Q o  revoke_tok γ }}}.
  Proof.
    iIntros (Φ) "HP HΦ".
    rewrite -wp_fupd.
    wp_lam. wp_alloc l as "Hl".
    iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
    iMod (inv_alloc Nside_channel _ (stages γ P Q l v) with "[Hl HP]") as "#Hinv".
    { iNext; iLeft; iFrame. }
113
    wp_pures; iModIntro; iApply "HΦ"; iFrame; iExists _, _; auto.
114
115
116
117
118
119
120
121
  Qed.

  Lemma revoke_works γ P Q v :
    {{{ is_offer γ P Q v  revoke_tok γ }}}
      revoke_offer v
    {{{ v', RET v'; ( v'' : val, v' = InjRV v''  can_push P Q v'')  (v' = InjLV #()  (Q #())) }}}.
  Proof.
    iIntros (Φ) "[Hinv Hγ] HΦ". iDestruct "Hinv" as (v' l) "[-> #Hinv]".
122
    wp_lam. wp_pures. wp_bind (CAS _ _ _).
123
124
125
126
127
128
    iInv Nside_channel as "Hstages" "Hclose".
    iDestruct "Hstages" as "[[Hl HP] | [[Hl HQ] | [[Hl H] | [Hl H]]]]".
    - wp_cas_suc.
      iMod ("Hclose" with "[Hl Hγ]") as "_".
      { iNext; iRight; iRight; iFrame. }
      iModIntro.
129
      wp_pures.
130
131
132
133
134
      by iApply "HΦ"; iLeft; iExists _; iFrame.
    - wp_cas_fail.
      iMod ("Hclose" with "[Hl Hγ]") as "_".
      { iNext; iRight; iRight; iLeft; iFrame. }
      iModIntro.
135
      wp_pures.
136
137
138
139
140
141
142
      iApply ("HΦ" with "[HQ]"); iRight; auto.
    - wp_cas_fail.
      iDestruct (own_valid_2 with "H Hγ") as %[].
    - wp_cas_fail.
      iDestruct (own_valid_2 with "H Hγ") as %[].
  Qed.

143
  Lemma take_works γ P Q Q' o Ψ :
144
145
    let do_pop : iProp Σ :=
        ( v xs, P (v :: xs) ={inner_mask}= P xs  Ψ (SOMEV v))%I in
146
    {{{ is_offer γ P Q o  access_inv P  (do_pop  Q') }}}
147
148
      take_offer o
    {{{ v', RET v';
149
        ( v'' : val, v' = InjRV v''  Ψ v')  (v' = InjLV #()  (do_pop  Q')) }}}.
150
151
152
153
154
155
156
157
158
159
160
161
162
  Proof.
    simpl; iIntros (Φ) "[H [Hopener Hupd]] HΦ"; iDestruct "H" as (v l) "[-> #Hinv]".
    wp_lam. wp_proj. wp_bind (CAS _ _ _).
    iInv Nside_channel as "Hstages" "Hclose".
    iDestruct "Hstages" as "[[Hl Hpush] | [[Hl HQ] | [[Hl Hγ] | [Hl Hγ]]]]".
    - iMod "Hopener" as (xs) "[HP Hcloser]".
      wp_cas_suc.
      iMod ("Hpush" with "HP") as "[HP HQ]".
      iMod ("Hupd" with "HP") as "[HP HΨ]".
      iMod ("Hcloser" with "HP") as "_".
      iMod ("Hclose" with "[Hl HQ]") as "_".
      { iRight; iLeft; iFrame. }
      iApply fupd_intro_mask; first done.
163
      wp_pures.
164
165
166
167
168
      iApply "HΦ"; iLeft; auto.
    - wp_cas_fail.
      iMod ("Hclose" with "[Hl HQ]") as "_".
      { iRight; iLeft; iFrame. }
      iModIntro.
169
      wp_pures.
170
171
172
173
174
      iApply "HΦ"; auto.
    - wp_cas_fail.
      iMod ("Hclose" with "[Hl Hγ]").
      { iRight; iRight; iFrame. }
      iModIntro.
175
      wp_pures.
176
177
178
179
180
      iApply "HΦ"; auto.
    - wp_cas_fail.
      iMod ("Hclose" with "[Hl Hγ]").
      { iRight; iRight; iFrame. }
      iModIntro.
181
      wp_pures.
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
      iApply "HΦ"; auto.
  Qed.

  Definition mailbox_inv P l : iProp Σ :=
    (l  NONEV  ( v' γ Q, l  SOMEV v'  is_offer γ P Q v'))%I.

  Definition is_mailbox P v : iProp Σ :=
    ( l, v = #l  inv Nmailbox (mailbox_inv P l))%I.

  Lemma mk_mailbox_works P :
    {{{ True }}} mk_mailbox #() {{{ v, RET v; is_mailbox P v }}}.
  Proof.
    iIntros (Φ) "_ HΦ".
    rewrite -wp_fupd. wp_lam. wp_alloc l as "Hl".
    iMod (inv_alloc Nmailbox _ (mailbox_inv P l) with "[Hl]") as "#Hinv".
    { iNext; by iLeft. }
    iModIntro.
    iApply "HΦ"; iExists _; auto.
  Qed.
201

202
  Lemma get_works Q P Ψ mailbox :
203
204
    let do_pop : iProp Σ :=
        ( v xs, P (v :: xs) ={inner_mask}= P xs  Ψ (SOMEV v))%I in
205
    {{{ is_mailbox P mailbox  access_inv P  (do_pop  Q) }}}
206
      get mailbox
207
    {{{ ov, RET ov; ( v, ov = SOMEV v  Ψ ov)  (ov = NONEV  (do_pop  Q)) }}}.
208
209
210
211
212
213
214
215
  Proof.
    simpl; iIntros (Φ) "[Hmail [Hopener Hpush]] HΦ". iDestruct "Hmail" as (l) "[-> #Hmail]".
    wp_lam. wp_bind (Load _).
    iInv Nmailbox as "[Hnone | Hsome]" "Hclose".
    - wp_load.
      iMod ("Hclose" with "[Hnone]") as "_".
      { by iLeft. }
      iModIntro.
216
      wp_pures.
217
      iApply "HΦ"; iRight; by iFrame.
218
    - iDestruct "Hsome" as (v' γ Q') "[Hl #Hoffer]".
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
      wp_load.
      iMod ("Hclose" with "[Hl Hoffer]") as "_".
      { iNext; iRight; iExists _, _, _; by iFrame. }
      iModIntro.
      wp_let. wp_match. wp_apply (take_works with "[Hpush Hopener]"); by iFrame.
  Qed.

  Lemma put_works P Q mailbox v :
    {{{ is_mailbox P mailbox  can_push P Q v }}}
      put mailbox v
    {{{ o, RET o; ( v', o = SOMEV v'  can_push P Q v')  (o = NONEV  Q #()) }}}.
  Proof.
    iIntros (Φ) "[Hmail Hpush] HΦ". iDestruct "Hmail" as (l) "[-> #Hmail]".
    wp_lam. wp_let. wp_apply (mk_offer_works with "Hpush").
    iIntros (o γ) "[#Hoffer Hrev]".
234
    wp_let. wp_bind (Store _ _). wp_pures.
235
236
237
238
239
    iInv Nmailbox as "[Hnone | Hsome]" "Hclose".
    - wp_store.
      iMod ("Hclose" with "[Hnone]") as "_".
      { iNext; iRight; iExists _, _, _; by iFrame. }
      iModIntro.
240
      wp_pures.
241
242
243
244
245
246
      wp_apply (revoke_works with "[Hrev]"); first auto.
      iIntros (v') "H"; iApply "HΦ"; auto.
    - iDestruct "Hsome" as (? ? ?) "[Hl _]". wp_store.
      iMod ("Hclose" with "[Hl]") as "_".
      { iNext; iRight; iExists _, _, _; by iFrame. }
      iModIntro.
247
      wp_pures.
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
      wp_apply (revoke_works with "[Hrev]"); first auto.
      iIntros (v') "H"; iApply "HΦ"; auto.
  Qed.

  Local Notation "l ↦{-} v" := ( q, l {q} v)%I
    (at level 20, format "l  ↦{-}  v") : bi_scope.

  Lemma partial_mapsto_duplicable l v :
    l {-} v - l {-} v  l {-} v.
  Proof.
    iIntros "H"; iDestruct "H" as (?) "[Hl Hl']"; iSplitL "Hl"; eauto.
  Qed.

  Lemma partial_mapsto_agree l v1 v2 :
    l {-} v1 - l {-} v2 - v1 = v2.
  Proof.
    iIntros "H1 H2".
    iDestruct "H1" as (?) "H1".
    iDestruct "H2" as (?) "H2".
    iApply (mapsto_agree with "H1 H2").
  Qed.

  Fixpoint is_list xs v : iProp Σ :=
271
272
    (match xs with
     | [] => v = NONEV
273
     | x :: xs =>  l (t : val), v = SOMEV #l%V  l {-} (x, t)%V  is_list xs t
274
275
     end)%I.

276
277
  Lemma is_list_disj xs v :
    is_list xs v - is_list xs v  (v = NONEV   l (h t : val), v = SOMEV #l  l {-} (h, t)%V).
278
  Proof.
279
280
281
282
    destruct xs; auto.
    iIntros "H"; iDestruct "H" as (l t) "(-> & Hl & Hstack)".
    iDestruct (partial_mapsto_duplicable with "Hl") as "[Hl1 Hl2]".
    iSplitR "Hl2"; first by (iExists _, _; iFrame). iRight; auto.
283
284
  Qed.

285
286
  Lemma is_list_unboxed xs v :
      is_list xs v - val_is_unboxed v  is_list xs v.
287
  Proof.
288
289
    iIntros "Hlist"; iDestruct (is_list_disj with "Hlist") as "[$ Heq]".
    iDestruct "Heq" as "[-> | H]"; first done; by iDestruct "H" as (? ? ?) "[-> ?]".
290
291
  Qed.

292
293
  Lemma is_list_empty xs :
    is_list xs (InjLV #()) - xs = [].
294
  Proof.
295
296
    destruct xs; iIntros "Hstack"; auto.
    iDestruct "Hstack" as (? ?) "(% & H)"; discriminate.
297
  Qed.
298
299
300
301
302

  Lemma is_list_cons xs l h t :
    l {-} (h, t)%V -
    is_list xs (InjRV #l) -
     ys, xs = h :: ys.
303
  Proof.
304
305
306
    destruct xs; first by iIntros "? %".
    iIntros "Hl Hstack"; iDestruct "Hstack" as (l' t') "(% & Hl' & Hrest)"; simplify_eq.
    iDestruct (partial_mapsto_agree with "Hl Hl'") as "%"; simplify_eq; iExists _; auto.
307
308
  Qed.

309
310
311
  Definition stack_inv P l :=
    ( v xs, l  v  is_list xs v  P xs)%I.

Daniel Gratzer's avatar
Daniel Gratzer committed
312
  Definition is_stack_pred P v :=
313
314
315
    ( mailbox l, v = (mailbox, #l)%V  is_mailbox P mailbox  inv Nstack (stack_inv P l))%I.

  Theorem mk_stack_works (P : list val  iProp Σ) :
Daniel Gratzer's avatar
Daniel Gratzer committed
316
    {{{ P [] }}} mk_stack #() {{{ v, RET v; is_stack_pred P v }}}.
317
  Proof.
318
319
    iIntros (Φ) "HP HΦ".
    rewrite -wp_fupd.
320
    wp_lam.
321
    wp_alloc l as "Hl".
322
    wp_apply mk_mailbox_works ; first done. iIntros (v) "#Hmailbox".
323
324
    iMod (inv_alloc Nstack _ (stack_inv P l) with "[Hl HP]") as "#Hinv".
    { by iNext; iExists _, []; iFrame. }
325
    wp_pures. iModIntro; iApply "HΦ"; iExists _; auto.
326
  Qed.
327

328
  Theorem push_works P s v Ψ :
Daniel Gratzer's avatar
Daniel Gratzer committed
329
    {{{ is_stack_pred P s   xs, P xs ={   N}= P (v :: xs)  Ψ #()}}}
330
331
332
333
      push s v
    {{{ RET #(); Ψ #() }}}.
  Proof.
    iIntros (Φ) "[Hstack Hupd] HΦ". iDestruct "Hstack" as (mailbox l) "(-> & #Hmailbox & #Hinv)".
Daniel Gratzer's avatar
Daniel Gratzer committed
334
335
    iAssert ( (xs : list val), P xs ={inner_mask}= P (v :: xs)  Ψ #())%I with "[Hupd]" as "Hupd".
    { iIntros (xs). by iApply inner_mask_promote. }
336
    iLöb as "IH" forall (v).
337
    wp_lam. wp_pures.
338
339
340
341
342
343
344
345
346
347
    wp_apply (put_works with "[Hupd]"); first auto. iIntros (o) "H".
    iDestruct "H" as "[Hsome | [-> HΨ]]".
    - iDestruct "Hsome" as (v') "[-> Hupd]".
      wp_match.
      wp_bind (Load _).
      iInv Nstack as (list xs) "(Hl & Hlist & HP)" "Hclose".
      wp_load.
      iMod ("Hclose" with "[Hl Hlist HP]") as "_".
      { iNext; iExists _, _; iFrame. }
      clear xs.
348
      iModIntro.
349
      wp_let. wp_alloc l' as "Hl'". wp_pures. wp_bind (CAS _ _ _).
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
      iInv Nstack as (list' xs) "(Hl & Hlist & HP)" "Hclose".
      iDestruct (is_list_unboxed with "Hlist") as "[>% Hlist]".
      destruct (decide (list = list')) as [ -> |].
      * wp_cas_suc.
        iMod (fupd_intro_mask' (  Nstack) inner_mask) as "Hupd'"; first solve_ndisj.
        iMod ("Hupd" with "HP") as "[HP HΨ]".
        iMod "Hupd'" as "_".
        iMod ("Hclose" with "[Hl Hl' HP Hlist]") as "_".
        { iNext; iExists (SOMEV _), (v' :: xs); iFrame; iExists _, _; iFrame; auto. }
        iModIntro.
        wp_if.
        by iApply ("HΦ" with "HΨ").
      * wp_cas_fail.
        iMod ("Hclose" with "[Hl HP Hlist]").
        { iExists _, _; iFrame. }
365
366
        iModIntro.
        wp_if.
Daniel Gratzer's avatar
Daniel Gratzer committed
367
        iApply ("IH" with "HΦ Hupd").
368
369
    - wp_match. iApply ("HΦ" with "HΨ").
  Qed.
370

371
  Theorem pop_works P s Ψ :
Daniel Gratzer's avatar
Daniel Gratzer committed
372
    {{{ is_stack_pred P s 
373
        ( v xs, P (v :: xs) ={   N}= P xs  Ψ (SOMEV v)) 
Daniel Gratzer's avatar
Daniel Gratzer committed
374
        (P [] ={   N}= P []  Ψ NONEV) }}}
375
376
377
      pop s
    {{{ v, RET v; Ψ v }}}.
  Proof.
378
    iIntros (Φ) "(Hstack & Hupd) HΦ".
379
    iDestruct "Hstack" as (mailbox l) "(-> & #Hmailbox & #Hinv)".
380
381
382
    iDestruct (bi.and_mono_r with "Hupd") as "Hupd"; first apply inner_mask_promote.
    iDestruct (bi.and_mono_l _ _ ( (v : val) (xs : list val), _)%I with "Hupd") as "Hupd".
    { iIntros "Hupdcons". iIntros (v xs). iSpecialize ("Hupdcons" $! v xs). iApply (inner_mask_promote with "Hupdcons"). }
383
384
    iLöb as "IH".
    wp_lam. wp_proj. wp_let. wp_proj. wp_let.
385
    wp_apply (get_works _ _ (λ v, Ψ v) with "[Hupd]").
386
387
388
389
390
391
392
393
394
    { iSplitR; first done.
      iFrame.
      iInv Nstack as (v xs) "(Hl & Hlist & HP)" "Hclose".
      iModIntro.
      iExists xs; iSplitL "HP"; first auto.
      iIntros "HP".
      iMod ("Hclose" with "[HP Hl Hlist]") as "_".
      { iNext; iExists _, _; iFrame. }
      auto. }
395
    iIntros (ov) "[Hsome | [-> Hupd]]".
396
    - iDestruct "Hsome" as (v) "[-> HΨ]".
397
      wp_pures.
398
399
400
401
402
403
404
405
      iApply ("HΦ" with "HΨ").
    - wp_match. wp_bind (Load _).
      iInv Nstack as (v xs) "(Hl & Hlist & HP)" "Hclose".
      wp_load.
      iDestruct (is_list_disj with "Hlist") as "[Hlist H]".
      iDestruct "H" as "[-> | HSome]".
      * iDestruct (is_list_empty with "Hlist") as %->.
        iMod (fupd_intro_mask' (  Nstack) inner_mask) as "Hupd'"; first solve_ndisj.
406
        iMod ("Hupd" with "HP") as "[HP HΨ]".
407
408
409
410
        iMod "Hupd'" as "_".
        iMod ("Hclose" with "[Hlist Hl HP]") as "_".
        { iNext; iExists _, _; iFrame. }
        iModIntro.
411
        wp_match.
412
413
414
415
        iApply ("HΦ" with "HΨ").
      * iDestruct "HSome" as (l' h t) "[-> Hl']".
        iMod ("Hclose" with "[Hlist Hl HP]") as "_".
        { iNext; iExists _, _; iFrame. }
416
        iModIntro.
417
418
419
420
421
422
        wp_match. wp_bind (Load _).
        iInv Nstack as (v xs') "(Hl & Hlist & HP)" "Hclose".
        iDestruct "Hl'" as (q) "Hl'".
        wp_load.
        iMod ("Hclose" with "[Hlist Hl HP]") as "_".
        { iNext; iExists _, _; iFrame. }
423
        iModIntro.
424
        wp_pures. wp_bind (CAS _ _ _).
425
426
427
428
429
430
        iInv Nstack as (v' xs'') "(Hl & Hlist & HP)" "Hclose".
        destruct (decide (v' = (SOMEV #l'))) as [ -> |].
        + wp_cas_suc.
          iDestruct (is_list_cons with "[Hl'] Hlist") as (ys) "%"; first by iExists _.
          simplify_eq.
          iMod (fupd_intro_mask' (  Nstack) inner_mask) as "Hupd'"; first solve_ndisj.
431
          iDestruct "Hupd" as "[Hupdcons _]".
432
433
434
435
436
437
438
439
          iMod ("Hupdcons" with "HP") as "[HP HΨ]".
          iMod "Hupd'" as "_".
          iDestruct "Hlist" as (l'' t') "(% & Hl'' & Hlist)"; simplify_eq.
          iDestruct "Hl''" as (q') "Hl''".
          iDestruct (mapsto_agree with "Hl' Hl''") as "%"; simplify_eq.
          iMod ("Hclose" with "[Hlist Hl HP]") as "_".
          { iNext; iExists _, _; iFrame. }
          iModIntro.
440
          wp_pures.
441
442
443
444
445
          iApply ("HΦ" with "HΨ").
        + wp_cas_fail.
          iMod ("Hclose" with "[Hlist Hl HP]") as "_".
          { iNext; iExists _, _; iFrame. }
          iModIntro.
446
          wp_pures.
447
          iApply ("IH" with "HΦ Hupd").
448
  Qed.
449
End proofs.
Daniel Gratzer's avatar
Daniel Gratzer committed
450
451
452
453

Program Definition spec {Σ} `{heapG Σ, channelG Σ} : concurrent_stack Σ :=
  {| is_stack := is_stack_pred; new_stack := mk_stack; stack_push := push; stack_pop := pop |} .
Solve Obligations of spec with eauto using pop_works, push_works, mk_stack_works.