Commit 307d1cae authored by Gaurav Parthasarathy's avatar Gaurav Parthasarathy

updated to CAS which returns old value read

parent ee38171a
Pipeline #17631 failed with stage
......@@ -97,7 +97,7 @@ rdcss_minor(rdcss_data, m1, n1, n2) :=
if n = n1 then
let p = NewProph in
let lnew = ref (injR ((m1, (n1, n2)), p)) in
if CAS(lln, ln, lnew) then
if CAS(lln, ln, lnew) = ln then
complete(lln, lm, lnew, m1, n1, n2, p); #true
else rdcss_minor(data, m1, n1, n2)
else #false
......@@ -116,7 +116,7 @@ Definition rdcss_minor : val :=
if: "n" = "n1" then
let: "p" := NewProph in
let: "lnew" := ref (InjR (("m1", ("n1", "n2")), "p")) in
if: CAS "lln" "ln" "lnew" then
if: (CAS "lln" "ln" "lnew") = "ln" then
complete "lln" "lm" "lnew" "m1" "n1" "n2" "p" ;; #true
else "rdcss_minor" "rdcss_data" "m1" "n1" "n2"
else #false
......@@ -177,10 +177,10 @@ Section rdcss_minor.
(** Definition of the invariant *)
Fixpoint val_to_some_loc (vs : list (val * val)) : option loc :=
Fixpoint val_to_some_loc (ln: loc) (vs : list (val * val)) : option loc :=
match vs with
| (#true , LitV (LitLoc l)) :: _ => Some l
| _ :: vs => val_to_some_loc vs
| (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.
......@@ -228,8 +228,8 @@ Section rdcss_minor.
Definition state_inv P Q (p : proph_id) n (lln ln l_ghost_winner : loc) γ_n γ_t γ_s : iProp Σ :=
( vs, proph p vs
(own γ_s (Cinl $ Excl ())
(lln {1/2} #ln ( pending_state P n (val_to_some_loc vs) l_ghost_winner γ_n
accepted_state (Q #true) (val_to_some_loc vs) l_ghost_winner ))
(lln {1/2} #ln ( pending_state P n (val_to_some_loc ln vs) l_ghost_winner γ_n
accepted_state (Q #true) (val_to_some_loc ln vs) l_ghost_winner ))
own γ_s (Cinr $ to_agree ()) done_state (Q #true) ln l_ghost_winner γ_t))%I.
Definition pau P Q γs m1 n1 n2 :=
......@@ -343,7 +343,7 @@ Section rdcss_minor.
(* We perform the CAS. *)
iCombine "Hlln Hlln'" as "Hlln".
wp_apply (wp_resolve with "Hp"); first done; wp_cas_suc.
iIntros (vs' ->) "Hp'". simpl.
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".
......@@ -381,7 +381,8 @@ Section rdcss_minor.
iDestruct (mapsto_agree with "Hlln Hlln'") as %[=->].
iCombine "Hlln Hlln'" as "Hlln".
wp_apply (wp_resolve with "Hp"); first done; wp_cas_suc.
iIntros (vs' ->). iDestruct "State" as "[Pending | Accepted]".
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]. *)
......@@ -443,8 +444,8 @@ Section rdcss_minor.
iModIntro. iSplitL "Q Hl_ghost' Hp Hvs Hs Hlln'".
{ iNext. iExists _. iFrame "Hp". iLeft. iFrame.
iRight. iSplitL "Hl_ghost'"; first by iExists _.
case_bool_decide; last done;
destruct (val_to_some_loc vs) eqn:Hvts; iFrame. }
case_bool_decide; simplify_eq;
destruct (val_to_some_loc ln vs) eqn:Hvts; iFrame. }
(* close outer inv *)
iModIntro. iSplitR "Hl_ghost'2 HQ Hn●".
{ eauto 12 with iFrame. }
......@@ -486,7 +487,7 @@ Section rdcss_minor.
iIntros "#InvC". iDestruct "InvC" as (γ_m γ_n lm lln) "[Heq InvC]".
iDestruct "Heq" as %[-> ->]. iIntros (Φ) "AU". iLöb as "IH".
wp_lam. wp_pures. wp_bind (!_)%E.
iInv rdcssN as (m' ln' q s) "(>Hlm & >Hlln & >[Hln [Hln' Hln'']] & >Hm● & Hrest)".
iInv rdcssN as (m ln q s) "(>Hlm & >Hlln & >[Hln [Hln' Hln'']] & >Hm● & Hrest)".
wp_load. destruct s as [n|m1' n1' n2' p].
- iDestruct "Hrest" as "(Hc' & Hn●)".
destruct (decide (n1 = n)) as [-> | Hneq].
......@@ -500,8 +501,8 @@ Section rdcss_minor.
wp_let. wp_alloc ly as "Hly".
wp_let. wp_bind (CAS _ _ _)%E.
(* open outer invariant again to CAS lln *)
iInv rdcssN as (m2 ln'' q2 s) "(>Hlm & >Hlln & >Hln & >Hm● & Hrest)".
destruct (decide (ln' = ln'')) as [<- | Hn].
iInv rdcssN as (m' ln' q2 s) "(>Hlm & >Hlln & >Hln & >Hm● & Hrest)".
destruct (decide (ln = ln')) as [<- | Hn].
* (* CAS succeeds *)
iDestruct (mapsto_agree with "Hln' Hln") as %<-%state_to_val_inj.
iDestruct "Hrest" as ">[Hlln' Hn●]". iCombine "Hlln Hlln'" as "Hlln".
......@@ -511,21 +512,23 @@ Section rdcss_minor.
iMod (own_alloc (Excl ())) as (γ_t) "Token"; first done.
iMod (own_alloc (Cinl $ Excl ())) as (γ_s) "Hs"; first done.
iDestruct "Hlln" as "[Hlln Hlln']".
set (winner := default ly (val_to_some_loc proph_values)).
set (winner := default ly (val_to_some_loc ly proph_values)).
iMod (inv_alloc stateN _ (state_inv AU_later _ _ _ _ _ winner _ _ _)
with "[AU Hs Hp' Hlln' Hn●]") as "#Hinv".
{ iNext. iExists _. iFrame "Hp'". iLeft. iFrame. iLeft.
iFrame. destruct (val_to_some_loc proph_values); simpl; done. }
iFrame. destruct (val_to_some_loc ly proph_values); simpl; done. }
iModIntro. iDestruct "Hly" as "[Hly1 Hly2]". iSplitR "Hln' Token". {
(* close invariant *)
iNext. iExists _, _, _, (Updating m1 n n2 p'). eauto 10 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. iFrame. }
wp_op. case_bool_decide; simplify_eq.
wp_if. by iApply "IH".
+ (* values do not match: commit *)
iMod "AU" as (m'' n'') "[[Hm◯ Hn◯] [_ Hclose]]"; simpl.
......@@ -631,4 +634,3 @@ Definition atomic_rdcss_minor `{!heapG Σ, rdcssminorG Σ} :
spec.rdcss_content_exclusive := rdcss_content_exclusive |}.
Typeclasses Opaque rdcss_content is_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