concurrent_stack1.v 6.29 KB
Newer Older
1
From iris.base_logic.lib Require Import invariants.
2 3
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Import notation proofmode.
Daniel Gratzer's avatar
Daniel Gratzer committed
4
From iris_examples.concurrent_stacks Require Import specs.
5 6
Set Default Proof Using "Type".

Daniel Gratzer's avatar
Daniel Gratzer committed
7 8
(** Stack 1: No helping, bag spec. *)

9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24
Definition new_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.
25 26

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

30 31 32 33 34 35 36 37
  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.
38

39 40 41 42 43 44 45 46 47 48 49 50 51
  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.

  Definition is_list_pre (P : val  iProp Σ) (F : option loc -d> iProp Σ) :
     option loc -d> iProp Σ := λ v, match v with
     | None => True
     | Some l =>  (h : val) (t : option loc), l {-} (h, oloc_to_val t)%V  P h   F t
     end%I.
52

53
  Local Instance is_list_contr (P : val  iProp Σ) : Contractive (is_list_pre P).
54
  Proof.
55
    rewrite /is_list_pre => n f f' Hf v.
56 57 58 59
    repeat (f_contractive || f_equiv).
    apply Hf.
  Qed.

60 61 62 63
  Definition is_list_def (P : val -> iProp Σ) := fixpoint (is_list_pre P).
  Definition is_list_aux P : seal (@is_list_def P). by eexists. Qed.
  Definition is_list P := unseal (is_list_aux P).
  Definition is_list_eq P : @is_list P = @is_list_def P := seal_eq (is_list_aux P).
64

65 66 67 68 69
  Lemma is_list_unfold (P : val  iProp Σ) v :
    is_list P v ⊣⊢ is_list_pre P (is_list P) v.
  Proof.
    rewrite is_list_eq. apply (fixpoint_unfold (is_list_pre P)).
  Qed.
70

71 72 73 74 75
  Lemma is_list_dup (P : val  iProp Σ) v :
    is_list P v - is_list P v  match v with
      | None => True
      | Some l =>  h t, l {-} (h, oloc_to_val t)%V
      end.
76
  Proof.
77 78 79 80 81 82
    iIntros "Hstack". iDestruct (is_list_unfold with "Hstack") as "Hstack".
    destruct v as [l|].
    - iDestruct "Hstack" as (h t) "(Hl & Hlist)".
      iDestruct (partial_mapsto_duplicable with "Hl") as "[Hl1 Hl2]".
      rewrite (is_list_unfold _ (Some _)); iSplitR "Hl2"; iExists _, _; by iFrame.
    - rewrite is_list_unfold; iSplitR; eauto.
83 84
  Qed.

85
  Definition stack_inv P v :=
86
    ( l ol', v = #l  l  oloc_to_val ol'  is_list P ol')%I.
87 88 89 90

  Definition is_stack (P : val  iProp Σ) v :=
    inv N (stack_inv P v).

Daniel Gratzer's avatar
Daniel Gratzer committed
91 92
  Theorem new_stack_spec P :
    {{{ True }}} new_stack #() {{{ s, RET s; is_stack P s }}}.
93
  Proof.
Daniel Gratzer's avatar
Daniel Gratzer committed
94
    iIntros (ϕ) "_ Hpost".
95
    iApply wp_fupd.
96
    wp_lam.
97 98
    wp_alloc  as "Hl".
    iMod (inv_alloc N  (stack_inv P #) with "[Hl]") as "Hinv".
99 100
    { iNext; iExists , None; iFrame;
      by iSplit; last (iApply is_list_unfold). }
Daniel Gratzer's avatar
Daniel Gratzer committed
101
    by iApply "Hpost".
102 103 104 105 106 107 108
  Qed.

  Theorem push_spec P s v :
    {{{ is_stack P s  P v }}} push s v {{{ RET #(); True }}}.
  Proof.
    iIntros (Φ) "[#Hstack HP] HΦ".
    iLöb as "IH".
109
    wp_lam. wp_let. wp_bind (Load _).
110 111 112 113
    iInv N as ( v') "(>% & Hl & Hlist)" "Hclose"; subst.
    wp_load.
    iMod ("Hclose" with "[Hl Hlist]") as "_".
    { iNext; iExists _, _; by iFrame. }
114
    iModIntro. wp_let. wp_alloc ' as "Hl'". wp_pures. wp_bind (CmpXchg _ _ _).
115
    iInv N as ('' v'') "(>% & >Hl & Hlist)" "Hclose"; simplify_eq.
116
    destruct (decide (v' = v'')) as [->|Hne].
117
    - wp_cmpxchg_suc. { destruct v''; left; done. }
118
      iMod ("Hclose" with "[HP Hl Hl' Hlist]") as "_".
119 120
      { iNext; iExists _, (Some '); iFrame; iSplit; first done;
        rewrite (is_list_unfold _ (Some _)). iExists _, _; iFrame; eauto. }
121
      iModIntro.
122
      wp_pures.
123
      by iApply "HΦ".
124
    - wp_cmpxchg_fail.
125 126
      { destruct v', v''; simpl; congruence. }
      { destruct v''; left; done. }
127 128 129
      iMod ("Hclose" with "[Hl Hlist]") as "_".
      { iNext; iExists _, _; by iFrame. }
      iModIntro.
130
      wp_pures.
131 132 133
      iApply ("IH" with "HP HΦ").
  Qed.

Daniel Gratzer's avatar
Daniel Gratzer committed
134
  Theorem pop_spec P s :
135 136 137 138 139 140
    {{{ is_stack P s }}} pop s {{{ ov, RET ov; ov = NONEV   v, ov = SOMEV v  P v }}}.
  Proof.
    iIntros (Φ) "#Hstack HΦ".
    iLöb as "IH".
    wp_lam. wp_bind (Load _).
    iInv N as ( v') "(>% & Hl & Hlist)" "Hclose"; subst.
141
    iDestruct (is_list_dup with "Hlist") as "[Hlist Hlist2]".
142 143 144
    wp_load.
    iMod ("Hclose" with "[Hl Hlist]") as "_".
    { iNext; iExists _, _; by iFrame. }
145
    iModIntro.
146
    destruct v' as [l|]; last first.
147 148
    - wp_match.
      iApply "HΦ"; by iLeft.
149
    - wp_match. wp_bind (Load _).
150
      iInv N as (' v') "(>% & Hl' & Hlist)" "Hclose". simplify_eq.
151
      iDestruct "Hlist2" as (???) "Hl".
152
      wp_load.
153 154
      iMod ("Hclose" with "[Hl' Hlist]") as "_".
      { iNext; iExists _, _; by iFrame. }
155
      iModIntro.
156
      wp_pures. wp_bind (CmpXchg _ _ _).
157
      iInv N as ('' v'') "(>% & Hl' & Hlist)" "Hclose". simplify_eq.
158
      destruct (decide (v'' = (Some l))) as [-> |].
159
      * rewrite is_list_unfold.
160
        iDestruct "Hlist" as (h' t') "(Hl'' & HP & Hlist)".
161
        iDestruct "Hl''" as (q') "Hl''".
162
        simpl.
163
        wp_cmpxchg_suc.
164
        iDestruct (mapsto_agree with "Hl'' Hl") as %[= <- <-%oloc_to_val_inj].
165 166
        iMod ("Hclose" with "[Hl' Hlist]") as "_".
        { iNext; iExists '', _; by iFrame. }
167
        iModIntro.
168
        wp_pures.
169
        iApply ("HΦ" with "[HP]"); iRight; iExists _; by iFrame.
170
      * wp_cmpxchg_fail. { destruct v''; simpl; congruence. }
171 172
        iMod ("Hclose" with "[Hl' Hlist]") as "_".
        { iNext; iExists '', _; by iFrame. }
173
        iModIntro.
174
        wp_pures.
175
        iApply ("IH" with "HΦ").
176 177
  Qed.
End stacks.
Daniel Gratzer's avatar
Daniel Gratzer committed
178

179 180
Program Definition spec {Σ} N `{heapG Σ} : concurrent_bag Σ :=
  {| is_bag := is_stack N; new_bag := new_stack; bag_push := push; bag_pop := pop |} .
Daniel Gratzer's avatar
Daniel Gratzer committed
181
Solve Obligations of spec with eauto using pop_spec, push_spec, new_stack_spec.