stack.v 16.9 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 189
    is_stack γs s -
    <<<  l, 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
    intros <-. iIntros "#Hinv" (Q Φ) "HQ AU".
Ralf Jung's avatar
Ralf Jung committed
194 195 196 197 198
    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. *)
    wp_apply (load_spec with "[HQ 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 202 203 204 205 206 207
    iAaccIntro with "H↦"; first by eauto 10 with iFrame.
    iIntros "?". iSplitL; first by eauto 10 with iFrame.
    iIntros "!> [HQ AU]". clear offer_rep l.
    (* Go on. *)
    wp_let. wp_apply alloc_spec; first done. iIntros (head_new) "Hhead_new".
    wp_let. wp_proj.
    (* CAS to change the head. *)
    wp_apply (cas_spec with "[HQ]"); [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 222 223 224 225 226 227 228 229 230
      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.
      iIntros "Q". wp_if. by iApply "HΦ".
    - (* 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.
      iIntros "HQ". wp_if.
      wp_apply alloc_spec; first done. iIntros (st_loc) "Hoffer_st".
      wp_let. wp_let. wp_proj.
      (* Make the offer *)
      wp_apply (store_spec with "[HQ]"); 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 241 242 243
      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.
      iIntros "!> HQ". wp_let.
      (* Retract the offer. *)
      wp_proj. wp_apply (store_spec with "[HQ]"); 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 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272
      iAaccIntro with "Hoffer↦"; first by eauto 10 with iFrame.
      iIntros "?". iSplitR "Htok".
      { iClear "Hoffer". iExists _, None, _. iFrame. done. }
      iIntros "!> HQ". wp_seq.
      clear stack_rep offer_rep l.
      (* See if someone took it. *)
      wp_apply (cas_spec with "[HQ]"); [done|iAccu|].
      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. }
        iIntros "HQ".
        iDestruct ("AU_back" with "Hst") as ">AU {AU_back Hoinv}". clear AU_later.
        wp_if. iApply ("IH" with "HQ AU").
      + (* 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. }
        iIntros "HQ". wp_if. by iApply "Hst".
      + (* 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 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371
  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.
    iIntros "#Hinv" (Q Φ) "HQ AU".
    iDestruct "Hinv" as (head offer) "[% #Hinv]". subst s.
    iLöb as "IH".
    wp_let. wp_proj.
    (* Load the old head *)
    wp_apply (load_spec with "[HQ]"); first by iAccu.
    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.
      iIntros "!> HQ". wp_match. by iApply "HΦ".
    - (* 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.
      iIntros "!> HQ". wp_match.
      wp_apply (atomic_wp_seq $! (load_spec _) with "Htail").
      iIntros "Htail". wp_let. wp_proj. wp_proj.
      (* CAS to change the head *)
      wp_apply (cas_spec with "[HQ]"); [done|iAccu|].
      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.
        iIntros "!> HQ". clear q' q offer_rep l.
        wp_if. wp_proj. by iApply "HΦ".
      + (* CAS failed.  Go on looking for an offer. *)
        iSplitR "AU"; first by eauto 10 with iFrame.
        iIntros "!> HQ". wp_if. clear rep stack_rep offer_rep l q tail v.
        wp_proj.
        (* Load the offer pointer. *)
        (* FIXME: [wp_apply (load_spec with "[HQ AU]"); first by iAccu.] here triggers an anomaly. *)
        wp_apply (load_spec with "[HQ]"); first by iAccu.
        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.
        iIntros "!> HQ". destruct offer_rep as [[v offer_st_loc]|]; last first.
        { (* No offer, just loop. *) wp_match. iApply ("IH" with "HQ AU"). }
        clear l stack_rep. wp_match. wp_proj.
        (* CAS to accept the offer. *)
        wp_apply (cas_spec with "[HQ]"); [done|iAccu|]. simpl.
        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.
          iIntros "!> HQ". wp_if. iApply ("IH" with "HQ AU"). }
        (* 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. }
        iIntros "!> !> HQ". wp_if. wp_proj. by iApply "HΦ".
  Qed.

372
End stack.
373

374 375 376 377 378 379 380
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 |}.

381
Global Typeclasses Opaque stack_content is_stack.