treiber.v 7.01 KB
Newer Older
Zhen Zhang's avatar
Zhen Zhang committed
1 2 3
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation.
4
From iris.algebra Require Import frac auth gmap csum.
Zhen Zhang's avatar
Zhen Zhang committed
5
From iris_atomic Require Import atomic misc.
Zhen Zhang's avatar
Zhen Zhang committed
6 7 8 9 10 11 12 13 14 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

Definition new_stack: val := λ: <>, ref (ref NONE).

Definition push: val :=
  rec: "push" "s" "x" :=
      let: "hd" := !"s" in
      let: "s'" := ref SOME ("x", "hd") in
      if: CAS "s" "hd" "s'"
        then #()
        else "push" "s" "x".

Definition pop: val :=
  rec: "pop" "s" :=
      let: "hd" := !"s" in
      match: !"hd" with
        SOME "cell" =>
        if: CAS "s" "hd" (Snd "cell")
          then SOME (Fst "cell")
          else "pop" "s"
      | NONE => NONE
      end.

Definition iter: val :=
  rec: "iter" "hd" "f" :=
      match: !"hd" with
        NONE => #()
      | SOME "cell" => "f" (Fst "cell") ;; "iter" (Snd "cell") "f"
      end.

Section proof.
  Context `{!heapG Σ} (N: namespace).

  Fixpoint is_list (hd: loc) (xs: list val) : iProp Σ :=
    match xs with
    | [] => ( q, hd { q } NONEV)%I
41
    | x :: xs => ( (hd': loc) q, hd { q } SOMEV (x, #hd')  is_list hd' xs)%I
Zhen Zhang's avatar
Zhen Zhang committed
42 43 44
    end.

  Lemma dup_is_list :  xs hd,
45
    is_list hd xs  is_list hd xs  is_list hd xs.
Zhen Zhang's avatar
Zhen Zhang committed
46 47
  Proof.
    induction xs as [|y xs' IHxs'].
48
    - iIntros (hd) "Hs".
Zhen Zhang's avatar
Zhen Zhang committed
49
      simpl. iDestruct "Hs" as (q) "[Hhd Hhd']". iSplitL "Hhd"; eauto.
50
    - iIntros (hd) "Hs". simpl.
Zhen Zhang's avatar
Zhen Zhang committed
51 52 53 54 55 56
      iDestruct "Hs" as (hd' q) "([Hhd Hhd'] & Hs')".
      iDestruct (IHxs' with "[Hs']") as "[Hs1 Hs2]"; first by iFrame.
      iSplitL "Hhd Hs1"; iExists hd', (q / 2)%Qp; by iFrame.
  Qed.

  Lemma uniq_is_list:
57
     xs ys hd, is_list hd xs  is_list hd ys  xs = ys.
Zhen Zhang's avatar
Zhen Zhang committed
58 59 60 61
  Proof.
    induction xs as [|x xs' IHxs'].
    - induction ys as [|y ys' IHys'].
      + auto.
62
      + iIntros (hd) "(Hxs & Hys)".
Zhen Zhang's avatar
Zhen Zhang committed
63 64
        simpl. iDestruct "Hys" as (hd' ?) "(Hhd & Hys')".
        iExFalso. iDestruct "Hxs" as (?) "Hhd'".
Robbert Krebbers's avatar
Robbert Krebbers committed
65
        (* FIXME: If I dont use the @ here and below through this file, it loops. *)
66
        by iDestruct (@mapsto_agree with "[$Hhd] [$Hhd']") as %?.
Zhen Zhang's avatar
Zhen Zhang committed
67
    - induction ys as [|y ys' IHys'].
68
      + iIntros (hd) "(Hxs & Hys)".
Zhen Zhang's avatar
Zhen Zhang committed
69 70 71
        simpl.
        iExFalso. iDestruct "Hxs" as (? ?) "(Hhd & _)".
        iDestruct "Hys" as (?) "Hhd'".
72
        by iDestruct (@mapsto_agree with "[$Hhd] [$Hhd']") as %?.
73
      + iIntros (hd) "(Hxs & Hys)".
Zhen Zhang's avatar
Zhen Zhang committed
74 75
        simpl. iDestruct "Hxs" as (? ?) "(Hhd & Hxs')".
        iDestruct "Hys" as (? ?) "(Hhd' & Hys')".
76
        iDestruct (@mapsto_agree with "[$Hhd] [$Hhd']") as %[= Heq].
Zhen Zhang's avatar
Zhen Zhang committed
77 78 79 80
        subst. iDestruct (IHxs' with "[Hxs' Hys']") as "%"; first by iFrame.
        by subst.
  Qed.

81
  Definition is_stack (s: loc) xs: iProp Σ := ( hd: loc, s  #hd  is_list hd xs)%I.
Zhen Zhang's avatar
Zhen Zhang committed
82

Ralf Jung's avatar
Ralf Jung committed
83
  Global Instance is_list_timeless xs hd: Timeless (is_list hd xs).
Zhen Zhang's avatar
Zhen Zhang committed
84 85
  Proof. generalize hd. induction xs; apply _. Qed.

Ralf Jung's avatar
Ralf Jung committed
86
  Global Instance is_stack_timeless xs hd: Timeless (is_stack hd xs).
Zhen Zhang's avatar
Zhen Zhang committed
87 88 89 90
  Proof. generalize hd. induction xs; apply _. Qed.

  Lemma new_stack_spec:
     (Φ: val  iProp Σ),
91
      ( s, is_stack s [] - Φ #s)  WP new_stack #() {{ Φ }}.
Zhen Zhang's avatar
Zhen Zhang committed
92
  Proof.
93
    iIntros (Φ) "HΦ". wp_seq.
Zhen Zhang's avatar
Zhen Zhang committed
94 95 96 97 98 99 100
    wp_bind (ref NONE)%E. wp_alloc l as "Hl".
    wp_alloc l' as "Hl'".
    iApply "HΦ". rewrite /is_stack. iExists l.
    iFrame. by iExists 1%Qp.
  Qed.

  Definition push_triple (s: loc) (x: val) :=
Ralf Jung's avatar
Ralf Jung committed
101
  atomic_triple (fun xs_hd: list val * loc =>
102
                     let '(xs, hd) := xs_hd in s  #hd  is_list hd xs)%I
Ralf Jung's avatar
Ralf Jung committed
103 104 105
                (fun xs_hd ret =>
                   let '(xs, hd) := xs_hd in 
                    hd': loc,
106 107
                     ret = #()  s  #hd'  hd'  SOMEV (x, #hd)  is_list hd xs)%I
                
Ralf Jung's avatar
Ralf Jung committed
108 109
                
                (push #s x).
Zhen Zhang's avatar
Zhen Zhang committed
110 111
  
  Lemma push_atomic_spec (s: loc) (x: val) :
112
    push_triple s x.
Zhen Zhang's avatar
Zhen Zhang committed
113
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
114
    rewrite /push_triple /atomic_triple.
Zhen Zhang's avatar
Zhen Zhang committed
115 116 117
    iIntros (P Q) "#Hvs".
    iLöb as "IH". iIntros "!# HP". wp_rec.
    wp_let. wp_bind (! _)%E.
Robbert Krebbers's avatar
Robbert Krebbers committed
118
    iMod ("Hvs" with "HP") as ([xs hd]) "[[Hs Hhd] [Hvs' _]]".
119 120
    wp_load. iMod ("Hvs'" with "[Hs Hhd]") as "HP"; first by iFrame.
    iModIntro. wp_let. wp_alloc l as "Hl". wp_let.
Zhen Zhang's avatar
Zhen Zhang committed
121
    wp_bind (CAS _ _ _)%E.
122
    iMod ("Hvs" with "HP") as ([xs' hd']) "[[Hs Hhd'] Hvs']".
Robbert Krebbers's avatar
Robbert Krebbers committed
123
    destruct (decide (hd = hd')) as [->|Hneq].
Zhen Zhang's avatar
Zhen Zhang committed
124
    * wp_cas_suc. iDestruct "Hvs'" as "[_ Hvs']".
125
      iMod ("Hvs'" $! #() with "[-]") as "HQ".
Zhen Zhang's avatar
Zhen Zhang committed
126
      { iExists l. iSplitR; first done. by iFrame. }
127
      iModIntro. wp_if. eauto.
Zhen Zhang's avatar
Zhen Zhang committed
128 129
    * wp_cas_fail.
      iDestruct "Hvs'" as "[Hvs' _]".
130 131
      iMod ("Hvs'" with "[-]") as "HP"; first by iFrame.
      iModIntro. wp_if. by iApply "IH".
Zhen Zhang's avatar
Zhen Zhang committed
132 133 134
  Qed.

  Definition pop_triple (s: loc) :=
Ralf Jung's avatar
Ralf Jung committed
135
  atomic_triple (fun xs_hd: list val * loc =>
136
                   let '(xs, hd) := xs_hd in s  #hd  is_list hd xs)%I
Ralf Jung's avatar
Ralf Jung committed
137 138
                (fun xs_hd ret =>
                   let '(xs, hd) := xs_hd in
139 140 141 142
                   (ret = NONEV  xs = []  s  #hd  is_list hd []) 
                   ( x q (hd': loc) xs', hd {q} SOMEV (x, #hd')  ret = SOMEV x 
                                          xs = x :: xs'⌝  s  #hd'  is_list hd' xs'))%I
                
Ralf Jung's avatar
Ralf Jung committed
143 144
                
                (pop #s).
Zhen Zhang's avatar
Zhen Zhang committed
145 146

  Lemma pop_atomic_spec (s: loc):
147
    pop_triple s.
Zhen Zhang's avatar
Zhen Zhang committed
148 149 150 151 152
  Proof.
    rewrite /pop_triple /atomic_triple.
    iIntros (P Q) "#Hvs".
    iLöb as "IH". iIntros "!# HP". wp_rec.
    wp_bind (! _)%E.
153
    iMod ("Hvs" with "HP") as ([xs hd]) "[[Hs Hhd] Hvs']".
Robbert Krebbers's avatar
Robbert Krebbers committed
154
    destruct xs as [|y' xs'].
Zhen Zhang's avatar
Zhen Zhang committed
155 156
    - simpl. wp_load. iDestruct "Hvs'" as "[_ Hvs']".
      iDestruct "Hhd" as (q) "[Hhd Hhd']".
157
      iMod ("Hvs'" $! NONEV with "[-Hhd]") as "HQ".
Zhen Zhang's avatar
Zhen Zhang committed
158
      { iLeft. iSplit=>//. iSplit=>//. iFrame. eauto. }
159
      iModIntro. wp_let. wp_load. wp_match.
160
      eauto.
Zhen Zhang's avatar
Zhen Zhang committed
161 162 163
    - simpl. iDestruct "Hhd" as (hd' q) "([[Hhd1 Hhd2] Hhd'] & Hxs')".
      iDestruct (dup_is_list with "[Hxs']") as "[Hxs1 Hxs2]"; first by iFrame.
      wp_load. iDestruct "Hvs'" as "[Hvs' _]".
164
      iMod ("Hvs'" with "[-Hhd1 Hhd2 Hxs1]") as "HP".
Zhen Zhang's avatar
Zhen Zhang committed
165
      { iFrame. iExists hd', (q / 2)%Qp. by iFrame. }
166
      iModIntro. wp_let. wp_load. wp_match. wp_proj.
167 168
      wp_bind (CAS _ _ _).
      iMod ("Hvs" with "HP") as ([xs hd'']) "[[Hs Hhd''] Hvs']".
Robbert Krebbers's avatar
Robbert Krebbers committed
169
      destruct (decide (hd = hd'')) as [->|Hneq].
Zhen Zhang's avatar
Zhen Zhang committed
170
      + wp_cas_suc. iDestruct "Hvs'" as "[_ Hvs']".
171
        iMod ("Hvs'" $! (SOMEV y') with "[-]") as "HQ".
Zhen Zhang's avatar
Zhen Zhang committed
172 173 174
        { iRight. iExists y', (q / 2 / 2)%Qp, hd', xs'.
          destruct xs as [|x' xs''].
          - simpl. iDestruct "Hhd''" as (?) "H".
175
            iExFalso. by iDestruct (@mapsto_agree with "[$Hhd1] [$H]") as %?.
Zhen Zhang's avatar
Zhen Zhang committed
176
          - simpl. iDestruct "Hhd''" as (hd''' ?) "(Hhd'' & Hxs'')".
177
            iDestruct (@mapsto_agree with "[$Hhd1] [$Hhd'']") as %[=].
178
            subst.
Zhen Zhang's avatar
Zhen Zhang committed
179 180 181
            iDestruct (uniq_is_list with "[Hxs1 Hxs'']") as "%"; first by iFrame. subst.
            repeat (iSplitR "Hxs1 Hs"; first done).
            iFrame. }
182
        iModIntro. wp_if. wp_proj. eauto.
Zhen Zhang's avatar
Zhen Zhang committed
183
      + wp_cas_fail. iDestruct "Hvs'" as "[Hvs' _]".
184 185
        iMod ("Hvs'" with "[-]") as "HP"; first by iFrame.
        iModIntro. wp_if. by iApply "IH".
Zhen Zhang's avatar
Zhen Zhang committed
186 187
  Qed.
End proof.