From 3d17d6a3932de2c33bb7e8130fc1710773248788 Mon Sep 17 00:00:00 2001
From: Gaurav Parthasarathy <gauravp@student.ethz.ch>
Date: Sat, 15 Jun 2019 22:28:08 +0200
Subject: [PATCH] implement and verify RDCSS (on integers only, for now)
---
_CoqProject | 3 +
theories/logatom/rdcss/lib/gc.v | 245 +++++++++++++
theories/logatom/rdcss/rdcss.v | 632 ++++++++++++++++++++++++++++++++
theories/logatom/rdcss/spec.v | 47 +++
4 files changed, 927 insertions(+)
create mode 100644 theories/logatom/rdcss/lib/gc.v
create mode 100644 theories/logatom/rdcss/rdcss.v
create mode 100644 theories/logatom/rdcss/spec.v
diff --git a/_CoqProject b/_CoqProject
index cffa7ccb..dcc37e6b 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -107,3 +107,6 @@ theories/logatom/snapshot/spec.v
theories/logatom/snapshot/atomic_snapshot.v
theories/logatom/conditional_increment/spec.v
theories/logatom/conditional_increment/cinc.v
+theories/logatom/rdcss/rdcss.v
+theories/logatom/rdcss/spec.v
+theories/logatom/rdcss/lib/gc.v
diff --git a/theories/logatom/rdcss/lib/gc.v b/theories/logatom/rdcss/lib/gc.v
new file mode 100644
index 00000000..85365ba9
--- /dev/null
+++ b/theories/logatom/rdcss/lib/gc.v
@@ -0,0 +1,245 @@
+From iris.algebra Require Import auth excl gmap.
+From iris.base_logic.lib Require Export own invariants.
+From iris.proofmode Require Import tactics.
+From iris.heap_lang Require Export lang locations lifting.
+Set Default Proof Using "Type".
+Import uPred.
+
+Definition gcN: namespace := nroot .@ "gc".
+
+Definition gc_mapUR : ucmraT := gmapUR loc $ optionR $ exclR $ valC.
+
+Definition to_gc_map (gcm: gmap loc val) : gc_mapUR := (λ v : val, Excl' v) <$> gcm.
+
+Class gcG (Σ : gFunctors) := GcG {
+ gc_inG :> inG Σ (authR (gc_mapUR));
+ gc_name : gname
+}.
+
+Arguments gc_name {_} _ : assert.
+
+Class gcPreG (Σ : gFunctors) := {
+ gc_preG_inG :> inG Σ (authR (gc_mapUR))
+}.
+
+Definition gcΣ : gFunctors :=
+ #[ GFunctor (authR (gc_mapUR)) ].
+
+Instance subG_gcPreG {Σ} : subG gcΣ Σ → gcPreG Σ.
+Proof. solve_inG. Qed.
+
+Section defs.
+
+ Context `{!invG Σ, !heapG Σ, gG: gcG Σ}.
+
+ Definition gc_inv_P: iProp Σ :=
+ ((∃(gcm: gmap loc val), own (gc_name gG) (◠to_gc_map gcm) ∗ ([∗ map] l ↦ v ∈ gcm, (l ↦ v)) ) )%I.
+
+ Definition gc_inv : iProp Σ := inv gcN gc_inv_P.
+
+ Definition gc_mapsto (l: loc) (v: val) : iProp Σ := own (gc_name gG) (◯ {[l := Excl' v]}).
+
+ Definition is_gc_loc (l: loc) : iProp Σ := own (gc_name gG) (◯ {[l := None]}).
+
+End defs.
+
+Section to_gc_map.
+
+ Lemma to_gc_map_valid gcm: ✓ to_gc_map gcm.
+ Proof. intros l. rewrite lookup_fmap. by case (gcm !! l). Qed.
+
+ Lemma to_gc_map_empty: to_gc_map ∅ = ∅.
+ Proof. by rewrite /to_gc_map fmap_empty. Qed.
+
+ Lemma to_gc_map_singleton l v: to_gc_map {[l := v]} = {[l := Excl' v]}.
+ Proof. by rewrite /to_gc_map fmap_insert fmap_empty. Qed.
+
+ Lemma to_gc_map_insert l v gcm:
+ to_gc_map (<[l := v]> gcm) = <[l := Excl' v]> (to_gc_map gcm).
+ Proof. by rewrite /to_gc_map fmap_insert. Qed.
+
+ Lemma to_gc_map_delete l gcm :
+ to_gc_map (delete l gcm) = delete l (to_gc_map gcm).
+ Proof. by rewrite /to_gc_map fmap_delete. Qed.
+
+ Lemma lookup_to_gc_map_None gcm l :
+ gcm !! l = None → to_gc_map gcm !! l = None.
+ Proof. by rewrite /to_gc_map lookup_fmap=> ->. Qed.
+
+ Lemma lookup_to_gc_map_Some gcm l v :
+ gcm !! l = Some v → to_gc_map gcm !! l = Some (Excl' v).
+ Proof. by rewrite /to_gc_map lookup_fmap=> ->. Qed.
+
+
+ Lemma lookup_to_gc_map_Some_2 gcm l w :
+ to_gc_map gcm !! l = Some w → ∃ v, gcm !! l = Some v.
+ Proof.
+ rewrite /to_gc_map lookup_fmap. rewrite fmap_Some.
+ intros (x & Hsome & Heq). eauto.
+ Qed.
+
+ Lemma lookup_to_gc_map_Some_3 gcm l w :
+ to_gc_map gcm !! l = Some (Excl' w) → gcm !! l = Some w.
+ Proof.
+ rewrite /to_gc_map lookup_fmap. rewrite fmap_Some.
+ intros (x & Hsome & Heq). by inversion Heq.
+ Qed.
+
+ Lemma excl_option_included (v: val) y:
+ ✓ y → Excl' v ≼ y → y = Excl' v.
+ Proof.
+ intros ? H. destruct y.
+ - apply Some_included_exclusive in H;[ | apply _ | done ].
+ setoid_rewrite leibniz_equiv_iff in H.
+ by rewrite H.
+ - apply is_Some_included in H.
+ + by inversion H.
+ + by eapply mk_is_Some.
+ Qed.
+
+ Lemma gc_map_singleton_included gcm l v :
+ {[l := Some (Excl v)]} ≼ to_gc_map gcm → gcm !! l = Some v.
+ Proof.
+ rewrite singleton_included.
+ setoid_rewrite Some_included_total.
+ intros (y & Hsome & Hincluded).
+ pose proof (lookup_valid_Some _ _ _ (to_gc_map_valid gcm) Hsome) as Hvalid.
+ pose proof (excl_option_included _ _ Hvalid Hincluded) as Heq.
+ rewrite Heq in Hsome.
+ apply lookup_to_gc_map_Some_3.
+ by setoid_rewrite leibniz_equiv_iff in Hsome.
+ Qed.
+End to_gc_map.
+
+Lemma gc_init `{!invG Σ, !heapG Σ, !gcPreG Σ} E:
+ (|==> ∃ _ : gcG Σ, |={E}=> gc_inv)%I.
+Proof.
+ iMod (own_alloc (â— (to_gc_map ∅))) as (γ) "Hâ—".
+ { rewrite auth_auth_valid. exact: to_gc_map_valid. }
+ iModIntro.
+ iExists (GcG Σ _ γ).
+ iAssert (gc_inv_P (gG := GcG Σ _ γ)) with "[Hâ—]" as "P".
+ {
+ iExists _. iFrame.
+ by iApply big_sepM_empty.
+ }
+ iMod ((inv_alloc gcN E gc_inv_P) with "P") as "#InvGC".
+ iModIntro. iFrame "#".
+Qed.
+
+Section gc.
+ 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.
+
+ Global Instance is_gc_loc_timeless (l: loc): Timeless (is_gc_loc l).
+ Proof. rewrite /is_gc_loc. apply _. Qed.
+
+ Global Instance gc_mapsto_timeless (l: loc) (v: val): Timeless (gc_mapsto l v).
+ Proof. rewrite /is_gc_loc. apply _. Qed.
+
+ Global Instance gc_inv_P_timeless: Timeless gc_inv_P.
+ Proof. rewrite /gc_inv_P. apply _. Qed.
+
+ Lemma make_gc l v E: ↑gcN ⊆ E → gc_inv -∗ l ↦ v ={E}=∗ gc_mapsto l v.
+ Proof.
+ iIntros (HN) "#Hinv Hl".
+ iMod (inv_open_timeless _ gcN _ with "Hinv") as "[P Hclose]"=>//.
+ iDestruct "P" as (gcm) "[Hâ— HsepM]".
+ destruct (gcm !! l) as [v' | ] eqn: Hlookup.
+ - (* auth map contains l --> contradiction *)
+ iDestruct (big_sepM_lookup with "HsepM") as "Hl'"=>//.
+ by iDestruct (mapsto_valid_2 with "Hl Hl'") as %?.
+ - iMod (own_update with "Hâ—") as "[Hâ— Hâ—¯]".
+ {
+ apply lookup_to_gc_map_None in Hlookup.
+ apply (auth_update_alloc _ (to_gc_map (<[l := v]> gcm)) (to_gc_map ({[l := v]}))).
+ rewrite to_gc_map_insert to_gc_map_singleton.
+ pose proof (to_gc_map_valid gcm).
+ setoid_rewrite alloc_singleton_local_update=>//.
+ }
+ iMod ("Hclose" with "[Hâ— HsepM Hl]").
+ + iExists _.
+ iDestruct (big_sepM_insert with "[HsepM Hl]") as "HsepM"=>//; iFrame. iFrame.
+ + iModIntro. by rewrite /gc_mapsto to_gc_map_singleton.
+ Qed.
+
+ Lemma gc_is_gc l v: gc_mapsto l v -∗ is_gc_loc l.
+ Proof.
+ iIntros "Hgc_l". rewrite /gc_mapsto.
+ assert (Excl' v = (Excl' v) â‹… None)%I as ->. { done. }
+ rewrite -op_singleton auth_frag_op own_op.
+ iDestruct "Hgc_l" as "[_ Hâ—¯_none]".
+ iFrame.
+ Qed.
+
+ 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.
+ iPureIntro.
+ apply auth_both_valid in Hvalid as [Hincluded Hvalid].
+ setoid_rewrite singleton_included in Hincluded.
+ destruct Hincluded as (y & Hsome & _).
+ eapply lookup_to_gc_map_Some_2.
+ by apply leibniz_equiv_iff in Hsome.
+ Qed.
+
+ 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".
+ iDestruct (own_valid with "Hcomb") as %Hvalid.
+ iPureIntro.
+ apply auth_both_valid in Hvalid as [Hincluded Hvalid].
+ by apply gc_map_singleton_included.
+ Qed.
+
+ (** 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".
+ iMod (inv_open_timeless _ gcN _ with "Hinv") as "[P Hclose]"=>//.
+ 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]"=>//.
+ iFrame. iIntros (w) "Hl".
+ iMod (own_update_2 with "Hâ— Hgc_l") as "[Hâ— Hâ—¯]".
+ { apply (auth_update _ _ (<[l := Excl' w]> (to_gc_map gcm)) {[l := Excl' w]}).
+ eapply singleton_local_update.
+ { by apply lookup_to_gc_map_Some in Hsome. }
+ by apply option_local_update, exclusive_local_update.
+ }
+ 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.
+
+ Lemma is_gc_access l E: ↑gcN ⊆ E → gc_inv -∗ is_gc_loc l ={E, E ∖ ↑gcN}=∗ ∃ v, l ↦ v ∗ (l ↦ v ={E ∖ ↑gcN, E}=∗ ⌜TrueâŒ).
+ Proof.
+ iIntros (HN) "#Hinv Hgc_l".
+ iMod (inv_open_timeless _ gcN _ with "Hinv") as "[P Hclose]"=>//.
+ iModIntro.
+ iDestruct "P" as (gcm) "[Hâ— HsepM]".
+ iDestruct (is_gc_lookup_Some with "Hgc_l Hâ—") as %Hsome.
+ destruct Hsome as [v Hsome].
+ iDestruct (big_sepM_lookup_acc with "HsepM") as "[Hl HsepM]"=>//.
+ iExists _. iFrame.
+ iIntros "Hl".
+ iMod ("Hclose" with "[Hâ— HsepM Hl]"); last done.
+ iExists _. iFrame.
+ by (iApply ("HsepM" with "Hl")).
+ Qed.
+
+End gc.
diff --git a/theories/logatom/rdcss/rdcss.v b/theories/logatom/rdcss/rdcss.v
new file mode 100644
index 00000000..0904c759
--- /dev/null
+++ b/theories/logatom/rdcss/rdcss.v
@@ -0,0 +1,632 @@
+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.
+From iris.heap_lang Require Import proofmode notation.
+From iris_examples.logatom.rdcss Require Import spec.
+From iris_examples.logatom.rdcss Require Export gc.
+Import uPred bi List Decidable.
+Set Default Proof Using "Type".
+
+(** Using prophecy variables with helping: implementing a simplified version of
+ the restricted double-compare single-swap from "A Practical Multi-Word Compare-and-Swap Operation" by Harris et al. (DISC 2002)
+ *)
+
+(** * Implementation of the functions. *)
+
+(* 1) l_m corresponds to the A location in the paper and can differ when helping another thread
+ in the same RDCSS instance.
+ 2) l_n corresponds to the B location in the paper and identifies a single RDCSS instance.
+ 3) Values stored at the B location have type
+
+ Int + Ref (Ref * Int * Int * Int * Proph)
+
+ 3.1) If the value is injL n, then no operation is on-going and the logical state is n.
+ 3.2) If the value is injR (Ref (l_m', m1', n1', n2', p)), then an operation is on-going
+ with corresponding A location l_m'. The reference pointing to the tuple of values
+ corresponds to the descriptor in the paper. We use the name l_descr for the
+ such a descriptor reference.
+*)
+
+(*
+ new_rdcss() :=
+ let l_n = ref ( ref(injL 0) ) in
+ ref l_n
+ *)
+Definition new_rdcss : val :=
+ λ: <>,
+ let: "l_n" := ref (InjL #0) in "l_n".
+
+(*
+ complete(l_descr, l_n) :=
+ let (l_m, m1, n1, n2, p) := !l_descr in
+ (* data = (l_m, m1, n1, n2, p) *)
+ let l_ghost = ref #() in
+ let n_new = (if !l_m = m1 then n1 else n2) in
+ Resolve (CAS l_n (InjR l_descr) (ref (InjL n_new))) p l_ghost ; #().
+ *)
+Definition complete : val :=
+ λ: "l_descr" "l_n",
+ let: "data" := !"l_descr" in
+ (* data = (l_m, m1, n1, n2, p) *)
+ let: "l_m" := Fst (Fst (Fst (Fst ("data")))) in
+ let: "m1" := Snd (Fst (Fst (Fst ("data")))) in
+ let: "n1" := Snd (Fst (Fst ("data"))) in
+ let: "n2" := Snd (Fst ("data")) in
+ let: "p" := Snd ("data") in
+ let: "l_ghost" := ref #() in
+ let: "n_new" := (if: !"l_m" = "m1" then "n2" else "n1") in
+ Resolve (CAS "l_n" (InjR "l_descr") (InjL "n_new")) "p" "l_ghost" ;; #().
+
+(*
+ get(l_n) :=
+ match: !l_n with
+ | injL n => n
+ | injR (l_descr) =>
+ complete(l_descr, l_n);
+ get(l_n)
+ end.
+ *)
+Definition get : val :=
+ rec: "get" "l_n" :=
+ match: !"l_n" with
+ InjL "n" => "n"
+ | InjR "l_descr" =>
+ complete "l_descr" "l_n" ;;
+ "get" "l_n"
+ end.
+
+(*
+ rdcss(l_m, l_n, m1, n1, n2) :=
+ let p := NewProph in
+ let l_descr := ref (l_m, m1, n1, n2, p) in
+ (rec: rdcss_inner()
+ let r := CAS(l_n, InjL n1, InjR l_descr) in
+ match r with
+ InjL n =>
+ if n = n1 then
+ complete(l_descr, l_n) ; n1
+ else
+ n
+ | InjR l_descr_other =>
+ complete(l_descr_other, l_n) ;
+ rdcss_inner()
+ end
+ )()
+*)
+Definition rdcss: val :=
+ λ: "l_m" "l_n" "m1" "n1" "n2",
+ (* allocate fresh descriptor *)
+ let: "p" := NewProph in
+ let: "l_descr" := ref ("l_m", "m1", "n1", "n2", "p") in
+ (* start rdcss computation with allocated descriptor *)
+ ( rec: "rdcss_inner" "_" :=
+ let: "r" := (CAS "l_n" (InjL "n1") (InjR "l_descr")) in
+ match: "r" with
+ InjL "n" =>
+ (* non-descriptor value read, check if CAS was successful *)
+ if: "n" = "n1" then
+ (* CAS was successful, finish operation *)
+ complete "l_descr" "l_n" ;; "n1"
+ else
+ (* CAS failed, hence we could linearize at the CAS *)
+ "n"
+ | InjR "l_descr_other" =>
+ (* a descriptor from a different operation was read, try to help and then restart *)
+ complete "l_descr_other" "l_n" ;;
+ "rdcss_inner" #()
+ end
+ ) #().
+
+(** ** Proof setup *)
+
+Definition numUR := authR $ optionUR $ exclR ZC.
+Definition tokenUR := exclR unitC.
+Definition one_shotUR := csumR (exclR unitC) (agreeR unitC).
+
+Class rdcssG Σ := RDCSSG {
+ rdcss_numG :> inG Σ numUR;
+ rdcss_tokenG :> inG Σ tokenUR;
+ rdcss_one_shotG :> inG Σ one_shotUR;
+ }.
+
+Definition rdcssΣ : gFunctors :=
+ #[GFunctor numUR; GFunctor tokenUR; GFunctor one_shotUR].
+
+Instance subG_rdcssΣ {Σ} : subG rdcssΣ Σ → rdcssG Σ.
+Proof. solve_inG. Qed.
+
+Section rdcss.
+ Context {Σ} `{!heapG Σ, !rdcssG Σ, !gcG Σ }.
+ Context (N : namespace).
+
+ Local Definition descrN := N .@ "descr".
+ Local Definition rdcssN := N .@ "rdcss".
+
+ (** Updating and synchronizing the number RAs *)
+
+ Lemma sync_num_values γ_n (n m : Z) :
+ own γ_n (â— Excl' n) -∗ own γ_n (â—¯ Excl' m) -∗ ⌜n = mâŒ.
+ Proof.
+ iIntros "Hâ— Hâ—¯". iCombine "Hâ—" "Hâ—¯" as "H". iDestruct (own_valid with "H") as "H".
+ by iDestruct "H" as %[H%Excl_included%leibniz_equiv _]%auth_both_valid.
+ Qed.
+
+ Lemma update_num_value γ_n (n1 n2 m : Z) :
+ own γ_n (◠Excl' n1) -∗ own γ_n (◯ Excl' n2) ==∗ own γ_n (◠Excl' m) ∗ own γ_n (◯ Excl' m).
+ Proof.
+ iIntros "Hâ— Hâ—¯". iCombine "Hâ—" "Hâ—¯" as "H". rewrite -own_op. iApply (own_update with "H").
+ by apply auth_update, option_local_update, exclusive_local_update.
+ Qed.
+
+ Definition rdcss_content (γ_n : gname) (n : Z) := (own γ_n (◯ Excl' n))%I.
+
+ (** Definition of the invariant *)
+
+ Fixpoint val_to_some_loc (ln: loc) (vs : list (val * val)) : option loc :=
+ match vs with
+ | (InjRV (LitV (LitLoc ln')), LitV (LitLoc l)) :: _ => if bool_decide(ln = ln') then Some l else None
+ | _ :: vs => val_to_some_loc ln vs
+ | _ => None
+ end.
+
+ Inductive abstract_state : Set :=
+ | Quiescent : Z → abstract_state
+ | Updating : loc → loc → Z → Z → Z → proph_id → abstract_state.
+
+ Definition state_to_val (s : abstract_state) : val :=
+ match s with
+ | Quiescent n => InjLV #n
+ | Updating ld lm m1 n1 n2 p => InjRV #ld
+ end.
+
+ Definition own_token γ := (own γ (Excl ()))%I.
+
+ Definition pending_state P (n1 : 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' n1))%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.
+
+ (* 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 owning half of [l_descr] serves as a
+ "location" token to ensure there is no ABA going on. Notice how [rdcss_inv]
+ owns *more than* half of its [l_descr] in the Updating state,
+ which means we know that the [l_descr] there and here cannot be the same. *)
+ Definition done_state Qn (l_descr l_ghost_winner : loc) (γ_t : gname) :=
+ ((Qn ∨ own_token γ_t) ∗ l_ghost_winner ↦ - ∗ (l_descr ↦{1/2} -) )%I.
+
+ (* Invariant expressing the descriptor protocol.
+ 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 descr_inv P Q (p : proph_id) n (l_n l_descr l_ghost_winner : loc) γ_n γ_t γ_s : iProp Σ :=
+ (∃ vs, proph p vs ∗
+ (own γ_s (Cinl $ Excl ()) ∗
+ (l_n ↦{1/2} InjRV #l_descr ∗ ( pending_state P n (val_to_some_loc l_descr vs) l_ghost_winner γ_n
+ ∨ accepted_state (Q #n) (val_to_some_loc l_descr vs) l_ghost_winner ))
+ ∨ own γ_s (Cinr $ to_agree ()) ∗ done_state (Q #n) l_descr l_ghost_winner γ_t))%I.
+
+ Definition pau P Q γ l_m m1 n1 n2 :=
+ (▷ P -∗ ◇ AU << ∀ (m n : Z), (gc_mapsto l_m #m) ∗ rdcss_content γ n >> @ (⊤∖↑N)∖↑gcN, ∅
+ << (gc_mapsto l_m #m) ∗ (rdcss_content γ (if (decide ((m = m1) ∧ (n = n1))) then n2 else n)),
+ COMM Q #n >>)%I.
+
+ Definition rdcss_inv γ_n l_n :=
+ (∃ (s : abstract_state),
+ l_n ↦{1/2} (state_to_val s) ∗
+ match s with
+ | Quiescent n =>
+ (* (InjLV #n) = state_to_val (Quiescent n) *)
+ (* In this state the CAS which expects to read (InjRV _) in
+ [complete] fails always.*)
+ l_n ↦{1/2} (InjLV #n) ∗ own γ_n (◠Excl' n)
+ | Updating l_descr l_m m1 n1 n2 p =>
+ ∃ q P Q l_ghost_winner γ_t γ_s,
+ (* (InjRV #l_descr) = state_to_val (Updating l_descr l_m m1 n1 n2 p) *)
+ (* There are two pieces of per-[descr]-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. *)
+ (* We own *more than* half of [l_descr], which shows that this cannot
+ be the [l_descr] of any [descr] protocol in the [done] state. *)
+ l_descr ↦{1/2 + q} (#l_m, #m1, #n1, #n2, #p)%V ∗
+ inv descrN (descr_inv P Q p n1 l_n l_descr l_ghost_winner γ_n γ_t γ_s) ∗
+ □ pau P Q γ_n l_m m1 n1 n2 ∗ is_gc_loc l_m
+ end)%I.
+
+ Local Hint Extern 0 (environments.envs_entails _ (rdcss_inv _ _)) => unfold rdcss_inv.
+
+ Definition is_rdcss (γ_n : gname) (rdcss_data: val) :=
+ (∃ (l_n : loc), ⌜rdcss_data = #l_n⌠∧ inv rdcssN (rdcss_inv γ_n l_n) ∧ gc_inv ∧ ⌜N ## gcNâŒ)%I.
+
+ Global Instance is_rdcss_persistent γ_n l_n: Persistent (is_rdcss γ_n l_n) := _.
+
+ Global Instance rdcss_content_timeless γ_n n : Timeless (rdcss_content γ_n n) := _.
+
+ Global Instance abstract_state_inhabited: Inhabited abstract_state := populate (Quiescent 0).
+
+ Lemma rdcss_content_exclusive γ_n l_n_1 l_n_2 :
+ rdcss_content γ_n l_n_1 -∗ rdcss_content γ_n l_n_2 -∗ False.
+ Proof.
+ iIntros "Hn1 Hn2". iDestruct (own_valid_2 with "Hn1 Hn2") as %?.
+ done.
+ Qed.
+
+ (** A few more helper lemmas that will come up later *)
+
+ Lemma mapsto_valid_3 l v1 v2 q :
+ l ↦ v1 -∗ l ↦{q} v2 -∗ ⌜FalseâŒ.
+ Proof.
+ iIntros "Hl1 Hl2". iDestruct (mapsto_valid_2 with "Hl1 Hl2") as %Hv.
+ apply (iffLR (frac_valid' _)) in Hv. by apply Qp_not_plus_q_ge_1 in Hv.
+ Qed.
+
+ (** 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 n l_n l_descr l_ghost γ_n γ_t γ_s :
+ inv descrN (descr_inv P Q p n l_n l_descr l_ghost γ_n γ_t γ_s) -∗
+ own γ_s (Cinr (to_agree ())) -∗
+ □(own_token γ_t ={⊤}=∗ ▷ (Q #n)).
+ Proof.
+ iIntros "#Hinv #Hs !# Ht".
+ iInv descrN 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 "[Qn | >T]"; last first.
+ { iDestruct (own_valid_2 with "Ht T") as %Contra.
+ by inversion Contra. }
+ iSplitR "Qn"; last done. iIntros "!> !>". unfold descr_inv.
+ iExists _. iFrame "Hp". iRight.
+ unfold done_state. iFrame "#∗".
+ Qed.
+
+ (** ** Proof of [complete] *)
+
+ (** The part of [complete] for the succeeding thread that moves from [accepted] to [done] state *)
+ Lemma complete_succeeding_thread_pending (γ_n γ_t γ_s : gname) l_n P Q p
+ (n1 n : Z) (l_descr l_ghost : loc) Φ :
+ inv rdcssN (rdcss_inv γ_n l_n) -∗
+ inv descrN (descr_inv P Q p n1 l_n l_descr l_ghost γ_n γ_t γ_s) -∗
+ l_ghost ↦{1 / 2} #() -∗
+ (□(own_token γ_t ={⊤}=∗ ▷ (Q #n1)) -∗ Φ #()) -∗
+ own γ_n (◠Excl' n) -∗
+ WP Resolve (CAS #l_n (InjRV #l_descr) (InjLV #n)) #p #l_ghost ;; #() {{ v, Φ v }}.
+ Proof.
+ iIntros "#InvC #InvS Hl_ghost HQ Hnâ—". wp_bind (Resolve _ _ _)%E.
+ iInv rdcssN as (s) "(>Hln & Hrest)".
+ iInv descrN 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 & >Hln' & [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 (InjRV l_descr) = (state_to_val s), because
+ while a [descr] protocol is not [done], it owns enough of
+ the [rdcss] protocol to ensure that does not move anywhere else. *)
+ destruct s as [n' |ld' lm' m1' n1' n2' p'].
+ { simpl. iDestruct (mapsto_agree with "Hln Hln'") as %Heq. inversion Heq. }
+ iDestruct (mapsto_agree with "Hln Hln'") as %[= ->].
+ simpl.
+ iDestruct "Hrest" as (q P' Q' l_ghost' γ_t' γ_s') "([>Hld >Hld'] & Hrest)".
+ (* We perform the CAS. *)
+ iCombine "Hln Hln'" as "Hln".
+ wp_apply (wp_resolve with "Hp"); first done. wp_cas_suc.
+ iIntros (vs' ->) "Hp'". simpl. case_bool_decide; simplify_eq.
+ (* 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 Hp' Hld".
+ (* Update state to Done. *)
+ { iNext. iExists _. iFrame "Hp'". iRight. unfold done_state.
+ iFrame "#∗". iSplitR "Hld"; iExists _; done. }
+ iModIntro. iSplitR "HQ".
+ { iNext. iDestruct "Hln" as "[Hln1 Hln2]".
+ iExists (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 γ_n γ_t γ_s l_n l_descr P Q p n1 n l_ghost_inv l_ghost Φ :
+ l_ghost_inv ≠l_ghost →
+ inv rdcssN (rdcss_inv γ_n l_n) -∗
+ inv descrN (descr_inv P Q p n1 l_n l_descr l_ghost_inv γ_n γ_t γ_s) -∗
+ (□(own_token γ_t ={⊤}=∗ ▷ (Q #n1)) -∗ Φ #()) -∗
+ WP Resolve (CAS #l_n (InjRV #l_descr) (InjLV #n)) #p #l_ghost ;; #() {{ v, Φ v }}.
+ Proof.
+ iIntros (Hnl) "#InvC #InvS HQ". wp_bind (Resolve _ _ _)%E.
+ iInv rdcssN as (s) "(>Hln & Hrest)".
+ iInv descrN as (vs) "(>Hp & [NotDone | [#Hs Done]])".
+ { (* If the [descr] 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 "(_ & >Hln' & State)".
+ iDestruct (mapsto_agree with "Hln Hln'") as %[=->].
+ iCombine "Hln Hln'" as "Hlln".
+ wp_apply (wp_resolve with "Hp"); first done; wp_cas_suc.
+ iIntros (vs' ->). simpl. case_bool_decide; simplify_eq.
+ 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. }
+ (* So, we know our protocol is [Done]. *)
+ (* It must be that (state_to_val s) ≠l because we are in the failing thread. *)
+ destruct s as [n' |l_descr' ].
+ { (* (injL n) is the current value, hence the CAS fails *)
+ (* FIXME: proof duplication *)
+ wp_apply (wp_resolve with "Hp"); first done. wp_cas_fail.
+ iIntros (vs' ->) "Hp". iModIntro.
+ iSplitL "Done Hp". { iNext. iExists _. iFrame "#∗". } iModIntro.
+ iSplitL "Hln Hrest". { iNext. iExists _. iFrame. iFrame. }
+ wp_seq. iApply "HQ".
+ iApply state_done_extract_Q; done.
+ }
+ (* (injR l_descr') is the current value *)
+ destruct (decide (l_descr' = l_descr)) as [->|Hn]. {
+ (* The [descr] protocol is [done] while still being the active protocol
+ of the [rdcss] instance? Impossible, now we will own more than the whole descriptor location! *)
+ iDestruct "Done" as "(_ & _ & >Hld)".
+ iDestruct "Hld" as (v') "Hld".
+ iDestruct "Hrest" as (q P' Q' l_ghost' γ_t' γ_s') "(>[Hld' Hld''] & Hrest)".
+ iDestruct (mapsto_combine with "Hld Hld'") as "[Hld _]".
+ rewrite Qp_half_half. iDestruct (mapsto_valid_3 with "Hld Hld''") as "[]".
+ }
+ (* The CAS fails. *)
+ wp_apply (wp_resolve with "Hp"); first done. wp_cas_fail.
+ iIntros (vs' ->) "Hp". iModIntro.
+ iSplitL "Done Hp". { iNext. iExists _. iFrame "#∗". } iModIntro.
+ iSplitL "Hln Hrest". { iNext. iExists _. iFrame. iFrame. }
+ wp_seq. iApply "HQ".
+ iApply state_done_extract_Q; done.
+ Qed.
+
+ (** ** Proof of [complete] *)
+ (* 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 (l_n l_m l_descr : loc) (m1 n1 n2 : Z) (p : proph_id) γ_n γ_t γ_s l_ghost_inv P Q q:
+ N ## gcN →
+ inv rdcssN (rdcss_inv γ_n l_n) -∗
+ inv descrN (descr_inv P Q p n1 l_n l_descr l_ghost_inv γ_n γ_t γ_s) -∗
+ □ pau P Q γ_n l_m m1 n1 n2 -∗
+ is_gc_loc l_m -∗
+ gc_inv -∗
+ {{{ l_descr ↦{q} (#l_m, #m1, #n1, #n2, #p) }}}
+ complete #l_descr #l_n
+ {{{ RET #(); □ (own_token γ_t ={⊤}=∗ ▷(Q #n1)) }}}.
+ Proof.
+ iIntros (Hdisj) "#InvC #InvS #PAU #isGC #InvGC".
+ iModIntro. iIntros (Φ) "Hld HQ". wp_lam. wp_let.
+ wp_bind (! _)%E. wp_load. iClear "Hld". wp_pures.
+ wp_alloc l_ghost as "[Hl_ghost' Hl_ghost'2]". wp_pures.
+ wp_bind (! _)%E.
+ (* open outer invariant *)
+ iInv rdcssN as (s) "(>Hln & 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 *)
+ (* we need to move from [pending] to [accepted]. *)
+ iInv descrN as (vs) "(>Hp & [(>Hs & >Hln' & [Pending | Accepted]) | [#Hs Done]])".
+ + (* Pending: update to accepted *)
+ iDestruct "Pending" as "[P >[Hvs Hnâ—]]".
+ iDestruct ("PAU" with "P") as ">AU".
+ iMod (gc_access with "InvGC") as "Hgc"; first solve_ndisj.
+ (* open and *COMMIT* AU, sync B location l_n and A location l_m *)
+ iMod "AU" as (m' n') "[CC [_ Hclose]]".
+ iDestruct "CC" as "[Hgc_lm Hnâ—¯]".
+ (* sync B location and update it if required *)
+ iDestruct (sync_num_values with "Hnâ— Hnâ—¯") as %->.
+ iMod (update_num_value _ _ _ (if decide (m' = m1 ∧ n' = n') then n2 else n') with "Hn◠Hn◯")
+ as "[Hnâ— Hnâ—¯]".
+ (* get access to A location *)
+ iDestruct ("Hgc" with "Hgc_lm") as "[Hl Hgc_close]".
+ (* read A location *)
+ wp_load.
+ (* sync A location *)
+ iMod ("Hgc_close" with "Hl") as "[Hgc_lm Hgc_close]".
+ (* give back access to A location *)
+ iMod ("Hclose" with "[Hnâ—¯ Hgc_lm]") as "Q"; first by iFrame.
+ iModIntro. iMod "Hgc_close" as "_".
+ (* close descr inv *)
+ iModIntro. iSplitL "Q Hl_ghost' Hp Hvs Hs Hln'".
+ { iModIntro. iNext. iExists _. iFrame "Hp". iLeft. iFrame.
+ iRight. iSplitL "Hl_ghost'"; first by iExists _.
+ destruct (val_to_some_loc l_descr vs) eqn:Hvts; iFrame. }
+ (* close outer inv *)
+ iModIntro. iSplitR "Hl_ghost'2 HQ Hnâ—".
+ { iModIntro. iExists _. iFrame. eauto. }
+ iModIntro.
+ destruct (decide (m' = m1)) as [-> | ?];
+ wp_op;
+ case_bool_decide; simplify_eq; wp_if; wp_pures;
+ [rewrite decide_True; last done | rewrite decide_False; last tauto];
+ iApply (complete_succeeding_thread_pending
+ with "InvC InvS Hl_ghost'2 HQ Hnâ—").
+ + (* Accepted: contradiction *)
+ iDestruct "Accepted" as "[>Hl_ghost_inv _]".
+ iDestruct "Hl_ghost_inv" as (v') "Hlghost".
+ iCombine "Hl_ghost'" "Hl_ghost'2" as "Hl_ghost'".
+ by iDestruct (mapsto_valid_2 with "Hlghost Hl_ghost'") as %?.
+ + (* Done: contradiction *)
+ iDestruct "Done" as "[QT >[Hlghost _]]".
+ iDestruct "Hlghost" as (v') "Hlghost".
+ iCombine "Hl_ghost'" "Hl_ghost'2" as "Hl_ghost'".
+ by iDestruct (mapsto_valid_2 with "Hlghost Hl_ghost'") as %?.
+ - (* we are the failing thread *)
+ (* close invariant *)
+ iMod (is_gc_access with "InvGC isGC") as (v) "[Hlm Hclose]"; first solve_ndisj.
+ wp_load.
+ iMod ("Hclose" with "Hlm") as "_". iModIntro.
+ iModIntro.
+ iSplitL "Hln Hrest".
+ { iExists _. iFrame. iFrame. }
+ (* two equal proofs depending on value of m1 *)
+ wp_op.
+ destruct (decide (v = #m1)) as [-> | ];
+ case_bool_decide; simplify_eq; wp_if; wp_pures;
+ iApply (complete_failing_thread
+ with "InvC InvS HQ"); done.
+ Qed.
+
+ (** ** Proof of [rdcss] *)
+ Lemma rdcss_spec γ_n v (l_m: loc) (m1 n1 n2: Z) :
+ is_rdcss γ_n v -∗ is_gc_loc l_m -∗
+ <<< ∀ (m n: Z), gc_mapsto l_m #m ∗ rdcss_content γ_n n >>>
+ rdcss #l_m v #m1 #n1 #n2 @((⊤∖↑N)∖↑gcN)
+ <<< gc_mapsto l_m #m ∗ rdcss_content γ_n (if decide (m = m1 ∧ n = n1) then n2 else n), RET #n >>>.
+ Proof.
+ iIntros "Hrdcss #GC". iDestruct "Hrdcss" as (l_n) "(Heq & #InvR & #InvGC & Hdisj)".
+ iDestruct "Heq" as %->. iDestruct "Hdisj" as %Hdisj. iIntros (Φ) "AU".
+ (* allocate fresh descriptor *)
+ wp_lam. wp_pures.
+ wp_apply wp_new_proph; first done.
+ iIntros (proph_values p') "Hp'".
+ wp_let. wp_alloc l_descr as "Hld".
+ wp_let.
+ (* invoke inner recursive function [rdcss_inner] *)
+ (* FIXME: would be nice to put iLöb here to avoid another
+ wp_pures tactic at the end *)
+ wp_pures. iLöb as "IH".
+ wp_bind (CAS _ _ _)%E.
+ (* open outer invariant for the CAS *)
+ iInv rdcssN as (s) "(>Hln & Hrest)".
+ destruct s as [n|l_descr' lm' m1' n1' n2' p].
+ - (* l_n ↦ injL n *)
+ (* a non-value descriptor n is currently stored at l_n *)
+ iDestruct "Hrest" as ">[Hln' Hnâ—]".
+ destruct (decide (n1 = n)) as [-> | Hneq].
+ + (* values match -> CAS is successful *)
+ iCombine "Hln Hln'" as "Hln".
+ wp_cas_suc.
+ (* Initialize new [descr] protocol .*)
+ iDestruct (laterable with "AU") as (AU_later) "[AU #AU_back]".
+ iMod (own_alloc (Excl ())) as (γ_t) "Token"; first done.
+ iMod (own_alloc (Cinl $ Excl ())) as (γ_s) "Hs"; first done.
+ iDestruct "Hln" as "[Hln Hln']".
+ set (winner := default l_descr (val_to_some_loc l_descr proph_values)).
+ iMod (inv_alloc descrN _ (descr_inv AU_later _ _ _ _ _ winner _ _ _)
+ with "[AU Hs Hp' Hln' Hnâ—]") as "#Hinv".
+ {
+ iNext. iExists _. iFrame "Hp'". iLeft. iFrame. iLeft.
+ iFrame. destruct (val_to_some_loc l_descr proph_values); simpl; done.
+ }
+ iModIntro. iDestruct "Hld" as "[Hld1 [Hld2 Hld3]]". iSplitR "Hld2 Token".
+ { (* close outer invariant *)
+ iNext. iCombine "Hld1 Hld3" as "Hld1". iExists (Updating l_descr l_m m1 n n2 p').
+ eauto 12 with iFrame.
+ }
+ wp_let. wp_match.
+ wp_op. case_bool_decide; simplify_eq.
+ wp_if. wp_apply (complete_spec with "[] [] [] [] [] [$Hld2]");[ done..|].
+ iIntros "Ht". iMod ("Ht" with "Token") as "Φ". by wp_seq.
+ + (* values do not match -> CAS fails
+ we can commit here *)
+ wp_cas_fail.
+ iMod "AU" as (m'' n'') "[[Hmâ—¯ Hnâ—¯] [_ Hclose]]"; simpl.
+ (* synchronize B location *)
+ iDestruct (sync_num_values with "Hnâ— Hnâ—¯") as %->.
+ iMod ("Hclose" with "[Hm◯ Hn◯]") as "HΦ".
+ { destruct (decide _) as [[_ ?] | _]; [done | iFrame ]. }
+ iModIntro. iSplitR "HΦ".
+ { iModIntro. iExists (Quiescent n''). iFrame. }
+ wp_let. wp_match. wp_op. case_bool_decide; simplify_eq.
+ wp_if. iFrame.
+ - (* l_n ↦ injR l_ndescr' *)
+ (* a descriptor l_descr' is currently stored at l_n -> CAS fails
+ try to help the on-going operation *)
+ wp_cas_fail.
+ iModIntro.
+ (* extract descr invariant *)
+ iDestruct "Hrest" as (q P Q l_ghost γ_t γ_s) "([Hld1 [Hld2 Hld3]] & #InvS & #P_AU & #P_GC)".
+ iSplitR "AU Hld2 Hld Hp'".
+ (* close invariant, retain some permission to l_descr', so it can be read later *)
+ { iModIntro. iExists (Updating l_descr' lm' m1' n1' n2' p). iFrame. eauto 12 with iFrame. }
+ wp_let. wp_match.
+ wp_apply (complete_spec with "[] [] [] [] [] [$Hld2]"); [done..|].
+ iIntros "_". wp_seq. wp_pures.
+ iApply ("IH" with "AU Hp' Hld").
+ Qed.
+
+ (** ** Proof of [new_rdcss] *)
+ Lemma new_rdcss_spec :
+ N ## gcN → gc_inv -∗
+ {{{ True }}}
+ new_rdcss #()
+ {{{ l_n γ_n, RET l_n ; is_rdcss γ_n l_n ∗ rdcss_content γ_n 0 }}}.
+ Proof.
+ iIntros (Hdisj) "#InvGC". iModIntro.
+ iIntros (Φ) "_ HΦ". wp_lam. wp_apply wp_fupd.
+ wp_alloc ln as "Hln".
+ iMod (own_alloc (◠Excl' 0 ⋅ ◯ Excl' 0)) as (γ_n) "[Hn◠Hn◯]".
+ { by apply auth_both_valid. }
+ iMod (inv_alloc rdcssN _ (rdcss_inv γ_n ln)
+ with "[Hln Hnâ—]") as "#InvR".
+ { iNext. iDestruct "Hln" as "[Hln1 Hln2]".
+ iExists (Quiescent 0). iFrame. }
+ wp_let.
+ iModIntro.
+ iApply ("HΦ" $! #ln γ_n).
+ iSplitR; last by iFrame. iExists ln. by iFrame "#".
+ Qed.
+
+ (** ** Proof of [get] *)
+ Lemma get_spec γ_n v :
+ is_rdcss γ_n v -∗
+ <<< ∀ (n : Z), rdcss_content γ_n n >>>
+ get v @(⊤∖↑N)
+ <<< rdcss_content γ_n n, RET #n >>>.
+ Proof.
+ iIntros "Hrdcss". iDestruct "Hrdcss" as (l_n) "(Heq & #InvR & #InvGC & Hdisj)".
+ iDestruct "Heq" as %->. iDestruct "Hdisj" as %Hdisj. iIntros (Φ) "AU".
+ iLöb as "IH". wp_lam. repeat (wp_proj; wp_let). wp_bind (! _)%E.
+ iInv rdcssN as (s) "(>Hln & Hrest)".
+ wp_load.
+ destruct s as [n|l_descr lm m1 n1 n2 p].
+ - iMod "AU" as (au_n) "[Hnâ—¯ [_ Hclose]]"; simpl.
+ iDestruct "Hrest" as "[Hln' Hnâ—]".
+ iDestruct (sync_num_values with "Hnâ— Hnâ—¯") as %->.
+ iMod ("Hclose" with "Hn◯") as "HΦ".
+ iModIntro. iSplitR "HΦ". {
+ iNext. iExists (Quiescent au_n). iFrame.
+ }
+ wp_match. iApply "HΦ".
+ - iDestruct "Hrest" as (q P Q l_ghost γ_t γ_s) "([Hld [Hld' Hld'']] & #InvS & #PAU & #GC)".
+ iModIntro. iSplitR "AU Hld'". {
+ iNext. iExists (Updating l_descr lm m1 n1 n2 p). eauto 11 with iFrame.
+ }
+ wp_match.
+ wp_apply (complete_spec with "[] [] [] [] [] [$Hld']"); [done..|].
+ iIntros "Ht". wp_seq. iApply "IH". iApply "AU".
+ Qed.
+
+End rdcss.
+
+Definition atomic_rdcss `{!heapG Σ, !rdcssG Σ, !gcG Σ} :
+ spec.atomic_rdcss Σ :=
+ {| spec.new_rdcss_spec := new_rdcss_spec;
+ spec.rdcss_spec := rdcss_spec;
+ spec.get_spec := get_spec;
+ spec.rdcss_content_exclusive := rdcss_content_exclusive |}.
+
+Typeclasses Opaque rdcss_content is_rdcss.
diff --git a/theories/logatom/rdcss/spec.v b/theories/logatom/rdcss/spec.v
new file mode 100644
index 00000000..58f9709a
--- /dev/null
+++ b/theories/logatom/rdcss/spec.v
@@ -0,0 +1,47 @@
+From stdpp Require Import namespaces.
+From iris.heap_lang Require Export lifting notation.
+From iris.program_logic Require Export atomic.
+From iris_examples.logatom.rdcss Require Export gc.
+Set Default Proof Using "Type".
+
+(** A general logically atomic interface for conditional increment. *)
+Record atomic_rdcss {Σ} `{!heapG Σ, !gcG Σ} := AtomicRdcss {
+ (* -- operations -- *)
+ new_rdcss : val;
+ rdcss: val;
+ get : val;
+ (* -- other data -- *)
+ name : Type;
+ name_eqdec : EqDecision name;
+ name_countable : Countable name;
+ (* -- predicates -- *)
+ is_rdcss (N : namespace) (γ : name) (v : val) : iProp Σ;
+ rdcss_content (γ : name) (n : Z) : iProp Σ;
+ (* -- predicate properties -- *)
+ is_rdcss_persistent N γ v : Persistent (is_rdcss N γ v);
+ rdcss_content_timeless γ n : Timeless (rdcss_content γ n);
+ rdcss_content_exclusive γ n1 n2 : rdcss_content γ n1 -∗ rdcss_content γ n2 -∗ False;
+ (* -- operation specs -- *)
+ new_rdcss_spec N :
+ N ## gcN → gc_inv -∗
+ {{{ True }}}
+ new_rdcss #()
+ {{{ lln γ, RET lln ; is_rdcss N γ lln ∗ rdcss_content γ 0 }}};
+ rdcss_spec N γ v lm (m1 n1 n2 : Z):
+ is_rdcss N γ v -∗ is_gc_loc lm -∗
+ <<< ∀ (m n: Z), gc_mapsto lm #m ∗ rdcss_content γ n >>>
+ rdcss #lm v #m1 #n1 #n2 @((⊤∖↑N)∖↑gcN)
+ <<< gc_mapsto lm #m ∗ rdcss_content γ (if decide (m = m1 ∧ n = n1) then n2 else n), RET #n >>>;
+ get_spec N γ v:
+ is_rdcss N γ v -∗
+ <<< ∀ (n : Z), rdcss_content γ n >>>
+ get v @(⊤∖↑N)
+ <<< rdcss_content γ n, RET #n >>>;
+}.
+Arguments atomic_rdcss _ {_} {_}.
+
+
+Existing Instances
+ is_rdcss_persistent rdcss_content_timeless
+ name_countable name_eqdec.
+
--
GitLab