Commit 52a034af authored by Gaurav Parthasarathy's avatar Gaurav Parthasarathy

generalized to rdcss (descriptor allocated in each iteration)

parent d76c337b
Pipeline #17825 canceled with stage
......@@ -76,41 +76,46 @@ Definition get : val :=
end.
(*
rdcss(l_n, l_m, m1, n1, n2) :=
match: !l_n with
| injL n =>
rdcss(l_m, l_n, m1, n1, n2) :=
let p := NewProph in
let l_descr := ref (l_m, m1, n1, n2, p) in
let r := CAS(l_n, InjL n1, InjR l_descr) in
match r with
InjL n =>
if n = n1 then
let p = NewProph in
let l_descr = ref (injR (l_m, m1, n1, n2, p)) in
if CAS(l_n, injL n1, l_descr) = injL n1 then
complete(l_n, l_m, l_descr, m1, n1, n2, p); #true
else rdcss(l_n, m1, n1, n2)
else #false
| injR l_descr =>
let (l_m', m1', n1', n2', p') := !l_descr
complete(l_n, lm', l_desr, m1', n1', n2', p');
rdcss(lln, m1, n1, n2)
complete(l_descr, l_m, l_n, m1, n1, n2, p) ;; #true
else
(* CAS failed, hence we could linearize at the CAS *)
#false
| InjR l_descr =>
let (l_m', m1', n1', n2', p') := !l_descr in
complete(l_descr, l_m', l_n, m1', n1', n2', p') ;;
rdcss(l_m, l_n, m1, n1, n2)
end.
*)
Definition rdcss: val :=
rec: "rdcss" "l_m" "l_n" "m1" "n1" "n2" :=
match: !"l_n" with
let: "p" := NewProph in
let: "l_descr" := ref ("l_m", "m1", "n1", "n2", "p") in
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
let: "p" := NewProph in
let: "l_descr" := ref ("l_m", "m1", "n1", "n2", "p") in
if: (CAS "l_n" (InjL "n1") (InjR "l_descr")) = (InjL "n1") then
complete "l_descr" "l_m" "l_n" "m1" "n1" "n2" "p" ;; #true
else "rdcss" "l_m" "l_n" "m1" "n1" "n2"
else #false
(* CAS was successful, finish operation *)
complete "l_descr" "l_m" "l_n" "m1" "n1" "n2" "p" ;; #true
else
(* CAS failed, hence we could linearize at the CAS *)
#false
| InjR "l_descr" =>
(* a descriptor from a different operation was read, try to help and then restart *)
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: "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
complete "l_descr" "l_m'" "l_n" "m1'" "n1'" "n2'" "p'" ;;
"rdcss" "l_m" "l_n" "m1" "n1" "n2"
end.
......@@ -503,91 +508,74 @@ Section rdcss.
Proof.
iIntros (Hdisj) "#InvC #GC #InvGC". iDestruct "InvC" as (l_n) "[Heq InvC]".
iDestruct "Heq" as %->. iIntros (Φ) "AU". iLöb as "IH".
wp_lam. wp_pures. wp_bind (!_)%E.
(* 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. wp_bind (CAS _ _ _)%E.
(* open outer invariant for the CAS *)
iInv rdcssN as (s) "(>Hln & Hrest)".
wp_load. destruct s as [n|l_descr lm' m1' n1' n2' p].
- iDestruct "Hrest" as "(Hln' & Hn●)".
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: try to register with a CAS *)
iModIntro. iSplitR "AU".
{ iModIntro. iExists (Quiescent n). iFrame. }
wp_match.
wp_op. case_bool_decide; simplify_eq; wp_if.
wp_apply wp_new_proph; first done.
iIntros (proph_values p') "Hp'".
wp_let. wp_alloc l_descr as "Hld".
wp_let. wp_pures. wp_bind (CAS _ _ _)%E.
(* open outer invariant again to CAS l_n *)
iInv rdcssN as (s) "(>Hln & Hrest)".
destruct s as [n'|l_descr' lm' m1' n1' n2' p] eqn:Hs.
* (* We read injL n' *)
simpl.
iDestruct "Hrest"as ">[Hln' Hn●]".
destruct (decide (n = n')) as [<- | Hn].
{
(* CAS succeeds *)
(*iDestruct (mapsto_agree with "Hln' Hln") as %<-%state_to_val_inj.*)
iCombine "Hln Hln'" as "Hln".
wp_cas_suc.
(* Initialize new [state] 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 stateN _ (state_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]". iSplitR "Token". {
(* close invariant *)
iNext. iExists (Updating l_descr l_m m1 n n2 p').
eauto 12 with iFrame.
}
wp_op. case_bool_decide; simplify_eq.
wp_if. wp_apply complete_spec; [done..|].
iIntros "Ht". iMod ("Ht" with "Token") as "Φ". by wp_seq.
}
{
(* CAS fails: closing invariant and invoking IH *)
wp_cas_fail.
iModIntro. iSplitR "AU".
{ iModIntro. iExists s. rewrite Hs. iFrame. }
wp_op. case_bool_decide; simplify_eq.
wp_if. by iApply "IH".
}
*
(* We read (injR l_descr'), hence CAS fails: closing invariant and invoking IH *)
wp_cas_fail.
iModIntro. iSplitR "AU".
{ iModIntro. iExists s. rewrite Hs. iFrame. }
wp_op.
wp_if. by iApply "IH".
+ (* values do not match: commit *)
iMod "AU" as (m'' n'') "[[Hm◯ Hn◯] [_ Hclose]]"; simpl.
iDestruct (sync_num_values with "Hn● Hn◯") as %->.
iMod ("Hclose" with "[Hm◯ Hn◯]") as "HΦ".
{ destruct (decide _) as [[_ ?] | _]; [done | iFrame ]. }
+ (* values match -> CAS is successful *)
iCombine "Hln Hln'" as "Hln".
wp_cas_suc.
(* Initialize new [state] 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 stateN _ (state_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]". iSplitR "Token".
{ (* close outer invariant *)
iNext. 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; [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_match.
case_bool_decide; simplify_eq.
wp_let. wp_match. case_bool_decide; simplify_eq.
wp_op.
case_bool_decide; simplify_eq. wp_if. iFrame.
- (* l' ↦ injR *)
- (* 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 state invariant *)
iDestruct "Hrest" as (q P Q l_ghost γ_t γ_s) "([Hld [Hld' Hld'']] & #InvS & #P_AU & #P_GC)".
iSplitR "AU Hld'".
(* close invariant, retain some permission to ld, so that we can read it later *)
{ iModIntro. iExists (Updating l_descr lm' m1' n1' n2' p). iFrame. eauto 10 with iFrame. }
wp_match. wp_bind (!_)%E.
(*read ld*)
iDestruct "Hrest" as (q P Q l_ghost γ_t γ_s) "([Hld1 [Hld2 Hld3]] & #InvS & #P_AU & #P_GC)".
iSplitR "AU Hld2".
(* close invariant, retain some permission to l_descr', so that we can read it later *)
{ iModIntro. iExists (Updating l_descr' lm' m1' n1' n2' p). iFrame. eauto 12 with iFrame. }
wp_let. wp_match. wp_bind (!_)%E.
(*read l_descr*)
wp_load. wp_pures.
wp_apply complete_spec; [done..|].
iIntros "_". wp_seq. by iApply "IH".
Qed.
(** ** Proof of [new_rdcss] *)
Lemma new_rdcss_spec :
{{{ True }}}
new_rdcss #()
......@@ -607,6 +595,7 @@ Section rdcss.
iSplitR; last by iFrame. iExists ln. iSplit; done.
Qed.
(** ** Proof of [get_spec] *)
Lemma get_spec γ_n v :
N ## gcN gc_inv - is_rdcss γ_n v -
<<< (n : Z), rdcss_content γ_n n >>>
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment