cinc.v 24.7 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 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
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
    let f = ref false in
    ref (f, c)
 *)
Definition new_counter : val :=
  λ: <>,
    let: "c" := ref (ref (InjL #0)) in
    let: "f" := ref #true in
    ("f", "c").

(*
  set_flag(ctr, b) :=
    ctr.1 <- b
 *)
Definition set_flag : val :=
  λ: "ctr" "b",
    Fst "ctr" <- "b".

(*
  complete(c, f, x, n, p) :=
    Resolve CAS(c, x, ref (injL (if !f then n+1 else n))) p (ref ()) ;; ()
 *)
Definition complete : val :=
  λ: "c" "f" "x" "n" "p",
    Resolve (CAS "c" "x" (ref (InjL (if: !"f" then "n" + #1 else "n")))) "p" (ref #()) ;; #().

(*
  get(c, f) :=
    let x = !c in
    match !x with
    | injL n      => n
    | injR (n, p) => complete c f x n p; get(c, f)
 *)
Definition get : val :=
  rec: "get" "ctr" :=
    let: "f" := Fst "ctr" in
    let: "c" := Snd "ctr" in
    let: "x" := !"c" in
    match: !"x" with
      InjL "n"    => "n"
    | InjR "args" =>
        complete "c" "f" "x" (Fst "args") (Snd "args") ;;
        "get" "ctr"
    end.

(*
  cinc(c, f) :=
    let x = !c in
    match !x with
    | injL n =>
        let p := new proph in
        let y := ref (injR (n, p)) in
        if CAS(c, x, y) then complete(c, f, y, n, p)
        else cinc(c, f)
    | injR (n, p) =>
        complete(c, f, x, n, p);
        cinc(c, f)
 *)
Definition cinc : val :=
  rec: "cinc" "ctr" :=
    let: "f" := Fst "ctr" in
    let: "c" := Snd "ctr" in
    let: "x" := !"c" in
    match: !"x" with
      InjL "n" =>
        let: "p" := NewProph in
        let: "y" := ref (InjR ("n", "p")) in
        if: CAS "c" "x" "y" then complete "c" "f" "y" "n" "p" ;; Skip
        else "cinc" "ctr"
    | InjR "args'" =>
        complete "c" "f" "x" (Fst "args'") (Snd "args'") ;;
        "cinc" "ctr"
    end.

(** ** Proof setup *)

93 94 95 96
Definition flagUR     := authR $ optionUR $ exclR boolC.
Definition numUR      := authR $ optionUR $ exclR ZC.
Definition tokenUR    := exclR unitC.
Definition one_shotUR := csumR (exclR unitC) (agreeR unitC).
97 98

Class cincG Σ := ConditionalIncrementG {
99 100 101 102
                     cinc_flagG     :> inG Σ flagUR;
                     cinc_numG      :> inG Σ numUR;
                     cinc_tokenG    :> inG Σ tokenUR;
                     cinc_one_shotG :> inG Σ one_shotUR;
103 104 105
                   }.

Definition cincΣ : gFunctors :=
106
  #[GFunctor flagUR; GFunctor numUR; GFunctor tokenUR; GFunctor one_shotUR].
107 108 109 110 111 112 113 114 115 116 117

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

Section conditional_counter.
  Context {Σ} `{!heapG Σ, !cincG Σ}.
  Context (N : namespace).

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

118
  (** Updating and synchronizing the counter and flag RAs *)
119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147

  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 sync_flag_values γ_n (b1 b2 : bool) :
    own γ_n ( Excl' b1) - own γ_n ( Excl' b2) - b1 = b2.
  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.

  Lemma update_flag_value γ_n (b1 b2 b : bool) :
    own γ_n ( Excl' b1) - own γ_n ( Excl' b2) == own γ_n ( Excl' b)  own γ_n ( Excl' b).
  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.

148 149
  Definition counter_content (γs : gname * gname) (b : bool) (n : Z) :=
    (own γs.1 ( Excl' b)  own γs.2 ( Excl' n))%I.
150 151 152 153 154 155 156 157 158 159 160 161 162 163 164


  (** Definition of the invariant *)

  Fixpoint val_to_some_loc (vs : list (val * val)) : option loc :=
    match vs with
    | (#true , LitV (LitLoc l)) :: _  => Some l
    | _                         :: vs => val_to_some_loc vs
    | _                               => None
    end.

  Inductive abstract_state : Set :=
  | injl : Z  abstract_state
  | injr : Z  proph_id  abstract_state.

165 166 167 168 169
  Definition state_to_val (s : abstract_state) : val :=
    match s with
    | injl n => InjLV #n
    | injr n p => InjRV (#n,#p)
    end.
170

171 172 173 174
  Global Instance state_to_val_inj : Inj (=) (=) state_to_val.
  Proof.
    intros [|] [|]; simpl; intros Hv; inversion_clear Hv; done.
  Qed.
175

176
  Definition own_token γ := (own γ (Excl ()))%I.
177

178 179
  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.
180

181 182 183 184
  (* 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.
185

186 187 188 189 190
  (* The same thread then wins the CAS and moves from [accepted] to [done].
     Then, the [γ_t] token guards the transition to take out [Q].
     Remember that the thread winning the CAS might be just helping.  The token
     is owned by the thread whose request this is.
     In this state, [l_ghost_winner] serves as a token to make sure that
Ralf Jung's avatar
Ralf Jung committed
191 192 193 194
     only the CAS winner can transition to here, and owning half of[l] serves as a
     "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. *)
195
  Definition done_state Q (l l_ghost_winner : loc) (γ_t : gname) :=
196
    ((Q  own_token γ_t)  l_ghost_winner  -  l {1/2} -)%I.
197 198 199 200 201 202

  (* 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 Σ :=
203
    ( vs, proph p vs 
204 205 206 207
      (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.
208 209

  Definition pau P Q γs :=
210 211
    ( P -  AU <<  (b : bool) (n : Z), counter_content γs b n >> @ ∖↑N, 
                 << counter_content γs b (if b then n + 1 else n), COMM Q >>)%I.
212

213 214
  Definition counter_inv γ_b γ_n f c :=
    ( (b : bool) (l : loc) (q : Qp) (s : abstract_state),
Ralf Jung's avatar
Ralf Jung committed
215 216
       (* We own *more than* half of [l], which shows that this cannot
          be the [l] of any [state] protocol in the [done] state. *)
217
       f  #b  c {1/2} #l  l {1/2 + q} (state_to_val s) 
218
       own γ_b ( Excl' b) 
219 220 221 222 223 224 225 226 227 228 229 230
       match s with
        | injl n => c {1/2} #l  own γ_n ( Excl' n)
        | injr n p =>
            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) 
              pau P Q (γ_b, γ_n)
       end)%I.

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

233 234 235 236
  Definition is_counter (γs : gname * gname) (ctr : val) :=
    ( (γ_b γ_n : gname) (f c : loc),
        ⌜γs = (γ_b, γ_n)  ctr = (#f, #c)%V 
        inv counterN (counter_inv γ_b γ_n f c))%I.
237 238 239

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

240
  Global Instance counter_content_timeless γs b n : Timeless (counter_content γs b n) := _.
241 242 243

  Global Instance abstract_state_inhabited: Inhabited abstract_state := populate (injl 0).

244 245 246 247 248 249
  Lemma counter_content_exclusive γs f1 c1 f2 c2 :
    counter_content γs f1 c1 - counter_content γs f2 c2 - False.
  Proof.
    iIntros "[Hb1 _] [Hb2 _]". iDestruct (own_valid_2 with "Hb1 Hb2") as %?.
    done.
  Qed.
250 251 252 253 254 255 256 257 258 259

  (** 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.

260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279
  (** 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.
280 281 282

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

283 284 285 286 287 288
  (** The part of [complete] for the succeeding thread that moves from [accepted] to [done] state *)
  Lemma complete_succeeding_thread_pending (γ_b γ_n γ_t γ_s : gname) f_l c_l P Q p
        (m n : Z) (l l_ghost l_new : loc) Φ :
    inv counterN (counter_inv γ_b γ_n f_l c_l) -
    inv stateN (state_inv P Q p m c_l l l_ghost γ_n γ_t γ_s) -
    pau P Q (γ_b, γ_n) -
289
    l_ghost {1 / 2} #() -
290
    ((own_token γ_t ={}=  Q) - Φ #()) -
291 292 293 294
    own γ_n ( Excl' n) -
    l_new  InjLV #n -
    WP Resolve (CAS #c_l #l #l_new) #p #l_ghost ;; #() {{ v, Φ v }}.
  Proof.
295 296
    iIntros "#InvC #InvS PAU Hl_ghost HQ Hn● [Hl_new Hl_new']". wp_bind (Resolve _ _ _)%E.
    iInv counterN as (b' l' q s) "(>Hf & >Hc & >[Hl Hl'] & Hb● & Hrest)".
297 298 299 300 301
    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".
302
        by iDestruct (mapsto_valid_2 with "Hl_ghost Hlghost") as %?.
303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323
    }
    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 %[= ->].
    (* We perform the CAS. *)
    iCombine "Hc Hc'" as "Hc".
    wp_apply (wp_resolve with "Hp"); first done; wp_cas_suc.
    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.
324
    iSplitL "Hl_ghost_inv Hl_ghost Q Hp' Hl".
325 326
    (* Update state to Done. *)
    { iNext. iExists _. iFrame "Hp'". iRight. unfold done_state.
327
      iFrame "#∗". iSplitR "Hl"; iExists _; done. }
328 329 330 331 332
    iModIntro. iSplitR "HQ".
    { iNext. iDestruct "Hc" as "[Hc1 Hc2]".
      iExists _, l_new, _, (injl n). iFrame. }
    iApply wp_fupd. wp_seq. iApply "HQ".
    iApply state_done_extract_Q; done.
333 334 335
  Qed.

  (** The part of [complete] for the failing thread *)
336
  Lemma complete_failing_thread γ_b γ_n γ_t γ_s f_l c_l l P Q p m n l_ghost_inv l_ghost l_new Φ :
337
    l_ghost_inv  l_ghost 
338 339 340 341
    inv counterN (counter_inv γ_b γ_n f_l c_l) -
    inv stateN (state_inv P Q p m c_l l l_ghost_inv γ_n γ_t γ_s) -
    pau P Q (γ_b, γ_n) -
    ((own_token γ_t ={}=  Q) - Φ #()) -
342 343 344
    l_new  InjLV #n -
    WP Resolve (CAS #c_l #l #l_new) #p #l_ghost ;; #() {{ v, Φ v }}.
  Proof.
345
    iIntros (Hnl) "#InvC #InvS PAU HQ Hl_new". wp_bind (Resolve _ _ _)%E.
346
    iInv counterN as (b' l' q s) "(>Hf & >Hc & >[Hl Hl'] & >Hb● & Hrest)".
347 348 349 350 351 352 353 354 355 356
    iInv stateN as (vs) "(>Hp & [NotDone | [#Hs Done]])".
    { (* If the [state] protocol is not done yet, we can show that it
         is the active protocol still (l = l').  But then the CAS would
         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".
        wp_apply (wp_resolve with "Hp"); first done; wp_cas_suc.
        iIntros (vs' ->). iDestruct "State" as "[Pending | Accepted]".
357
        + iDestruct "Pending" as "[_ [Hvs _]]". iDestruct "Hvs" as %Hvs. by inversion Hvs.
358 359 360 361 362
        + 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
363 364 365 366 367
         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 "[]".
368 369
    }
    (* The CAS fails. *)
370 371 372
    wp_apply (wp_resolve with "Hp"); first done. wp_cas_fail.
    iIntros (vs' ->) "Hp". iModIntro.
    iSplitL "Done Hp". { iNext. iExists _. iFrame "#∗". } iModIntro.
373
    iSplitL "Hf Hc Hb● Hrest Hl Hl'". { eauto 10 with iFrame. }
374 375
    wp_seq. iApply "HQ".
    iApply state_done_extract_Q; done.
376 377 378
  Qed.

  (** ** Proof of [complete] *)
379 380 381 382
  (* 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. *)
Ralf Jung's avatar
Ralf Jung committed
383 384 385 386
  Lemma complete_spec (c f l : loc) (n : Z) (p : proph_id) γ_b γ_n γ_t γ_s l_ghost_inv P Q :
    inv counterN (counter_inv γ_b γ_n f c) -
    inv stateN (state_inv P Q p n c l l_ghost_inv γ_n γ_t γ_s) -
     pau P Q (γ_b, γ_n) -
387 388
    {{{ True }}}
       complete #c #f #l #n #p
389
    {{{ RET #();  (own_token γ_t ={}= Q) }}}.
390
  Proof.
Ralf Jung's avatar
Ralf Jung committed
391
    iIntros "#InvC #InvS #PAU".
392 393 394
    iModIntro. iIntros (Φ) "_ HQ". wp_lam. wp_pures.
    wp_alloc l_ghost as "[Hl_ghost' Hl_ghost'2]". wp_bind (! _)%E. simpl.
    (* open outer invariant to read `f` *)
395
    iInv counterN as (b' l' q s) "(>Hf & >Hc & >Hl' & >Hb● & Hrest)".
396
    wp_load.
397 398 399
    (* two different proofs depending on whether we are succeeding thread *)
    destruct (decide (l_ghost_inv = l_ghost)) as [-> | Hnl].
    - (* we are the succeeding thread *)
400 401
      (* we need to move from [pending] to [accepted]. *)
      iInv stateN as (vs) "(>Hp & [(>Hs & >Hc' & [Pending | Accepted]) | [#Hs Done]])".
402
      + (* Pending: update to accepted *)
403
        iDestruct "Pending" as "[P >[Hvs Hn●]]".
404
        iDestruct ("PAU" with "P") as ">AU".
405
        (* open and *COMMIT* AU, sync flag and counter *)
406 407 408 409 410 411 412 413
        iMod "AU" as (b2 n2) "[CC [_ Hclose]]".
        iDestruct "CC" as "[Hb◯ Hn◯]". simpl.
        iDestruct (sync_flag_values with "Hb● Hb◯") as %->.
        iDestruct (sync_counter_values with "Hn● Hn◯") as %->.
        iMod (update_counter_value _ _ _ (if b2 then n2 + 1 else n2) with "Hn● Hn◯")
          as "[Hn● Hn◯]".
        iMod ("Hclose" with "[Hn◯ Hb◯]") as "Q"; first by iFrame.
        (* close state inv *)
414 415 416 417
        iModIntro. iSplitL "Q Hl_ghost' Hp Hvs Hs Hc'".
        { iNext. iExists _. iFrame "Hp". iLeft. iFrame.
          iRight. iSplitL "Hl_ghost'"; first by iExists _.
          destruct (val_to_some_loc vs) eqn:Hvts; iFrame. }
418 419
        (* close outer inv *)
        iModIntro. iSplitR "Hl_ghost'2 HQ Hn●".
Ralf Jung's avatar
Ralf Jung committed
420
        { eauto 12 with iFrame. }
421
        destruct b2; wp_if; [ wp_op | .. ];
422
        wp_alloc l_new as "Hl_new"; wp_pures;
423
          iApply (complete_succeeding_thread_pending
424
                    with "InvC InvS PAU Hl_ghost'2 HQ Hn● Hl_new").
425 426 427 428 429 430 431 432 433 434 435 436
      + (* 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 %?.
    - (* we are the failing thread *)
      (* close invariant *)
437
      iModIntro.
438
      iSplitL "Hf Hc Hrest Hl' Hb●". { eauto 10 with iFrame. }
439
      (* two equal proofs depending on value of b1 *)
440 441 442
      destruct b'; wp_if; [ wp_op | ..]; wp_alloc Hl_new as "Hl_new"; wp_pures;
        iApply (complete_failing_thread
                  with "InvC InvS PAU HQ Hl_new"); done.
443 444 445 446
  Qed.

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

447 448 449 450 451
  Lemma cinc_spec γs v :
    is_counter γs v -
    <<<  (b : bool) (n : Z), counter_content γs b n >>>
        cinc v @∖↑N
    <<< counter_content γs b (if b then n + 1 else n), RET #() >>>.
452
  Proof.
453
    iIntros "#InvC". iDestruct "InvC" as (γ_b γ_n f_l c_l) "[Heq InvC]".
454
    iDestruct "Heq" as %[-> ->]. iIntros (Φ) "AU". iLöb as "IH".
455
    wp_lam. wp_proj. wp_let. wp_proj. wp_let. wp_bind (!_)%E.
456
    iInv counterN as (b' l' q s) "(>Hf & >Hc & >[Hl [Hl' Hl'']] & >Hb● & Hrest)".
457 458
    wp_load. destruct s as [n|n p].
    - iDestruct "Hrest" as "(Hc' & Hv)".
459
      iModIntro. iSplitR "AU Hl'".
460
      { iModIntro. iExists _, _, (q/2)%Qp, (injl n). iFrame. }
461 462
      wp_let. wp_load. wp_match. wp_apply wp_new_proph; first done.
      iIntros (l_ghost p') "Hp'".
463
      wp_let. wp_alloc ly as "Hly".
464 465
      wp_let. wp_bind (CAS _ _ _)%E.
      (* open outer invariant again to CAS c_l *)
466
      iInv counterN as (b2 l'' q2 s) "(>Hf & >Hc & >Hl & >Hb● & Hrest)".
467 468
      destruct (decide (l' = l'')) as [<- | Hn].
      + (* CAS succeeds *)
469
        iDestruct (mapsto_agree with "Hl' Hl") as %<-%state_to_val_inj.
470
        iDestruct "Hrest" as ">[Hc' Hn●]". iCombine "Hc Hc'" as "Hc".
471
        wp_cas_suc.
472
        (* Initialize new [state] protocol .*)
473
        iDestruct (laterable with "AU") as (AU_later) "[AU #AU_back]".
474 475 476
        iMod (own_alloc (Excl ())) as (γ_t) "Token"; first done.
        iMod (own_alloc (Cinl $ Excl ())) as (γ_s) "Hs"; first done.
        iDestruct "Hc" as "[Hc Hc']".
477 478
        set (winner := default ly (val_to_some_loc l_ghost)).
        iMod (inv_alloc stateN _ (state_inv AU_later _ _ _ _ _ winner _ _ _)
479
               with "[AU Hs Hp' Hc' Hn●]") as "#Hinv".
480 481 482 483
        { 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 *)
Ralf Jung's avatar
Ralf Jung committed
484
          iNext. iExists _, _, _, (injr n p'). eauto 10 with iFrame.
485
        }
Ralf Jung's avatar
Ralf Jung committed
486
        wp_if. wp_apply complete_spec; [done..|].
487
        iIntros "Ht". iMod ("Ht" with "Token") as "Φ". wp_seq. by wp_lam.
488 489
      + (* CAS fails: closing invariant and invoking IH *)
        wp_cas_fail.
490 491
        iModIntro. iSplitR "AU".
        { iModIntro. iExists _, _, _, s. iFrame. }
492 493
        wp_if. by iApply "IH".
    - (* l' ↦ injR *)
494
      iModIntro.
495
      (* extract state invariant *)
496
      iDestruct "Hrest" as (P Q l_ghost γ_t γ_s) "[#InvS #P_AU]".
497 498
      iSplitR "Hl' AU".
      (* close invariant *)
499 500
      { iModIntro. iExists _, _, _, (injr n p). iFrame. eauto 10 with iFrame. }
      wp_let. wp_load. wp_match. wp_pures.
Ralf Jung's avatar
Ralf Jung committed
501
      wp_apply complete_spec; [done..|].
502 503 504 505 506 507
      iIntros "_". wp_seq. by iApply "IH".
  Qed.

  Lemma new_counter_spec :
    {{{ True }}}
        new_counter #()
508
    {{{ ctr γs, RET ctr ; is_counter γs ctr  counter_content γs true 0 }}}.
509 510
  Proof.
    iIntros (Φ) "_ HΦ". wp_lam. wp_apply wp_fupd.
511
    wp_alloc l_n as "Hl_n".
512
    wp_alloc l_c as "Hl_c". wp_let.
513 514 515 516 517
    wp_alloc l_f as "Hl_f". wp_let. wp_pair.
    iMod (own_alloc ( Excl' true    Excl' true)) as (γ_b) "[Hb● Hb◯]".
    { by apply auth_both_valid. }
    iMod (own_alloc ( Excl' 0    Excl' 0)) as (γ_n) "[Hn● Hn◯]".
    { by apply auth_both_valid. }
518
    iMod (inv_alloc counterN _ (counter_inv γ_b γ_n l_f l_c)
519
      with "[Hl_f Hl_c Hl_n Hb● Hn●]") as "#InvC".
520
    { iNext. iDestruct "Hl_c" as "[Hl_c1 Hl_c2]".
521 522
      iDestruct "Hl_n" as "[??]".
      iExists true, l_n, (1/2)%Qp, (injl 0). iFrame. }
523
    iModIntro.
524 525
    iApply ("HΦ" $! (#l_f, #l_c)%V (γ_b, γ_n)).
    iSplitR; last by iFrame. iExists γ_b, γ_n, l_f, l_c. iSplit; done.
526 527
  Qed.

528 529 530 531 532
  Lemma set_flag_spec γs v (new_b : bool) :
    is_counter γs v -
    <<<  (b : bool) (n : Z), counter_content γs b n >>>
        set_flag v #new_b @∖↑N
    <<< counter_content γs new_b n, RET #() >>>.
533
  Proof.
534 535
    iIntros "#InvC" (Φ) "AU". iDestruct "InvC" as (γ_b γ_n f_l c_l) "[Heq InvC]".
    iDestruct "Heq" as %[-> ->]. wp_lam. wp_let. wp_proj.
536
    iInv counterN as (b c q s) "(>Hf & >Hc & >[Hl Hl'] & >Hb● & Hrest)".
537 538 539 540 541 542
    iMod "AU" as (b' n') "[[Hb◯ Hn◯] [_ Hclose]]"; simpl.
    wp_store.
    iDestruct (sync_flag_values with "Hb● Hb◯") as %HEq; subst b.
    iDestruct (update_flag_value with "Hb● Hb◯") as ">[Hb● Hb◯]".
    iMod ("Hclose" with "[Hn◯ Hb◯]") as "HΦ"; first by iFrame.
    iModIntro. iModIntro. iSplitR "HΦ"; last done.
543
    iNext. iExists new_b, c, q, _. iFrame. done.
544 545
  Qed.

546 547 548 549 550
  Lemma get_spec γs v :
    is_counter γs v -
    <<<  (b : bool) (n : Z), counter_content γs b n >>>
        get v @∖↑N
    <<< counter_content γs b n, RET #n >>>.
551
  Proof.
552 553
    iIntros "#InvC" (Φ) "AU". iDestruct "InvC" as (γ_b γ_n f_l c_l) "[Heq InvC]".
    iDestruct "Heq" as %[-> ->]. iLöb as "IH". wp_lam. repeat (wp_proj; wp_let). wp_bind (! _)%E.
554
    iInv counterN as (b c q s) "(>Hf & >Hc & >[Hl [Hl' Hl'']] & >Hb● & Hrest)".
555 556 557 558
    wp_load.
    destruct s as [n|n p].
    - iMod "AU" as (au_b au_n) "[[Hb◯ Hn◯] [_ Hclose]]"; simpl.
      iDestruct "Hrest" as "[Hc' Hn●]".
559 560
      iDestruct (sync_counter_values with "Hn● Hn◯") as %->.
      iMod ("Hclose" with "[Hn◯ Hb◯]") as "HΦ"; first by iFrame.
561 562
      iModIntro. iSplitR "HΦ Hl'". {
        iNext. iExists b, c, (q/2)%Qp, (injl au_n). iFrame.
563 564
      }
      wp_let. wp_load. wp_match. iApply "HΦ".
565 566
    - iDestruct "Hrest" as (P Q l_ghost γ_t γ_s) "[#InvS #PAU]".
      iModIntro. iSplitR "AU Hl'". {
Ralf Jung's avatar
Ralf Jung committed
567
        iNext. iExists b, c, (q/2)%Qp, (injr n p). eauto 10 with iFrame.
568 569
      }
      wp_let. wp_load. wp_match. repeat wp_proj. wp_bind (complete _ _ _ _ _)%E.
Ralf Jung's avatar
Ralf Jung committed
570
      wp_apply complete_spec; [done..|].
571 572 573 574
      iIntros "Ht". wp_seq. iApply "IH". iApply "AU".
  Qed.

End conditional_counter.
575 576 577 578 579 580 581 582 583 584

Definition atomic_cinc `{!heapG Σ, cincG Σ} :
  spec.atomic_cinc Σ :=
  {| spec.new_counter_spec := new_counter_spec;
     spec.cinc_spec := cinc_spec;
     spec.set_flag_spec := set_flag_spec;
     spec.get_spec := get_spec;
     spec.counter_content_exclusive := counter_content_exclusive |}.

Typeclasses Opaque counter_content is_counter.