Commit 34205ce9 authored by Gaurav Parthasarathy's avatar Gaurav Parthasarathy

rdcss only allocates one descriptor now (using inner recursive function)

parent 52a034af
Pipeline #17828 canceled with stage
......@@ -80,45 +80,52 @@ Definition get : val :=
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
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.
(rec: rdcss_inner(l_descr, l_m, l_n, m1, n1, n2)
match r with
InjL n =>
if n = n1 then
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
)(l_descr, l_m, l_n, m1, n1, n2)
*)
Definition rdcss: val :=
rec: "rdcss" "l_m" "l_n" "m1" "n1" "n2" :=
λ: "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
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_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
complete "l_descr" "l_m'" "l_n" "m1'" "n1'" "n2'" "p'" ;;
"rdcss" "l_m" "l_n" "m1" "n1" "n2"
end.
(* start rdcss computation with allocated descriptor *)
(
rec: "rdcss_inner" "l_descr" "l_m" "l_n" "m1" "n1" "n2" :=
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_m" "l_n" "m1" "n1" "n2" "p" ;; #true
else
(* CAS failed, hence we could linearize at the CAS *)
#false
| InjR "l_descr_other" =>
(* a descriptor from a different operation was read, try to help and then restart *)
let: "data" := !"l_descr_other" 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
complete "l_descr_other" "l_m'" "l_n" "m1'" "n1'" "n2'" "p'" ;;
"rdcss_inner" "l_descr" "l_m" "l_n" "m1" "n1" "n2"
end
) "l_descr" "l_m" "l_n" "m1" "n1" "n2".
(** ** Proof setup *)
......@@ -182,13 +189,6 @@ Section rdcss.
| Updating ld lm m1 n1 n2 p => InjRV #ld
end.
(*
Global Instance state_to_val_inj : Inj (=) (=) state_to_val.
Proof.
intros [|] [|]; simpl; intros Hv; inversion_clear Hv; done.
Qed.
*)
Definition own_token γ := (own γ (Excl ()))%I.
Definition pending_state P (n1 : Z) (proph_winner : option loc) l_ghost_winner (γ_n : gname) :=
......@@ -507,13 +507,18 @@ Section rdcss.
<<< gc_mapsto l_m #m rdcss_content γ_n (if decide (m = m1 n = n1) then n2 else n), RET #(bool_decide (n = n1)) >>>.
Proof.
iIntros (Hdisj) "#InvC #GC #InvGC". iDestruct "InvC" as (l_n) "[Heq InvC]".
iDestruct "Heq" as %->. iIntros (Φ) "AU". iLöb as "IH".
iDestruct "Heq" as %->. 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. wp_bind (CAS _ _ _)%E.
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].
......@@ -565,14 +570,15 @@ Section rdcss.
iModIntro.
(* extract state invariant *)
iDestruct "Hrest" as (q P Q l_ghost γ_t γ_s) "([Hld1 [Hld2 Hld3]] & #InvS & #P_AU & #P_GC)".
iSplitR "AU Hld2".
iSplitR "AU Hld2 Hld Hp'".
(* 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*)
(* read l_descr *)
wp_load. wp_pures.
wp_apply complete_spec; [done..|].
iIntros "_". wp_seq. by iApply "IH".
iIntros "_". wp_seq. wp_pures.
iApply ("IH" with "AU Hp' Hld").
Qed.
(** ** Proof of [new_rdcss] *)
......
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