strengthen cinc spec: flag can be any GC'ed location

theories/logatom/conditional_increment/cinc.v

@@ -15,22 +15,11 @@ Set Default Proof Using "Type".
 (*
   new_counter() :=
     let c = ref (injL 0) in
-    let f = ref false in
-    ref (f, c)
+    ref 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".
+    ref (ref (InjL #0)).
 
 (*
   complete(c, f, x, n, p) :=
@@ -38,78 +27,82 @@ Definition set_flag : val :=
  *)
 Definition complete : val :=
   λ: "c" "f" "x" "n" "p",
-    Resolve (CAS "c" "x" (ref (InjL (if: !"f" then "n" + #1 else "n")))) "p" (ref #()) ;; #().
+    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
+    Resolve (CAS "c" "x" (ref (InjL "new_n"))) "p" "l_ghost" ;; #().
 
 (*
-  get(c, f) :=
+  get c :=
     let x = !c in
     match !x with
     | injL n      => n
-    | injR (n, p) => complete c f x n p; get(c, f)
+    | injR (f, 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
+  rec: "get" "c" :=
     let: "x" := !"c" in
     match: !"x" with
       InjL "n"    => "n"
     | InjR "args" =>
-        complete "c" "f" "x" (Fst "args") (Snd "args") ;;
-        "get" "ctr"
+        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"
     end.
 
 (*
-  cinc(c, f) :=
+  cinc c f :=
     let x = !c in
     match !x with
     | injL n =>
         let p := new proph in
-        let y := ref (injR (n, p)) in
+        let y := ref (injR (n, f, 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)
+        else cinc c f
+    | injR (f', 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
+  rec: "cinc" "c" "f" :=
     let: "x" := !"c" in
     match: !"x" with
       InjL "n" =>
         let: "p" := NewProph in
-        let: "y" := ref (InjR ("n", "p")) in
+        let: "y" := ref (InjR ("f", "n", "p")) in
         if: CAS "c" "x" "y" then complete "c" "f" "y" "n" "p" ;; Skip
-        else "cinc" "ctr"
+        else "cinc" "c" "f"
     | InjR "args'" =>
-        complete "c" "f" "x" (Fst "args'") (Snd "args'") ;;
-        "cinc" "ctr"
+        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"
     end.
 
 (** ** Proof setup *)
 
-Definition flagUR     := authR $ optionUR $ exclR boolO.
 Definition numUR      := authR $ optionUR $ exclR ZO.
 Definition tokenUR    := exclR unitO.
 Definition one_shotUR := csumR (exclR unitO) (agreeR unitO).
 
 Class cincG Σ := ConditionalIncrementG {
-                     cinc_flagG     :> inG Σ flagUR;
                      cinc_numG      :> inG Σ numUR;
                      cinc_tokenG    :> inG Σ tokenUR;
                      cinc_one_shotG :> inG Σ one_shotUR;
                    }.
 
 Definition cincΣ : gFunctors :=
-  #[GFunctor flagUR; GFunctor numUR; GFunctor tokenUR; GFunctor one_shotUR].
+  #[GFunctor numUR; GFunctor tokenUR; GFunctor one_shotUR].
 
 Instance subG_cincΣ {Σ} : subG cincΣ Σ → cincG Σ.
 Proof. solve_inG. Qed.
 
 Section conditional_counter.
-  Context {Σ} `{!heapG Σ, !cincG Σ}.
+  Context {Σ} `{!heapG Σ, !gcG Σ, !cincG Σ}.
   Context (N : namespace).
 
   Local Definition stateN   := N .@ "state".
@@ -124,13 +117,6 @@ Section conditional_counter.
       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.
@@ -138,16 +124,8 @@ Section conditional_counter.
     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.
-
-  Definition counter_content (γs : gname * gname) (b : bool) (n : Z) :=
-    (own γs.1 (◯ Excl' b) ∗ own γs.2 (◯ Excl' n))%I.
-
+  Definition counter_content (γs : gname) (n : Z) :=
+    (own γs (◯ Excl' n))%I.
 
   (** Definition of the invariant *)
 
@@ -160,12 +138,12 @@ Section conditional_counter.
 
   Inductive abstract_state : Set :=
   | Quiescent : Z → abstract_state
-  | Updating : Z → proph_id → abstract_state.
+  | Updating : loc → Z → proph_id → abstract_state.
 
   Definition state_to_val (s : abstract_state) : val :=
     match s with
     | Quiescent n => InjLV #n
-    | Updating n p => InjRV (#n,#p)
+    | Updating f n p => InjRV (#f,#n,#p)
     end.
 
   Global Instance state_to_val_inj : Inj (=) (=) state_to_val.
@@ -206,45 +184,42 @@ Section conditional_counter.
         ∨ 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.
 
-  Definition pau P Q γs :=
-    (▷ 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.
+  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.
 
-  Definition counter_inv γ_b γ_n f c :=
-    (∃ (b : bool) (l : loc) (q : Qp) (s : abstract_state),
+  Definition counter_inv γ_n c :=
+    (∃ (l : loc) (q : Qp) (s : abstract_state),
        (* We own *more than* half of [l], which shows that this cannot
           be the [l] of any [state] protocol in the [done] state. *)
-       f ↦ #b ∗ c ↦{1/2} #l ∗ l ↦{1/2 + q} (state_to_val s) ∗
-       own γ_b (● Excl' b) ∗
+       c ↦{1/2} #l ∗ l ↦{1/2 + q} (state_to_val s) ∗
        match s with
         | Quiescent n => c ↦{1/2} #l ∗ own γ_n (● Excl' n)
-        | Updating n p =>
+        | Updating f 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)
+             □ pau P Q γ_n f ∗ is_gc_loc f
        end)%I.
 
-  Local Hint Extern 0 (environments.envs_entails _ (counter_inv _ _ _ _)) => unfold counter_inv.
+  Local Hint Extern 0 (environments.envs_entails _ (counter_inv _ _)) => unfold counter_inv.
 
-  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.
+  Definition is_counter (γ_n : gname) (ctr : val) :=
+    (∃ (c : loc), ⌜ctr = #c ∧ N ## gcN⌝ ∗ gc_inv ∗ inv counterN (counter_inv γ_n c))%I.
 
   Global Instance is_counter_persistent γs ctr : Persistent (is_counter γs ctr) := _.
 
-  Global Instance counter_content_timeless γs b n : Timeless (counter_content γs b n) := _.
+  Global Instance counter_content_timeless γs n : Timeless (counter_content γs n) := _.
 
   Global Instance abstract_state_inhabited: Inhabited abstract_state := populate (Quiescent 0).
 
-  Lemma counter_content_exclusive γs f1 c1 f2 c2 :
-    counter_content γs f1 c1 -∗ counter_content γs f2 c2 -∗ False.
+  Lemma counter_content_exclusive γs c1 c2 :
+    counter_content γs c1 -∗ counter_content γs c2 -∗ False.
   Proof.
-    iIntros "[Hb1 _] [Hb2 _]". iDestruct (own_valid_2 with "Hb1 Hb2") as %?.
+    iIntros "Hb1 Hb2". iDestruct (own_valid_2 with "Hb1 Hb2") as %?.
     done.
   Qed.
 
@@ -281,19 +256,18 @@ Section conditional_counter.
   (** ** Proof of [complete] *)
 
   (** 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
+  Lemma complete_succeeding_thread_pending (γ_n γ_t γ_s : gname) 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 counterN (counter_inv γ_n c_l) -∗
     inv stateN (state_inv P Q p m c_l l l_ghost γ_n γ_t γ_s) -∗
-    pau P Q (γ_b, γ_n) -∗
     l_ghost ↦{1 / 2} #() -∗
     (□(own_token γ_t ={⊤}=∗ ▷ Q) -∗ Φ #()) -∗
     own γ_n (● Excl' n) -∗
     l_new ↦ InjLV #n -∗
     WP Resolve (CAS #c_l #l #l_new) #p #l_ghost ;; #() {{ v, Φ v }}.
   Proof.
-    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)".
+    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)".
     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. *)
@@ -327,23 +301,22 @@ Section conditional_counter.
       iFrame "#∗". iSplitR "Hl"; iExists _; done. }
     iModIntro. iSplitR "HQ".
     { iNext. iDestruct "Hc" as "[Hc1 Hc2]".
-      iExists _, l_new, _, (Quiescent n). iFrame. }
+      iExists l_new, _, (Quiescent n). iFrame. }
     iApply wp_fupd. wp_seq. iApply "HQ".
     iApply state_done_extract_Q; done.
   Qed.
 
   (** The part of [complete] for the failing thread *)
-  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 Φ :
+  Lemma complete_failing_thread γ_n γ_t γ_s c_l l P Q p m n l_ghost_inv l_ghost l_new Φ :
     l_ghost_inv ≠ l_ghost →
-    inv counterN (counter_inv γ_b γ_n f_l c_l) -∗
+    inv counterN (counter_inv γ_n 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) -∗ Φ #()) -∗
     l_new ↦ InjLV #n -∗
     WP Resolve (CAS #c_l #l #l_new) #p #l_ghost ;; #() {{ v, Φ v }}.
   Proof.
-    iIntros (Hnl) "#InvC #InvS PAU HQ Hl_new". wp_bind (Resolve _ _ _)%E.
-    iInv counterN as (b' l' q s) "(>Hf & >Hc & >[Hl Hl'] & >Hb● & Hrest)".
+    iIntros (Hnl) "#InvC #InvS HQ Hl_new". wp_bind (Resolve _ _ _)%E.
+    iInv counterN as (l' q s) "(>Hc & >[Hl Hl'] & Hrest)".
     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
@@ -370,7 +343,7 @@ Section conditional_counter.
     wp_apply (wp_resolve with "Hp"); first done. wp_cas_fail.
     iIntros (vs' ->) "Hp". iModIntro.
     iSplitL "Done Hp". { iNext. iExists _. iFrame "#∗". } iModIntro.
-    iSplitL "Hf Hc Hb● Hrest Hl Hl'". { eauto 10 with iFrame. }
+    iSplitL "Hc Hrest Hl Hl'". { eauto 10 with iFrame. }
     wp_seq. iApply "HQ".
     iApply state_done_extract_Q; done.
   Qed.
@@ -380,20 +353,23 @@ Section conditional_counter.
      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. *)
-  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) -∗
+  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) -∗
     inv stateN (state_inv P Q p n c l l_ghost_inv γ_n γ_t γ_s) -∗
-    □ pau P Q (γ_b, γ_n) -∗
+    □ pau P Q γ_n f -∗
+    is_gc_loc f -∗
     {{{ True }}}
        complete #c #f #l #n #p
     {{{ RET #(); □ (own_token γ_t ={⊤}=∗ ▷Q) }}}.
   Proof.
-    iIntros "#InvC #InvS #PAU".
+    iIntros (?) "#GC #InvC #InvS #PAU #isGC".
     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` *)
-    iInv counterN as (b' l' q s) "(>Hf & >Hc & >Hl' & >Hb● & Hrest)".
-    wp_load.
+    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)".
     (* two different proofs depending on whether we are succeeding thread *)
     destruct (decide (l_ghost_inv = l_ghost)) as [-> | Hnl].
     - (* we are the succeeding thread *)
@@ -402,26 +378,29 @@ Section conditional_counter.
       + (* Pending: update to accepted *)
         iDestruct "Pending" as "[P >[Hvs Hn●]]".
         iDestruct ("PAU" with "P") as ">AU".
+        iMod (gc_access with "GC") as "Hgc"; first solve_ndisj.
         (* open and *COMMIT* AU, sync flag and counter *)
-        iMod "AU" as (b2 n2) "[CC [_ Hclose]]".
-        iDestruct "CC" as "[Hb◯ Hn◯]". simpl.
-        iDestruct (sync_flag_values with "Hb● Hb◯") as %->.
+        iMod "AU" as (b n2) "[[Hn◯ Hf] [_ Hclose]]".
+        iDestruct ("Hgc" with "Hf") as "[Hf Hfclose]".
+        wp_load.
+        iMod ("Hfclose" with "Hf") as "[Hf Hfclose]".
         iDestruct (sync_counter_values with "Hn● Hn◯") as %->.
-        iMod (update_counter_value _ _ _ (if b2 then n2 + 1 else n2) with "Hn● Hn◯")
+        iMod (update_counter_value _ _ _ (if b then n2 + 1 else n2) with "Hn● Hn◯")
           as "[Hn● Hn◯]".
-        iMod ("Hclose" with "[Hn◯ Hb◯]") as "Q"; first by iFrame.
+        iMod ("Hclose" with "[Hn◯ Hf]") as "Q"; first by iFrame.
+        iModIntro. iMod "Hfclose" as "_".
         (* close state inv *)
-        iModIntro. iSplitL "Q Hl_ghost' Hp Hvs Hs Hc'".
+        iIntros "!> !>". 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. }
         (* close outer inv *)
         iModIntro. iSplitR "Hl_ghost'2 HQ Hn●".
         { eauto 12 with iFrame. }
-        destruct b2; wp_if; [ wp_op | .. ];
+        destruct b;
         wp_alloc l_new as "Hl_new"; wp_pures;
           iApply (complete_succeeding_thread_pending
-                    with "InvC InvS PAU Hl_ghost'2 HQ Hn● Hl_new").
+                    with "InvC InvS Hl_ghost'2 HQ Hn● Hl_new").
       + (* Accepted: contradiction *)
         iDestruct "Accepted" as "[>Hl_ghost_inv _]".
         iDestruct "Hl_ghost_inv" as (v) "Hlghost".
@@ -432,43 +411,51 @@ Section conditional_counter.
         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 *)
+    - (* 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.
       (* close invariant *)
-      iModIntro.
-      iSplitL "Hf Hc Hrest Hl' Hb●". { eauto 10 with iFrame. }
+      iModIntro. iSplitL "Hc Hrest Hl'". { eauto 10 with iFrame. }
       (* two equal proofs depending on value of b1 *)
-      destruct b'; wp_if; [ wp_op | ..]; wp_alloc Hl_new as "Hl_new"; wp_pures;
+      wp_pures.
+      destruct (bool_decide (val_for_compare b = #true));
+      wp_alloc Hl_new as "Hl_new"; wp_pures;
         iApply (complete_failing_thread
-                  with "InvC InvS PAU HQ Hl_new"); done.
+                  with "InvC InvS HQ Hl_new"); done.
   Qed.
 
   (** ** Proof of [cinc] *)
 
-  Lemma cinc_spec γs v :
+  Lemma cinc_spec γs v (f: loc) :
     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 #() >>>.
+    <<< ∀ (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 #() >>>.
   Proof.
-    iIntros "#InvC". iDestruct "InvC" as (γ_b γ_n f_l c_l) "[Heq InvC]".
-    iDestruct "Heq" as %[-> ->]. iIntros (Φ) "AU". iLöb as "IH".
-    wp_lam. wp_proj. wp_let. wp_proj. wp_let. wp_bind (!_)%E.
-    iInv counterN as (b' l' q s) "(>Hf & >Hc & >[Hl [Hl' Hl'']] & >Hb● & Hrest)".
-    wp_load. destruct s as [n|n p].
+    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'].
     - iDestruct "Hrest" as "(Hc' & Hv)".
       iModIntro. iSplitR "AU Hl'".
-      { iModIntro. iExists _, _, (q/2)%Qp, (Quiescent n). iFrame. }
+      { iModIntro. iExists _, (q/2)%Qp, (Quiescent n). iFrame. }
       wp_let. wp_load. wp_match. wp_apply wp_new_proph; first done.
       iIntros (l_ghost p') "Hp'".
       wp_let. wp_alloc ly as "Hly".
       wp_let. wp_bind (CAS _ _ _)%E.
       (* open outer invariant again to CAS c_l *)
-      iInv counterN as (b2 l'' q2 s) "(>Hf & >Hc & >Hl & >Hb● & Hrest)".
+      iInv counterN as (l'' q2 s) "(>Hc & >Hl & Hrest)".
       destruct (decide (l' = l'')) as [<- | Hn].
       + (* CAS succeeds *)
         iDestruct (mapsto_agree with "Hl' Hl") as %<-%state_to_val_inj.
         iDestruct "Hrest" as ">[Hc' Hn●]". iCombine "Hc Hc'" as "Hc".
         wp_cas_suc.
+        (* 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.
         (* Initialize new [state] protocol .*)
         iDestruct (laterable with "AU") as (AU_later) "[AU #AU_back]".
         iMod (own_alloc (Excl ())) as (γ_t) "Token"; first done.
@@ -481,103 +468,83 @@ Section conditional_counter.
           iFrame. destruct (val_to_some_loc l_ghost); simpl; done. }
         iModIntro. iDestruct "Hly" as "[Hly1 Hly2]". iSplitR "Hl' Token". {
           (* close invariant *)
-          iNext. iExists _, _, _, (Updating n p'). eauto 10 with iFrame.
+          iNext. iExists _, _, (Updating f n p'). eauto 10 with iFrame.
         }
         wp_if. wp_apply complete_spec; [done..|].
         iIntros "Ht". iMod ("Ht" with "Token") as "Φ". wp_seq. by wp_lam.
       + (* CAS fails: closing invariant and invoking IH *)
         wp_cas_fail.
         iModIntro. iSplitR "AU".
-        { iModIntro. iExists _, _, _, s. iFrame. }
+        { iModIntro. iExists _, _, s. iFrame. }
         wp_if. by iApply "IH".
     - (* l' ↦ injR *)
       iModIntro.
       (* extract state invariant *)
-      iDestruct "Hrest" as (P Q l_ghost γ_t γ_s) "[#InvS #P_AU]".
+      iDestruct "Hrest" as (P Q l_ghost γ_t γ_s) "(#InvS & #P_AU & #Hgc)".
       iSplitR "Hl' AU".
       (* close invariant *)
-      { iModIntro. iExists _, _, _, (Updating n p). iFrame. eauto 10 with iFrame. }
+      { iModIntro. iExists _, _, (Updating f' n' p'). iFrame. eauto 10 with iFrame. }
       wp_let. wp_load. wp_match. wp_pures.
       wp_apply complete_spec; [done..|].
       iIntros "_". wp_seq. by iApply "IH".
   Qed.
 
   Lemma new_counter_spec :
+    N ## gcN →
+    gc_inv -∗
     {{{ True }}}
         new_counter #()
-    {{{ ctr γs, RET ctr ; is_counter γs ctr ∗ counter_content γs true 0 }}}.
+    {{{ ctr γs, RET ctr ; is_counter γs ctr ∗ counter_content γs 0 }}}.
   Proof.
-    iIntros (Φ) "_ HΦ". wp_lam. wp_apply wp_fupd.
+    iIntros (?) "#GC". iIntros (Φ) "!# _ HΦ". wp_lam. wp_apply wp_fupd.
     wp_alloc l_n as "Hl_n".
-    wp_alloc l_c as "Hl_c". wp_let.
-    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. }
+    wp_alloc l_c as "Hl_c".
     iMod (own_alloc (● Excl' 0  ⋅ ◯ Excl' 0)) as (γ_n) "[Hn● Hn◯]".
     { by apply auth_both_valid. }
-    iMod (inv_alloc counterN _ (counter_inv γ_b γ_n l_f l_c)
-      with "[Hl_f Hl_c Hl_n Hb● Hn●]") as "#InvC".
+    iMod (inv_alloc counterN _ (counter_inv γ_n l_c)
+      with "[Hl_c Hl_n Hn●]") as "#InvC".
     { iNext. iDestruct "Hl_c" as "[Hl_c1 Hl_c2]".
       iDestruct "Hl_n" as "[??]".
-      iExists true, l_n, (1/2)%Qp, (Quiescent 0). iFrame. }
+      iExists l_n, (1/2)%Qp, (Quiescent 0). iFrame. }
     iModIntro.
-    iApply ("HΦ" $! (#l_f, #l_c)%V (γ_b, γ_n)).
-    iSplitR; last by iFrame. iExists γ_b, γ_n, l_f, l_c. iSplit; done.
-  Qed.
-
-  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 #() >>>.
-  Proof.
-    iIntros "#InvC" (Φ) "AU". iDestruct "InvC" as (γ_b γ_n f_l c_l) "[Heq InvC]".
-    iDestruct "Heq" as %[-> ->]. wp_lam. wp_let. wp_proj.
-    iInv counterN as (b c q s) "(>Hf & >Hc & >[Hl Hl'] & >Hb● & Hrest)".
-    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.
-    iNext. iExists new_b, c, q, _. iFrame. done.
+    iApply ("HΦ" $! #l_c γ_n).
+    iSplitR; last by iFrame. iExists _. eauto with iFrame.
   Qed.
 
   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 >>>.
+    <<< ∀ (n : Z), counter_content γs n >>>
+        get v @⊤∖↑N∖↑gcN
+    <<< counter_content γs n, RET #n >>>.
   Proof.
-    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.
-    iInv counterN as (b c q s) "(>Hf & >Hc & >[Hl [Hl' Hl'']] & >Hb● & Hrest)".
+    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)".
     wp_load.
-    destruct s as [n|n p].
-    - iMod "AU" as (au_b au_n) "[[Hb◯ Hn◯] [_ Hclose]]"; simpl.
+    destruct s as [n|f n p].
+    - iMod "AU" as (au_n) "[Hn◯ [_ Hclose]]"; simpl.
       iDestruct "Hrest" as "[Hc' Hn●]".
       iDestruct (sync_counter_values with "Hn● Hn◯") as %->.
-      iMod ("Hclose" with "[Hn◯ Hb◯]") as "HΦ"; first by iFrame.
+      iMod ("Hclose" with "Hn◯") as "HΦ".
       iModIntro. iSplitR "HΦ Hl'". {
-        iNext. iExists b, c, (q/2)%Qp, (Quiescent au_n). iFrame.
+        iNext. iExists c, (q/2)%Qp, (Quiescent au_n). iFrame.
       }
       wp_let. wp_load. wp_match. iApply "HΦ".
-    - iDestruct "Hrest" as (P Q l_ghost γ_t γ_s) "[#InvS #PAU]".
+    - iDestruct "Hrest" as (P Q l_ghost γ_t γ_s) "(#InvS & #PAU & #Hgc)".
       iModIntro. iSplitR "AU Hl'". {
-        iNext. iExists b, c, (q/2)%Qp, (Updating n p). eauto 10 with iFrame.
+        iNext. iExists c, (q/2)%Qp, (Updating _ _ p). eauto 10 with iFrame.
       }
-      wp_let. wp_load. wp_match. repeat wp_proj. wp_bind (complete _ _ _ _ _)%E.
+      wp_let. wp_load. wp_pures. wp_bind (complete _ _ _ _ _)%E.
       wp_apply complete_spec; [done..|].
       iIntros "Ht". wp_seq. iApply "IH". iApply "AU".
   Qed.
 
 End conditional_counter.
 
-Definition atomic_cinc `{!heapG Σ, cincG Σ} :
+Definition atomic_cinc `{!heapG Σ, !cincG Σ, !gcG Σ} :
   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 |}.
 

theories/logatom/conditional_increment/spec.v

 From stdpp Require Import namespaces.
 From iris.heap_lang Require Export lifting notation.
 From iris.program_logic Require Export atomic.
+From iris_examples.logatom.lib Require Export gc.
 Set Default Proof Using "Type".
 
 (** A general logically atomic interface for conditional increment. *)
-Record atomic_cinc {Σ} `{!heapG Σ} := AtomicCinc {
+Record atomic_cinc {Σ} `{!heapG Σ, !gcG Σ} := AtomicCinc {
   (* -- operations -- *)
   new_counter : val;
   cinc : val;
-  set_flag : val;
   get : val;
   (* -- other data -- *)
   name : Type;
@@ -16,34 +16,31 @@ Record atomic_cinc {Σ} `{!heapG Σ} := AtomicCinc {
   name_countable : Countable name;
   (* -- predicates -- *)
   is_counter (N : namespace) (γs : name) (v : val) : iProp Σ;
-  counter_content (γs : name) (flag : bool) (c : Z) : iProp Σ;
+  counter_content (γs : name) (c : Z) : iProp Σ;
   (* -- predicate properties -- *)
   is_counter_persistent N γs v : Persistent (is_counter N γs v);
-  counter_content_timeless γs f c : Timeless (counter_content γs f c);
-  counter_content_exclusive γs f1 c1 f2 c2 :
-    counter_content γs f1 c1 -∗ counter_content γs f2 c2 -∗ False;
+  counter_content_timeless γs c : Timeless (counter_content γs c);
+  counter_content_exclusive γs  c1 c2 :
+    counter_content γs c1 -∗ counter_content γs c2 -∗ False;
   (* -- operation specs -- *)
   new_counter_spec N :
+    N ## gcN →
+    gc_inv -∗
     {{{ True }}}
         new_counter #()
-    {{{ ctr γs, RET ctr ; is_counter N γs ctr ∗ counter_content γs true 0 }}};
-  cinc_spec N γs v :
+    {{{ ctr γs, RET ctr ; is_counter N γs ctr ∗ counter_content γs 0 }}};
+  cinc_spec N γs v (f : loc) :
     is_counter N γ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 #() >>>;
-  set_flag_spec N γs v (new_b: bool) :
-    is_counter N γs v -∗
-    <<< ∀ (b : bool) (n : Z), counter_content γs b n >>>
-        set_flag v #new_b @⊤∖↑N
-    <<< counter_content γs new_b n, RET #() >>>;
+    <<< ∀ (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 #() >>>;
   get_spec N γs v:
     is_counter N γs v -∗
-    <<< ∀ (b : bool) (n : Z), counter_content γs b n >>>
-        get v @⊤∖↑N
-    <<< counter_content γs b n, RET #n >>>;
+    <<< ∀ (n : Z), counter_content γs n >>>
+        get v @⊤∖↑N∖↑gcN
+    <<< counter_content γs n, RET #n >>>;
 }.
-Arguments atomic_cinc _ {_}.
+Arguments atomic_cinc _ {_ _}.
 
 Existing Instances
   is_counter_persistent counter_content_timeless

theories/logatom/lib/gc.v

@@ -7,7 +7,7 @@ Import uPred.
 
 Definition gcN: namespace := nroot .@ "gc".
 
-Definition gc_mapUR : ucmraT := gmapUR loc $ optionR $ exclR $ valC.
+Definition gc_mapUR : ucmraT := gmapUR loc $ optionR $ exclR $ valO.
 
 Definition to_gc_map (gcm: gmap loc val) : gc_mapUR := (λ v : val, Excl' v) <$> gcm.
 
@@ -112,7 +112,9 @@ Section to_gc_map.
 End to_gc_map.
 
 Section gc.
-  Context `{!invG Σ, !heapG Σ, gG: gcG Σ}.
+  Context `{!invG Σ, !heapG Σ, !gcG Σ}.
+
+  (* FIXME: still needs a constructor. *)
 
   Global Instance is_gc_loc_persistent (l: loc): Persistent (is_gc_loc l).
   Proof. rewrite /is_gc_loc. apply _. Qed.
@@ -158,7 +160,7 @@ Section gc.
     iFrame.
   Qed.
 
-  Lemma is_gc_lookup_Some  l gcm: is_gc_loc l -∗ own (gc_name gG) (● to_gc_map gcm) -∗ ⌜∃ v, gcm !! l = Some v⌝.
+  Lemma is_gc_lookup_Some  l gcm: is_gc_loc l -∗ own (gc_name _) (● to_gc_map gcm) -∗ ⌜∃ v, gcm !! l = Some v⌝.
     iIntros "Hgc_l H◯".
     iCombine "H◯ Hgc_l" as "Hcomb".
     iDestruct (own_valid with "Hcomb") as %Hvalid.
@@ -170,7 +172,7 @@ Section gc.
     by apply leibniz_equiv_iff in Hsome.
   Qed.
 
-  Lemma gc_mapsto_lookup_Some l v gcm: gc_mapsto l v -∗ own (gc_name gG) (● to_gc_map gcm) -∗ ⌜ gcm !! l = Some v ⌝.
+  Lemma gc_mapsto_lookup_Some l v gcm: gc_mapsto l v -∗ own (gc_name _) (● to_gc_map gcm) -∗ ⌜ gcm !! l = Some v ⌝.
   Proof.
     iIntros "Hgc_l H●".
     iCombine "H● Hgc_l" as "Hcomb".
@@ -180,12 +182,17 @@ Section gc.
     by apply gc_map_singleton_included.
   Qed.
 
-  Lemma gc_access l v E:
-    ↑gcN ⊆ E → gc_inv -∗ gc_mapsto l v ={E, E ∖ ↑gcN}=∗ (l ↦ v ∗ (∀ w, l ↦ w ={E ∖ ↑gcN, E}=∗ gc_mapsto l w)).
+  (** An accessor to make use of [gc_mapsto].
+    This opens the invariant *before* consuming [gc_mapsto] so that you can use
+    this before opening an atomic update that provides [gc_mapsto]!. *)
+  Lemma gc_access E:
+    ↑gcN ⊆ E →
+    gc_inv ={E, E ∖ ↑gcN}=∗ ∀ l v, gc_mapsto l v -∗
+      (l ↦ v ∗ (∀ w, l ↦ w ==∗ gc_mapsto l w ∗ |={E ∖ ↑gcN, E}=> True)).
   Proof.
-    iIntros (HN) "#Hinv Hgc_l".
+    iIntros (HN) "#Hinv".
     iMod (inv_open_timeless _ gcN _ with "Hinv") as "[P Hclose]"=>//.
-    iModIntro.
+    iIntros "!>" (l v) "Hgc_l".
     iDestruct "P" as (gcm) "[H● HsepM]".
     iDestruct (gc_mapsto_lookup_Some with "Hgc_l H●") as %Hsome.
     iDestruct (big_sepM_delete with "HsepM") as "[Hl HsepM]"=>//. 
@@ -199,6 +206,7 @@ Section gc.
     iDestruct (big_sepM_insert with "[Hl HsepM]") as "HsepM"; [ | iFrame | ].
     { apply lookup_delete. }
     rewrite insert_delete. rewrite <- to_gc_map_insert.
+    iModIntro. iFrame.
     iMod ("Hclose" with "[H● HsepM]"); [ iExists _; by iFrame | by iModIntro].
   Qed.