Commit e27e771f authored by Ralf Jung's avatar Ralf Jung

cleanup RDCSS a bit and port to latest CmpXchg

parent 3d17d6a3
Pipeline #17971 passed with stage
in 19 minutes and 21 seconds
...@@ -109,4 +109,3 @@ theories/logatom/conditional_increment/spec.v ...@@ -109,4 +109,3 @@ theories/logatom/conditional_increment/spec.v
theories/logatom/conditional_increment/cinc.v theories/logatom/conditional_increment/cinc.v
theories/logatom/rdcss/rdcss.v theories/logatom/rdcss/rdcss.v
theories/logatom/rdcss/spec.v theories/logatom/rdcss/spec.v
theories/logatom/rdcss/lib/gc.v
...@@ -11,7 +11,7 @@ Definition gc_mapUR : ucmraT := gmapUR loc $ optionR $ exclR $ valO. ...@@ -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. 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_inG :> inG Σ (authR (gc_mapUR));
gc_name : gname gc_name : gname
}. }.
...@@ -111,11 +111,25 @@ Section to_gc_map. ...@@ -111,11 +111,25 @@ Section to_gc_map.
Qed. Qed.
End to_gc_map. 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. Section gc.
Context `{!invG Σ, !heapG Σ, !gcG Σ}. Context `{!invG Σ, !heapG Σ, !gcG Σ}.
(* FIXME: still needs a constructor. *)
Global Instance is_gc_loc_persistent (l: loc): Persistent (is_gc_loc l). Global Instance is_gc_loc_persistent (l: loc): Persistent (is_gc_loc l).
Proof. rewrite /is_gc_loc. apply _. Qed. Proof. rewrite /is_gc_loc. apply _. Qed.
......
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.
...@@ -4,7 +4,6 @@ From iris.program_logic Require Export atomic. ...@@ -4,7 +4,6 @@ From iris.program_logic Require Export atomic.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation.
From iris_examples.logatom.rdcss Require Import spec. From iris_examples.logatom.rdcss Require Import spec.
From iris_examples.logatom.rdcss Require Export gc.
Import uPred bi List Decidable. Import uPred bi List Decidable.
Set Default Proof Using "Type". Set Default Proof Using "Type".
...@@ -43,7 +42,7 @@ Definition new_rdcss : val := ...@@ -43,7 +42,7 @@ Definition new_rdcss : val :=
(* data = (l_m, m1, n1, n2, p) *) (* data = (l_m, m1, n1, n2, p) *)
let l_ghost = ref #() in let l_ghost = ref #() in
let n_new = (if !l_m = m1 then n1 else n2) 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 := Definition complete : val :=
λ: "l_descr" "l_n", λ: "l_descr" "l_n",
...@@ -56,7 +55,7 @@ Definition complete : val := ...@@ -56,7 +55,7 @@ Definition complete : val :=
let: "p" := Snd ("data") in let: "p" := Snd ("data") in
let: "l_ghost" := ref #() in let: "l_ghost" := ref #() in
let: "n_new" := (if: !"l_m" = "m1" then "n2" else "n1") 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) := get(l_n) :=
...@@ -81,10 +80,10 @@ Definition get : val := ...@@ -81,10 +80,10 @@ Definition get : val :=
let p := NewProph in let p := NewProph in
let l_descr := ref (l_m, m1, n1, n2, p) in let l_descr := ref (l_m, m1, n1, n2, p) in
(rec: rdcss_inner() (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 match r with
InjL n => InjL n =>
if n = n1 then if b then
complete(l_descr, l_n) ; n1 complete(l_descr, l_n) ; n1
else else
n n
...@@ -101,15 +100,15 @@ Definition rdcss: val := ...@@ -101,15 +100,15 @@ Definition rdcss: val :=
let: "l_descr" := ref ("l_m", "m1", "n1", "n2", "p") in let: "l_descr" := ref ("l_m", "m1", "n1", "n2", "p") in
(* start rdcss computation with allocated descriptor *) (* start rdcss computation with allocated descriptor *)
( rec: "rdcss_inner" "_" := ( rec: "rdcss_inner" "_" :=
let: "r" := (CAS "l_n" (InjL "n1") (InjR "l_descr")) in let: "r" := CmpXchg "l_n" (InjL "n1") (InjR "l_descr") in
match: "r" with match: Fst "r" with
InjL "n" => InjL "n" =>
(* non-descriptor value read, check if CAS was successful *) (* non-descriptor value read, check if CAS was successful *)
if: "n" = "n1" then if: Snd "r" then
(* CAS was successful, finish operation *) (* CmpXchg was successful, finish operation *)
complete "l_descr" "l_n" ;; "n1" complete "l_descr" "l_n" ;; "n1"
else else
(* CAS failed, hence we could linearize at the CAS *) (* CmpXchg failed, hence we could linearize at the CmpXchg *)
"n" "n"
| InjR "l_descr_other" => | InjR "l_descr_other" =>
(* a descriptor from a different operation was read, try to help and then restart *) (* a descriptor from a different operation was read, try to help and then restart *)
...@@ -120,9 +119,9 @@ Definition rdcss: val := ...@@ -120,9 +119,9 @@ Definition rdcss: val :=
(** ** Proof setup *) (** ** Proof setup *)
Definition numUR := authR $ optionUR $ exclR ZC. Definition numUR := authR $ optionUR $ exclR ZO.
Definition tokenUR := exclR unitC. Definition tokenUR := exclR unitO.
Definition one_shotUR := csumR (exclR unitC) (agreeR unitC). Definition one_shotUR := csumR (exclR unitO) (agreeR unitO).
Class rdcssG Σ := RDCSSG { Class rdcssG Σ := RDCSSG {
rdcss_numG :> inG Σ numUR; rdcss_numG :> inG Σ numUR;
...@@ -163,10 +162,10 @@ Section rdcss. ...@@ -163,10 +162,10 @@ Section rdcss.
(** Definition of the invariant *) (** Definition of the invariant *)
Fixpoint val_to_some_loc (ln: loc) (vs : list (val * val)) : option loc := Fixpoint val_to_some_loc (pvs : list (val * val)) : option loc :=
match vs with match pvs with
| (InjRV (LitV (LitLoc ln')), LitV (LitLoc l)) :: _ => if bool_decide(ln = ln') then Some l else None | ((_, #true)%V, LitV (LitLoc l)) :: _ => Some l
| _ :: vs => val_to_some_loc ln vs | _ :: vs => val_to_some_loc vs
| _ => None | _ => None
end. end.
...@@ -210,10 +209,12 @@ Section rdcss. ...@@ -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 Σ := 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 ( vs, proph p vs
(own γ_s (Cinl $ Excl ()) (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 (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 l_descr vs) l_ghost_winner )) 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. 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 := Definition pau P Q γ l_m m1 n1 n2 :=
( P - AU << (m n : Z), (gc_mapsto l_m #m) rdcss_content γ n >> @ (∖↑N)∖↑gcN, ( 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)), << (gc_mapsto l_m #m) (rdcss_content γ (if (decide ((m = m1) (n = n1))) then n2 else n)),
...@@ -269,7 +270,7 @@ Section rdcss. ...@@ -269,7 +270,7 @@ Section rdcss.
apply (iffLR (frac_valid' _)) in Hv. by apply Qp_not_plus_q_ge_1 in Hv. apply (iffLR (frac_valid' _)) in Hv. by apply Qp_not_plus_q_ge_1 in Hv.
Qed. 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]. *) 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 : 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) - inv descrN (descr_inv P Q p n l_n l_descr l_ghost γ_n γ_t γ_s) -
...@@ -300,7 +301,7 @@ Section rdcss. ...@@ -300,7 +301,7 @@ Section rdcss.
l_ghost {1 / 2} #() - l_ghost {1 / 2} #() -
((own_token γ_t ={}= (Q #n1)) - Φ #()) - ((own_token γ_t ={}= (Q #n1)) - Φ #()) -
own γ_n ( Excl' n) - 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. Proof.
iIntros "#InvC #InvS Hl_ghost HQ Hn●". wp_bind (Resolve _ _ _)%E. iIntros "#InvC #InvS Hl_ghost HQ Hn●". wp_bind (Resolve _ _ _)%E.
iInv rdcssN as (s) "(>Hln & Hrest)". iInv rdcssN as (s) "(>Hln & Hrest)".
...@@ -328,8 +329,8 @@ Section rdcss. ...@@ -328,8 +329,8 @@ Section rdcss.
iDestruct "Hrest" as (q P' Q' l_ghost' γ_t' γ_s') "([>Hld >Hld'] & Hrest)". iDestruct "Hrest" as (q P' Q' l_ghost' γ_t' γ_s') "([>Hld >Hld'] & Hrest)".
(* We perform the CAS. *) (* We perform the CAS. *)
iCombine "Hln Hln'" as "Hln". iCombine "Hln Hln'" as "Hln".
wp_apply (wp_resolve with "Hp"); first done. wp_cas_suc. wp_apply (wp_resolve with "Hp"); first done. wp_cmpxchg_suc.
iIntros (vs' ->) "Hp'". simpl. case_bool_decide; simplify_eq. iIntros (vs' ->) "Hp'". simpl.
(* Update to Done. *) (* Update to Done. *)
iDestruct "Accepted" as "[Hl_ghost_inv [HEq Q]]". iDestruct "Accepted" as "[Hl_ghost_inv [HEq Q]]".
iMod (own_update with "Hs") as "Hs". iMod (own_update with "Hs") as "Hs".
...@@ -352,7 +353,7 @@ Section rdcss. ...@@ -352,7 +353,7 @@ Section rdcss.
inv rdcssN (rdcss_inv γ_n l_n) - 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) - inv descrN (descr_inv P Q p n1 l_n l_descr l_ghost_inv γ_n γ_t γ_s) -
((own_token γ_t ={}= (Q #n1)) - Φ #()) - ((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. Proof.
iIntros (Hnl) "#InvC #InvS HQ". wp_bind (Resolve _ _ _)%E. iIntros (Hnl) "#InvC #InvS HQ". wp_bind (Resolve _ _ _)%E.
iInv rdcssN as (s) "(>Hln & Hrest)". iInv rdcssN as (s) "(>Hln & Hrest)".
...@@ -364,8 +365,8 @@ Section rdcss. ...@@ -364,8 +365,8 @@ Section rdcss.
iDestruct "NotDone" as "(_ & >Hln' & State)". iDestruct "NotDone" as "(_ & >Hln' & State)".
iDestruct (mapsto_agree with "Hln Hln'") as %[=->]. iDestruct (mapsto_agree with "Hln Hln'") as %[=->].
iCombine "Hln Hln'" as "Hlln". iCombine "Hln Hln'" as "Hlln".
wp_apply (wp_resolve with "Hp"); first done; wp_cas_suc. wp_apply (wp_resolve with "Hp"); first done; wp_cmpxchg_suc.
iIntros (vs' ->). simpl. case_bool_decide; simplify_eq. iIntros (vs' ->). simpl.
iDestruct "State" as "[Pending | Accepted]". iDestruct "State" as "[Pending | Accepted]".
+ iDestruct "Pending" as "[_ [Hvs _]]". iDestruct "Hvs" as %Hvs. by inversion Hvs. + iDestruct "Pending" as "[_ [Hvs _]]". iDestruct "Hvs" as %Hvs. by inversion Hvs.
+ iDestruct "Accepted" 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. ...@@ -374,10 +375,10 @@ Section rdcss.
destruct s as [n' |l_descr' ]. destruct s as [n' |l_descr' ].
{ (* (injL n) is the current value, hence the CAS fails *) { (* (injL n) is the current value, hence the CAS fails *)
(* FIXME: proof duplication *) (* 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. iIntros (vs' ->) "Hp". iModIntro.
iSplitL "Done Hp". { iNext. iExists _. iFrame "#∗". } iModIntro. iSplitL "Done Hp". { by eauto 12 with iFrame. } iModIntro.
iSplitL "Hln Hrest". { iNext. iExists _. iFrame. iFrame. } iSplitL "Hln Hrest". { by eauto 12 with iFrame. }
wp_seq. iApply "HQ". wp_seq. iApply "HQ".
iApply state_done_extract_Q; done. iApply state_done_extract_Q; done.
} }
...@@ -392,10 +393,10 @@ Section rdcss. ...@@ -392,10 +393,10 @@ Section rdcss.
rewrite Qp_half_half. iDestruct (mapsto_valid_3 with "Hld Hld''") as "[]". rewrite Qp_half_half. iDestruct (mapsto_valid_3 with "Hld Hld''") as "[]".
} }
(* The CAS fails. *) (* 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. iIntros (vs' ->) "Hp". iModIntro.
iSplitL "Done Hp". { iNext. iExists _. iFrame "#∗". } iModIntro. iSplitL "Done Hp". { by eauto 12 with iFrame. } iModIntro.
iSplitL "Hln Hrest". { iNext. iExists _. iFrame. iFrame. } iSplitL "Hln Hrest". { by eauto 12 with iFrame. }
wp_seq. iApply "HQ". wp_seq. iApply "HQ".
iApply state_done_extract_Q; done. iApply state_done_extract_Q; done.
Qed. Qed.
...@@ -452,10 +453,10 @@ Section rdcss. ...@@ -452,10 +453,10 @@ Section rdcss.
iModIntro. iSplitL "Q Hl_ghost' Hp Hvs Hs Hln'". iModIntro. iSplitL "Q Hl_ghost' Hp Hvs Hs Hln'".
{ iModIntro. iNext. iExists _. iFrame "Hp". iLeft. iFrame. { iModIntro. iNext. iExists _. iFrame "Hp". iLeft. iFrame.
iRight. iSplitL "Hl_ghost'"; first by iExists _. 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 *) (* close outer inv *)
iModIntro. iSplitR "Hl_ghost'2 HQ Hn●". iModIntro. iSplitR "Hl_ghost'2 HQ Hn●".
{ iModIntro. iExists _. iFrame. eauto. } { by eauto 12 with iFrame. }
iModIntro. iModIntro.
destruct (decide (m' = m1)) as [-> | ?]; destruct (decide (m' = m1)) as [-> | ?];
wp_op; wp_op;
...@@ -491,24 +492,22 @@ Section rdcss. ...@@ -491,24 +492,22 @@ Section rdcss.
(** ** Proof of [rdcss] *) (** ** Proof of [rdcss] *)
Lemma rdcss_spec γ_n v (l_m: loc) (m1 n1 n2: Z) : 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 >>> <<< (m n: Z), gc_mapsto l_m #m rdcss_content γ_n n >>>
rdcss #l_m v #m1 #n1 #n2 @((∖↑N)∖↑gcN) 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 >>>. <<< gc_mapsto l_m #m rdcss_content γ_n (if decide (m = m1 n = n1) then n2 else n), RET #n >>>.
Proof. 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". iDestruct "Heq" as %->. iDestruct "Hdisj" as %Hdisj. iIntros (Φ) "AU".
(* allocate fresh descriptor *) (* allocate fresh descriptor *)
wp_lam. wp_pures. wp_lam. wp_pures.
wp_apply wp_new_proph; first done. wp_apply wp_new_proph; first done.
iIntros (proph_values p') "Hp'". iIntros (proph_values p') "Hp'".
wp_let. wp_alloc l_descr as "Hld". wp_let. wp_alloc l_descr as "Hld".
wp_let. wp_pures.
(* invoke inner recursive function [rdcss_inner] *) (* invoke inner recursive function [rdcss_inner] *)
(* FIXME: would be nice to put iLöb here to avoid another iLöb as "IH".
wp_pures tactic at the end *) wp_bind (CmpXchg _ _ _)%E.
wp_pures. iLöb as "IH".
wp_bind (CAS _ _ _)%E.
(* open outer invariant for the CAS *) (* open outer invariant for the CAS *)
iInv rdcssN as (s) "(>Hln & Hrest)". iInv rdcssN as (s) "(>Hln & Hrest)".
destruct s as [n|l_descr' lm' m1' n1' n2' p]. destruct s as [n|l_descr' lm' m1' n1' n2' p].
...@@ -518,31 +517,34 @@ Section rdcss. ...@@ -518,31 +517,34 @@ Section rdcss.
destruct (decide (n1 = n)) as [-> | Hneq]. destruct (decide (n1 = n)) as [-> | Hneq].
+ (* values match -> CAS is successful *) + (* values match -> CAS is successful *)
iCombine "Hln Hln'" as "Hln". 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 .*) (* Initialize new [descr] protocol .*)
iDestruct (laterable with "AU") as (AU_later) "[AU #AU_back]". iDestruct (laterable with "AU") as (AU_later) "[AU #AU_back]".
iMod (own_alloc (Excl ())) as (γ