concurrent_stack1.v 6.06 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.
4 5
Set Default Proof Using "Type".

6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21
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.
22 23

Section stacks.
24
  Context `{!heapG Σ} (N : namespace).
25 26
  Implicit Types l : loc.

27 28 29 30 31 32 33 34
  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.
35

36 37 38
  Definition is_list_pre (P : val  iProp Σ) (F : val -c> iProp Σ) :
     val -c> iProp Σ := λ v,
    (v  NONEV   (l : loc) (h t : val), v  SOMEV #l  l {-} (h, t)%V  P h   F t)%I.
39

40
  Local Instance is_list_contr (P : val  iProp Σ) : Contractive (is_list_pre P).
41
  Proof.
42
    rewrite /is_list_pre => n f f' Hf v.
43 44 45 46
    repeat (f_contractive || f_equiv).
    apply Hf.
  Qed.

47 48 49 50
  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).
51

52 53 54 55 56
  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.
57

58 59 60
  (* TODO: shouldn't have to explicitly return is_list *)
  Lemma is_list_unboxed (P : val  iProp Σ) v :
      is_list P v - val_is_unboxed v  is_list P v.
61
  Proof.
62 63 64
    iIntros "Hstack"; iSplit; last done;
    iDestruct (is_list_unfold with "Hstack") as "[->|Hstack]";
    last iDestruct "Hstack" as (l h t) "(-> & _)"; done.
65 66
  Qed.

67 68
  Lemma is_list_disj (P : val  iProp Σ) v :
    is_list P v - is_list P v  (v  NONEV   (l : loc) h t, v  SOMEV #l%V  l {-} (h, t)%V).
69 70
  Proof.
    iIntros "Hstack".
71 72 73 74 75
    iDestruct (is_list_unfold with "Hstack") as "[%|Hstack]"; simplify_eq.
    - rewrite is_list_unfold; iSplitR; [iLeft|]; eauto.
    - iDestruct "Hstack" as (l h t) "(% & Hl & Hlist)".
      iDestruct (partial_mapsto_duplicable with "Hl") as "[Hl1 Hl2]"; simplify_eq.
      rewrite (is_list_unfold _ (InjRV _)); iSplitR "Hl2"; iRight; iExists _, _, _; by iFrame.
76 77
  Qed.

78 79 80 81 82 83 84 85
  Definition stack_inv P v :=
    ( l v', v = #l  l  v'  is_list P v')%I.

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

  Theorem mk_stack_spec P :
    WP new_stack #() {{ s, is_stack P s }}%I.
86
  Proof.
87
    iApply wp_fupd.
88
    wp_lam.
89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136
    wp_alloc  as "Hl".
    iMod (inv_alloc N  (stack_inv P #) with "[Hl]") as "Hinv".
    { iNext; iExists , NONEV; iFrame;
      by iSplit; last (iApply is_list_unfold; iLeft). }
    done.
  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".
    wp_lam. wp_lam. wp_bind (Load _).
    iInv N as ( v') "(>% & Hl & Hlist)" "Hclose"; subst.
    wp_load.
    iMod ("Hclose" with "[Hl Hlist]") as "_".
    { iNext; iExists _, _; by iFrame. }
    iModIntro. wp_let. wp_alloc ' as "Hl'". wp_let. wp_bind (CAS _ _ _).
    iInv N as ('' v'') "(>% & >Hl & Hlist)" "Hclose"; simplify_eq.
    destruct (decide (v' = v'')) as [ -> |].
    - iDestruct (is_list_unboxed with "Hlist") as "[>% Hlist]".
      wp_cas_suc.
      iMod ("Hclose" with "[HP Hl Hl' Hlist]") as "_".
      { iNext; iExists _, (InjRV #'); iFrame; iSplit; first done;
        rewrite (is_list_unfold _ (InjRV _)). iRight; iExists _, _, _; iFrame; eauto. }
      iModIntro.
      wp_if.
      by iApply "HΦ".
    - iDestruct (is_list_unboxed with "Hlist") as "[>% Hlist]".
      wp_cas_fail.
      iMod ("Hclose" with "[Hl Hlist]") as "_".
      { iNext; iExists _, _; by iFrame. }
      iModIntro.
      wp_if.
      iApply ("IH" with "HP HΦ").
  Qed.

  Theorem pop_works P s :
    {{{ 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.
    wp_load.
    iDestruct (is_list_disj with "Hlist") as "[Hlist Hdisj]".
    iMod ("Hclose" with "[Hl Hlist]") as "_".
    { iNext; iExists _, _; by iFrame. }
137
    iModIntro.
138 139 140 141 142 143 144
    iDestruct "Hdisj" as "[-> | Heq]".
    - wp_match.
      iApply "HΦ"; by iLeft.
    - iDestruct "Heq" as (l h t) "[-> Hl]".
      wp_match. wp_bind (Load _).
      iInv N as (' v') "(>% & Hl' & Hlist)" "Hclose". simplify_eq.
      iDestruct "Hl" as (q) "Hl".
145
      wp_load.
146 147
      iMod ("Hclose" with "[Hl' Hlist]") as "_".
      { iNext; iExists _, _; by iFrame. }
148
      iModIntro.
149 150 151 152 153 154 155 156 157 158 159
      wp_let. wp_proj. wp_bind (CAS _ _ _).
      iInv N as ('' v'') "(>% & Hl' & Hlist)" "Hclose". simplify_eq.
      destruct (decide (v'' = InjRV #l)) as [-> |].
      * rewrite is_list_unfold.
        iDestruct "Hlist" as "[>% | H]"; first done.
        iDestruct "H" as (''' h' t') "(>% & Hl'' & HP & Hlist)"; simplify_eq.
        iDestruct "Hl''" as (q') "Hl''".
        wp_cas_suc.
        iDestruct (mapsto_agree with "Hl'' Hl") as "%"; simplify_eq.
        iMod ("Hclose" with "[Hl' Hlist]") as "_".
        { iNext; iExists '', _; by iFrame. }
160 161
        iModIntro.
        wp_if.
162 163 164 165 166
        wp_proj.
        iApply ("HΦ" with "[HP]"); iRight; iExists h; by iFrame.
      * wp_cas_fail.
        iMod ("Hclose" with "[Hl' Hlist]") as "_".
        { iNext; iExists '', _; by iFrame. }
167 168
        iModIntro.
        wp_if.
169
        iApply ("IH" with "HΦ").
170 171
  Qed.
End stacks.