cinc.v 23.2 KB
Newer Older
1
From iris.algebra Require Import excl auth agree frac list cmra csum.
2 3 4 5
From iris.base_logic.lib Require Export invariants.
From iris.program_logic Require Export atomic.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation.
6
From iris_examples.logatom.conditional_increment Require Import spec.
7 8 9 10 11 12 13 14 15 16 17
Import uPred bi List Decidable.
Set Default Proof Using "Type".

(** Using prophecy variables with helping: implementing conditional counter from
    "Logical Relations for Fine-Grained Concurrency" by Turon et al. (POPL 2013) *)

(** * Implementation of the functions. *)

(*
  new_counter() :=
    let c = ref (injL 0) in
18
    ref c
19 20 21
 *)
Definition new_counter : val :=
  λ: <>,
22
    ref (ref (InjL #0)).
23 24 25

(*
  complete(c, f, x, n, p) :=
26
    Resolve CmpXchg(c, x, ref (injL (if !f then n+1 else n))) p (ref ()) ;; ()
27 28 29
 *)
Definition complete : val :=
  λ: "c" "f" "x" "n" "p",
30 31 32 33
    let: "l_ghost" := ref #() in
    (* Compare with #true to make this a total operation that never
       gets stuck, no matter the value stored in [f]. *)
    let: "new_n" := if: !"f" = #true then "n" + #1 else "n" in
34
    Resolve (CmpXchg "c" "x" (ref (InjL "new_n"))) "p" "l_ghost" ;; #().
35 36

(*
37
  get c :=
38 39 40
    let x = !c in
    match !x with
    | injL n      => n
41
    | injR (f, n, p) => complete c f x n p; get(c, f)
42 43
 *)
Definition get : val :=
44
  rec: "get" "c" :=
45 46 47 48
    let: "x" := !"c" in
    match: !"x" with
      InjL "n"    => "n"
    | InjR "args" =>
49 50 51 52 53
        let: "f" := Fst (Fst "args") in
        let: "n" := Snd (Fst "args") in
        let: "p" := Snd "args" in
        complete "c" "f" "x" "n" "p" ;;
        "get" "c"
54 55 56
    end.

(*
57
  cinc c f :=
58 59 60 61
    let x = !c in
    match !x with
    | injL n =>
        let p := new proph in
62
        let y := ref (injR (n, f, p)) in
63
        if CAS(c, x, y) then complete(c, f, y, n, p)
64 65 66 67
        else cinc c f
    | injR (f', n', p') =>
        complete(c, f', x, n', p');
        cinc c f
68 69
 *)
Definition cinc : val :=
70
  rec: "cinc" "c" "f" :=
71 72 73 74
    let: "x" := !"c" in
    match: !"x" with
      InjL "n" =>
        let: "p" := NewProph in
75
        let: "y" := ref (InjR ("f", "n", "p")) in
76
        if: CAS "c" "x" "y" then complete "c" "f" "y" "n" "p" ;; Skip
77
        else "cinc" "c" "f"
78
    | InjR "args'" =>
79 80 81 82 83
        let: "f'" := Fst (Fst "args'") in
        let: "n'" := Snd (Fst "args'") in
        let: "p'" := Snd "args'" in
        complete "c" "f'" "x" "n'" "p'" ;;
        "cinc" "c" "f"
84 85 86 87
    end.

(** ** Proof setup *)

Robbert Krebbers's avatar
Robbert Krebbers committed
88 89 90
Definition numUR      := authR $ optionUR $ exclR ZO.
Definition tokenUR    := exclR unitO.
Definition one_shotUR := csumR (exclR unitO) (agreeR unitO).
91 92

Class cincG Σ := ConditionalIncrementG {
93 94 95
                     cinc_numG      :> inG Σ numUR;
                     cinc_tokenG    :> inG Σ tokenUR;
                     cinc_one_shotG :> inG Σ one_shotUR;
96 97 98
                   }.

Definition cincΣ : gFunctors :=
99
  #[GFunctor numUR; GFunctor tokenUR; GFunctor one_shotUR].
100 101 102 103 104

Instance subG_cincΣ {Σ} : subG cincΣ Σ  cincG Σ.
Proof. solve_inG. Qed.

Section conditional_counter.
105
  Context {Σ} `{!heapG Σ, !gcG Σ, !cincG Σ}.
106 107 108 109 110
  Context (N : namespace).

  Local Definition stateN   := N .@ "state".
  Local Definition counterN := N .@ "counter".

111
  (** Updating and synchronizing the counter and flag RAs *)
112 113 114 115 116 117 118 119 120 121 122 123 124 125 126

  Lemma sync_counter_values γ_n (n m : Z) :
    own γ_n ( Excl' n) - own γ_n ( Excl' m) - n = m.
  Proof.
    iIntros "H● H◯". iCombine "H●" "H◯" as "H". iDestruct (own_valid with "H") as "H".
      by iDestruct "H" as %[H%Excl_included%leibniz_equiv _]%auth_both_valid.
  Qed.

  Lemma update_counter_value γ_n (n1 n2 m : Z) :
    own γ_n ( Excl' n1) - own γ_n ( Excl' n2) == own γ_n ( Excl' m)  own γ_n ( Excl' m).
  Proof.
    iIntros "H● H◯". iCombine "H●" "H◯" as "H". rewrite -own_op. iApply (own_update with "H").
    by apply auth_update, option_local_update, exclusive_local_update.
  Qed.

127 128
  Definition counter_content (γs : gname) (n : Z) :=
    (own γs ( Excl' n))%I.
129 130 131 132 133

  (** Definition of the invariant *)

  Fixpoint val_to_some_loc (vs : list (val * val)) : option loc :=
    match vs with
134
    | ((_, #true)%V, LitV (LitLoc l)) :: _  => Some l
135 136 137 138 139
    | _                         :: vs => val_to_some_loc vs
    | _                               => None
    end.

  Inductive abstract_state : Set :=
140
  | Quiescent : Z  abstract_state
141
  | Updating : loc  Z  proph_id  abstract_state.
142

143 144
  Definition state_to_val (s : abstract_state) : val :=
    match s with
145
    | Quiescent n => InjLV #n
146
    | Updating f n p => InjRV (#f,#n,#p)
147
    end.
148

149 150 151 152
  Global Instance state_to_val_inj : Inj (=) (=) state_to_val.
  Proof.
    intros [|] [|]; simpl; intros Hv; inversion_clear Hv; done.
  Qed.
153

154
  Definition own_token γ := (own γ (Excl ()))%I.
155

156 157
  Definition pending_state P (n : Z) (proph_winner : option loc) l_ghost_winner (γ_n : gname) :=
    (P  match proph_winner with None => True | Some l => l = l_ghost_winner end  own γ_n ( Excl' n))%I.
158

159 160 161 162
  (* After the prophecy said we are going to win the race, we commit and run the AU,
     switching from [pending] to [accepted]. *)
  Definition accepted_state Q (proph_winner : option loc) (l_ghost_winner : loc) :=
    (l_ghost_winner {1/2} -  match proph_winner with None => True | Some l => l = l_ghost_winner  Q end)%I.
163

164
  (* The same thread then wins the CmpXchg and moves from [accepted] to [done].
165
     Then, the [γ_t] token guards the transition to take out [Q].
166
     Remember that the thread winning the CmpXchg might be just helping.  The token
167 168
     is owned by the thread whose request this is.
     In this state, [l_ghost_winner] serves as a token to make sure that
169
     only the CmpXchg winner can transition to here, and owning half of[l] serves as a
Ralf Jung's avatar
Ralf Jung committed
170 171 172
     "location" token to ensure there is no ABA going on. Notice how [counter_inv]
     owns *more than* half of its [l], which means we know that the [l] there
     and here cannot be the same. *)
173
  Definition done_state Q (l l_ghost_winner : loc) (γ_t : gname) :=
174
    ((Q  own_token γ_t)  l_ghost_winner  -  l {1/2} -)%I.
175 176 177 178 179 180

  (* We always need the [proph] in here so that failing threads coming late can
     always resolve their stuff.
     Moreover, we need a way for anyone who has observed the [done] state to
     prove that we will always remain [done]; that's what the one-shot token [γ_s] is for. *)
  Definition state_inv P Q (p : proph_id) n (c_l l l_ghost_winner : loc) γ_n γ_t γ_s : iProp Σ :=
181
    ( vs, proph p vs 
182 183 184 185
      (own γ_s (Cinl $ Excl ()) 
       (c_l {1/2} #l  ( pending_state P n (val_to_some_loc vs) l_ghost_winner γ_n
         accepted_state Q (val_to_some_loc vs) l_ghost_winner ))
        own γ_s (Cinr $ to_agree ())  done_state Q l l_ghost_winner γ_t))%I.
186

187 188 189
  Definition pau P Q γs f :=
    ( P -  AU <<  (b : bool) (n : Z), counter_content γs n  gc_mapsto f #b >> @ ∖↑N∖↑gcN, 
                 << counter_content γs (if b then n + 1 else n)  gc_mapsto f #b, COMM Q >>)%I.
190

191 192
  Definition counter_inv γ_n c :=
    ( (l : loc) (q : Qp) (s : abstract_state),
Ralf Jung's avatar
Ralf Jung committed
193 194
       (* We own *more than* half of [l], which shows that this cannot
          be the [l] of any [state] protocol in the [done] state. *)
195
       c {1/2} #l  l {1/2 + q} (state_to_val s) 
196
       match s with
197
        | Quiescent n => c {1/2} #l  own γ_n ( Excl' n)
198
        | Updating f n p =>
199 200 201 202 203 204
            P Q l_ghost_winner γ_t γ_s,
             (* There are two pieces of per-[state]-protocol ghost state:
             - [γ_t] is a token owned by whoever created this protocol and used
               to get out the [Q] in the end.
             - [γ_s] reflects whether the protocol is [done] yet or not. *)
             inv stateN (state_inv P Q p n c l l_ghost_winner γ_n γ_t γ_s) 
205
              pau P Q γ_n f  is_gc_loc f
206 207
       end)%I.

208
  Local Hint Extern 0 (environments.envs_entails _ (counter_inv _ _)) => unfold counter_inv.
Ralf Jung's avatar
Ralf Jung committed
209

210 211
  Definition is_counter (γ_n : gname) (ctr : val) :=
    ( (c : loc), ctr = #c  N ## gcN  gc_inv  inv counterN (counter_inv γ_n c))%I.
212 213 214

  Global Instance is_counter_persistent γs ctr : Persistent (is_counter γs ctr) := _.

215
  Global Instance counter_content_timeless γs n : Timeless (counter_content γs n) := _.
216

217
  Global Instance abstract_state_inhabited: Inhabited abstract_state := populate (Quiescent 0).
218

219 220
  Lemma counter_content_exclusive γs c1 c2 :
    counter_content γs c1 - counter_content γs c2 - False.
221
  Proof.
222
    iIntros "Hb1 Hb2". iDestruct (own_valid_2 with "Hb1 Hb2") as %?.
223 224
    done.
  Qed.
225 226 227 228 229 230 231 232 233 234

  (** A few more helper lemmas that will come up later *)

  Lemma mapsto_valid_3 l v1 v2 q :
    l  v1 - l {q} v2 - False.
  Proof.
    iIntros "Hl1 Hl2". iDestruct (mapsto_valid_2 with "Hl1 Hl2") as %Hv.
    apply (iffLR (frac_valid' _)) in Hv. by apply Qp_not_plus_q_ge_1 in Hv.
  Qed.

235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254
  (** Once a [state] protocol is [done] (as reflected by the [γ_s] token here),
      we can at any later point in time extract the [Q]. *)
  Lemma state_done_extract_Q P Q p m c_l l l_ghost γ_n γ_t γ_s :
    inv stateN (state_inv P Q p m c_l l l_ghost γ_n γ_t γ_s) -
    own γ_s (Cinr (to_agree ())) -
    (own_token γ_t ={}=  Q).
  Proof.
    iIntros "#Hinv #Hs !# Ht".
    iInv stateN as (vs) "(Hp & [NotDone | Done])".
    * (* Moved back to NotDone: contradiction. *)
      iDestruct "NotDone" as "(>Hs' & _ & _)".
      iDestruct (own_valid_2 with "Hs Hs'") as %?. contradiction.
    * iDestruct "Done" as "(_ & QT & Hghost)".
      iDestruct "QT" as "[Q | >T]"; last first.
      { iDestruct (own_valid_2 with "Ht T") as %Contra.
          by inversion Contra. }
      iSplitR "Q"; last done. iIntros "!> !>". unfold state_inv.
      iExists _. iFrame "Hp". iRight.
      unfold done_state. iFrame "#∗".
  Qed.
255 256 257

  (** ** Proof of [complete] *)

258
  (** The part of [complete] for the succeeding thread that moves from [accepted] to [done] state *)
259
  Lemma complete_succeeding_thread_pending (γ_n γ_t γ_s : gname) c_l P Q p
260
        (m n : Z) (l l_ghost l_new : loc) Φ :
261
    inv counterN (counter_inv γ_n c_l) -
262
    inv stateN (state_inv P Q p m c_l l l_ghost γ_n γ_t γ_s) -
263
    l_ghost {1 / 2} #() -
264
    ((own_token γ_t ={}=  Q) - Φ #()) -
265 266
    own γ_n ( Excl' n) -
    l_new  InjLV #n -
267
    WP Resolve (CmpXchg #c_l #l #l_new) #p #l_ghost ;; #() {{ v, Φ v }}.
268
  Proof.
269 270
    iIntros "#InvC #InvS Hl_ghost HQ Hn● [Hl_new Hl_new']". wp_bind (Resolve _ _ _)%E.
    iInv counterN as (l' q s) "(>Hc & >[Hl Hl'] & Hrest)".
271 272 273 274 275
    iInv stateN as (vs) "(>Hp & [NotDone | Done])"; last first.
    { (* We cannot be [done] yet, as we own the "ghost location" that serves
         as token for that transition. *)
      iDestruct "Done" as "(_ & _ & Hlghost & _)".
      iDestruct "Hlghost" as (v') ">Hlghost".
276
        by iDestruct (mapsto_valid_2 with "Hl_ghost Hlghost") as %?.
277 278 279 280 281 282 283 284 285 286 287 288
    }
    iDestruct "NotDone" as "(>Hs & >Hc' & [Pending | Accepted])".
    { (* We also cannot be [Pending] any more we have [own γ_n] showing that this
       transition has happened   *)
       iDestruct "Pending" as "[_ >[_ Hn●']]".
       iCombine "Hn●" "Hn●'" as "Contra".
       iDestruct (own_valid with "Contra") as %Contra. by inversion Contra.
    }
    (* So, we are [Accepted]. Now we can show that l = l', because
       while a [state] protocol is not [done], it owns enough of
       the [counter] protocol to ensure that does not move anywhere else. *)
    iDestruct (mapsto_agree with "Hc Hc'") as %[= ->].
289
    (* We perform the CmpXchg. *)
290
    iCombine "Hc Hc'" as "Hc".
291
    wp_apply (wp_resolve with "Hp"); first done; wp_cmpxchg_suc.
292 293 294 295 296 297
    iIntros (vs' ->) "Hp'". simpl.
    (* Update to Done. *)
    iDestruct "Accepted" as "[Hl_ghost_inv [HEq Q]]".
    iMod (own_update with "Hs") as "Hs".
    { apply (cmra_update_exclusive (Cinr (to_agree ()))). done. }
    iDestruct "Hs" as "#Hs'". iModIntro.
298
    iSplitL "Hl_ghost_inv Hl_ghost Q Hp' Hl".
299 300
    (* Update state to Done. *)
    { iNext. iExists _. iFrame "Hp'". iRight. unfold done_state.
301
      iFrame "#∗". iSplitR "Hl"; iExists _; done. }
302 303
    iModIntro. iSplitR "HQ".
    { iNext. iDestruct "Hc" as "[Hc1 Hc2]".
304
      iExists l_new, _, (Quiescent n). iFrame. }
305 306
    iApply wp_fupd. wp_seq. iApply "HQ".
    iApply state_done_extract_Q; done.
307 308 309
  Qed.

  (** The part of [complete] for the failing thread *)
310
  Lemma complete_failing_thread γ_n γ_t γ_s c_l l P Q p m n l_ghost_inv l_ghost l_new Φ :
311
    l_ghost_inv  l_ghost 
312
    inv counterN (counter_inv γ_n c_l) -
313 314
    inv stateN (state_inv P Q p m c_l l l_ghost_inv γ_n γ_t γ_s) -
    ((own_token γ_t ={}=  Q) - Φ #()) -
315
    l_new  InjLV #n -
316
    WP Resolve (CmpXchg #c_l #l #l_new) #p #l_ghost ;; #() {{ v, Φ v }}.
317
  Proof.
318 319
    iIntros (Hnl) "#InvC #InvS HQ Hl_new". wp_bind (Resolve _ _ _)%E.
    iInv counterN as (l' q s) "(>Hc & >[Hl Hl'] & Hrest)".
320 321
    iInv stateN as (vs) "(>Hp & [NotDone | [#Hs Done]])".
    { (* If the [state] protocol is not done yet, we can show that it
322
         is the active protocol still (l = l').  But then the CmpXchg would
323 324 325 326 327
         succeed, and our prophecy would have told us that.
         So here we can prove that the prophecy was wrong. *)
        iDestruct "NotDone" as "(_ & >Hc' & State)".
        iDestruct (mapsto_agree with "Hc Hc'") as %[=->].
        iCombine "Hc Hc'" as "Hc".
328
        wp_apply (wp_resolve with "Hp"); first done; wp_cmpxchg_suc.
329
        iIntros (vs' ->). iDestruct "State" as "[Pending | Accepted]".
330
        + iDestruct "Pending" as "[_ [Hvs _]]". iDestruct "Hvs" as %Hvs. by inversion Hvs.
331 332 333 334 335
        + iDestruct "Accepted" as "[_ [Hvs _]]". iDestruct "Hvs" as %Hvs. by inversion Hvs. }
    (* So, we know our protocol is [Done]. *)
    (* It must be that l' ≠ l because we are in the failing thread. *)
    destruct (decide (l' = l)) as [->|Hn]. {
      (* The [state] protocol is [done] while still being the active protocol
336 337 338 339 340
         of the [counter]?  Impossible, now we will own more than the whole location! *)
      iDestruct "Done" as "(_ & _ & >Hl'')".
      iDestruct "Hl''" as (v') "Hl''".
      iDestruct (mapsto_combine with "Hl Hl''") as "[Hl _]".
      rewrite Qp_half_half. iDestruct (mapsto_valid_3 with "Hl Hl'") as "[]".
341
    }
342 343
    (* The CmpXchg fails. *)
    wp_apply (wp_resolve with "Hp"); first done. wp_cmpxchg_fail.
344 345
    iIntros (vs' ->) "Hp". iModIntro.
    iSplitL "Done Hp". { iNext. iExists _. iFrame "#∗". } iModIntro.
346
    iSplitL "Hc Hrest Hl Hl'". { eauto 10 with iFrame. }
347 348
    wp_seq. iApply "HQ".
    iApply state_done_extract_Q; done.
349 350 351
  Qed.

  (** ** Proof of [complete] *)
352 353 354 355
  (* The postcondition basically says that *if* you were the thread to own
     this request, then you get [Q].  But we also try to complete other
     thread's requests, which is why we cannot ask for the token
     as a precondition. *)
356 357 358 359
  Lemma complete_spec (c f l : loc) (n : Z) (p : proph_id) γ_n γ_t γ_s l_ghost_inv P Q :
    N ## gcN 
    gc_inv -
    inv counterN (counter_inv γ_n c) -
Ralf Jung's avatar
Ralf Jung committed
360
    inv stateN (state_inv P Q p n c l l_ghost_inv γ_n γ_t γ_s) -
361 362
     pau P Q γ_n f -
    is_gc_loc f -
363 364
    {{{ True }}}
       complete #c #f #l #n #p
365
    {{{ RET #();  (own_token γ_t ={}= Q) }}}.
366
  Proof.
367
    iIntros (?) "#GC #InvC #InvS #PAU #isGC".
368
    iModIntro. iIntros (Φ) "_ HQ". wp_lam. wp_pures.
369 370 371 372
    wp_alloc l_ghost as "[Hl_ghost' Hl_ghost'2]". wp_pures.
    wp_bind (! _)%E. simpl.
    (* open outer invariant *)
    iInv counterN as (l' q s) "(>Hc & >Hl' & Hrest)".
373 374 375
    (* two different proofs depending on whether we are succeeding thread *)
    destruct (decide (l_ghost_inv = l_ghost)) as [-> | Hnl].
    - (* we are the succeeding thread *)
376 377
      (* we need to move from [pending] to [accepted]. *)
      iInv stateN as (vs) "(>Hp & [(>Hs & >Hc' & [Pending | Accepted]) | [#Hs Done]])".
378
      + (* Pending: update to accepted *)
379
        iDestruct "Pending" as "[P >[Hvs Hn●]]".
380
        iDestruct ("PAU" with "P") as ">AU".
381
        iMod (gc_access with "GC") as "Hgc"; first solve_ndisj.
382
        (* open and *COMMIT* AU, sync flag and counter *)
383 384 385 386
        iMod "AU" as (b n2) "[[Hn◯ Hf] [_ Hclose]]".
        iDestruct ("Hgc" with "Hf") as "[Hf Hfclose]".
        wp_load.
        iMod ("Hfclose" with "Hf") as "[Hf Hfclose]".
387
        iDestruct (sync_counter_values with "Hn● Hn◯") as %->.
388
        iMod (update_counter_value _ _ _ (if b then n2 + 1 else n2) with "Hn● Hn◯")
389
          as "[Hn● Hn◯]".
390 391
        iMod ("Hclose" with "[Hn◯ Hf]") as "Q"; first by iFrame.
        iModIntro. iMod "Hfclose" as "_".
392
        (* close state inv *)
393
        iIntros "!> !>". iSplitL "Q Hl_ghost' Hp Hvs Hs Hc'".
394 395 396
        { iNext. iExists _. iFrame "Hp". iLeft. iFrame.
          iRight. iSplitL "Hl_ghost'"; first by iExists _.
          destruct (val_to_some_loc vs) eqn:Hvts; iFrame. }
397 398
        (* close outer inv *)
        iModIntro. iSplitR "Hl_ghost'2 HQ Hn●".
Ralf Jung's avatar
Ralf Jung committed
399
        { eauto 12 with iFrame. }
400
        destruct b;
401
        wp_alloc l_new as "Hl_new"; wp_pures;
402
          iApply (complete_succeeding_thread_pending
403
                    with "InvC InvS Hl_ghost'2 HQ Hn● Hl_new").
404 405 406 407 408 409 410 411 412 413
      + (* Accepted: contradiction *)
        iDestruct "Accepted" as "[>Hl_ghost_inv _]".
        iDestruct "Hl_ghost_inv" as (v) "Hlghost".
        iCombine "Hl_ghost'" "Hl_ghost'2" as "Hl_ghost'".
        by iDestruct (mapsto_valid_2 with "Hlghost Hl_ghost'") as %?.
      + (* Done: contradiction *)
        iDestruct "Done" as "[QT >[Hlghost _]]".
        iDestruct "Hlghost" as (v) "Hlghost".
        iCombine "Hl_ghost'" "Hl_ghost'2" as "Hl_ghost'".
        by iDestruct (mapsto_valid_2 with "Hlghost Hl_ghost'") as %?.
414 415 416 417
    - (* we are the failing thread. exploit that [f] is a GC location. *)
      iMod (is_gc_access with "GC isGC") as (b) "[H↦ Hclose]"; first solve_ndisj.
      wp_load.
      iMod ("Hclose" with "H↦") as "_". iModIntro.
418
      (* close invariant *)
419
      iModIntro. iSplitL "Hc Hrest Hl'". { eauto 10 with iFrame. }
420
      (* two equal proofs depending on value of b1 *)
421
      wp_pures.
422
      destruct (bool_decide (b = #true));
423
      wp_alloc Hl_new as "Hl_new"; wp_pures;
424
        iApply (complete_failing_thread
425
                  with "InvC InvS HQ Hl_new"); done.
426 427 428 429
  Qed.

  (** ** Proof of [cinc] *)

430
  Lemma cinc_spec γs v (f: loc) :
431
    is_counter γs v -
432 433 434
    <<<  (b : bool) (n : Z), counter_content γs n  gc_mapsto f #b >>>
        cinc v #f @∖↑N∖↑gcN
    <<< counter_content γs (if b then n + 1 else n)  gc_mapsto f #b, RET #() >>>.
435
  Proof.
436 437 438 439 440
    iIntros "#InvC". iDestruct "InvC" as (c_l [-> ?]) "[#GC #InvC]".
    iIntros (Φ) "AU". iLöb as "IH".
    wp_lam. wp_pures. wp_bind (!_)%E.
    iInv counterN as (l' q s) "(>Hc & >[Hl [Hl' Hl'']] & Hrest)".
    wp_load. destruct s as [n|f' n' p'].
441
    - iDestruct "Hrest" as "(Hc' & Hv)".
442
      iModIntro. iSplitR "AU Hl'".
443
      { iModIntro. iExists _, (q/2)%Qp, (Quiescent n). iFrame. }
444 445
      wp_let. wp_load. wp_match. wp_apply wp_new_proph; first done.
      iIntros (l_ghost p') "Hp'".
446
      wp_let. wp_alloc ly as "Hly".
447
      wp_let. wp_bind (CmpXchg _ _ _)%E.
448
      (* open outer invariant again to CAS c_l *)
449
      iInv counterN as (l'' q2 s) "(>Hc & >Hl & Hrest)".
450 451
      destruct (decide (l' = l'')) as [<- | Hn].
      + (* CAS succeeds *)
452
        iDestruct (mapsto_agree with "Hl' Hl") as %<-%state_to_val_inj.
453
        iDestruct "Hrest" as ">[Hc' Hn●]". iCombine "Hc Hc'" as "Hc".
454
        wp_cmpxchg_suc.
455 456 457 458
        (* Take a "peek" at [AU] and abort immediately to get [gc_is_gc f]. *)
        iMod "AU" as (b' n') "[[CC Hf] [Hclose _]]".
        iDestruct (gc_is_gc with "Hf") as "#Hgc".
        iMod ("Hclose" with "[CC Hf]") as "AU"; first by iFrame.
459
        (* Initialize new [state] protocol .*)
460
        iDestruct (laterable with "AU") as (AU_later) "[AU #AU_back]".
461 462 463
        iMod (own_alloc (Excl ())) as (γ_t) "Token"; first done.
        iMod (own_alloc (Cinl $ Excl ())) as (γ_s) "Hs"; first done.
        iDestruct "Hc" as "[Hc Hc']".
464 465
        set (winner := default ly (val_to_some_loc l_ghost)).
        iMod (inv_alloc stateN _ (state_inv AU_later _ _ _ _ _ winner _ _ _)
466
               with "[AU Hs Hp' Hc' Hn●]") as "#Hinv".
467 468 469 470
        { iNext. iExists _. iFrame "Hp'". iLeft. iFrame. iLeft.
          iFrame. destruct (val_to_some_loc l_ghost); simpl; done. }
        iModIntro. iDestruct "Hly" as "[Hly1 Hly2]". iSplitR "Hl' Token". {
          (* close invariant *)
471
          iNext. iExists _, _, (Updating f n p'). eauto 10 with iFrame.
472
        }
473
        wp_pures. wp_apply complete_spec; [done..|].
474
        iIntros "Ht". iMod ("Ht" with "Token") as "Φ". wp_seq. by wp_lam.
475
      + (* CAS fails: closing invariant and invoking IH *)
476
        wp_cmpxchg_fail.
477
        iModIntro. iSplitR "AU".
478
        { iModIntro. iExists _, _, s. iFrame. }
479
        wp_pures. by iApply "IH".
480
    - (* l' ↦ injR *)
481
      iModIntro.
482
      (* extract state invariant *)
483
      iDestruct "Hrest" as (P Q l_ghost γ_t γ_s) "(#InvS & #P_AU & #Hgc)".
484 485
      iSplitR "Hl' AU".
      (* close invariant *)
486
      { iModIntro. iExists _, _, (Updating f' n' p'). iFrame. eauto 10 with iFrame. }
487
      wp_let. wp_load. wp_match. wp_pures.
Ralf Jung's avatar
Ralf Jung committed
488
      wp_apply complete_spec; [done..|].
489 490 491 492
      iIntros "_". wp_seq. by iApply "IH".
  Qed.

  Lemma new_counter_spec :
493 494
    N ## gcN 
    gc_inv -
495 496
    {{{ True }}}
        new_counter #()
497
    {{{ ctr γs, RET ctr ; is_counter γs ctr  counter_content γs 0 }}}.
498
  Proof.
499
    iIntros (?) "#GC". iIntros (Φ) "!# _ HΦ". wp_lam. wp_apply wp_fupd.
500
    wp_alloc l_n as "Hl_n".
501
    wp_alloc l_c as "Hl_c".
502 503
    iMod (own_alloc ( Excl' 0    Excl' 0)) as (γ_n) "[Hn● Hn◯]".
    { by apply auth_both_valid. }
504 505
    iMod (inv_alloc counterN _ (counter_inv γ_n l_c)
      with "[Hl_c Hl_n Hn●]") as "#InvC".
506
    { iNext. iDestruct "Hl_c" as "[Hl_c1 Hl_c2]".
507
      iDestruct "Hl_n" as "[??]".
508
      iExists l_n, (1/2)%Qp, (Quiescent 0). iFrame. }
509
    iModIntro.
510 511
    iApply ("HΦ" $! #l_c γ_n).
    iSplitR; last by iFrame. iExists _. eauto with iFrame.
512 513
  Qed.

514 515
  Lemma get_spec γs v :
    is_counter γs v -
516 517 518
    <<<  (n : Z), counter_content γs n >>>
        get v @∖↑N∖↑gcN
    <<< counter_content γs n, RET #n >>>.
519
  Proof.
520 521 522
    iIntros "#InvC" (Φ) "AU". iDestruct "InvC" as (c_l [-> ?]) "[GC InvC]".
    iLöb as "IH". wp_lam. wp_bind (! _)%E.
    iInv counterN as (c q s) "(>Hc & >[Hl [Hl' Hl'']] & Hrest)".
523
    wp_load.
524 525
    destruct s as [n|f n p].
    - iMod "AU" as (au_n) "[Hn◯ [_ Hclose]]"; simpl.
526
      iDestruct "Hrest" as "[Hc' Hn●]".
527
      iDestruct (sync_counter_values with "Hn● Hn◯") as %->.
528
      iMod ("Hclose" with "Hn◯") as "HΦ".
529
      iModIntro. iSplitR "HΦ Hl'". {
530
        iNext. iExists c, (q/2)%Qp, (Quiescent au_n). iFrame.
531 532
      }
      wp_let. wp_load. wp_match. iApply "HΦ".
533
    - iDestruct "Hrest" as (P Q l_ghost γ_t γ_s) "(#InvS & #PAU & #Hgc)".
534
      iModIntro. iSplitR "AU Hl'". {
535
        iNext. iExists c, (q/2)%Qp, (Updating _ _ p). eauto 10 with iFrame.
536
      }
537
      wp_let. wp_load. wp_pures. wp_bind (complete _ _ _ _ _)%E.
Ralf Jung's avatar
Ralf Jung committed
538
      wp_apply complete_spec; [done..|].
539 540 541 542
      iIntros "Ht". wp_seq. iApply "IH". iApply "AU".
  Qed.

End conditional_counter.
543

544
Definition atomic_cinc `{!heapG Σ, !cincG Σ, !gcG Σ} :
545 546 547 548 549 550 551
  spec.atomic_cinc Σ :=
  {| spec.new_counter_spec := new_counter_spec;
     spec.cinc_spec := cinc_spec;
     spec.get_spec := get_spec;
     spec.counter_content_exclusive := counter_content_exclusive |}.

Typeclasses Opaque counter_content is_counter.