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.