concurrent_stack1.v 5.89 KB
Newer Older
1 2 3 4 5 6 7
From iris.base_logic Require Import base_logic.
From iris.proofmode Require Import tactics.
From iris.base_logic.lib Require Import invariants.
From iris.program_logic Require Export weakestpre hoare.
From iris.heap_lang Require Export lang.
From iris.algebra Require Import agree list.
From iris.heap_lang Require Import assert proofmode notation.
8 9 10

From iris_examples.concurrent_stacks Require Import spec.

11 12
Set Default Proof Using "Type".

13 14
(** Stack 1: No helping, bag spec. *)

15 16 17 18 19
Definition mk_stack : val :=
  λ: "_",
  let: "r" := ref NONEV in
  (rec: "pop" "n" :=
     match: !"r" with
20
       NONE => NONE
21
     | SOME "hd" =>
22
       if: CAS "r" (SOME "hd") (Snd !"hd")
23
       then SOME (Fst !"hd")
24 25 26 27
       else "pop" "n"
     end,
    rec: "push" "n" :=
       let: "r'" := !"r" in
28
       let: "r''" := SOME (Alloc ("n", "r'")) in
29 30 31 32 33 34 35 36
       if: CAS "r" "r'" "r''"
       then #()
       else "push" "n").

Section stacks.
  Context `{!heapG Σ}.
  Implicit Types l : loc.

37 38 39 40 41 42 43 44 45 46 47 48 49 50
  Definition oloc_to_val (h : option loc) : val :=
    match h with
    | None => NONEV
    | Some l => SOMEV #l
    end.
  Local Instance oloc_to_val_inj : Inj (=) (=) oloc_to_val.
  Proof. rewrite /Inj /oloc_to_val=>??. repeat case_match; congruence. Qed.

  Definition is_stack_pre (P : val  iProp Σ) (F : option loc -c> iProp Σ) :
     option loc -c> iProp Σ := λ v,
    (match v with
     | None => True
     | Some l =>  q h t, l {q} (h, oloc_to_val t)  P h   F t
     end)%I.
51 52 53 54 55 56 57 58 59 60 61 62 63

  Local Instance is_stack_contr (P : val  iProp Σ): Contractive (is_stack_pre P).
  Proof.
    rewrite /is_stack_pre => n f f' Hf v.
    repeat (f_contractive || f_equiv).
    apply Hf.
  Qed.

  Definition is_stack_def (P : val -> iProp Σ) := fixpoint (is_stack_pre P).
  Definition is_stack_aux P : seal (@is_stack_def P). by eexists. Qed.
  Definition is_stack P := unseal (is_stack_aux P).
  Definition is_stack_eq P : @is_stack P = @is_stack_def P := seal_eq (is_stack_aux P).

64 65
  Definition stack_inv P l :=
    ( ol, l  oloc_to_val ol  is_stack P ol)%I.
66 67 68 69 70 71 72 73


  Lemma is_stack_unfold (P : val  iProp Σ) v :
      is_stack P v  is_stack_pre P (is_stack P) v.
  Proof.
    rewrite is_stack_eq. apply (fixpoint_unfold (is_stack_pre P)).
  Qed.

74 75 76
  Lemma is_stack_copy (P : val  iProp Σ) ol :
      is_stack P ol - is_stack P ol 
           (match ol with None => True | Some l =>  q h t, l {q} (h, oloc_to_val t) end).
77 78
  Proof.
    iIntros "Hstack".
79 80 81 82
    iDestruct (is_stack_unfold with "Hstack") as "Hstack". destruct ol; last first.
    - iSplitL; try iApply is_stack_unfold; auto.
    - iDestruct "Hstack" as (q h t) "[[Hl1 Hl2] [HP Hrest]]".
      iSplitR "Hl2"; try iApply is_stack_unfold; simpl; eauto 10 with iFrame.
83 84
  Qed.

85
  (* Per-element invariant (i.e., bag spec). *)
86
  Theorem stack_works P Φ :
87 88
     ( (f f : val),
            ( WP f #() {{ v, ( v', v  SOMEV v'  P v')    v  NONEV }})
89 90 91 92 93 94 95 96 97
         - ( (v : val),  (P v - WP f v {{ v, True }}))
         - Φ (f, f)%V)%I
    - WP mk_stack #()  {{ Φ }}.
  Proof.
    iIntros "HΦ".
    wp_lam.
    wp_alloc l as "Hl".
    pose proof (nroot .@ "N") as N.
    rewrite -wp_fupd.
98 99 100
    iMod (inv_alloc N _ (stack_inv P l) with "[Hl]") as "#Hisstack".
    { iExists None; iFrame; auto.
      iApply is_stack_unfold. auto. }
101 102 103
    wp_let.
    iModIntro.
    iApply "HΦ".
104
    - iIntros "!#".
105 106 107 108
      iLöb as "IH".
      wp_rec.
      wp_bind (! #l)%E.
      iInv N as "Hstack" "Hclose".
109
      iDestruct "Hstack" as (v') "[Hl' Hstack]".
110
      wp_load.
111 112 113 114 115 116 117 118 119 120
      destruct v' as [l'|]; simpl; last first.
      + iMod ("Hclose" with "[Hl' Hstack]") as "_".
        { rewrite /stack_inv. eauto with iFrame. }
        iModIntro. wp_match. by iRight.
      + iDestruct (is_stack_copy with "Hstack") as "[Hstack Hmy]".
        iDestruct "Hmy" as (q h t) "Hl".
        iMod ("Hclose" with "[Hl' Hstack]") as "_".
        { rewrite /stack_inv. eauto with iFrame. }
        iModIntro. wp_match.
        wp_load. wp_proj.
121 122
        wp_bind (CAS _ _ _).
        iInv N as "Hstack" "Hclose".
123 124 125 126 127 128
        iDestruct "Hstack" as (v'') "[Hl'' Hstack]".
        destruct (decide (oloc_to_val v'' = oloc_to_val (Some l'))) as [->%oloc_to_val_inj|Hne].
        * simpl. wp_cas_suc.
          iDestruct (is_stack_unfold with "Hstack") as "Hstack".
          iDestruct "Hstack" as (q' h' t') "[Hl' [HP Hstack]]".
          iDestruct (mapsto_agree with "Hl Hl'") as %[= <- <-%oloc_to_val_inj].
129
          iMod ("Hclose" with "[Hl'' Hstack]").
130
          { iExists _. auto with iFrame. }
131 132
          iModIntro.
          wp_if.
133
          wp_load.
134
          wp_proj.
135
          eauto.
136
        * simpl in Hne. wp_cas_fail.
137
          iMod ("Hclose" with "[Hl'' Hstack]").
138
          { iExists v''; iFrame; auto. }
139 140 141 142 143 144 145 146
          iModIntro.
          wp_if.
          iApply "IH".
    - iIntros (v) "!# HP".
      iLöb as "IH".
      wp_rec.
      wp_bind (! _)%E.
      iInv N as "Hstack" "Hclose".
147
      iDestruct "Hstack" as (v') "[Hl' Hstack]".
148 149
      wp_load.
      iMod ("Hclose" with "[Hl' Hstack]").
150
      { iExists v'. iFrame. }
151 152
      iModIntro.
      wp_let.
153
      wp_alloc r'' as "Hr''".
154 155 156
      wp_let.
      wp_bind (CAS _ _ _).
      iInv N as "Hstack" "Hclose".
157 158 159 160 161
      iDestruct "Hstack" as (v'') "[Hl'' Hstack]".
      wp_cas as ->%oloc_to_val_inj|_.
      + destruct v'; by right.
      + iMod ("Hclose" with "[Hl'' Hr'' HP Hstack]").
        iExists (Some r'').
162
        iFrame; auto.
163
        iNext.
164
        iApply is_stack_unfold.
165 166
        simpl.
        iExists _, _, v'. iFrame.
167 168 169
        iModIntro.
        wp_if.
        done.
170 171
      + iMod ("Hclose" with "[Hl'' Hstack]").
        iExists v''; iFrame; auto.
172 173 174 175 176 177
        iModIntro.
        wp_if.
        iApply "IH".
        done.
  Qed.
End stacks.
178 179 180 181 182 183 184

Program Definition is_concurrent_bag `{!heapG Σ} : concurrent_bag Σ :=
  {| spec.mk_bag := mk_stack |}.
Next Obligation.
  iIntros (??? P Φ) "_ HΦ". iApply stack_works.
  iNext. iIntros (f f) "Hpop Hpush". iApply "HΦ". iFrame.
Qed.