stack.v 16.2 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.elimination_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
Class stackG Σ := StackG {
Robbert Krebbers's avatar
Robbert Krebbers committed
16 17
  stack_tokG :> inG Σ (exclR unitO);
  stack_stateG :> inG Σ (authR (optionUR $ exclR (listO valO)));
18 19
 }.
Definition stackΣ : gFunctors :=
Robbert Krebbers's avatar
Robbert Krebbers committed
20
  #[GFunctor (exclR unitO); GFunctor (authR (optionUR $ exclR (listO valO)))].
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
  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 :=
45
    rec: "push" "stack" "val" :=
46 47 48 49 50 51 52 53 54 55 56 57
      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. *)
58
        "push" "stack" "val"
59 60 61 62 63 64 65 66 67 68 69 70 71
      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. *)
72
          SOME (Fst "head_old_data")
73 74 75 76 77 78 79 80 81 82
        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. *)
83
              SOME (Fst "offer")
84 85 86 87 88 89
            else
              (* Someone else was faster. Just try again. *)
              "pop" "stack"
          end
      end.

90 91 92 93 94
  (** 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) := _.

95 96 97 98 99 100
  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
101 102 103 104 105 106 107 108 109
  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 :=
110
    match l with
Ralf Jung's avatar
Ralf Jung committed
111
    | nil => rep = None
112 113
    | v::l =>  ( : loc) q (rep' : option loc), rep = Some ℓ⌝ 
                               {q} (v, stack_elem_to_val rep')  list_inv l rep'
114 115
    end%I.

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

118 119
  Inductive offer_state := OfferPending | OfferRevoked | OfferAccepted | OfferAcked.

Ralf Jung's avatar
Ralf Jung committed
120 121
  Local Instance: Inhabited offer_state := populate OfferPending.

122 123 124 125 126 127 128 129 130 131 132 133 134
  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
135
      | _ => own γo (Excl ())
136 137
      end)%I.

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

140 141 142 143 144 145
  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 *)
146
                 ( P -  AU <<  l, stack_content γs l >> @ ∖↑N, 
147 148 149
                               << stack_content γs (v::l), COMM Q >>)
    end%I.

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

153 154 155 156 157 158 159 160
  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
161
       head  stack_elem_to_val stack_rep  list_inv l stack_rep 
162 163
       offer  offer_to_val offer_rep  is_offer γs offer_rep)%I.

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

166
  Definition is_stack (γs : gname) (s : val) : iProp :=
167
    ( head offer : loc, s = (#head, #offer)%V  inv stackN (stack_inv γs head offer))%I.
168 169 170 171 172 173 174 175 176 177
  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◯]".
Hai Dang's avatar
Hai Dang committed
178
    { apply auth_both_valid. split; done. }
179
    iMod (inv_alloc stackN _ (stack_inv γs head offer) with "[-HΦ Hs◯]").
Ralf Jung's avatar
Ralf Jung committed
180
    { iNext. iExists None, None, _. iFrame. done. }
181
    wp_pures. iApply "HΦ". iFrame "Hs◯". iModIntro. iExists _, _. auto.
182 183
  Qed.

184
  Lemma push_spec γs s (v : val) :
Ralf Jung's avatar
Ralf Jung committed
185
    is_stack γs s -
186
    <<<  l : list val, stack_content γs l >>>
187
      push s v @ ∖↑N
Ralf Jung's avatar
Ralf Jung committed
188 189
    <<< stack_content γs (v::l), RET #() >>>.
  Proof.
Ralf Jung's avatar
Ralf Jung committed
190
    iIntros "#Hinv". iIntros (Φ) "AU".
Ralf Jung's avatar
Ralf Jung committed
191 192
    iDestruct "Hinv" as (head offer) "[% #Hinv]". subst s.
    iLöb as "IH".
193
    wp_lam.
Ralf Jung's avatar
Ralf Jung committed
194
    (* Load the old head. *)
Ralf Jung's avatar
Ralf Jung committed
195 196
    awp_apply load_spec without "AU".
    iInv stackN as (stack_rep offer_rep l) "(Hs● & >H↦ & Hrem)".
Ralf Jung's avatar
Ralf Jung committed
197 198
    iAaccIntro with "H↦"; first by eauto 10 with iFrame.
    iIntros "?". iSplitL; first by eauto 10 with iFrame.
199
    iIntros "!> AU". clear offer_rep l.
Ralf Jung's avatar
Ralf Jung committed
200 201 202
    (* Go on. *)
    wp_let. wp_apply alloc_spec; first done. iIntros (head_new) "Hhead_new".
    (* CAS to change the head. *)
Ralf Jung's avatar
Ralf Jung committed
203 204
    awp_apply cas_spec; [by destruct stack_rep|].
    iInv stackN as (stack_rep' offer_rep l) "(>Hs● & >H↦ & Hlist & Hoffer)".
205
    iAaccIntro with "H↦"; first by eauto 10 with iFrame.
Ralf Jung's avatar
Ralf Jung committed
206 207 208 209 210 211
    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
Hai Dang's avatar
Hai Dang committed
212
        %[->%Excl_included%leibniz_equiv _]%auth_both_valid.
Ralf Jung's avatar
Ralf Jung committed
213
      iMod (own_update_2 with "Hs● Hl'") as "[Hs● Hl']".
214
      { eapply auth_update, option_local_update, (exclusive_local_update _ (Excl _)). done. }
Ralf Jung's avatar
Ralf Jung committed
215 216 217
      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.
Ralf Jung's avatar
Ralf Jung committed
218
      wp_if. by iApply "HΦ".
Ralf Jung's avatar
Ralf Jung committed
219 220 221
    - (* 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.
Ralf Jung's avatar
Ralf Jung committed
222
      wp_if.
Ralf Jung's avatar
Ralf Jung committed
223 224
      wp_apply alloc_spec; first done. iIntros (st_loc) "Hoffer_st".
      (* Make the offer *)
Ralf Jung's avatar
Ralf Jung committed
225 226
      awp_apply store_spec.
      iInv stackN as (stack_rep offer_rep l) "(Hs● & >H↦ & Hlist & >Hoffer↦ & Hoffer)".
Ralf Jung's avatar
Ralf Jung committed
227 228 229 230 231 232 233 234
      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. }
Ralf Jung's avatar
Ralf Jung committed
235
      clear stack_rep offer_rep l. iIntros "!>".
Ralf Jung's avatar
Ralf Jung committed
236
      (* Retract the offer. *)
Ralf Jung's avatar
Ralf Jung committed
237 238
      awp_apply store_spec.
      iInv stackN as (stack_rep offer_rep l) "(Hs● & >H↦ & Hlist & >Hoffer↦ & Hoffer)".
Ralf Jung's avatar
Ralf Jung committed
239 240 241
      iAaccIntro with "Hoffer↦"; first by eauto 10 with iFrame.
      iIntros "?". iSplitR "Htok".
      { iClear "Hoffer". iExists _, None, _. iFrame. done. }
Ralf Jung's avatar
Ralf Jung committed
242
      iIntros "!>". wp_seq.
Ralf Jung's avatar
Ralf Jung committed
243 244
      clear stack_rep offer_rep l.
      (* See if someone took it. *)
Ralf Jung's avatar
Ralf Jung committed
245 246
      awp_apply cas_spec; [done|].
      iInv offerN as (offer_st) "[>Hst↦ Hst]".
Ralf Jung's avatar
Ralf Jung committed
247 248 249 250 251 252
      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. }
        iDestruct ("AU_back" with "Hst") as ">AU {AU_back Hoinv}". clear AU_later.
253
        wp_if. iApply ("IH" with "AU").
Ralf Jung's avatar
Ralf Jung committed
254 255 256 257 258 259
      + (* 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. }
Ralf Jung's avatar
Ralf Jung committed
260
        wp_if. by iApply "Hst".
Ralf Jung's avatar
Ralf Jung committed
261 262 263 264 265
      + (* Offer got acked by someone else? Impossible! *)
        iDestruct "Hst" as ">Hst".
        iDestruct (own_valid_2 with "Htok Hst") as %[].
  Qed.

266 267 268 269 270 271 272
  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.
Ralf Jung's avatar
Ralf Jung committed
273
    iIntros "#Hinv". iIntros (Φ) "AU".
274
    iDestruct "Hinv" as (head offer) "[% #Hinv]". subst s.
275
    iLöb as "IH". wp_lam. wp_pures.
276
    (* Load the old head *)
Ralf Jung's avatar
Ralf Jung committed
277 278
    awp_apply load_spec.
    iInv stackN as (stack_rep offer_rep l) "(>Hs● & >H↦ & Hlist & Hrem)".
279 280 281 282 283 284 285
    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
Hai Dang's avatar
Hai Dang committed
286
        %[->%Excl_included%leibniz_equiv _]%auth_both_valid.
287 288
      iMod ("Hclose" with "Hl'") as "HΦ".
      iSplitR "HΦ"; first by eauto 10 with iFrame.
Ralf Jung's avatar
Ralf Jung committed
289
      iIntros "!>". wp_pures. by iApply "HΦ".
290 291 292 293
    - (* 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.
Ralf Jung's avatar
Ralf Jung committed
294
      iIntros "!>". wp_match.
295
      wp_apply (atomic_wp_seq $! (load_spec _) with "Htail").
296
      iIntros "Htail". wp_pures.
297
      (* CAS to change the head *)
Ralf Jung's avatar
Ralf Jung committed
298 299
      awp_apply cas_spec; [done|].
      iInv stackN as (stack_rep offer_rep l) "(>Hs● & >H↦ & Hlist & Hrem)".
300 301 302 303 304 305 306 307
      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
Hai Dang's avatar
Hai Dang committed
308
          %[->%Excl_included%leibniz_equiv _]%auth_both_valid.
309 310 311 312 313 314 315 316 317
        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.
Ralf Jung's avatar
Ralf Jung committed
318
        iIntros "!>". clear q' q offer_rep l.
319
        wp_pures. by iApply "HΦ".
320 321
      + (* CAS failed.  Go on looking for an offer. *)
        iSplitR "AU"; first by eauto 10 with iFrame.
Ralf Jung's avatar
Ralf Jung committed
322
        iIntros "!>". wp_if. clear rep stack_rep offer_rep l q tail v.
323 324
        wp_proj.
        (* Load the offer pointer. *)
Ralf Jung's avatar
Ralf Jung committed
325 326
        awp_apply load_spec.
        iInv stackN as (stack_rep offer_rep l) "(>Hs● & >H↦ & Hlist & >Hoff↦ & #Hoff)".
327 328
        iAaccIntro with "Hoff↦"; first by eauto 10 with iFrame.
        iIntros "Hoff↦". iSplitR "AU"; first by eauto 10 with iFrame.
Ralf Jung's avatar
Ralf Jung committed
329
        iIntros "!>". destruct offer_rep as [[v offer_st_loc]|]; last first.
330
        { (* No offer, just loop. *) wp_match. iApply ("IH" with "AU"). }
331 332
        clear l stack_rep. wp_match. wp_proj.
        (* CAS to accept the offer. *)
Ralf Jung's avatar
Ralf Jung committed
333 334
        awp_apply cas_spec; [done|]. simpl.
        iDestruct "Hoff" as (Poff Qoff γo) "[#Hoinv #AUoff]".
335 336 337 338 339 340
        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.
Ralf Jung's avatar
Ralf Jung committed
341
          iIntros "!>". wp_if. iApply ("IH" with "AU"). }
342 343 344 345 346 347
        (* 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
Hai Dang's avatar
Hai Dang committed
348
          %[->%Excl_included%leibniz_equiv _]%auth_both_valid.
349 350 351 352 353
        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
Hai Dang's avatar
Hai Dang committed
354
          %[->%Excl_included%leibniz_equiv _]%auth_both_valid.
355 356 357 358 359
        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. }
Ralf Jung's avatar
Ralf Jung committed
360
        iIntros "!> !>". wp_pures. by iApply "HΦ".
361 362
  Qed.

363
End stack.
364

365 366 367 368 369 370 371
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
372
Typeclasses Opaque stack_content is_stack.