From e27e771fb68552aa5c52cb949965deea72aa1a76 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 24 Jun 2019 14:18:34 +0200
Subject: [PATCH] cleanup RDCSS a bit and port to latest CmpXchg
---
_CoqProject | 1 -
theories/logatom/lib/gc.v | 20 ++-
theories/logatom/rdcss/lib/gc.v | 245 --------------------------------
theories/logatom/rdcss/rdcss.v | 105 +++++++-------
theories/logatom/rdcss/spec.v | 6 +-
5 files changed, 73 insertions(+), 304 deletions(-)
delete mode 100644 theories/logatom/rdcss/lib/gc.v
diff --git a/_CoqProject b/_CoqProject
index dcc37e6b..1cf8c323 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -109,4 +109,3 @@ 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/lib/gc.v b/theories/logatom/lib/gc.v
index ecd69be0..9ed34a0b 100644
--- a/theories/logatom/lib/gc.v
+++ b/theories/logatom/lib/gc.v
@@ -11,7 +11,7 @@ Definition gc_mapUR : ucmraT := gmapUR loc $ optionR $ exclR $ valO.
Definition to_gc_map (gcm: gmap loc val) : gc_mapUR := (λ v : val, Excl' v) <$> gcm.
-Class gcG (Σ : gFunctors) := Gc_mapG {
+Class gcG (Σ : gFunctors) := GcG {
gc_inG :> inG Σ (authR (gc_mapUR));
gc_name : gname
}.
@@ -111,11 +111,25 @@ Section to_gc_map.
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.
diff --git a/theories/logatom/rdcss/lib/gc.v b/theories/logatom/rdcss/lib/gc.v
deleted file mode 100644
index 85365ba9..00000000
--- a/theories/logatom/rdcss/lib/gc.v
+++ /dev/null
@@ -1,245 +0,0 @@
-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
index 0904c759..602c5914 100644
--- a/theories/logatom/rdcss/rdcss.v
+++ b/theories/logatom/rdcss/rdcss.v
@@ -4,7 +4,6 @@ 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".
@@ -43,7 +42,7 @@ Definition new_rdcss : val :=
(* 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 ; #().
+ Resolve (CmpXchg l_n (InjR l_descr) (ref (InjL n_new))) p l_ghost ; #().
*)
Definition complete : val :=
λ: "l_descr" "l_n",
@@ -56,7 +55,7 @@ Definition complete : val :=
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" ;; #().
+ Resolve (CmpXchg "l_n" (InjR "l_descr") (InjL "n_new")) "p" "l_ghost" ;; #().
(*
get(l_n) :=
@@ -81,10 +80,10 @@ Definition get : val :=
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
+ let (r, b) := CmpXchg(l_n, InjL n1, InjR l_descr) in
match r with
InjL n =>
- if n = n1 then
+ if b then
complete(l_descr, l_n) ; n1
else
n
@@ -101,15 +100,15 @@ Definition rdcss: val :=
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
+ let: "r" := CmpXchg "l_n" (InjL "n1") (InjR "l_descr") in
+ match: Fst "r" with
InjL "n" =>
(* non-descriptor value read, check if CAS was successful *)
- if: "n" = "n1" then
- (* CAS was successful, finish operation *)
+ if: Snd "r" then
+ (* CmpXchg was successful, finish operation *)
complete "l_descr" "l_n" ;; "n1"
else
- (* CAS failed, hence we could linearize at the CAS *)
+ (* CmpXchg failed, hence we could linearize at the CmpXchg *)
"n"
| InjR "l_descr_other" =>
(* a descriptor from a different operation was read, try to help and then restart *)
@@ -120,9 +119,9 @@ Definition rdcss: val :=
(** ** Proof setup *)
-Definition numUR := authR $ optionUR $ exclR ZC.
-Definition tokenUR := exclR unitC.
-Definition one_shotUR := csumR (exclR unitC) (agreeR unitC).
+Definition numUR := authR $ optionUR $ exclR ZO.
+Definition tokenUR := exclR unitO.
+Definition one_shotUR := csumR (exclR unitO) (agreeR unitO).
Class rdcssG Σ := RDCSSG {
rdcss_numG :> inG Σ numUR;
@@ -163,10 +162,10 @@ Section rdcss.
(** 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
+ Fixpoint val_to_some_loc (pvs : list (val * val)) : option loc :=
+ match pvs with
+ | ((_, #true)%V, LitV (LitLoc l)) :: _ => Some l
+ | _ :: vs => val_to_some_loc vs
| _ => None
end.
@@ -210,10 +209,12 @@ Section rdcss.
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 ))
+ (l_n ↦{1/2} InjRV #l_descr ∗ ( pending_state P n (val_to_some_loc vs) l_ghost_winner γ_n
+ ∨ accepted_state (Q #n) (val_to_some_loc vs) l_ghost_winner ))
∨ own γ_s (Cinr $ to_agree ()) ∗ done_state (Q #n) l_descr l_ghost_winner γ_t))%I.
+ Local Hint Extern 0 (environments.envs_entails _ (descr_inv _ _ _ _ _ _ _ _ _ _)) => unfold descr_inv.
+
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)),
@@ -269,7 +270,7 @@ Section rdcss.
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),
+ (** Once a [descr] 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) -∗
@@ -300,7 +301,7 @@ Section rdcss.
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 }}.
+ WP Resolve (CmpXchg #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)".
@@ -328,8 +329,8 @@ Section rdcss.
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.
+ wp_apply (wp_resolve with "Hp"); first done. wp_cmpxchg_suc.
+ iIntros (vs' ->) "Hp'". simpl.
(* Update to Done. *)
iDestruct "Accepted" as "[Hl_ghost_inv [HEq Q]]".
iMod (own_update with "Hs") as "Hs".
@@ -352,7 +353,7 @@ Section rdcss.
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 }}.
+ WP Resolve (CmpXchg #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)".
@@ -364,8 +365,8 @@ Section rdcss.
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.
+ wp_apply (wp_resolve with "Hp"); first done; wp_cmpxchg_suc.
+ iIntros (vs' ->). simpl.
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. }
@@ -374,10 +375,10 @@ Section rdcss.
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.
+ wp_apply (wp_resolve with "Hp"); first done. wp_cmpxchg_fail.
iIntros (vs' ->) "Hp". iModIntro.
- iSplitL "Done Hp". { iNext. iExists _. iFrame "#∗". } iModIntro.
- iSplitL "Hln Hrest". { iNext. iExists _. iFrame. iFrame. }
+ iSplitL "Done Hp". { by eauto 12 with iFrame. } iModIntro.
+ iSplitL "Hln Hrest". { by eauto 12 with iFrame. }
wp_seq. iApply "HQ".
iApply state_done_extract_Q; done.
}
@@ -392,10 +393,10 @@ Section rdcss.
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.
+ wp_apply (wp_resolve with "Hp"); first done. wp_cmpxchg_fail.
iIntros (vs' ->) "Hp". iModIntro.
- iSplitL "Done Hp". { iNext. iExists _. iFrame "#∗". } iModIntro.
- iSplitL "Hln Hrest". { iNext. iExists _. iFrame. iFrame. }
+ iSplitL "Done Hp". { by eauto 12 with iFrame. } iModIntro.
+ iSplitL "Hln Hrest". { by eauto 12 with iFrame. }
wp_seq. iApply "HQ".
iApply state_done_extract_Q; done.
Qed.
@@ -452,10 +453,10 @@ Section rdcss.
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. }
+ destruct (val_to_some_loc vs) eqn:Hvts; iFrame. }
(* close outer inv *)
iModIntro. iSplitR "Hl_ghost'2 HQ Hnâ—".
- { iModIntro. iExists _. iFrame. eauto. }
+ { by eauto 12 with iFrame. }
iModIntro.
destruct (decide (m' = m1)) as [-> | ?];
wp_op;
@@ -491,24 +492,22 @@ Section rdcss.
(** ** Proof of [rdcss] *)
Lemma rdcss_spec γ_n v (l_m: loc) (m1 n1 n2: Z) :
- is_rdcss γ_n v -∗ is_gc_loc l_m -∗
+ is_rdcss γ_n v -∗
<<< ∀ (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)".
+ iIntros "Hrdcss". 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.
+ wp_pures.
(* 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.
+ iLöb as "IH".
+ wp_bind (CmpXchg _ _ _)%E.
(* open outer invariant for the CAS *)
iInv rdcssN as (s) "(>Hln & Hrest)".
destruct s as [n|l_descr' lm' m1' n1' n2' p].
@@ -518,31 +517,34 @@ Section rdcss.
destruct (decide (n1 = n)) as [-> | Hneq].
+ (* values match -> CAS is successful *)
iCombine "Hln Hln'" as "Hln".
- wp_cas_suc.
+ wp_cmpxchg_suc.
+ (* Take a "peek" at [AU] and abort immediately to get [gc_is_gc f]. *)
+ iMod "AU" as (b' n') "[[Hf CC] [Hclose _]]".
+ iDestruct (gc_is_gc with "Hf") as "#Hgc".
+ iMod ("Hclose" with "[Hf CC]") as "AU"; first by iFrame.
(* 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)).
+ set (winner := default l_descr (val_to_some_loc 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.
+ iFrame. destruct (val_to_some_loc 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..|].
+ wp_pures.
+ 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.
+ wp_cmpxchg_fail.
iMod "AU" as (m'' n'') "[[Hmâ—¯ Hnâ—¯] [_ Hclose]]"; simpl.
(* synchronize B location *)
iDestruct (sync_num_values with "Hnâ— Hnâ—¯") as %->.
@@ -550,19 +552,18 @@ Section rdcss.
{ 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.
+ wp_pures. 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.
+ wp_cmpxchg_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_pures.
wp_apply (complete_spec with "[] [] [] [] [] [$Hld2]"); [done..|].
iIntros "_". wp_seq. wp_pures.
iApply ("IH" with "AU Hp' Hld").
diff --git a/theories/logatom/rdcss/spec.v b/theories/logatom/rdcss/spec.v
index 58f9709a..40b025b3 100644
--- a/theories/logatom/rdcss/spec.v
+++ b/theories/logatom/rdcss/spec.v
@@ -1,7 +1,7 @@
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.
+From iris_examples.logatom.lib Require Export gc.
Set Default Proof Using "Type".
(** A general logically atomic interface for conditional increment. *)
@@ -27,8 +27,8 @@ Record atomic_rdcss {Σ} `{!heapG Σ, !gcG Σ} := AtomicRdcss {
{{{ 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 -∗
+ rdcss_spec N γ v (lm : loc) (m1 n1 n2 : Z):
+ is_rdcss N γ v -∗
<<< ∀ (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 >>>;
--
GitLab