From 67ee87b89f81133970cd7db85ee04b85948b3110 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 11 Jun 2019 18:05:05 +0200
Subject: [PATCH] simplify conditional counter: get rid of histories; instead
of heap metadata for ABA protection
Also needs a new token and splitting ownership of the "main" protocol location.
---
opam | 2 +-
theories/logatom/cinc.v | 922 +++++++++++++---------------------------
2 files changed, 287 insertions(+), 637 deletions(-)
diff --git a/opam b/opam
index 5bc8ccbd..99479444 100644
--- a/opam
+++ b/opam
@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_examples"]
depends: [
- "coq-iris" { (= "dev.2019-06-10.2.47f304f6") | (= "dev") }
+ "coq-iris" { (= "dev.2019-06-11.2.0a05a8c0") | (= "dev") }
"coq-autosubst" { = "dev.coq86" }
]
diff --git a/theories/logatom/cinc.v b/theories/logatom/cinc.v
index 1f010799..a38d36d4 100644
--- a/theories/logatom/cinc.v
+++ b/theories/logatom/cinc.v
@@ -1,4 +1,4 @@
-From iris.algebra Require Import excl auth agree frac list cmra.
+From iris.algebra Require Import excl auth agree frac list cmra csum.
From iris.base_logic.lib Require Export invariants.
From iris.program_logic Require Export atomic.
From iris.proofmode Require Import tactics.
@@ -89,244 +89,20 @@ Definition cinc : val :=
(** ** Proof setup *)
-(** To represent histories of allocated locations, we need some helper lemmas
- about suffixes on lists. *)
-Section suffixes.
-
- Lemma suffix_trans (h1 h2 h3 : list loc) :
- h1 `suffix_of` h2 →
- h2 `suffix_of` h3 →
- h1 `suffix_of` h3.
- Proof.
- intros [? ->] [? ->]. rewrite app_assoc. by eexists.
- Qed.
-
- Lemma suffix_eq (h1 h2 : list loc) :
- h1 `suffix_of` h2 →
- h2 `suffix_of` h1 →
- h1 = h2.
- Proof.
- intros [xs ->] [ys Heq]. rewrite <- app_nil_l in Heq at 1. rewrite app_assoc in Heq.
- apply app_inv_tail, eq_sym in Heq. by apply app_eq_nil in Heq as [_ ->].
- Qed.
-
- Lemma suffix_in (h1 h2 : list loc) l :
- h1 `suffix_of` h2 →
- In l h1 →
- In l h2.
- Proof.
- destruct h1 as [|y ys]; first done.
- intros Hs Hin. destruct Hs as [l2' ->]. apply in_or_app. by right.
- Qed.
-
- Lemma suffix_in_head (h1 h2 : list loc) l :
- h1 `suffix_of` h2 →
- Some l = head h1 →
- In l h2.
- Proof.
- destruct h1 as [|y ys]; first done.
- intros Hs [=->]. eapply suffix_in; first done. apply in_eq.
- Qed.
-
- (** A helper lemma that will come up in the proof of [complete] *)
- Lemma nodup_suffix_contradiction (l1 l2 l3 : loc) (H1 H2 H3 : list loc) :
- Some l1 = hd_error H1 →
- Some l2 = hd_error H2 →
- Some l3 = hd_error H3 →
- In l3 H1 →
- H1 `suffix_of` H2 →
- H2 `suffix_of` H3 →
- l2 ≠l3 →
- NoDup H3 →
- False.
- Proof.
- intros Heq Heq' Heq'' Hin Hs Hs' Hn Hd.
- destruct Hs' as [xs ->]. destruct Hs as [ys ->]. destruct (in_split _ _ Hin) as (x & y & ->).
- do 2 rewrite app_assoc in Hd. apply NoDup_remove_2 in Hd.
- (* xs, ys, and x must be empty *)
- destruct xs as [|x' xs]; last first.
- { simpl in *. inversion Heq''. subst.
- contradict Hd. by left. }
- destruct ys as [|y' ys]; last first.
- { simpl in *. inversion Heq''; subst.
- contradict Hd. by left. }
- destruct x as [|z' zs]; last first.
- { simpl in *. inversion Heq''; subst.
- contradict Hd. by left. }
- simpl in *. inversion Heq'; done.
- Qed.
-
-End suffixes.
-
-(** Resource algebra for histories *)
-Section histories.
-
- Inductive hist :=
- | histv (h : list loc) : hist
- | histbot : hist.
-
- Inductive hist_equiv : Equiv hist :=
- | Hist_equiv h1 h2 : h1 = h2 → h1 ≡ h2.
-
- Existing Instance hist_equiv.
-
- Instance hist_equiv_Equivalence : @Equivalence hist equiv.
- Proof.
- split.
- - move => [|]; by constructor.
- - move => [?|] []; inversion 1; subst; by constructor.
- - move => [?|] [] [];
- inversion 1; inversion 1; subst; by constructor.
- Qed.
-
- Canonical Structure histC : ofeT := discreteC hist.
-
- Instance hist_valid : Valid hist :=
- λ x, match x with histv _ => True | histbot => False end.
-
- Instance hist_op : Op hist := λ h1 h2,
- match h1, h2 with
- | histv h1', histv h2' =>
- if decide (h1' `suffix_of` h2')
- then h2
- else if decide (h2' `suffix_of` h1')
- then h1
- else histbot
- | _, _ =>
- histbot
- end.
-
- Arguments op _ _ !_ !_ /.
-
- Instance hist_PCore : PCore hist := Some.
-
- Global Instance hist_op_comm: Comm equiv hist_op.
- Proof.
- intros [h1|] [h2|]; auto. simpl.
- case_decide as H1; [case_decide as H2|auto]; last auto.
- constructor. destruct H1. subst. destruct H2.
- rewrite <- app_nil_l in H at 1. rewrite app_assoc in H.
- by apply app_inv_tail, eq_sym, app_eq_nil in H as [-> ->].
- Qed.
-
- Global Instance hist_op_idemp : IdemP eq hist_op.
- Proof. intros [|]; [by simpl; rewrite decide_True|auto]. Qed.
-
- Lemma hist_op_l h1 h2 (Le: h1 `suffix_of` h2) :
- histv h1 â‹… histv h2 = histv h2.
- Proof. simpl. case_decide; done. Qed.
-
- Lemma hist_op_r h1 h2 (Le: h1 `suffix_of` h2) :
- histv h2 â‹… histv h1 = histv h2.
- Proof.
- simpl. case_decide.
- - f_equal. by apply suffix_eq.
- - by case_decide.
- Qed.
-
- Global Instance hist_op_assoc: Assoc equiv (op: Op hist).
- Proof.
- intros [h1|] [h2|] [h3|]; eauto; simpl.
- - repeat (case_decide; auto).
- + rewrite !hist_op_l; auto. etrans; eauto.
- + simpl. repeat case_decide; last done.
- * destruct H as [xs ->]. destruct H2 as [ys [[k [->->]] | [k [->->]]]%app_eq_inv].
- ** contradict H1. by apply suffix_app_r.
- ** contradict H0. by apply suffix_app_r.
- * contradict H1. by etrans.
- + rewrite hist_op_l; [by rewrite hist_op_r|auto].
- + rewrite !hist_op_r; auto. by etrans.
- + simpl. rewrite !decide_False; auto.
- + simpl. rewrite !decide_False; auto.
- + simpl. case_decide.
- * exfalso. apply H. by etrans.
- * case_decide; last done. exfalso.
- destruct H4 as [xs ->]. destruct H2 as [ys [[k [->->]] | [k [->->]]]%app_eq_inv].
- ** contradict H0. by apply suffix_app_r.
- ** contradict H. by apply suffix_app_r.
- - simpl. repeat case_decide; auto.
- Qed.
-
- Lemma hist_included h1 h2 :
- histv h1 ≼ histv h2 ↔ h1 `suffix_of` h2.
- Proof.
- split.
- - move => [[?|]]; simpl; last by inversion 1.
- case_decide.
- * inversion 1. naive_solver.
- * case_decide; inversion 1; naive_solver.
- - intros. exists (histv h2). by rewrite hist_op_l.
- Qed.
-
- Lemma hist_valid_op h1 h2 :
- ✓ (histv h1 ⋅ histv h2) → h1 `suffix_of` h2 ∨ h2 `suffix_of` h1.
- Proof. simpl. case_decide; first by left. case_decide; [by right|done]. Qed.
-
- Lemma hist_core_self (X: hist) : core X = X.
- Proof. done. Qed.
-
- Instance hist_unit : Unit hist := histv nil.
-
- Definition hist_ra_mixin : RAMixin hist.
- Proof.
- apply ra_total_mixin; eauto.
- - intros [?|] [?|] [?|]; auto; inversion 1; naive_solver.
- - by destruct 1; constructor.
- - destruct 1. naive_solver.
- - apply hist_op_assoc.
- - apply hist_op_comm.
- - intros ?. by rewrite hist_core_self idemp_L.
- - intros [|] [|]; simpl; done.
- Qed.
-
- Canonical Structure histR := discreteR hist hist_ra_mixin.
-
- Global Instance hist_cmra_discrete : CmraDiscrete histR.
- Proof. apply discrete_cmra_discrete. Qed.
-
- Global Instance hist_core (h: hist) : CoreId h.
- Proof.
- rewrite /CoreId. reflexivity.
- Qed.
-
- Definition hist_ucmra_mixin : UcmraMixin hist.
- Proof.
- split; [done| |auto]. intros [|]; [simpl|done]. done.
- Qed.
-
- Lemma hist_local_update h1 X h2 :
- h1 `suffix_of` h2 → (histv h1, X) ~l~> (histv h2, histv h2).
- Proof.
- intros Le. rewrite local_update_discrete.
- move => [[h3|]|] /= ? Eq; split => //; last first; move : Eq.
- - destruct X; by inversion 1.
- - destruct X; rewrite /cmra_op /= => Eq;
- repeat case_decide; auto; inversion Eq; subst; try naive_solver.
- + constructor. inversion H1. subst. f_equal. by apply suffix_eq.
- + constructor. inversion H2. subst. f_equal. apply suffix_eq; by etrans.
- + inversion H3; subst. by apply (suffix_trans _ _ _ H0) in Le.
- Qed.
-
- Canonical Structure histUR := UcmraT hist hist_ucmra_mixin.
-
-End histories.
-
-Definition histListUR := optionUR $ prodR fracR $ agreeR $ listC locC.
-
-Definition historyUR := prodUR (authUR histListUR) (authUR histUR).
-Definition flagUR := authR $ optionUR $ exclR boolC.
-Definition numUR := authR $ optionUR $ exclR ZC.
-Definition tokenUR := authR $ optionUR $ exclR valC.
+Definition flagUR := authR $ optionUR $ exclR boolC.
+Definition numUR := authR $ optionUR $ exclR ZC.
+Definition tokenUR := exclR unitC.
+Definition one_shotUR := csumR (exclR unitC) (agreeR unitC).
Class cincG Σ := ConditionalIncrementG {
- cinc_historyG :> inG Σ historyUR;
- cinc_flagG :> inG Σ flagUR;
- cinc_numG :> inG Σ numUR;
- cinc_tokenG :> inG Σ tokenUR;
+ cinc_flagG :> inG Σ flagUR;
+ cinc_numG :> inG Σ numUR;
+ cinc_tokenG :> inG Σ tokenUR;
+ cinc_one_shotG :> inG Σ one_shotUR;
}.
Definition cincΣ : gFunctors :=
- #[GFunctor historyUR; GFunctor flagUR; GFunctor numUR; GFunctor tokenUR].
+ #[GFunctor flagUR; GFunctor numUR; GFunctor tokenUR; GFunctor one_shotUR].
Instance subG_cincΣ {Σ} : subG cincΣ Σ → cincG Σ.
Proof. solve_inG. Qed.
@@ -338,84 +114,7 @@ Section conditional_counter.
Local Definition stateN := N .@ "state".
Local Definition counterN := N .@ "counter".
- Definition token : tokenUR :=
- â— Excl' #().
-
- Definition histList (H : list loc) (q : Qp) : histListUR :=
- Some (q, to_agree H).
-
- Definition half_history_frag (H : list loc) : historyUR :=
- (â—¯ (histList H (1/2)%Qp), â—¯ (histv H)).
-
- Definition full_history_frag (H : list loc) : historyUR :=
- (â—¯ (histList H 1%Qp), â—¯ (histv H)).
-
- Definition full_history_auth (H : list loc) : historyUR :=
- (â— (histList H 1%Qp), â— (histv H)).
-
- Definition hist_snapshot H : historyUR :=
- (â—¯ None, â—¯ histv H).
-
- Global Instance snapshot_persistent H γ_h : Persistent (own γ_h (hist_snapshot H)).
- Proof.
- apply own_core_persistent. rewrite /CoreId. done.
- Qed.
-
- (** Updating and synchronizing history RAs *)
-
- Lemma sync_histories H1 H2 γ_h :
- own γ_h (half_history_frag H1) -∗ own γ_h (half_history_frag H2) -∗ ⌜H1 = H2âŒ.
- Proof.
- iIntros "H1 H2". iCombine "H1" "H2" as "H". iPoseProof (own_valid with "H") as "H".
- iDestruct "H" as %H. iPureIntro. destruct H as [[_ Hl1%agree_op_inv] _].
- by apply to_agree_inj, leibniz_equiv in Hl1.
- Qed.
-
- Lemma add_half_histories (H : list loc) γ_h :
- own γ_h (half_history_frag H) -∗
- own γ_h (half_history_frag H) -∗
- own γ_h (full_history_frag H).
- Proof.
- iIntros "H1 H2". iCombine "H1" "H2" as "H". done.
- Qed.
-
- Lemma update_history H H' l γ_h :
- own γ_h (full_history_auth H) -∗
- own γ_h (half_history_frag H) -∗
- own γ_h (half_history_frag H') ==∗
- own γ_h (full_history_auth (l :: H)) ∗
- own γ_h (half_history_frag (l :: H)) ∗
- own γ_h (half_history_frag (l :: H)).
- Proof.
- iIntros "Hâ— H1â—¯ H2â—¯". iDestruct (sync_histories with "H1â—¯ H2â—¯") as %<-.
- iDestruct (add_half_histories with "H1â—¯ H2â—¯") as "Hâ—¯".
- iCombine "Hâ— Hâ—¯" as "H". rewrite -own_op -own_op.
- iApply (own_update with "H"). apply prod_update.
- - apply auth_update, option_local_update. rewrite pair_op frac_op' agree_idemp.
- rewrite Qp_div_2. apply exclusive_local_update. by constructor.
- - apply auth_update. simpl. rewrite hist_op_l; last done.
- by apply hist_local_update, suffix_cons_r.
- Qed.
-
- Lemma sync_snapshot H1 H2 H2' γ_h :
- own γ_h (full_history_auth H1) -∗ own γ_h (â—¯ H2', â—¯ histv H2) -∗ ⌜H2 `suffix_of` H1âŒ.
- Proof.
- iIntros "Hâ— Hâ—¯". iCombine "Hâ—" "Hâ—¯" as "H".
- by iDestruct (own_valid with "H") as %[_ [Hs%hist_included _]%auth_both_valid].
- Qed.
-
- Lemma extract_snapshot H γ_h :
- own γ_h (half_history_frag H) -∗ □ own γ_h (hist_snapshot H).
- Proof.
- iIntros "H".
- iAssert (own γ_h (half_history_frag H) ∗ own γ_h (hist_snapshot H))%I with "[H]" as "[_ H2]".
- { rewrite -own_op pair_op.
- assert (â—¯ histList H (1 / 2) â‹… â—¯ None = â—¯ (histList H (1 / 2) â‹… None)) as Heq by apply auth_frag_op.
- assert (â—¯ histv H â‹… â—¯ histv H = â—¯ (histv H â‹… histv H)) as Heq' by apply auth_frag_op.
- rewrite Heq Heq' right_id. rewrite <- core_id_dup; first done. by rewrite /CoreId. }
- rewrite intuitionistically_into_persistently.
- by iApply persistent.
- Qed.
+ (** Updating and synchronizing the counter and flag RAs *)
Lemma sync_counter_values γ_n (n m : Z) :
own γ_n (â— Excl' n) -∗ own γ_n (â—¯ Excl' m) -∗ ⌜n = mâŒ.
@@ -424,9 +123,6 @@ Section conditional_counter.
by iDestruct "H" as %[H%Excl_included%leibniz_equiv _]%auth_both_valid.
Qed.
-
- (** Updating and synchronizing the counter and flag RAs *)
-
Lemma sync_flag_values γ_n (b1 b2 : bool) :
own γ_n (â— Excl' b1) -∗ own γ_n (â—¯ Excl' b2) -∗ ⌜b1 = b2âŒ.
Proof.
@@ -448,8 +144,8 @@ Section conditional_counter.
by apply auth_update, option_local_update, exclusive_local_update.
Qed.
- Definition counter_content (γs : gname * gname * gname) (c : bool * Z) :=
- (own γs.1.2 (◯ Excl' c.1) ∗ own γs.2 (◯ Excl' c.2))%I.
+ Definition counter_content (γs : gname * gname) (c : bool * Z) :=
+ (own γs.1 (◯ Excl' c.1) ∗ own γs.2 (◯ Excl' c.2))%I.
(** Definition of the invariant *)
@@ -474,55 +170,84 @@ Section conditional_counter.
destruct l0; try by right. simpl in H. inversion H. by left.
Qed.
+ (** Removing a #false does not change the result. *)
+ Lemma val_to_loc_pop_false vs (l : loc) :
+ val_to_some_loc ((#false, #l)::vs) = val_to_some_loc vs.
+ Proof. reflexivity. Qed.
+
Inductive abstract_state : Set :=
| injl : Z → abstract_state
| injr : Z → proph_id → abstract_state.
- Definition own_token γ_t := (own γ_t token)%I.
+ Definition state_to_val (s : abstract_state) : val :=
+ match s with
+ | injl n => InjLV #n
+ | injr n p => InjRV (#n,#p)
+ end.
- Definition used_up l γ_h :=
- (∃ H, â–¡ own γ_h (hist_snapshot H) ∗ ⌜In l H ∧ Some l ≠head HâŒ)%I.
+ Global Instance state_to_val_inj : Inj (=) (=) state_to_val.
+ Proof.
+ intros [|] [|]; simpl; intros Hv; inversion_clear Hv; done.
+ Qed.
- Definition not_done_state H l (γ_h : gname) :=
- (own γ_h (half_history_frag H) ∗ ⌜Some l = head HâŒ)%I.
+ Definition own_token γ := (own γ (Excl ()))%I.
- Definition pending_state P (n : Z) vs l_ghost (γ_h γ_n : gname) :=
- (P ∗ ⌜match val_to_some_loc vs with None => True | Some l => l = l_ghost end⌠∗ own γ_n (◠Excl' n))%I.
+ Definition loc_token (l: loc) := (∃ γ, meta l N γ ∗ own_token γ)%I.
- Definition accepted_state Q vs (l l_ghost : loc) (γ_h : gname) :=
- (l_ghost ↦{1/2} - ∗ match val_to_some_loc vs with None => True | Some l => ⌜l = l_ghost⌠∗ Q end)%I.
+ 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.
- Definition done_state Q (l l_ghost : loc) (γ_t γ_h : gname) :=
- ((Q ∨ own_token γ_t) ∗ l_ghost ↦ - ∗ used_up l γ_h)%I.
+ (* 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.
- Definition state_inv P Q (p : proph_id) n l l_ghost H γ_h γ_n γ_t : iProp Σ :=
+ (* 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
+ only the CAS winner can transition to here, and [loc_token l] serves as a
+ "location" token to ensure there is no ABA going on. *)
+ Definition done_state Q (l l_ghost_winner : loc) (γ_t : gname) :=
+ ((Q ∨ own_token γ_t) ∗ l_ghost_winner ↦ - ∗ loc_token l)%I.
+
+ (* 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 Σ :=
(∃ vs, proph p vs ∗
- ((not_done_state H l γ_h ∗
- ( pending_state P n vs l_ghost γ_h γ_n
- ∨ accepted_state Q vs l l_ghost γ_h ))
- ∨ done_state Q l l_ghost γ_t γ_h))%I.
+ (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.
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 counter_inv γ_h γ_b γ_n f c :=
- (∃ (b : bool) (l : loc) (H : list loc) (q : Qp) (v : val),
- f ↦ #b ∗ c ↦ #l ∗ l ↦{q} v ∗
- own γ_h (full_history_auth H) ∗
- own γ_h (half_history_frag H) ∗
- ([∗ list] l ∈ H, ∃ q, l ↦{q} -) ∗
- ⌜Some l = head H ∧ NoDup H⌠∗
+ Definition counter_inv γ_b γ_n f c :=
+ (∃ (b : bool) (l : loc) (q : Qp) (s : abstract_state),
+ f ↦ #b ∗ c ↦{1/2} #l ∗ l ↦{q} (state_to_val s) ∗
own γ_b (◠Excl' b) ∗
- ((∃ (n : Z), ⌜v = InjLV #n⌠∗ own γ_h (half_history_frag H) ∗ own γ_n (◠Excl' n)) ∨
- (∃ (n : Z) (p : proph_id), ⌜v = InjRV(#n,#p)⌠∗
- ∃ P Q l_ghost γ_t, inv stateN (state_inv P Q p n l l_ghost H γ_h γ_n γ_t) ∗
- □ pau P Q (γ_h, γ_b, γ_n))))%I.
-
- Definition is_counter (γs : gname * gname * gname) (ctr : val) :=
- (∃ (γ_h γ_b γ_n : gname) (f c : loc),
- ⌜γs = (γ_h, γ_b, γ_n) ∧ ctr = (#f, #c)%V⌠∗
- inv counterN (counter_inv γ_h γ_b γ_n f c))%I.
+ loc_token l ∗ (* the "location" token for ABA protection; also see [done_state] *)
+ 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.
+
+ 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.
Global Instance is_counter_persistent γs ctr : Persistent (is_counter γs ctr) := _.
@@ -540,233 +265,193 @@ Section conditional_counter.
apply (iffLR (frac_valid' _)) in Hv. by apply Qp_not_plus_q_ge_1 in Hv.
Qed.
- Instance in_dec (l : loc) H: Decision (In l H).
+ Lemma loc_token_exclusive l :
+ loc_token l -∗ loc_token l -∗ False.
Proof.
- induction H as [|a H IH].
- - right. naive_solver.
- - destruct (decide (l = a)).
- + left. naive_solver.
- + destruct IH; [ left | right]; naive_solver.
+ iIntros "Hl1 Hl2".
+ iDestruct "Hl1" as (γ1) "[Hm1 Ht1]".
+ iDestruct "Hl2" as (γ2) "[Hm2 Ht2]".
+ iDestruct (meta_agree with "Hm1 Hm2") as %->.
+ iDestruct (own_valid_2 with "Ht1 Ht2") as %Hcontra.
+ by inversion Hcontra.
Qed.
- Lemma nodup_fresh_loc l v H:
- NoDup H → l ↦ v -∗ ([∗ list] l ∈ H, ∃ q, l ↦{q} -) -∗ ⌜NoDup (l :: H)âŒ.
+ Lemma loc_token_alloc v :
+ {{{ True }}} ref v {{{ l, RET #l; l ↦ v ∗ loc_token l }}}.
Proof.
- intros Hd. iIntros "Hl Hls".
- destruct (decide (In l H)) as [(x1 & x2 & ->)%in_split | Hn%NoDup_cons]; last done.
- - destruct x1 as [|x1 x1s];
- [ rewrite app_nil_l in Hd; rewrite app_nil_l; iDestruct "Hls" as "[Hl' _]" |
- iDestruct "Hls" as "[_ [Hl' _]]" ];
- iDestruct "Hl'" as (q v') "Hl'";
- by iDestruct (mapsto_valid_3 with "Hl Hl'") as %?.
- - by iPureIntro.
+ iIntros (Φ) "HT HΦ". iApply wp_fupd.
+ wp_apply (wp_alloc with "HT"). iIntros (l_new) "[Hl_new Hm_new]".
+ iMod (own_alloc (Excl ())) as (γ_l) "Htok"; first done.
+ iMod ((meta_set _ _ γ_l N) with "Hm_new") as "Hm"; first done.
+ iApply "HΦ". iFrame "Hl_new". iExists _. by iFrame.
Qed.
+ (** 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.
(** ** Proof of [complete] *)
- (** The part of [complete] for the succeeding thread that moves from [pending] to [accepted] state *)
-
- Lemma complete_succeeding_thread_pending γ_h γ_b γ_n γ_t f_l c_l P Q p (m n : Z) l l_ghost l_new H Φ :
- Some l = head H →
- inv counterN (counter_inv γ_h γ_b γ_n f_l c_l) -∗
- inv stateN (state_inv P Q p m l l_ghost H γ_h γ_n γ_t) -∗
- pau P Q (γ_h, γ_b, γ_n) -∗
+ (** 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) -∗
l_ghost ↦{1 / 2} #() -∗
- ((own_token γ_t ={⊤}=∗ ▷ Q) -∗ Φ #()) -∗
+ (□(own_token γ_t ={⊤}=∗ ▷ Q) -∗ Φ #()) -∗
own γ_n (◠Excl' n) -∗
l_new ↦ InjLV #n -∗
+ loc_token l_new -∗
WP Resolve (CAS #c_l #l #l_new) #p #l_ghost ;; #() {{ v, Φ v }}.
Proof.
- iIntros (Heq) "#InvC #InvS PAU Hl_ghost HQ Hnâ— Hl_new". wp_bind (Resolve _ _ _)%E.
- iInv counterN as (b' l' H' q v) "[>Hf [>Hc [>Hl' [>Hâ— [>Hâ—¯ [>HlH [>Heq [Hbâ— Hrest]]]]]]]]".
- iDestruct "Heq" as %[Heq'' Hd']. simpl.
- iDestruct ((nodup_fresh_loc _ _ _ Hd') with "Hl_new HlH") as %Hd''.
- (* It must be that l' = l because we are in the succeeding thread. *)
- destruct (decide (l' = l)) as [->|HNeq]; last first. {
- iInv stateN as (vs') "[>Hp' [[>[Hhâ—¯ _] State] | Done]]".
- - iDestruct "State" as "[Pending | Accepted]".
- + iDestruct "Pending" as "[_ >[_ Hnâ—']]".
- iCombine "Hnâ—'" "Hnâ—" as "Contra".
- iDestruct (own_valid with "Contra") as %Contra. by inversion Contra.
- + iDestruct (sync_histories with "Hhâ—¯ Hâ—¯") as %->.
- rewrite <- Heq'' in Heq. by inversion Heq.
- - iDestruct "Done" as "[_ >[Hlghost _]]".
- wp_apply (wp_resolve with "Hp'"); first done. wp_cas_fail.
- iDestruct "Hlghost" as (?) "Hlghost".
- by iDestruct (mapsto_valid_2 with "Hlghost Hl_ghost") as %?.
- }
- (* To apply the CAS, we need the prophecy variable, so we open the state invariant. *)
- iInv stateN as (vs') "[>Hp' [[>[Hhâ—¯ Heq'] State] | Done]]".
- - iDestruct "State" as "[Pending | Accepted]".
- + (* Pending: contradiction. *)
- iDestruct "Pending" as "[_ >[_ Hnâ—']]".
- iCombine "Hnâ—" "Hnâ—'" as "Contra".
- iDestruct (own_valid with "Contra") as %Contra. by inversion Contra.
- + (* We perform the CAS. *)
- iDestruct (sync_histories with "Hâ—¯ Hhâ—¯") as %->.
- wp_apply (wp_resolve with "Hp'"); first done; wp_cas_suc.
- destruct (val_to_some_loc vs') eqn:Hvtsl; last first. {
- (* Wrong prophecy: contradiction. *)
- iIntros (vs ->). inversion Hvtsl.
- }
- (* Update to Done. *)
- iDestruct "Accepted" as "[Hl_ghost_inv H]".
- rewrite Hvtsl. iDestruct "H" as "[HEq Q]".
- (* The first element of H is l. *)
- destruct H as [|l' H]; inversion Heq; subst l'.
- (* And we have l ≠l_new. *)
- destruct (decide (l = l_new)) as [->|HNeq]. {
- iDestruct "HlH" as "[Hl HlH]". iDestruct "Hl" as (q' v') "Hl".
- by iDestruct (mapsto_valid_3 with "Hl_new Hl") as %Contra.
- }
- (* Update histories. *)
- iDestruct (update_history _ _ l_new with "Hâ— Hâ—¯ Hhâ—¯") as ">[Hhâ— [Hâ—¯ Hâ—¯']]".
- iIntros (pv' ->) "Hp". iModIntro.
- (* Extract snapshot to prove used_up. *)
- iDestruct (extract_snapshot with "Hâ—¯'") as "#Hs".
- iSplitL "Hl_ghost_inv Hl_ghost Q Hp".
- (* Update state to Done. *)
- { iNext. iExists _. iSplitL "Hp"; first done. repeat iRight.
- iDestruct "Hl_ghost_inv" as (v'') "Hl_ghost''".
- iDestruct (mapsto_agree with "Hl_ghost Hl_ghost''") as %<-.
- iCombine "Hl_ghost" "Hl_ghost''" as "Hl_ghost'".
- iSplitL "Q"; first by iFrame. iSplitL "Hl_ghost'"; first by eauto.
- iExists (l_new :: l :: H). iSplit; first done. iPureIntro.
- split; first by apply in_cons, in_eq. by intros [=->]. }
- iModIntro. iSplitR "HQ".
- { iNext. iExists _, _, _, _, _. iSplitL "Hf"; first done.
- iSplitL "Hc"; first done. iDestruct "Hl_new" as "[$ Hl_new]".
- iSplitL "Hhâ—"; first done. iSplitL "Hâ—¯'"; first done.
- iSplitL "HlH Hl_new". { iSplitL "Hl_new"; first by iExists _, _. iFrame. }
- iSplit; first done. iSplitL "Hbâ—"; first done. iLeft. iExists n. by iFrame. }
- iApply wp_fupd. wp_seq. iApply "HQ". iModIntro. iIntros "Ht".
- iInv stateN as (vs') "[>Hp' [[>[Hhâ—¯ Heq'] _] | Done]]".
- * iInv counterN as (b5 l5 H5 q5 v5) "[>Hf [>Hc [>Hl [>Hâ— [>Hâ—¯ _]]]]]".
- iDestruct (sync_histories with "Hâ—¯ Hhâ—¯") as %->.
- by iDestruct (sync_snapshot with "Hâ— Hs") as %?%suffix_cons_not.
- * iDestruct "Done" as "[QT [>Hlghost Usedup]]".
- iModIntro. iDestruct (later_intro with "Ht") as "Ht".
- iDestruct (later_or with "QT") as "[Q | T]"; last first.
- { iCombine "Ht" "T" as "Contra". iDestruct (own_valid with "Contra") as "#Contra'".
- iSplitL; try iModIntro; try iNext; iDestruct "Contra'" as %Contra;
- by inversion Contra. }
- iSplitR "Q"; last done. iNext. iExists _. iSplitL "Hp'"; first done.
- repeat iRight. iFrame.
- - (* Done: contradiction. *)
- iDestruct "Done" as "[QT [>Hlghost Usedup]]".
- iDestruct "Hlghost" as (v') "Hlghost".
+ iIntros "#InvC #InvS PAU Hl_ghost HQ Hnâ— Hlntok Hl_new". wp_bind (Resolve _ _ _)%E.
+ iInv counterN as (b' l' q s) "(>Hf & >Hc & >Hl' & Hbâ— & Hltok & 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. *)
+ iDestruct "Done" as "(_ & _ & Hlghost & _)".
+ iDestruct "Hlghost" as (v') ">Hlghost".
by iDestruct (mapsto_valid_2 with "Hl_ghost Hlghost") as %?.
+ }
+ 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.
+ iSplitL "Hl_ghost_inv Hl_ghost Q Hltok Hp'".
+ (* Update state to Done. *)
+ { iNext. iExists _. iFrame "Hp'". iRight. unfold done_state.
+ iFrame "#∗". iExists _. done. }
+ 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.
Qed.
(** The part of [complete] for the failing thread *)
-
- Lemma complete_failing_thread γ_h γ_b γ_n γ_t f_l c_l l1 l H1 H P Q p m n l_ghost_inv l_ghost l_new Φ :
- Some l1 = head H1 →
- In l H1 →
+ 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 Φ :
l_ghost_inv ≠l_ghost →
- inv counterN (counter_inv γ_h γ_b γ_n f_l c_l) -∗
- inv stateN (state_inv P Q p m l l_ghost_inv H γ_h γ_n γ_t) -∗
- pau P Q (γ_h, γ_b, γ_n) -∗
- □ own γ_h (hist_snapshot H1) -∗
- ((own_token γ_t ={⊤}=∗ ▷ Q) -∗ Φ #()) -∗
+ 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) -∗ Φ #()) -∗
l_new ↦ InjLV #n -∗
WP Resolve (CAS #c_l #l #l_new) #p #l_ghost ;; #() {{ v, Φ v }}.
Proof.
- iIntros (Heq Hin Hnl) "#InvC #InvS PAU #Hs1 HQ Hl_new". wp_bind (Resolve _ _ _)%E.
- iInv counterN as (b l' H' q v) "[>Hf [>Hc [>Hl [>Hâ— [>Hâ—¯ [HlH [>Heq [Hbâ— Hrest]]]]]]]]".
- iDestruct (extract_snapshot with "Hâ—¯") as "#Hs2".
- iDestruct (sync_snapshot with "Hâ— Hs1") as %H12.
- (* It must be that l' = l because we are in the succeeding thread. *)
- destruct (decide (l' = l)) as [->|Hn]. {
- iInv stateN as (vs') "[>Hp' [[>[Hhâ—¯ _] State] | Done]]".
- - wp_apply (wp_resolve with "Hp'"); first done; wp_cas_suc. iIntros (vs ->).
- iDestruct "State" as "[Pending | Accepted]".
+ iIntros (Hnl) "#InvC #InvS PAU HQ Hl_new". wp_bind (Resolve _ _ _)%E.
+ iInv counterN as (b' l' q s) "(>Hf & >Hc & >Hl' & >Hbâ— & >Hltok & 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
+ 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]".
+ iDestruct "Pending" as "[_ [Hvs _]]". iDestruct "Hvs" as %Hvs. by inversion Hvs.
- + iDestruct "Accepted" as "[_ [Hvs _]]". iDestruct "Hvs" as %Hvs. by inversion Hvs.
- - iDestruct "Done" as "[QT [>Hlghost Usedup]]".
- iDestruct "Usedup" as (H'') "[Hs >Usedup]".
- iDestruct "Usedup" as %[Hin' Hn].
- iDestruct "Heq" as %[Heq' Hd'].
- iMod (intuitionistically_elim with "Hs") as "Hs".
- iDestruct (sync_snapshot with "Hâ— Hs") as %Hs'.
- destruct Hs' as [xs ->]. destruct (in_split _ _ Hin) as (x & y & ->).
- destruct xs as [|z zs]; first done.
- simpl in *. inversion Heq'; subst. destruct (in_split _ _ Hin') as (x1 & x2 & ->).
- rewrite app_comm_cons in Hd'. rewrite app_assoc in Hd'.
- apply (NoDup_remove _ _ _) in Hd' as [_ Contra].
- rewrite <- app_comm_cons in Contra. simpl in *. exfalso. eauto.
+ + 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
+ of the [counter]? Impossible, we got the location token for that! *)
+ iDestruct "Done" as "(_ & _ & >Hltok')".
+ iDestruct (loc_token_exclusive with "Hltok Hltok'") as "[]".
}
(* The CAS fails. *)
- iInv stateN as (vs') "[>Hp' State]".
- wp_apply (wp_resolve with "Hp'"); first done. wp_cas_fail.
- iDestruct (extract_snapshot with "Hâ—¯") as "#Hs".
- iIntros (vs ->) "Hp". iModIntro. iDestruct "Heq" as %[Heq' Hd'].
- iSplitL "State Hp". { iNext. iExists vs. iFrame. } iModIntro.
- iSplitL "Hf Hc Hl Hâ— Hâ—¯ HlH Hbâ— Hrest". { iNext. iExists _, _, _, _. eauto with iFrame. }
- wp_seq. iApply "HQ". iIntros "Ht".
- iInv counterN as (b3 l3 H3 q3 v3) "[>Hf [>Hc [>Hl [>Hâ— [>Hâ—¯ [HlH [>Heq [Hbâ— Hrest]]]]]]]]".
- iDestruct "Heq" as %[Heq'' Hd''].
- iInv stateN as (vs') "[>Hp' [[>[Hhâ—¯ Heq'] _] | Done]]".
- - iDestruct (sync_histories with "Hâ—¯ Hhâ—¯") as %->.
- iDestruct (sync_snapshot with "Hâ— Hs") as %Hs.
- iDestruct "Heq'" as %Heq'''. rewrite <- Heq'' in Heq'''.
- inversion Heq'''. subst. exfalso.
- by eapply (nodup_suffix_contradiction _ _ _ _ _ _ Heq Heq' Heq'').
- - iDestruct "Done" as "[[Q | >T] Hrest']"; iModIntro.
- + iSplitL "Ht Hp' Hrest'".
- { iNext. iExists _. iSplitL "Hp'"; first done. repeat iRight. iFrame. }
- iModIntro. iSplitR "Q"; last done. iNext. iExists _, _, _, _. eauto with iFrame.
- + iCombine "T" "Ht" as "Contra".
- iDestruct (own_valid with "Contra") as %Contra. by inversion Contra.
+ 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' Hltok". { iNext. iExists _, _, _, _. iFrame. }
+ wp_seq. iApply "HQ".
+ iApply state_done_extract_Q; done.
Qed.
(** ** Proof of [complete] *)
-
- Lemma complete_spec (c f l : loc) H (n : Z) (p : proph_id) γs γ_t l_ghost_inv P Q :
+ (* 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. *)
+ Lemma complete_spec (c f l : loc) (n : Z) (p : proph_id) γs γ_t γ_s l_ghost_inv P Q :
is_counter γs (#f, #c) -∗
- inv stateN (state_inv P Q p n l l_ghost_inv H γs.1.1 γs.2 γ_t) -∗
+ inv stateN (state_inv P Q p n c l l_ghost_inv γs.2 γ_t γ_s) -∗
□ pau P Q γs -∗
{{{ True }}}
complete #c #f #l #n #p
- {{{ RET #(); own_token γ_t ={⊤}=∗ ▷Q }}}.
+ {{{ RET #(); □ (own_token γ_t ={⊤}=∗ ▷Q) }}}.
Proof.
- iIntros "#InvC #InvS #PAU". destruct γs as [[γ_h γ_b] γ_n].
- iDestruct "InvC" as (??? f_l c_l [[=<-<-<-][=->->]]) "#InvC".
+ iIntros "#InvC #InvS #PAU". destruct γs as [γ_b γ_n].
+ iDestruct "InvC" as (?? f_l c_l [[=<-<-][=->->]]) "#InvC".
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 (b1 l1 H1 q1 v1) "[>Hf [>Hc [>Hl [>Hâ— [>Hâ—¯ [Hlh1 [>Heq [Hbâ— Hrest]]]]]]]]".
- iDestruct "Heq" as %[Heq Hd]. wp_load.
+ iInv counterN as (b' l' q s) "(>Hf & >Hc & >Hl' & >Hbâ— & >Hltok & Hrest)".
+ wp_load.
(* two different proofs depending on whether we are succeeding thread *)
destruct (decide (l_ghost_inv = l_ghost)) as [-> | Hnl].
- (* we are the succeeding thread *)
- (* we need to move from pending to accepted. *)
- iInv stateN as (vs') "[>Hp' [[>[Hhâ—¯ Heq] [Pending | Accepted]] | Done]]".
+ (* we need to move from [pending] to [accepted]. *)
+ iInv stateN as (vs) "(>Hp & [(>Hs & >Hc' & [Pending | Accepted]) | [#Hs Done]])".
+ (* Pending: update to accepted *)
- iDestruct "Pending" as "[P >[Hvs Hnâ—]]". iDestruct "Heq" as %Heq'.
+ iDestruct "Pending" as "[P >[Hvs Hnâ—]]".
iDestruct ("PAU" with "P") as ">AU".
- (* open AU, sync flag and counter *)
+ (* 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 %->.
iDestruct (sync_counter_values with "Hnâ— Hnâ—¯") as %->.
- iDestruct (sync_histories with "Hâ—¯ Hhâ—¯") as %->.
- rewrite <- Heq in Heq'. inversion_clear Heq'; subst.
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 *)
- iModIntro. iSplitL "Q Hâ—¯ Hl_ghost' Hp' Hvs".
- { iNext. iExists _. iSplitL "Hp'"; first done. iLeft.
- iSplitL "Hâ—¯"; first by iFrame. iRight. iSplitL "Hl_ghost'"; first by iExists _.
- destruct (val_to_some_loc vs') eqn:Hvts; iFrame. }
+ 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. }
(* close outer inv *)
iModIntro. iSplitR "Hl_ghost'2 HQ Hnâ—".
- { iNext. iExists _, _, _, _, _. iFrame. done. }
- destruct b2; wp_if; [ wp_op | .. ]; wp_alloc l_new as "Hl_new"; wp_pures;
- iApply ((complete_succeeding_thread_pending _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ Heq)
- with "InvC InvS PAU Hl_ghost'2 HQ Hnâ— Hl_new").
+ { iNext. iExists _, _, _, _. iFrame. done. }
+ destruct b2; wp_if; [ wp_op | .. ];
+ wp_apply (loc_token_alloc with "[//]"); iIntros (l_new) "[Hl_new Hm_new]";
+ wp_pures;
+ iApply (complete_succeeding_thread_pending
+ with "InvC InvS PAU Hl_ghost'2 HQ Hnâ— Hl_new Hm_new").
+ (* Accepted: contradiction *)
iDestruct "Accepted" as "[>Hl_ghost_inv _]".
iDestruct "Hl_ghost_inv" as (v) "Hlghost".
@@ -778,32 +463,13 @@ Section conditional_counter.
iCombine "Hl_ghost'" "Hl_ghost'2" as "Hl_ghost'".
by iDestruct (mapsto_valid_2 with "Hlghost Hl_ghost'") as %?.
- (* we are the failing thread *)
- (* extract history and assert that it contains l *)
- iDestruct (extract_snapshot with "Hâ—¯") as "#Hs1".
- iAssert (|={⊤ ∖ ↑counterN}=> (⌜In l H1⌠∗ own γ_h (full_history_auth H1)))%I with "[Hâ—]" as "Hin". {
- iInv stateN as (vs') "[>Hp' [[>[Hhâ—¯ Heq'] State] | Done]]".
- - iDestruct (sync_snapshot with "Hâ— Hhâ—¯") as %Hs1. iDestruct "Heq'" as %Heq'.
- iModIntro. iSplitR "Hâ—".
- { iNext. iExists _. iSplitL "Hp'"; first done. iLeft. iFrame. done. }
- iModIntro. iFrame. iPureIntro. by eapply suffix_in_head.
- - iDestruct "Done" as "[QT [>Hlghost Usedup]]".
- iDestruct "Usedup" as (H') "[Hs >Usedup]". iDestruct "Usedup" as %[Hin Hn].
- iMod (intuitionistically_elim with "Hs") as "Hs".
- iDestruct (sync_snapshot with "Hâ— Hs") as %Hs'.
- iModIntro. iSplitR "Hâ—".
- { iNext. iExists _. iSplitL "Hp'"; first done. repeat iRight. iFrame.
- iExists _. iSplit; last by iPureIntro. iDestruct "Hs" as "#Hs". iModIntro.
- iApply "Hs". }
- iModIntro. iSplit; last done.
- iPureIntro. by eapply suffix_in.
- }
(* close invariant *)
- iMod "Hin" as (Hin) "Hâ—". iModIntro.
- iSplitL "Hf Hc Hâ— Hâ—¯ Hbâ— Hrest Hl Hlh1". { iNext. iExists _, _, _, _. eauto with iFrame. }
+ iModIntro.
+ iSplitL "Hf Hc Hrest Hl' Hbâ— Hltok". { iNext. iExists _, _, _, _. iFrame. }
(* two equal proofs depending on value of b1 *)
- destruct b1; wp_if; [ wp_op | ..]; wp_alloc Hl_new as "Hl_new"; wp_pures;
- iApply ((complete_failing_thread _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ Heq Hin Hnl)
- with "InvC InvS PAU Hs1 HQ Hl_new").
+ 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.
Qed.
(** ** Proof of [cinc] *)
@@ -814,96 +480,84 @@ Section conditional_counter.
cinc (f, c)%V @⊤∖↑N
<<< counter_content γs (b, if b then n + 1 else n), RET #() >>>.
Proof.
- iIntros "#InvC". iDestruct "InvC" as (γ_h γ_b γ_n f_l c_l) "[Heq InvC]".
+ 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' H' q v) "[>Hf [>Hc [>[Hl Hl'] [>Hâ— [>Hâ—¯ [Hlh [>Heq [>Hbâ— Hv]]]]]]]]".
- wp_load. simpl. iDestruct "Hv" as "[Hv|Hv]".
- - iDestruct "Hv" as (n) "[% Hv]"; subst v.
- iModIntro. iSplitR "Hl' AU".
- { iModIntro. iExists _, _, _, (q/2)%Qp, (InjLV #n). eauto with iFrame. }
+ iInv counterN as (b' l' q s) "(>Hf & >Hc & >[Hl Hl'] & >Hbâ— & >Hltok & Hrest)".
+ wp_load. destruct s as [n|n p].
+ - iDestruct "Hrest" as "(Hc' & Hv)".
+ iModIntro. iSplitR "AU Hl".
+ { iModIntro. iExists _, _, (q/2)%Qp, (injl 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 to read c_l *)
- iInv counterN as (b l'' H'' q' v') "[>Hf [>Hc [>Hl'2 [>Hâ— [>Hâ—¯ [>Hlh [>Heq [Hbâ— Hrest]]]]]]]]".
- iDestruct "Heq" as %[Heq Hd].
- (* assert that ly is not in the history *)
- iDestruct (extract_snapshot with "Hâ—¯") as "#Hs".
- iDestruct ((nodup_fresh_loc _ _ _ Hd) with "Hly Hlh") as %Hd'.
+ wp_let. wp_apply (loc_token_alloc with "[//]"); iIntros (ly) "[Hly Hmy]".
+ 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â— & >Hltok & Hrest)".
destruct (decide (l' = l'')) as [<- | Hn].
+ (* CAS succeeds *)
- wp_cas_suc.
- (* We need to update the half history with `ly`.
- For that we will need to get the second half of the history *)
- iDestruct "Hrest" as "[InjL | InjR]";
- iPoseProof (mapsto_agree with "Hl' Hl'2") as "#Heq"; last first.
- { (* injR: contradiction *)
- iDestruct "InjR" as (??) "[Heq' InjR_rest]".
- iDestruct "Heq'" as %->. iDestruct "Heq" as %Heq'. inversion Heq'. }
- (* injL: update history *)
- iDestruct "InjL" as (n'') "[Heq' [Hâ—¯' Hnâ—]]".
- iDestruct "Heq'" as %->. simpl. iDestruct "Heq" as %[=<-].
- iPoseProof ((update_history _ _ ly) with "Hâ— Hâ—¯ Hâ—¯'") as ">[Hâ— [Hâ—¯' Hâ—¯'']]".
+ iDestruct (mapsto_agree with "Hl Hl'") as %<-%state_to_val_inj.
+ iDestruct "Hrest" as ">[Hc' Hnâ—]". iCombine "Hc Hc'" as "Hc".
+ wp_cas_suc. iClear "Hltok".
+ (* Initialize new [state] protocol .*)
iDestruct (laterable with "AU") as (AU_later) "[AU #AU_back]".
- iDestruct (own_alloc token) as ">Ht"; first by apply auth_auth_valid.
- iDestruct "Ht" as (γ_t) "Token".
+ iMod (own_alloc (Excl ())) as (γ_t) "Token"; first done.
+ iMod (own_alloc (Cinl $ Excl ())) as (γ_s) "Hs"; first done.
+ iDestruct "Hc" as "[Hc Hc']".
+ (* FIXME: This is three times almost the same thing to allocate the
+ invariant etc, it should be possible to deduplicate that. *)
destruct (val_to_some_loc l_ghost) eqn:H.
* destruct (val_to_some_loc_some l_ghost l H) as [v1 [v2 [vs' [-> HCases]]]].
destruct HCases as [[-> ->] | Hl].
- ++ iMod (inv_alloc stateN _ (state_inv AU_later _ _ _ _ _ _ _ _ γ_t)
- with "[AU Hâ—¯' Hp' Hnâ—]") as "#Hinv".
- { iNext. iExists _. iSplitL "Hp'"; first done. iLeft.
- iSplitL "Hâ—¯'"; first by iFrame. iLeft. by iFrame. }
+ ++ iMod (inv_alloc stateN _ (state_inv AU_later _ _ _ _ _ _ _ _ _)
+ with "[AU Hs Hp' Hc' Hnâ—]") as "#Hinv".
+ { iNext. iExists _. iFrame "Hp'". iLeft. iFrame. iLeft.
+ iFrame. simpl. done. }
iModIntro. iDestruct "Hly" as "[Hly1 Hly2]". iSplitR "Hl' Token". {
(* close invariant *)
- iNext. iExists _, ly, _, _, _. iFrame.
- iSplitL "Hly1"; first by eauto. iSplit; first by iPureIntro.
- iRight. iExists _, _. iSplit; first done. iExists _, _, _, _. iSplit; done.
+ iNext. iExists _, _, _, (injr n p'). iFrame.
+ iExists _, _, _, _, _. iSplit; done.
}
- wp_if.
- wp_apply complete_spec; [iExists _, _, _, _, _; eauto | done | done | done | ..].
+ wp_if. wp_apply complete_spec; [iExists _, _, _, _; eauto | done | done | done | ..].
iIntros "Ht". iMod ("Ht" with "Token") as "Φ". wp_seq. by wp_lam.
- ++ iMod (inv_alloc stateN _ (state_inv AU_later _ _ _ ly l _ _ _ γ_t)
- with "[AU Hâ—¯' Hp' Hnâ—]") as "#Hinv".
- { iNext. iExists _. iSplitL "Hp'"; first done. iLeft.
- iSplitL "Hâ—¯'"; first by iFrame. iLeft. iFrame. by rewrite H. }
+ ++ iMod (inv_alloc stateN _ (state_inv AU_later _ _ _ _ _ _ _ _ _)
+ with "[AU Hs Hp' Hc' Hnâ—]") as "#Hinv".
+ { iNext. iExists _. iSplitL "Hp'"; first done. iLeft. iFrame.
+ iLeft. iFrame. by rewrite H. }
iModIntro. iDestruct "Hly" as "[Hly1 Hly2]". iSplitR "Hl' Token". {
(* close invariant *)
- iNext. iExists _, ly, _, _, _. iFrame.
- iSplitL "Hly1"; first by eauto. iSplit; first by iPureIntro.
- iRight. iExists _, _. iSplit; first done. iExists _, _, _, _. iSplit; done.
+ iNext. iExists _, _, _, (injr n p'). iFrame.
+ iExists _, _, _, _, _. iSplit; done.
}
wp_if.
- wp_apply complete_spec; [iExists _, _, _, _, _; eauto | done | done | done | ..].
+ wp_apply complete_spec; [iExists _, _, _, _; eauto | done | done | done | ..].
iIntros "Ht". iMod ("Ht" with "Token") as "Φ". wp_seq. by wp_lam.
- * iMod (inv_alloc stateN _ (state_inv AU_later _ _ _ ly l' _ _ _ γ_t)
- with "[AU Hâ—¯' Hp' Hnâ—]") as "#Hinv".
- { iNext. iExists _. iSplitL "Hp'"; first done. iLeft.
- iSplitL "Hâ—¯'"; first by iFrame. iLeft. iFrame. by rewrite H. }
+ * iMod (inv_alloc stateN _ (state_inv AU_later _ _ _ _ _ _ _ _ _)
+ with "[AU Hs Hp' Hc' Hnâ—]") as "#Hinv".
+ { iNext. iExists _. iSplitL "Hp'"; first done. iLeft. iFrame.
+ iLeft. iFrame. by rewrite H. }
iModIntro. iDestruct "Hly" as "[Hly1 Hly2]". iSplitR "Hl' Token". {
(* close invariant *)
- iNext. iExists _, ly, _, _, _. iFrame.
- iSplitL "Hly1"; first by eauto. iSplit; first by iPureIntro.
- iRight. iExists _, _. iSplit; first done. iExists _, _, _, _. iSplit; done.
+ iNext. iExists _, _, _, (injr n p'). iFrame.
+ iExists _, _, ly, _, _. iSplit; done.
}
wp_if.
- wp_apply complete_spec; [iExists _, _, _, _, _; eauto | done | done | done | ..].
+ wp_apply complete_spec; [iExists _, _, _, _; eauto | done | done | 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 "Hl' AU".
- iModIntro. iExists _, _, _, _. eauto 10 with iFrame.
+ iModIntro. iSplitR "AU".
+ { iModIntro. iExists _, _, _, s. iFrame. }
wp_if. by iApply "IH".
- (* l' ↦ injR *)
- iModIntro. iDestruct "Hv" as (n p) "[% Hrest]"; subst v.
+ iModIntro.
(* extract state invariant *)
- iDestruct "Hrest" as (P Q l_ghost γ_t) "[#InvS #P_AU]".
+ iDestruct "Hrest" as (P Q l_ghost γ_t γ_s) "[#InvS #P_AU]".
iSplitR "Hl' AU".
(* close invariant *)
- { iModIntro. iExists _, _, _, _, _. iFrame. iRight. eauto 10 with iFrame. }
- wp_let. wp_load. wp_match. repeat wp_proj.
- wp_apply complete_spec; [iExists _, _, _, _, _; eauto | done | done | done | ..].
+ { iModIntro. iExists _, _, _, (injr n p). iFrame. eauto 10 with iFrame. }
+ wp_let. wp_load. wp_match. wp_pures.
+ wp_apply complete_spec; [iExists _, _, _, _; eauto | done | done | done | ..].
iIntros "_". wp_seq. by iApply "IH".
Qed.
@@ -913,24 +567,20 @@ Section conditional_counter.
{{{ ctr γs, RET ctr ; is_counter γs ctr ∗ counter_content γs (true, 0) }}}.
Proof.
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_apply (loc_token_alloc with "[//]"); iIntros (l_n) "[Hl_n Hltok]".
+ wp_alloc l_c as "Hl_c". wp_let.
wp_alloc l_f as "Hl_f". wp_let. wp_pair.
- iMod (own_alloc (full_history_auth [l_n] ⋅ full_history_frag [l_n])) as (γ_h) "[Hh◠Hh◯]".
- { rewrite pair_op. apply pair_valid. split; by apply auth_both_valid. }
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. }
- iMod (inv_alloc counterN _ (counter_inv γ_h γ_b γ_n l_f l_c)
- with "[Hl_f Hl_c Hl_n Hhâ— Hhâ—¯ Hbâ— Hnâ—]") as "#InvC".
- { iNext. iDestruct "Hhâ—¯" as "[Hhâ—¯1 Hhâ—¯2]". iDestruct "Hl_n" as "[Hl_n1 Hl_n2]".
- iExists true, l_n, [l_n], _, (InjLV #0). iFrame.
- iSplitL "Hl_n1". { simpl. iSplitL; last done. by iExists _, _. }
- iSplitR. { iPureIntro. split; first done. apply NoDup_cons. apply in_nil. apply NoDup_nil. }
- iLeft. iExists 0. iSplitR; first done. iFrame. }
+ iMod (inv_alloc counterN _ (counter_inv γ_b γ_n l_f l_c)
+ with "[Hl_f Hl_c Hl_n Hltok Hbâ— Hnâ—]") as "#InvC".
+ { iNext. iDestruct "Hl_c" as "[Hl_c1 Hl_c2]".
+ iExists true, l_n, _, (injl 0). iFrame. }
iModIntro.
- iApply ("HΦ" $! (#l_f, #l_c)%V (γ_h, γ_b, γ_n)).
- iSplitR; last by iFrame. iExists γ_h, γ_b, γ_n, l_f, l_c. iSplit; done.
+ 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 f c (new_b : bool) :
@@ -940,16 +590,16 @@ Section conditional_counter.
<<< counter_content γs (new_b, n), RET #() >>>.
Proof.
iIntros "#InvC" (Φ) "AU". wp_lam. wp_let. wp_proj.
- iDestruct "InvC" as (γ_h γ_b γ_n l_f l_c) "[[HEq1 HEq2] InvC]".
+ iDestruct "InvC" as (γ_b γ_n l_f l_c) "[[HEq1 HEq2] InvC]".
iDestruct "HEq1" as %->. iDestruct "HEq2" as %HEq. inversion HEq; subst; clear HEq.
- iInv counterN as (b c H q v) "[>Hl_f [>Hl_c [>Hl [>Hâ— [>Hâ—¯ [>HlH [>HEq [Hbâ— H]]]]]]]]".
+ iInv counterN as (b c q s) "(>Hf & >Hc & >[Hl Hl'] & >Hbâ— & >Hltok & 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, H, q, v. iFrame.
+ iNext. iExists new_b, c, q, _. iFrame. done.
Qed.
Lemma get_spec γs f c :
@@ -959,26 +609,26 @@ Section conditional_counter.
<<< counter_content γs (b, n), RET #n >>>.
Proof.
iIntros "#InvC" (Φ) "AU". iLöb as "IH". wp_lam. repeat (wp_proj; wp_let). wp_bind (! _)%E.
- iDestruct "InvC" as (γ_h γ_b γ_n l_f l_c) "[[HEq1 HEq2] InvC]".
+ iDestruct "InvC" as (γ_b γ_n l_f l_c) "[[HEq1 HEq2] InvC]".
iDestruct "HEq1" as %->. iDestruct "HEq2" as %HEq. inversion HEq; subst.
- iInv counterN as (b c H q v) "[>Hl_f [>Hl_c [>[Hc Hc'] [>Hâ— [>Hâ—¯ [>HlH [>HEq [Hbâ— [H|H]]]]]]]]]".
- - wp_load. iDestruct "H" as (n) "[% [Hâ—¯2 Hnâ—]]". simpl in *; subst v.
- iMod "AU" as (au_b au_n) "[[Hbâ—¯ Hnâ—¯] [_ Hclose]]"; simpl.
+ iInv counterN as (b c q s) "(>Hf & >Hc & >[Hl Hl'] & >Hbâ— & >Hltok & Hrest)".
+ wp_load.
+ destruct s as [n|n p].
+ - iMod "AU" as (au_b au_n) "[[Hbâ—¯ 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.
- iModIntro. iSplitR "HΦ Hc'". {
- iNext. iExists b, c, H, (q/2)%Qp, (InjLV #au_n). iFrame.
- iLeft. iExists au_n. iFrame. done.
+ iModIntro. iSplitR "HΦ Hl'". {
+ iNext. iExists b, c, (q/2)%Qp, (injl au_n). iFrame.
}
wp_let. wp_load. wp_match. iApply "HΦ".
- - wp_load. iDestruct "H" as (n p) "[% H]". simpl in *; subst v.
- iDestruct "H" as (P Q l_ghost γ_t) "[#InvS #PAU]".
- iModIntro. iSplitR "AU Hc'". {
- iNext. iExists b, c, H, (q/2)%Qp, (InjRV(#n,#p)). iFrame.
- iRight. iExists n, p. iSplit; first done. iExists P, Q, l_ghost, γ_t. eauto.
+ - iDestruct "Hrest" as (P Q l_ghost γ_t γ_s) "[#InvS #PAU]".
+ iModIntro. iSplitR "AU Hl'". {
+ iNext. iExists b, c, (q/2)%Qp, (injr n p). iFrame.
+ iExists P, Q, l_ghost, γ_t, _. eauto.
}
wp_let. wp_load. wp_match. repeat wp_proj. wp_bind (complete _ _ _ _ _)%E.
- wp_apply complete_spec; [ iExists _, _, _, _, _; eauto | done | done | done | .. ].
+ wp_apply complete_spec; [ iExists _, _, _, _; eauto | done | done | done | .. ].
iIntros "Ht". wp_seq. iApply "IH". iApply "AU".
Qed.
--
GitLab