stack.v 16.7 KB
Newer Older
1
From iris.algebra Require Import excl auth list.
2
3
4
From iris.base_logic.lib Require Import invariants.
From iris.program_logic Require Import atomic.
From iris.proofmode Require Import tactics.
5
From iris.heap_lang Require Import proofmode atomic_heap.
6
From iris.bi.lib Require Import fractional.
7
From iris_examples.logatom_stack Require Import spec.
8
9
10
11
12
13
14
Set Default Proof Using "Type".

(** * Implement a concurrent stack with helping on top of an arbitrary atomic
heap. *)

(** The CMRA & functor we need. *)
(* Not bundling heapG, as it may be shared with other users. *)
15
16
17
18
19
20
Class stackG Σ := StackG {
  stack_tokG :> inG Σ (exclR unitC);
  stack_stateG :> inG Σ (authR (optionUR $ exclR (listC valC)));
 }.
Definition stackΣ : gFunctors :=
  #[GFunctor (exclR unitC); GFunctor (authR (optionUR $ exclR (listC valC)))].
21
22
23
24
25

Instance subG_stackΣ {Σ} : subG stackΣ Σ  stackG Σ.
Proof. solve_inG. Qed.

Section stack.
26
  Context `{!heapG Σ, stackG Σ} {aheap: atomic_heap Σ} (N : namespace).
27
  Notation iProp := (iProp Σ).
28

29
30
31
  Let offerN := N .@ "offer".
  Let stackN := N .@ "stack".

32
33
  Import atomic_heap.notation.

34
  (** Code. A stack is a pair of two pointers-to-option-pointers, one for the
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
  head element (if the stack is non-empty) and for the current offer (if it
  exists).  A stack element is a pair of a value an an optional pointer to the
  next element. *)
  Definition new_stack : val :=
    λ: <>,
      let: "head" := ref NONE in
      let: "offer" := ref NONE in
      ("head", "offer").

  Definition push : val :=
    rec: "push" "args" :=
      let: "stack" := Fst "args" in
      let: "val" := Snd "args" in
      let: "head_old" := !(Fst "stack") in
      let: "head_new" := ref ("val", "head_old") in
      if: CAS (Fst "stack") "head_old" (SOME "head_new") then #() else
      (* the CAS failed due to a race, let's try an offer on the side-channel *)
      let: "state" := ref #0 in
      let: "offer" := ("val", "state") in
      (Snd "stack") <- SOME "offer" ;;
      (* wait to see if anyone takes it *)
      (* okay, enough waiting *)
      (Snd "stack") <- NONE ;;
      if: CAS "state" #0 #2 then
        (* We retracted the offer. Just try the entire thing again. *)
        "push" "args"
      else
        (* Someone took the offer. We are done. *)
        #().

  Definition pop : val :=
    rec: "pop" "stack" :=
      match: !(Fst "stack") with
        NONE => NONE (* stack empty *)
      | SOME "head_old" =>
        let: "head_old_data" := !"head_old" in
        (* See if we can change the master head pointer *)
        if: CAS (Fst "stack") (SOME "head_old") (Snd "head_old_data") then
          (* That worked! We are done. Return the value. *)
74
          SOME (Fst "head_old_data")
75
76
77
78
79
80
81
82
83
84
        else
          (* See if there is an offer on the side-channel *)
          match: !(Snd "stack") with
            NONE =>
            (* Nope, no offer. Just try again. *)
            "pop" "stack"
          | SOME "offer" =>
            (* Try to accept the offer. *)
            if: CAS (Snd "offer") #0 #1 then
              (* Success! We are done. Return the offered value. *)
85
              SOME (Fst "offer")
86
87
88
89
90
91
            else
              (* Someone else was faster. Just try again. *)
              "pop" "stack"
          end
      end.

92
93
94
95
96
  (** Invariant and protocol. *)
  Definition stack_content (γs : gname) (l : list val) : iProp :=
    (own γs ( Excl' l))%I.
  Global Instance stack_content_timeless γs l : Timeless (stack_content γs l) := _.

97
98
99
100
101
102
  Lemma stack_content_exclusive γs l1 l2 :
    stack_content γs l1 - stack_content γs l2 - False.
  Proof.
    iIntros "Hl1 Hl2". iDestruct (own_valid_2 with "Hl1 Hl2") as %[].
  Qed.

Ralf Jung's avatar
Ralf Jung committed
103
104
105
106
107
108
109
110
111
  Definition stack_elem_to_val (stack_rep : option loc) : val :=
    match stack_rep with
    | None => NONEV
    | Some l => SOMEV #l
    end.
  Local Instance stack_elem_to_val_inj : Inj (=) (=) stack_elem_to_val.
  Proof. rewrite /Inj /stack_elem_to_val=>??. repeat case_match; congruence. Qed.

  Fixpoint list_inv (l : list val) (rep : option loc) : iProp :=
112
    match l with
Ralf Jung's avatar
Ralf Jung committed
113
    | nil => rep = None
114
115
    | v::l =>  ( : loc) q (rep' : option loc), rep = Some ℓ⌝ 
                               {q} (v, stack_elem_to_val rep')  list_inv l rep'
116
117
    end%I.

Ralf Jung's avatar
Ralf Jung committed
118
119
  Local Hint Extern 0 (environments.envs_entails _ (list_inv (_::_) _)) => simpl.

120
121
  Inductive offer_state := OfferPending | OfferRevoked | OfferAccepted | OfferAcked.

Ralf Jung's avatar
Ralf Jung committed
122
123
  Local Instance: Inhabited offer_state := populate OfferPending.

124
125
126
127
128
129
130
131
132
133
134
135
136
  Definition offer_state_rep (st : offer_state) : Z :=
    match st with
    | OfferPending => 0
    | OfferRevoked => 2
    | OfferAccepted => 1
    | OfferAcked => 1
    end.

  Definition offer_inv (st_loc : loc) (γo : gname) (P Q : iProp) : iProp :=
    ( st : offer_state, st_loc  #(offer_state_rep st) 
      match st with
      | OfferPending => P
      | OfferAccepted => Q
Ralf Jung's avatar
Ralf Jung committed
137
      | _ => own γo (Excl ())
138
139
      end)%I.

Ralf Jung's avatar
Ralf Jung committed
140
141
  Local Hint Extern 0 (environments.envs_entails _ (offer_inv _ _ _ _)) => unfold offer_inv.

142
143
144
145
146
147
  Definition is_offer (γs : gname) (offer_rep : option (val * loc)) :=
    match offer_rep with
    | None => True
    | Some (v, st_loc) =>
       P Q γo, inv offerN (offer_inv st_loc γo P Q) 
                (* The persistent part of the Laterable AU *)
148
                 ( P -  AU <<  l, stack_content γs l >> @ ∖↑N, 
149
150
151
                               << stack_content γs (v::l), COMM Q >>)
    end%I.

152
153
154
  Local Instance is_offer_persistent γs offer_rep : Persistent (is_offer γs offer_rep).
  Proof. destruct offer_rep as [[??]|]; apply _. Qed.

155
156
157
158
159
160
161
162
  Definition offer_to_val (offer_rep : option (val * loc)) : val :=
    match offer_rep with
    | None => NONEV
    | Some (v, l) => SOMEV (v, #l)
    end.

  Definition stack_inv (γs : gname) (head : loc) (offer : loc) : iProp :=
    ( stack_rep offer_rep l, own γs ( Excl' l) 
Ralf Jung's avatar
Ralf Jung committed
163
       head  stack_elem_to_val stack_rep  list_inv l stack_rep 
164
165
       offer  offer_to_val offer_rep  is_offer γs offer_rep)%I.

Ralf Jung's avatar
Ralf Jung committed
166
167
  Local Hint Extern 0 (environments.envs_entails _ (stack_inv _ _ _)) => unfold stack_inv.

168
  Definition is_stack (γs : gname) (s : val) : iProp :=
169
    ( head offer : loc, s = (#head, #offer)%V  inv stackN (stack_inv γs head offer))%I.
170
171
172
173
174
175
176
177
178
179
180
  Global Instance is_stack_persistent γs s : Persistent (is_stack γs s) := _.

  (** Proofs. *)
  Lemma new_stack_spec :
    {{{ True }}} new_stack #() {{{ γs s, RET s; is_stack γs s  stack_content γs [] }}}.
  Proof.
    iIntros (Φ) "_ HΦ". iApply wp_fupd. wp_lam.
    wp_apply alloc_spec; first done. iIntros (head) "Hhead". wp_let.
    wp_apply alloc_spec; first done. iIntros (offer) "Hoffer". wp_let.
    iMod (own_alloc ( Excl' []   Excl' [])) as (γs) "[Hs● Hs◯]".
    { apply auth_valid_discrete_2. split; done. }
181
    iMod (inv_alloc stackN _ (stack_inv γs head offer) with "[-HΦ Hs◯]").
Ralf Jung's avatar
Ralf Jung committed
182
    { iNext. iExists None, None, _. iFrame. done. }
183
184
185
    iApply "HΦ". iFrame "Hs◯". iModIntro. iExists _, _. auto.
  Qed.

186
187
  Lemma push_spec γs s e v :
    IntoVal e v 
Ralf Jung's avatar
Ralf Jung committed
188
    is_stack γs s -
189
    <<<  l : list val, stack_content γs l >>>
190
      push (s, e) @ ∖↑N
Ralf Jung's avatar
Ralf Jung committed
191
192
    <<< stack_content γs (v::l), RET #() >>>.
  Proof.
193
    iIntros (<-) "#Hinv". iApply wp_atomic_intro. iIntros (Φ) "AU".
Ralf Jung's avatar
Ralf Jung committed
194
195
196
197
    iDestruct "Hinv" as (head offer) "[% #Hinv]". subst s.
    iLöb as "IH".
    wp_let. wp_proj. wp_let. wp_proj. wp_let. wp_proj.
    (* Load the old head. *)
198
    wp_apply (load_spec with "[AU]"); first by iAccu.
199
    iAuIntro. iInv stackN as (stack_rep offer_rep l) "(Hs● & >H↦ & Hrem)".
Ralf Jung's avatar
Ralf Jung committed
200
201
    iAaccIntro with "H↦"; first by eauto 10 with iFrame.
    iIntros "?". iSplitL; first by eauto 10 with iFrame.
202
    iIntros "!> AU". clear offer_rep l.
Ralf Jung's avatar
Ralf Jung committed
203
204
205
206
    (* Go on. *)
    wp_let. wp_apply alloc_spec; first done. iIntros (head_new) "Hhead_new".
    wp_let. wp_proj.
    (* CAS to change the head. *)
207
    wp_apply cas_spec; [by destruct stack_rep|iAccu|].
208
209
    iAuIntro. iInv stackN as (stack_rep' offer_rep l) "(>Hs● & >H↦ & Hlist & Hoffer)".
    iAaccIntro with "H↦"; first by eauto 10 with iFrame.
Ralf Jung's avatar
Ralf Jung committed
210
211
212
213
214
215
216
217
    iIntros "H↦".
    destruct (decide (stack_elem_to_val stack_rep' = stack_elem_to_val stack_rep)) as
      [->%stack_elem_to_val_inj|_].
    - (* The CAS succeeded. Update everything accordingly. *)
      iMod "AU" as (l') "[Hl' [_ Hclose]]".
      iDestruct (own_valid_2 with "Hs● Hl'") as
        %[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2.
      iMod (own_update_2 with "Hs● Hl'") as "[Hs● Hl']".
218
      { eapply auth_update, option_local_update, (exclusive_local_update _ (Excl _)). done. }
Ralf Jung's avatar
Ralf Jung committed
219
220
221
      iMod ("Hclose" with "Hl'") as "HΦ". iModIntro.
      change (InjRV #head_new) with (stack_elem_to_val (Some head_new)).
      iSplitR "HΦ"; first by eauto 12 with iFrame.
222
      iIntros "_". wp_if. by iApply "HΦ".
Ralf Jung's avatar
Ralf Jung committed
223
224
225
    - (* The CAS failed, go on making an offer. *)
      iModIntro. iSplitR "AU"; first by eauto 8 with iFrame.
      clear stack_rep stack_rep' offer_rep l head_new.
226
      iIntros "H". wp_if.
Ralf Jung's avatar
Ralf Jung committed
227
228
229
      wp_apply alloc_spec; first done. iIntros (st_loc) "Hoffer_st".
      wp_let. wp_let. wp_proj.
      (* Make the offer *)
230
      wp_apply store_spec; first by iAccu.
231
      iAuIntro. iInv stackN as (stack_rep offer_rep l) "(Hs● & >H↦ & Hlist & >Hoffer↦ & Hoffer)".
Ralf Jung's avatar
Ralf Jung committed
232
233
234
235
236
237
238
239
240
      iAaccIntro with "Hoffer↦"; first by eauto 10 with iFrame.
      iMod (own_alloc (Excl ())) as (γo) "Htok"; first done.
      iDestruct (laterable with "AU") as (AU_later) "[AU #AU_back]".
      iMod (inv_alloc offerN _ (offer_inv st_loc γo AU_later _)  with "[AU Hoffer_st]") as "#Hoinv".
      { iNext. iExists OfferPending. iFrame. }
      iIntros "?". iSplitR "Htok".
      { iClear "Hoffer". iExists _, (Some (v, st_loc)), _. iFrame.
        rewrite /is_offer /=. iExists _, _, _. iFrame "AU_back Hoinv". done. }
      clear stack_rep offer_rep l.
241
      iIntros "!> _". wp_let.
Ralf Jung's avatar
Ralf Jung committed
242
      (* Retract the offer. *)
243
      wp_proj. wp_apply store_spec; first by iAccu.
244
      iAuIntro. iInv stackN as (stack_rep offer_rep l) "(Hs● & >H↦ & Hlist & >Hoffer↦ & Hoffer)".
Ralf Jung's avatar
Ralf Jung committed
245
246
247
      iAaccIntro with "Hoffer↦"; first by eauto 10 with iFrame.
      iIntros "?". iSplitR "Htok".
      { iClear "Hoffer". iExists _, None, _. iFrame. done. }
248
      iIntros "!> _". wp_seq.
Ralf Jung's avatar
Ralf Jung committed
249
250
      clear stack_rep offer_rep l.
      (* See if someone took it. *)
251
      wp_apply cas_spec; [done|iAccu|].
Ralf Jung's avatar
Ralf Jung committed
252
253
254
255
256
257
      iAuIntro. iInv offerN as (offer_st) "[>Hst↦ Hst]".
      iAaccIntro with "Hst↦"; first by eauto 10 with iFrame.
      iIntros "Hst↦". destruct offer_st; simpl.
      + (* Offer was still pending, and we revoked it. Loop around and try again. *)
        iModIntro. iSplitR "Hst".
        { iNext. iExists OfferRevoked. iFrame. }
258
        iIntros "_".
Ralf Jung's avatar
Ralf Jung committed
259
        iDestruct ("AU_back" with "Hst") as ">AU {AU_back Hoinv}". clear AU_later.
260
        wp_if. iApply ("IH" with "AU").
Ralf Jung's avatar
Ralf Jung committed
261
262
263
264
265
266
      + (* Offer revoked by someone else? Impossible! *)
        iDestruct "Hst" as ">Hst".
        iDestruct (own_valid_2 with "Htok Hst") as %[].
      + (* Offer got accepted by someone, awesome! We are done. *)
        iModIntro. iSplitR "Hst".
        { iNext. iExists OfferAcked. iFrame. }
267
        iIntros "_". wp_if. by iApply "Hst".
Ralf Jung's avatar
Ralf Jung committed
268
269
270
271
272
      + (* Offer got acked by someone else? Impossible! *)
        iDestruct "Hst" as ">Hst".
        iDestruct (own_valid_2 with "Htok Hst") as %[].
  Qed.

273
274
275
276
277
278
279
  Lemma pop_spec γs (s : val) :
    is_stack γs s -
    <<<  l, stack_content γs l >>>
      pop s @ ∖↑N
    <<< stack_content γs (tail l),
        RET match l with [] => NONEV | v :: _ => SOMEV v end >>>.
  Proof.
280
    iIntros "#Hinv". iApply wp_atomic_intro. iIntros (Φ) "AU".
281
282
283
284
    iDestruct "Hinv" as (head offer) "[% #Hinv]". subst s.
    iLöb as "IH".
    wp_let. wp_proj.
    (* Load the old head *)
285
    wp_apply load_spec; first by iAccu.
286
287
288
289
290
291
292
293
294
295
296
    iAuIntro. iInv stackN as (stack_rep offer_rep l) "(>Hs● & >H↦ & Hlist & Hrem)".
    iAaccIntro with "H↦"; first by eauto 10 with iFrame.
    iIntros "?". destruct l as [|v l]; simpl.
    - (* The list is empty! We are already done, but it's quite some work to
      prove that. *)
      iDestruct "Hlist" as ">%". subst stack_rep.
      iMod "AU" as (l') "[Hl' [_ Hclose]]".
      iDestruct (own_valid_2 with "Hs● Hl'") as
        %[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2.
      iMod ("Hclose" with "Hl'") as "HΦ".
      iSplitR "HΦ"; first by eauto 10 with iFrame.
297
      iIntros "!> _". wp_match. by iApply "HΦ".
298
299
300
301
    - (* Non-empty list, let's try to pop. *)
      iDestruct "Hlist" as (tail q rep) "[>% [[Htail Htail2] Hlist]]". subst stack_rep.
      iSplitR "AU Htail"; first by eauto 15 with iFrame.
      clear offer_rep l.
302
      iIntros "!> _". wp_match.
303
304
305
      wp_apply (atomic_wp_seq $! (load_spec _) with "Htail").
      iIntros "Htail". wp_let. wp_proj. wp_proj.
      (* CAS to change the head *)
306
      wp_apply cas_spec; [done|iAccu|].
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
      iAuIntro. iInv stackN as (stack_rep offer_rep l) "(>Hs● & >H↦ & Hlist & Hrem)".
      iAaccIntro with "H↦"; first by eauto 10 with iFrame.
      iIntros "H↦". change (InjRV #tail) with (stack_elem_to_val (Some tail)).
      destruct (decide (stack_elem_to_val stack_rep = stack_elem_to_val (Some tail))) as
        [->%stack_elem_to_val_inj|_].
      + (* CAS succeeded! It must still be the same head element in the list,
        and we are done. *)
        iMod "AU" as (l') "[Hl' [_ Hclose]]".
        iDestruct (own_valid_2 with "Hs● Hl'") as
          %[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2.
        destruct l as [|v' l]; simpl.
        { (* Contradiction. *) iDestruct "Hlist" as ">%". done. }
        iDestruct "Hlist" as (tail' q' rep') "[>Heq [>Htail' Hlist]]".
        iDestruct "Heq" as %[= <-].
        iDestruct (mapsto_agree with "Htail Htail'") as %[= <- <-%stack_elem_to_val_inj].
        iMod (own_update_2 with "Hs● Hl'") as "[Hs● Hl']".
        { eapply auth_update, option_local_update, (exclusive_local_update _ (Excl _)). done. }
        iMod ("Hclose" with "Hl'") as "HΦ {Htail Htail'}".
        iSplitR "HΦ"; first by eauto 10 with iFrame.
326
        iIntros "!> _". clear q' q offer_rep l.
327
328
329
        wp_if. wp_proj. by iApply "HΦ".
      + (* CAS failed.  Go on looking for an offer. *)
        iSplitR "AU"; first by eauto 10 with iFrame.
330
        iIntros "!> _". wp_if. clear rep stack_rep offer_rep l q tail v.
331
332
        wp_proj.
        (* Load the offer pointer. *)
333
        wp_apply load_spec; first by iAccu.
334
335
336
        iAuIntro. iInv stackN as (stack_rep offer_rep l) "(>Hs● & >H↦ & Hlist & >Hoff↦ & #Hoff)".
        iAaccIntro with "Hoff↦"; first by eauto 10 with iFrame.
        iIntros "Hoff↦". iSplitR "AU"; first by eauto 10 with iFrame.
337
338
        iIntros "!> _". destruct offer_rep as [[v offer_st_loc]|]; last first.
        { (* No offer, just loop. *) wp_match. iApply ("IH" with "AU"). }
339
340
        clear l stack_rep. wp_match. wp_proj.
        (* CAS to accept the offer. *)
341
        wp_apply cas_spec; [done|iAccu|]. simpl.
342
343
344
345
346
347
348
        iAuIntro. iDestruct "Hoff" as (Poff Qoff γo) "[#Hoinv #AUoff]".
        iInv offerN as (offer_st) "[>Hoff↦ Hoff]".
        iAaccIntro with "Hoff↦"; first by eauto 10 with iFrame.
        iIntros "Hoff↦".
        destruct (decide (#(offer_state_rep offer_st) = #0)) as [Heq|_]; last first.
        { (* CAS failed, we don't do a thing. *)
          iSplitR "AU"; first by eauto 10 with iFrame.
349
          iIntros "!> _". wp_if. iApply ("IH" with "AU"). }
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
        (* CAS succeeded! We accept and complete the offer. *)
        destruct offer_st; try done; []. clear Heq.
        iMod ("AUoff" with "Hoff") as "{AUoff IH} AUoff".
        iInv stackN as (stack_rep offer_rep l) "(>Hs● & >H↦ & Hlist & Hoff)".
        iMod "AUoff" as (l') "[Hl' [_ Hclose]]".
        iDestruct (own_valid_2 with "Hs● Hl'") as
          %[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2.
        iMod (own_update_2 with "Hs● Hl'") as "[Hs● Hl']".
        { eapply auth_update, option_local_update, (exclusive_local_update _ (Excl _)). done. }
        iMod ("Hclose" with "Hl'") as "HQoff".
        iMod "AU" as (l') "[Hl' [_ Hclose]]".
        iDestruct (own_valid_2 with "Hs● Hl'") as
          %[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2.
        iMod (own_update_2 with "Hs● Hl'") as "[Hs● Hl']".
        { eapply auth_update, option_local_update, (exclusive_local_update _ (Excl _)). done. }
        iMod ("Hclose" with "Hl'") as "HΦ".
        iSplitR "Hoff↦ HQoff HΦ"; first by eauto 10 with iFrame. iSplitR "HΦ".
        { iIntros "!> !> !>". iExists OfferAccepted. iFrame. }
368
        iIntros "!> !> _". wp_if. wp_proj. by iApply "HΦ".
369
370
  Qed.

371
End stack.
372

373
374
375
376
377
378
379
Definition elimination_stack `{!heapG Σ, stackG Σ} {aheap: atomic_heap Σ} :
  atomic_stack Σ :=
  {| spec.new_stack_spec := new_stack_spec;
     spec.push_spec := push_spec;
     spec.pop_spec := pop_spec;
     spec.stack_content_exclusive := stack_content_exclusive |}.

Ralf Jung's avatar
Ralf Jung committed
380
Typeclasses Opaque stack_content is_stack.