diff --git a/theories/logatom/conditional_increment/cinc.v b/theories/logatom/conditional_increment/cinc.v
index bb92592665c97b25116c3b0a9d679dd45cac564a..d3bbb481b6bca95aedca8f920b96ee44db8d3297 100644
--- a/theories/logatom/conditional_increment/cinc.v
+++ b/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 |}.
diff --git a/theories/logatom/conditional_increment/spec.v b/theories/logatom/conditional_increment/spec.v
index e464ff68850e9ff3ecd0e052464b9748a20e01a2..f816f411edaaf096b632359083f832eaf302a66e 100644
--- a/theories/logatom/conditional_increment/spec.v
+++ b/theories/logatom/conditional_increment/spec.v
@@ -1,14 +1,14 @@
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
diff --git a/theories/logatom/lib/gc.v b/theories/logatom/lib/gc.v
index ea371171d649247cb7c77b3933f71787d0602ad5..ecd69be06c92ce1a72d8ce7a720dd3dfcbcaa106 100644
--- a/theories/logatom/lib/gc.v
+++ b/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.