treiber.v 7.53 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.
Ralf Jung's avatar
Ralf Jung committed
4
5
From iris.algebra Require Import frac auth gmap dec_agree csum.
From iris.base_logic Require Import big_op.
Zhen Zhang's avatar
Zhen Zhang committed
6
From iris_atomic Require Import atomic misc.
Zhen Zhang's avatar
Zhen Zhang committed
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
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109

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.

Global Opaque new_stack push pop iter.

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

  Fixpoint is_list (hd: loc) (xs: list val) : iProp Σ :=
    match xs with
    | [] => ( q, hd { q } NONEV)%I
    | x :: xs => ( (hd': loc) q, hd { q } SOMEV (x, #hd')  is_list hd' xs)%I
    end.

  Lemma dup_is_list :  xs hd,
    heap_ctx  is_list hd xs  is_list hd xs  is_list hd xs.
  Proof.
    induction xs as [|y xs' IHxs'].
    - iIntros (hd) "(#? & Hs)".
      simpl. iDestruct "Hs" as (q) "[Hhd Hhd']". iSplitL "Hhd"; eauto.
    - iIntros (hd) "(#? & Hs)". simpl.
      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:
     xs ys hd, heap_ctx  is_list hd xs  is_list hd ys  xs = ys.
  Proof.
    induction xs as [|x xs' IHxs'].
    - induction ys as [|y ys' IHys'].
      + auto.
      + iIntros (hd) "(#? & Hxs & Hys)".
        simpl. iDestruct "Hys" as (hd' ?) "(Hhd & Hys')".
        iExFalso. iDestruct "Hxs" as (?) "Hhd'".
        iDestruct (heap_mapsto_op_1 with "[Hhd Hhd']") as "[% _]".
        { iSplitL "Hhd"; done. }
        done.
    - induction ys as [|y ys' IHys'].
      + iIntros (hd) "(#? & Hxs & Hys)".
        simpl.
        iExFalso. iDestruct "Hxs" as (? ?) "(Hhd & _)".
        iDestruct "Hys" as (?) "Hhd'".
        iDestruct (heap_mapsto_op_1 with "[Hhd Hhd']") as "[% _]".
        { iSplitL "Hhd"; done. }
        done.
      + iIntros (hd) "(#? & Hxs & Hys)".
        simpl. iDestruct "Hxs" as (? ?) "(Hhd & Hxs')".
        iDestruct "Hys" as (? ?) "(Hhd' & Hys')".
        iDestruct (heap_mapsto_op_1 with "[Hhd Hhd']") as "[% _]".
        { iSplitL "Hhd"; done. }
        inversion H3. (* FIXME: name *)
        subst. iDestruct (IHxs' with "[Hxs' Hys']") as "%"; first by iFrame.
        by subst.
  Qed.

  Definition is_stack (s: loc) xs: iProp Σ := ( hd: loc, s  #hd  is_list hd xs)%I.

  Global Instance is_list_timeless xs hd: TimelessP (is_list hd xs).
  Proof. generalize hd. induction xs; apply _. Qed.

  Global Instance is_stack_timeless xs hd: TimelessP (is_stack hd xs).
  Proof. generalize hd. induction xs; apply _. Qed.

  Lemma new_stack_spec:
     (Φ: val  iProp Σ),
      heapN  N 
      heap_ctx  ( s, is_stack s [] - Φ #s)  WP new_stack #() {{ Φ }}.
  Proof.
    iIntros (Φ HN) "[#Hh HΦ]". wp_seq.
    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) :=
110
111
  atomic_triple _ (fun xs_hd: list val * loc =>
                       let '(xs, hd) := xs_hd in s  #hd  is_list hd xs)%I
Zhen Zhang's avatar
Zhen Zhang committed
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
                  (fun xs_hd ret =>
                     let '(xs, hd) := xs_hd in 
                      hd': loc,
                       ret = #()  s  #hd'  hd'  SOMEV (x, #hd)  is_list hd xs)%I
                  (nclose heapN)
                  
                  (push #s x).
  
  Lemma push_atomic_spec (s: loc) (x: val) :
    heapN  N  heap_ctx  push_triple s x.
  Proof.
    iIntros (HN) "#?". rewrite /push_triple /atomic_triple.
    iIntros (P Q) "#Hvs".
    iLöb as "IH". iIntros "!# HP". wp_rec.
    wp_let. wp_bind (! _)%E.
Ralf Jung's avatar
Ralf Jung committed
127
128
129
    iMod ("Hvs" with "HP") as ([xs hd]) "[[Hs Hhd] [Hvs' _]]".
    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
130
    wp_bind (CAS _ _ _)%E.
Ralf Jung's avatar
Ralf Jung committed
131
    iMod ("Hvs" with "HP") as ([xs' hd']) "[[Hs Hhd'] Hvs']".
Zhen Zhang's avatar
Zhen Zhang committed
132
133
    destruct (decide (hd = hd')) as [->|Hneq].
    * wp_cas_suc. iDestruct "Hvs'" as "[_ Hvs']".
Ralf Jung's avatar
Ralf Jung committed
134
      iMod ("Hvs'" $! #() with "[-]") as "HQ".
Zhen Zhang's avatar
Zhen Zhang committed
135
      { iExists l. iSplitR; first done. by iFrame. }
136
      iModIntro. wp_if. eauto.
Zhen Zhang's avatar
Zhen Zhang committed
137
138
    * wp_cas_fail.
      iDestruct "Hvs'" as "[Hvs' _]".
Ralf Jung's avatar
Ralf Jung committed
139
140
      iMod ("Hvs'" with "[-]") as "HP"; first by iFrame.
      iModIntro. wp_if. by iApply "IH".
Zhen Zhang's avatar
Zhen Zhang committed
141
142
143
  Qed.

  Definition pop_triple (s: loc) :=
144
  atomic_triple _ (fun xs_hd: list val * loc =>
Zhen Zhang's avatar
Zhen Zhang committed
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
                     let '(xs, hd) := xs_hd in s  #hd  is_list hd xs)%I
                  (fun xs_hd ret =>
                     let '(xs, hd) := xs_hd in
                     (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
                  (nclose heapN)
                  
                  (pop #s).

  Lemma pop_atomic_spec (s: loc):
    heapN  N  heap_ctx  pop_triple s.
  Proof.
    iIntros (HN) "#?".
    rewrite /pop_triple /atomic_triple.
    iIntros (P Q) "#Hvs".
    iLöb as "IH". iIntros "!# HP". wp_rec.
    wp_bind (! _)%E.
Ralf Jung's avatar
Ralf Jung committed
163
    iMod ("Hvs" with "HP") as ([xs hd]) "[[Hs Hhd] Hvs']".
Zhen Zhang's avatar
Zhen Zhang committed
164
165
166
    destruct xs as [|y' xs'].
    - simpl. wp_load. iDestruct "Hvs'" as "[_ Hvs']".
      iDestruct "Hhd" as (q) "[Hhd Hhd']".
Ralf Jung's avatar
Ralf Jung committed
167
      iMod ("Hvs'" $! NONEV with "[-Hhd]") as "HQ".
Zhen Zhang's avatar
Zhen Zhang committed
168
      { iLeft. iSplit=>//. iSplit=>//. iFrame. eauto. }
Ralf Jung's avatar
Ralf Jung committed
169
      iModIntro. wp_let. wp_load. wp_match.
170
      eauto.
Zhen Zhang's avatar
Zhen Zhang committed
171
172
173
    - 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' _]".
Ralf Jung's avatar
Ralf Jung committed
174
      iMod ("Hvs'" with "[-Hhd1 Hhd2 Hxs1]") as "HP".
Zhen Zhang's avatar
Zhen Zhang committed
175
      { iFrame. iExists hd', (q / 2)%Qp. by iFrame. }
Ralf Jung's avatar
Ralf Jung committed
176
177
      iModIntro. wp_let. wp_load. wp_match. wp_proj.
      wp_bind (CAS _ _ _). iMod ("Hvs" with "HP") as ([xs hd'']) "[[Hs Hhd''] Hvs']".
Zhen Zhang's avatar
Zhen Zhang committed
178
179
      destruct (decide (hd = hd'')) as [->|Hneq].
      + wp_cas_suc. iDestruct "Hvs'" as "[_ Hvs']".
Ralf Jung's avatar
Ralf Jung committed
180
        iMod ("Hvs'" $! (SOMEV y') with "[-]") as "HQ".
Zhen Zhang's avatar
Zhen Zhang committed
181
182
183
184
185
186
187
188
189
190
191
192
193
        { iRight. iExists y', (q / 2 / 2)%Qp, hd', xs'.
          destruct xs as [|x' xs''].
          - simpl. iDestruct "Hhd''" as (?) "H".
            iExFalso. iDestruct (heap_mapsto_op_1 with "[Hhd1 H]") as "[% _]".
            { iSplitL "Hhd1"; done. }
            done.
          - simpl. iDestruct "Hhd''" as (hd''' ?) "(Hhd'' & Hxs'')".
            iDestruct (heap_mapsto_op_1 with "[Hhd1 Hhd'']") as "[% _]".
            { iSplitL "Hhd1"; done. }
            inversion H0. (* FIXME: bad naming *) subst.
            iDestruct (uniq_is_list with "[Hxs1 Hxs'']") as "%"; first by iFrame. subst.
            repeat (iSplitR "Hxs1 Hs"; first done).
            iFrame. }
Ralf Jung's avatar
Ralf Jung committed
194
        iModIntro. wp_if. wp_proj. eauto.
Zhen Zhang's avatar
Zhen Zhang committed
195
      + wp_cas_fail. iDestruct "Hvs'" as "[Hvs' _]".
Ralf Jung's avatar
Ralf Jung committed
196
197
        iMod ("Hvs'" with "[-]") as "HP"; first by iFrame.
        iModIntro. wp_if. by iApply "IH".
Zhen Zhang's avatar
Zhen Zhang committed
198
199
200
201
  Qed.

End proof.