Commit f1b868e3 authored by Gaurav Parthasarathy's avatar Gaurav Parthasarathy

generalized rdcss_minor to return boolean indicating if the n1 matches the...

generalized rdcss_minor to return boolean indicating if the n1 matches the value read at the second location lln
parent 6bf8e10f
......@@ -97,9 +97,9 @@ rdcss_minor(data, m1, n1, n2) :=
let p = NewProph in
let lnew = ref (injR ((m1, (n1, n2)), p)) in
if CAS(lln, ln, lnew) then
complete(lln, lm, lnew, m1, n1, n2, p); skip
complete(lln, lm, lnew, m1, n1, n2, p); #true
else rdcss_minor(data, m1, n1, n2)
else #()
else #false
| injR "( (m1', (n1', n2')), p')" =>
complete(lln, lm, ln, m1', n1', n2', p');
rdcss_minor(data, m1, n1, n2)
......@@ -116,9 +116,9 @@ Definition rdcss_minor : val :=
let: "p" := NewProph in
let: "lnew" := ref (InjR (("m1", ("n1", "n2")), "p")) in
if: CAS "lln" "ln" "lnew" then
complete "lln" "lm" "lnew" "m1" "n1" "n2" "p" ;; Skip
complete "lln" "lm" "lnew" "m1" "n1" "n2" "p" ;; #true
else "rdcss_minor" "data" "m1" "n1" "n2"
else #()
else #false
| InjR "args'" =>
(* args' = ( (m1', (n1', n2')) , p') *)
let: "m1'" := (Fst (Fst "args'")) in
......@@ -228,12 +228,12 @@ Section rdcss_minor.
( vs, proph p vs
(own γ_s (Cinl $ Excl ())
(c_l {1/2} #l ( pending_state P n (val_to_some_loc vs) l_ghost_winner γ_n
accepted_state Q (val_to_some_loc vs) l_ghost_winner ))
own γ_s (Cinr $ to_agree ()) done_state Q l l_ghost_winner γ_t))%I.
accepted_state (Q #true) (val_to_some_loc vs) l_ghost_winner ))
own γ_s (Cinr $ to_agree ()) done_state (Q #true) l l_ghost_winner γ_t))%I.
Definition pau P Q γs m1 n1 n2 :=
( P - AU << (m n : Z), data_content γs m n >> @ ∖↑N,
<< data_content γs m (if (decide ((m = m1) (n = n1))) then n2 else n), COMM Q >>)%I.
<< data_content γs m (if (decide ((m = m1) (n = n1))) then n2 else n), COMM Q (if decide (n = n1) then #true else #false) >>)%I.
Definition data_inv γ_m γ_n lm lln :=
( (m : Z) (ln : loc) (q : Qp) (s : abstract_state),
......@@ -287,7 +287,7 @@ Section rdcss_minor.
Lemma state_done_extract_Q P Q p n lln ln l_ghost γ_n γ_t γ_s :
inv stateN (state_inv P Q p n lln ln l_ghost γ_n γ_t γ_s) -
own γ_s (Cinr (to_agree ())) -
(own_token γ_t ={}= Q).
(own_token γ_t ={}= (Q #true)).
Proof.
iIntros "#Hinv #Hs !# Ht".
iInv stateN as (vs) "(Hp & [NotDone | Done])".
......@@ -312,7 +312,7 @@ Section rdcss_minor.
inv stateN (state_inv P Q p n1 lln ln l_ghost γ_n γ_t γ_s) -
pau P Q (γ_m, γ_n) m1 n1 n2 -
l_ghost {1 / 2} #() -
((own_token γ_t ={}= Q) - Φ #()) -
((own_token γ_t ={}= (Q #true)) - Φ #()) -
own γ_n ( Excl' n) -
l_new InjLV #n -
WP Resolve (CAS #lln #ln #l_new) #p #l_ghost ;; #() {{ v, Φ v }}.
......@@ -363,7 +363,7 @@ Section rdcss_minor.
inv dataN (data_inv γ_m γ_n lm lln) -
inv stateN (state_inv P Q p n1 lln ln l_ghost_inv γ_n γ_t γ_s) -
pau P Q (γ_m, γ_n) m1 n1 n2 -
((own_token γ_t ={}= Q) - Φ #()) -
((own_token γ_t ={}= (Q #true)) - Φ #()) -
l_new InjLV #n -
WP Resolve (CAS #lln #ln #l_new) #p #l_ghost ;; #() {{ v, Φ v }}.
Proof.
......@@ -411,7 +411,7 @@ Section rdcss_minor.
pau P Q (γ_m, γ_n) m1 n1 n2 -
{{{ True }}}
complete #lln #lm #ln #m1 #n1 #n2 #p
{{{ RET #(); (own_token γ_t ={}= Q) }}}.
{{{ RET #(); (own_token γ_t ={}= (Q #true)) }}}.
Proof.
iIntros "#InvC #InvS #PAU".
iModIntro. iIntros (Φ) "_ HQ". wp_lam. wp_pures.
......@@ -440,6 +440,7 @@ 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 _.
destruct (decide _); last done;
destruct (val_to_some_loc vs) eqn:Hvts; iFrame. }
(* close outer inv *)
iModIntro. iSplitR "Hl_ghost'2 HQ Hn●".
......@@ -477,7 +478,7 @@ Section rdcss_minor.
is_data γs v -
<<< (m n: Z), data_content γs m n >>>
rdcss_minor v #m1 #n1 #n2 @∖↑N
<<< data_content γs m (if decide (m = m1 n = n1) then n2 else n), RET #() >>>.
<<< data_content γs m (if decide (m = m1 n = n1) then n2 else n), RET if decide (n = n1) then #true else #false >>>.
Proof.
iIntros "#InvC". iDestruct "InvC" as (γ_m γ_n lm lln) "[Heq InvC]".
iDestruct "Heq" as %[-> ->]. iIntros (Φ) "AU". iLöb as "IH".
......@@ -517,7 +518,7 @@ Section rdcss_minor.
iNext. iExists _, _, _, (Updating m1 n n2 p'). eauto 10 with iFrame.
}
wp_if. wp_apply complete_spec; [done..|].
iIntros "Ht". iMod ("Ht" with "Token") as "Φ". wp_seq. by wp_lam.
iIntros "Ht". iMod ("Ht" with "Token") as "Φ". by wp_seq.
* (* CAS fails: closing invariant and invoking IH *)
wp_cas_fail.
iModIntro. iSplitR "AU".
......@@ -533,7 +534,7 @@ Section rdcss_minor.
{ iModIntro. iExists _, _, (q/2)%Qp, (Quiescent n''). iFrame. }
wp_let. wp_load. wp_match.
wp_op. case_bool_decide; simplify_eq; wp_if.
iFrame.
destruct (decide _); done.
- (* l' ↦ injR *)
iModIntro.
(* extract state invariant *)
......
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