concurrent_stack4.v 16.2 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 (CmpXchg _ _ _).
123 124
    iInv Nside_channel as "Hstages" "Hclose".
    iDestruct "Hstages" as "[[Hl HP] | [[Hl HQ] | [[Hl H] | [Hl H]]]]".
125
    - wp_cmpxchg_suc.
126 127 128
      iMod ("Hclose" with "[Hl Hγ]") as "_".
      { iNext; iRight; iRight; iFrame. }
      iModIntro.
129
      wp_pures.
130
      by iApply "HΦ"; iLeft; iExists _; iFrame.
131
    - wp_cmpxchg_fail.
132 133 134
      iMod ("Hclose" with "[Hl Hγ]") as "_".
      { iNext; iRight; iRight; iLeft; iFrame. }
      iModIntro.
135
      wp_pures.
136
      iApply ("HΦ" with "[HQ]"); iRight; auto.
137
    - wp_cmpxchg_fail.
138
      iDestruct (own_valid_2 with "H Hγ") as %[].
139
    - wp_cmpxchg_fail.
140 141 142
      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
  Proof.
    simpl; iIntros (Φ) "[H [Hopener Hupd]] HΦ"; iDestruct "H" as (v l) "[-> #Hinv]".
152
    wp_lam. wp_proj. wp_bind (CmpXchg _ _ _).
153 154 155
    iInv Nside_channel as "Hstages" "Hclose".
    iDestruct "Hstages" as "[[Hl Hpush] | [[Hl HQ] | [[Hl Hγ] | [Hl Hγ]]]]".
    - iMod "Hopener" as (xs) "[HP Hcloser]".
156
      wp_cmpxchg_suc.
157 158 159 160 161 162
      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
      iApply "HΦ"; iLeft; auto.
165
    - wp_cmpxchg_fail.
166 167 168
      iMod ("Hclose" with "[Hl HQ]") as "_".
      { iRight; iLeft; iFrame. }
      iModIntro.
169
      wp_pures.
170
      iApply "HΦ"; auto.
171
    - wp_cmpxchg_fail.
172 173 174
      iMod ("Hclose" with "[Hl Hγ]").
      { iRight; iRight; iFrame. }
      iModIntro.
175
      wp_pures.
176
      iApply "HΦ"; auto.
177
    - wp_cmpxchg_fail.
178 179 180
      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
      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.

270 271 272 273 274 275 276 277
  Definition oloc_to_val (ol: option loc) : val :=
    match ol with
    | None => NONEV
    | Some loc => SOMEV (#loc)
    end.
  Local Instance oloc_to_val_inj : Inj (=) (=) oloc_to_val.
  Proof. intros [|][|]; simpl; congruence. Qed.

278
  Fixpoint is_list xs v : iProp Σ :=
279 280 281 282
    (match xs, v with
     | [], None => True
     | x :: xs, Some l =>  t, l {-} (x, oloc_to_val t)%V  is_list xs t
     | _, _ => False
283 284
     end)%I.

285 286 287 288 289
  Lemma is_list_dup xs v :
    is_list xs v - is_list xs v  match v with
      | None => True
      | Some l =>  h t, l {-} (h, oloc_to_val t)%V
      end.
290
  Proof.
291 292
    destruct xs, v; simpl; auto; first by iIntros "[]".
    iIntros "H"; iDestruct "H" as (t) "(Hl & Hstack)".
293
    iDestruct (partial_mapsto_duplicable with "Hl") as "[Hl1 Hl2]".
294
    iSplitR "Hl2"; first by (iExists _; iFrame). by iExists _, _.
295 296
  Qed.

297
  Lemma is_list_empty xs :
298
    is_list xs None - xs = [].
299
  Proof.
300
    destruct xs; iIntros "Hstack"; auto.
301
  Qed.
302 303 304

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

313
  Definition stack_inv P l :=
314
    ( v xs, l  oloc_to_val v  is_list xs v  P xs)%I.
315

Daniel Gratzer's avatar
Daniel Gratzer committed
316
  Definition is_stack_pred P v :=
317 318 319
    ( 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
320
    {{{ P [] }}} mk_stack #() {{{ v, RET v; is_stack_pred P v }}}.
321
  Proof.
322 323
    iIntros (Φ) "HP HΦ".
    rewrite -wp_fupd.
324
    wp_lam.
325
    wp_alloc l as "Hl".
326
    wp_apply mk_mailbox_works ; first done. iIntros (v) "#Hmailbox".
327
    iMod (inv_alloc Nstack _ (stack_inv P l) with "[Hl HP]") as "#Hinv".
328
    { by iNext; iExists None, []; iFrame. }
329
    wp_pures. iModIntro; iApply "HΦ"; iExists _; auto.
330
  Qed.
331

332
  Theorem push_works P s v Ψ :
Daniel Gratzer's avatar
Daniel Gratzer committed
333
    {{{ is_stack_pred P s   xs, P xs ={   N}= P (v :: xs)  Ψ #()}}}
334 335 336 337
      push s v
    {{{ RET #(); Ψ #() }}}.
  Proof.
    iIntros (Φ) "[Hstack Hupd] HΦ". iDestruct "Hstack" as (mailbox l) "(-> & #Hmailbox & #Hinv)".
Daniel Gratzer's avatar
Daniel Gratzer committed
338 339
    iAssert ( (xs : list val), P xs ={inner_mask}= P (v :: xs)  Ψ #())%I with "[Hupd]" as "Hupd".
    { iIntros (xs). by iApply inner_mask_promote. }
340
    iLöb as "IH" forall (v).
341
    wp_lam. wp_pures.
342 343 344 345 346 347 348 349 350 351
    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.
352
      iModIntro.
353
      wp_let. wp_alloc l' as "Hl'". wp_pures. wp_bind (CmpXchg _ _ _).
354 355
      iInv Nstack as (list' xs) "(Hl & Hlist & HP)" "Hclose".
      destruct (decide (list = list')) as [ -> |].
356
      * wp_cmpxchg_suc. { destruct list'; left; done. }
357 358 359 360
        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 "_".
361
        { iNext; iExists (Some _), (v' :: xs); iFrame; iExists _; iFrame; auto. }
362
        iModIntro.
363
        wp_pures.
364
        by iApply ("HΦ" with "HΨ").
365
      * wp_cmpxchg_fail.
366 367
      { destruct list, list'; simpl; congruence. }
      { destruct list'; left; done. }
368 369
        iMod ("Hclose" with "[Hl HP Hlist]").
        { iExists _, _; iFrame. }
370
        iModIntro.
371
        wp_pures.
Daniel Gratzer's avatar
Daniel Gratzer committed
372
        iApply ("IH" with "HΦ Hupd").
373 374
    - wp_match. iApply ("HΦ" with "HΨ").
  Qed.
375

376
  Theorem pop_works P s Ψ :
Daniel Gratzer's avatar
Daniel Gratzer committed
377
    {{{ is_stack_pred P s 
378
        ( v xs, P (v :: xs) ={   N}= P xs  Ψ (SOMEV v)) 
Daniel Gratzer's avatar
Daniel Gratzer committed
379
        (P [] ={   N}= P []  Ψ NONEV) }}}
380 381 382
      pop s
    {{{ v, RET v; Ψ v }}}.
  Proof.
383
    iIntros (Φ) "(Hstack & Hupd) HΦ".
384
    iDestruct "Hstack" as (mailbox l) "(-> & #Hmailbox & #Hinv)".
385 386 387
    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"). }
388 389
    iLöb as "IH".
    wp_lam. wp_proj. wp_let. wp_proj. wp_let.
390
    wp_apply (get_works _ _ (λ v, Ψ v) with "[Hupd]").
391 392 393 394 395 396 397 398 399
    { 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. }
400
    iIntros (ov) "[Hsome | [-> Hupd]]".
401
    - iDestruct "Hsome" as (v) "[-> HΨ]".
402
      wp_pures.
403 404 405 406
      iApply ("HΦ" with "HΨ").
    - wp_match. wp_bind (Load _).
      iInv Nstack as (v xs) "(Hl & Hlist & HP)" "Hclose".
      wp_load.
407 408
      iDestruct (is_list_dup with "Hlist") as "[Hlist H]".
    destruct v as [l'|]; last first.
409 410
      * iDestruct (is_list_empty with "Hlist") as %->.
        iMod (fupd_intro_mask' (  Nstack) inner_mask) as "Hupd'"; first solve_ndisj.
411
        iMod ("Hupd" with "HP") as "[HP HΨ]".
412 413 414 415
        iMod "Hupd'" as "_".
        iMod ("Hclose" with "[Hlist Hl HP]") as "_".
        { iNext; iExists _, _; iFrame. }
        iModIntro.
416
        wp_match.
417
        iApply ("HΦ" with "HΨ").
418
      * iDestruct "H" as (h t) "Hl'".
419 420
        iMod ("Hclose" with "[Hlist Hl HP]") as "_".
        { iNext; iExists _, _; iFrame. }
421
        iModIntro.
422 423 424 425 426 427
        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. }
428
        iModIntro.
429
        wp_pures. wp_bind (CmpXchg _ _ _).
430
        iInv Nstack as (v' xs'') "(Hl & Hlist & HP)" "Hclose".
431
        destruct (decide (v' = (Some l'))) as [ -> |].
432
        + wp_cmpxchg_suc.
433 434 435
          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.
436
          iDestruct "Hupd" as "[Hupdcons _]".
437 438
          iMod ("Hupdcons" with "HP") as "[HP HΨ]".
          iMod "Hupd'" as "_".
439
          iDestruct "Hlist" as (t') "(Hl'' & Hlist)".
440 441 442 443 444
          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.
445
          wp_pures.
446
          iApply ("HΦ" with "HΨ").
447
        + wp_cmpxchg_fail. { destruct v'; simpl; congruence. }
448 449 450
          iMod ("Hclose" with "[Hlist Hl HP]") as "_".
          { iNext; iExists _, _; iFrame. }
          iModIntro.
451
          wp_pures.
452
          iApply ("IH" with "HΦ Hupd").
453
  Qed.
454
End proofs.
Daniel Gratzer's avatar
Daniel Gratzer committed
455 456 457 458

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.