concurrent_stack3.v 6.7 KB
Newer Older
1 2
From iris.program_logic Require Export weakestpre hoare.
From iris.heap_lang Require Export lang proofmode notation.
Daniel Gratzer's avatar
Daniel Gratzer committed
3
From iris_examples.concurrent_stacks Require Import specs.
4 5
Set Default Proof Using "Type".

Daniel Gratzer's avatar
Daniel Gratzer committed
6 7
(** Stack 3: No helping, CAP spec. *)

8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23
Definition mk_stack : val := λ: "_", ref NONEV.
Definition push : val :=
  rec: "push" "s" "v" :=
    let: "tail" := ! "s" in
    let: "new" := SOME (ref ("v", "tail")) in
    if: CAS "s" "tail" "new" then #() else "push" "s" "v".
Definition pop : val :=
  rec: "pop" "s" :=
    match: !"s" with
      NONE => NONEV
    | SOME "l" =>
      let: "pair" := !"l" in
      if: CAS "s" (SOME "l") (Snd "pair")
      then SOME (Fst "pair")
      else "pop" "s"
    end.
24 25

Section stack_works.
26
  Context `{!heapG Σ} (N : namespace).
27 28
  Implicit Types l : loc.

29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46
  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.

47 48 49 50 51 52 53 54
  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.

55
  Fixpoint is_list xs v : iProp Σ :=
56 57 58 59
    (match xs, v with
     | [], None => True
     | x :: xs, Some l =>  t, l {-} (x, oloc_to_val t)%V  is_list xs t
     | _, _ => False
60 61
     end)%I.

62 63 64 65 66
  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.
67
  Proof.
68 69
    destruct xs, v; simpl; auto; first by iIntros "[]".
    iIntros "H"; iDestruct "H" as (t) "(Hl & Hstack)".
70
    iDestruct (partial_mapsto_duplicable with "Hl") as "[Hl1 Hl2]".
71
    iSplitR "Hl2"; first by (iExists _; iFrame). by iExists _, _.
72 73
  Qed.

74
  Lemma is_list_empty xs :
75
    is_list xs None - xs = [].
76
  Proof.
77
    destruct xs; iIntros "Hstack"; auto.
78 79
  Qed.

80 81
  Lemma is_list_cons xs l h t :
    l {-} (h, t)%V -
82
    is_list xs (Some l) -
83
     ys, xs = h :: ys.
84
  Proof.
85
    destruct xs; first by iIntros "? %".
86
    iIntros "Hl Hstack"; iDestruct "Hstack" as (t') "(Hl' & Hrest)".
87
    iDestruct (partial_mapsto_agree with "Hl Hl'") as "%"; simplify_eq; iExists _; auto.
88
  Qed.
89 90

  Definition stack_inv P l :=
91
    ( v xs, l  oloc_to_val v  is_list xs v  P xs)%I.
92

Daniel Gratzer's avatar
Daniel Gratzer committed
93
  Definition is_stack_pred P v :=
94 95
    ( l, v = #l  inv N (stack_inv P l))%I.

Daniel Gratzer's avatar
Daniel Gratzer committed
96 97
  Theorem mk_stack_spec P :
    {{{ P [] }}} mk_stack #() {{{ v, RET v; is_stack_pred P v }}}.
98
  Proof.
99 100
    iIntros (Φ) "HP HΦ".
    rewrite -wp_fupd.
101
    wp_lam. wp_alloc l as "Hl".
102
    iMod (inv_alloc N _ (stack_inv P l) with "[Hl HP]") as "#Hinv".
103
    { iNext; iExists None, []; iFrame. }
104
    iModIntro; iApply "HΦ"; iExists _; auto.
105 106
  Qed.

Daniel Gratzer's avatar
Daniel Gratzer committed
107 108
  Theorem push_spec P s v Ψ :
    {{{ is_stack_pred P s   xs, P xs ={   N}= P (v :: xs)  Ψ #()}}}
109 110
      push s v
    {{{ RET #(); Ψ #() }}}.
111
  Proof.
112 113
    iIntros (Φ) "[Hstack Hupd] HΦ". iDestruct "Hstack" as (l) "[-> #Hinv]".
    iLöb as "IH".
114
    wp_lam. wp_pures. wp_bind (Load _).
115 116 117 118 119 120
    iInv N as (list xs) "(Hl & Hlist & HP)" "Hclose".
    wp_load.
    iMod ("Hclose" with "[Hl Hlist HP]") as "_".
    { iNext; iExists _, _; iFrame. }
    clear xs.
    iModIntro.
121
    wp_let. wp_alloc l' as "Hl'". wp_pures. wp_bind (CmpXchg _ _ _).
122 123
    iInv N as (list' xs) "(Hl & Hlist & HP)" "Hclose".
    destruct (decide (list = list')) as [ -> |].
124
    - wp_cmpxchg_suc. { destruct list'; left; done. }
125 126
      iMod ("Hupd" with "HP") as "[HP HΨ]".
      iMod ("Hclose" with "[Hl Hl' HP Hlist]") as "_".
127
      { iNext; iExists (Some _), (v :: xs); iFrame; iExists _; iFrame; auto. }
128
      iModIntro.
129
      wp_pures.
130
      by iApply ("HΦ" with "HΨ").
131
    - wp_cmpxchg_fail.
132 133
      { destruct list, list'; simpl; congruence. }
      { destruct list'; left; done. }
134 135 136
      iMod ("Hclose" with "[Hl HP Hlist]").
      { iExists _, _; iFrame. }
      iModIntro.
137
      wp_pures.
138 139
      iApply ("IH" with "Hupd HΦ").
  Qed.
140

Daniel Gratzer's avatar
Daniel Gratzer committed
141 142
  Theorem pop_spec P s Ψ :
    {{{ is_stack_pred P s 
143
        ( v xs, P (v :: xs) ={   N}= P xs  Ψ (SOMEV v)) 
144 145 146 147
        (P [] ={   N}= P []  Ψ NONEV) }}}
      pop s
    {{{ v, RET v; Ψ v }}}.
  Proof.
148
    iIntros (Φ) "(Hstack & Hupd) HΦ".
149 150 151 152 153
    iDestruct "Hstack" as (l) "[-> #Hinv]".
    iLöb as "IH".
    wp_lam. wp_bind (Load _).
    iInv N as (v xs) "(Hl & Hlist & HP)" "Hclose".
    wp_load.
154 155
    iDestruct (is_list_dup with "Hlist") as "[Hlist H]".
    destruct v as [l'|]; last first.
156
    - iDestruct (is_list_empty with "Hlist") as %->.
157
      iDestruct "Hupd" as "[_ Hupdnil]".
158 159 160 161 162 163
      iMod ("Hupdnil" with "HP") as "[HP HΨ]".
      iMod ("Hclose" with "[Hlist Hl HP]") as "_".
      { iNext; iExists _, _; iFrame. }
      iModIntro.
      wp_match.
      iApply ("HΦ" with "HΨ").
164
    - iDestruct "H" as (h t) "Hl'".
165 166 167 168 169 170
      iMod ("Hclose" with "[Hlist Hl HP]") as "_".
      { iNext; iExists _, _; iFrame. }
      iModIntro.
      wp_match. wp_bind (Load _).
      iInv N as (v xs') "(Hl & Hlist & HP)" "Hclose".
      iDestruct "Hl'" as (q) "Hl'".
171
      wp_load.
172 173
      iMod ("Hclose" with "[Hlist Hl HP]") as "_".
      { iNext; iExists _, _; iFrame. }
174
      iModIntro.
175
      wp_let. wp_proj. wp_bind (CmpXchg _ _ _). wp_pures.
176
      iInv N as (v' xs'') "(Hl & Hlist & HP)" "Hclose".
177
      destruct (decide (v' = (Some l'))) as [ -> |].
178
      * wp_cmpxchg_suc.
179 180
        iDestruct (is_list_cons with "[Hl'] Hlist") as (ys) "%"; first by iExists _.
        simplify_eq.
181
        iDestruct "Hupd" as "[Hupdcons _]".
182
        iMod ("Hupdcons" with "HP") as "[HP HΨ]".
183
        iDestruct "Hlist" as (t') "(Hl'' & Hlist)".
184 185 186 187
        iDestruct "Hl''" as (q') "Hl''".
        iDestruct (mapsto_agree with "Hl' Hl''") as "%"; simplify_eq.
        iMod ("Hclose" with "[Hlist Hl HP]") as "_".
        { iNext; iExists _, _; iFrame. }
188
        iModIntro.
189
        wp_pures.
190
        iApply ("HΦ" with "HΨ").
191
      * wp_cmpxchg_fail. { destruct v'; simpl; congruence. }
192 193
        iMod ("Hclose" with "[Hlist Hl HP]") as "_".
        { iNext; iExists _, _; iFrame. }
194
        iModIntro.
195
        wp_pures.
196
        iApply ("IH" with "Hupd HΦ").
197 198
  Qed.
End stack_works.
Daniel Gratzer's avatar
Daniel Gratzer committed
199 200 201 202

Program Definition spec {Σ} `{heapG Σ} : 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_spec, push_spec, mk_stack_spec.