Commit 04407ae9 authored by Gaurav Parthasarathy's avatar Gaurav Parthasarathy

adjusted return value of atomic triple to integer read at first location

parent 34205ce9
Pipeline #17829 canceled with stage
......@@ -109,10 +109,10 @@ Definition rdcss: val :=
(* 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
complete "l_descr" "l_m" "l_n" "m1" "n1" "n2" "p" ;; "n1"
else
(* CAS failed, hence we could linearize at the CAS *)
#false
"n"
| InjR "l_descr_other" =>
(* a descriptor from a different operation was read, try to help and then restart *)
let: "data" := !"l_descr_other" in
......@@ -208,8 +208,8 @@ Section rdcss.
"location" token to ensure there is no ABA going on. Notice how [rdcss_inv]
owns *more than* half of its [l_descr] in the Updating state,
which means we know that the [l_descr] there and here cannot be the same. *)
Definition done_state Q (l_descr l_ghost_winner : loc) (γ_t : gname) :=
((Q own_token γ_t) l_ghost_winner - (l_descr {1/2} -) )%I.
Definition done_state Qn (l_descr l_ghost_winner : loc) (γ_t : gname) :=
((Qn own_token γ_t) l_ghost_winner - (l_descr {1/2} -) )%I.
(* We always need the [proph] in here so that failing threads coming late can
always resolve their stuff.
......@@ -219,13 +219,13 @@ Section rdcss.
( vs, proph p vs
(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
accepted_state (Q #true) (val_to_some_loc l_descr vs) l_ghost_winner ))
own γ_s (Cinr $ to_agree ()) done_state (Q #true) l_descr l_ghost_winner γ_t))%I.
accepted_state (Q #n) (val_to_some_loc l_descr vs) l_ghost_winner ))
own γ_s (Cinr $ to_agree ()) done_state (Q #n) l_descr l_ghost_winner γ_t))%I.
Definition pau P Q γ l_m m1 n1 n2 :=
( 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)),
COMM Q #(bool_decide (n = n1)) >>)%I.
COMM Q #n >>)%I.
Definition rdcss_inv γ_n l_n :=
( (s : abstract_state),
......@@ -280,7 +280,7 @@ Section rdcss.
Lemma state_done_extract_Q P Q p n l_n l_descr l_ghost γ_n γ_t γ_s :
inv stateN (state_inv P Q p n l_n l_descr l_ghost γ_n γ_t γ_s) -
own γ_s (Cinr (to_agree ())) -
(own_token γ_t ={}= (Q #true)).
(own_token γ_t ={}= (Q #n)).
Proof.
iIntros "#Hinv #Hs !# Ht".
iInv stateN as (vs) "(Hp & [NotDone | Done])".
......@@ -288,10 +288,10 @@ Section rdcss.
iDestruct "NotDone" as "(>Hs' & _ & _)".
iDestruct (own_valid_2 with "Hs Hs'") as %?. contradiction.
* iDestruct "Done" as "(_ & QT & Hghost)".
iDestruct "QT" as "[Q | >T]"; last first.
iDestruct "QT" as "[Qn | >T]"; last first.
{ iDestruct (own_valid_2 with "Ht T") as %Contra.
by inversion Contra. }
iSplitR "Q"; last done. iIntros "!> !>". unfold state_inv.
iSplitR "Qn"; last done. iIntros "!> !>". unfold state_inv.
iExists _. iFrame "Hp". iRight.
unfold done_state. iFrame "#∗".
Qed.
......@@ -305,7 +305,7 @@ Section rdcss.
inv stateN (state_inv P Q p n1 l_n l_descr l_ghost γ_n γ_t γ_s) -
pau P Q γ_n l_m m1 n1 n2 -
l_ghost {1 / 2} #() -
((own_token γ_t ={}= (Q #true)) - Φ #()) -
((own_token γ_t ={}= (Q #n1)) - Φ #()) -
own γ_n ( Excl' n) -
WP Resolve (CAS #l_n (InjRV #l_descr) (InjLV #n)) #p #l_ghost ;; #() {{ v, Φ v }}.
......@@ -360,7 +360,7 @@ Section rdcss.
inv rdcssN (rdcss_inv γ_n l_n) -
inv stateN (state_inv P Q p n1 l_n l_descr l_ghost_inv γ_n γ_t γ_s) -
pau P Q γ_n l_m m1 n1 n2 -
((own_token γ_t ={}= (Q #true)) - Φ #()) -
((own_token γ_t ={}= (Q #n1)) - Φ #()) -
WP Resolve (CAS #l_n (InjRV #l_descr) (InjLV #n)) #p #l_ghost ;; #() {{ v, Φ v }}.
Proof.
......@@ -424,7 +424,7 @@ Section rdcss.
gc_inv -
{{{ True }}}
complete #l_descr #l_m #l_n #m1 #n1 #n2 #p
{{{ RET #(); (own_token γ_t ={}= (Q #true)) }}}.
{{{ RET #(); (own_token γ_t ={}= (Q #n1)) }}}.
Proof.
iIntros (Hdisj) "#InvC #InvS #PAU #isGC #InvGC".
iModIntro. iIntros (Φ) "_ HQ". wp_lam. wp_pures.
......@@ -461,7 +461,6 @@ Section rdcss.
iModIntro. iSplitL "Q Hl_ghost' Hp Hvs Hs Hln'".
{ iModIntro. iNext. iExists _. iFrame "Hp". iLeft. iFrame.
iRight. iSplitL "Hl_ghost'"; first by iExists _.
case_bool_decide; simplify_eq;
destruct (val_to_some_loc l_descr vs) eqn:Hvts; iFrame. }
(* close outer inv *)
iModIntro. iSplitR "Hl_ghost'2 HQ Hn●".
......@@ -504,7 +503,7 @@ Section rdcss.
N ## gcN is_rdcss γ_n v - is_gc_loc l_m - gc_inv -
<<< (m n: Z), gc_mapsto l_m #m rdcss_content γ_n n >>>
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 #(bool_decide (n = n1)) >>>.
<<< gc_mapsto l_m #m rdcss_content γ_n (if decide (m = m1 n = n1) then n2 else n), RET #n >>>.
Proof.
iIntros (Hdisj) "#InvC #GC #InvGC". iDestruct "InvC" as (l_n) "[Heq InvC]".
iDestruct "Heq" as %->. iIntros (Φ) "AU".
......@@ -560,9 +559,8 @@ Section rdcss.
{ destruct (decide _) as [[_ ?] | _]; [done | iFrame ]. }
iModIntro. iSplitR "HΦ".
{ iModIntro. iExists (Quiescent n''). iFrame. }
wp_let. wp_match. case_bool_decide; simplify_eq.
wp_op.
case_bool_decide; simplify_eq. wp_if. iFrame.
wp_let. wp_match. wp_op. case_bool_decide; simplify_eq.
wp_if. iFrame.
- (* l_n ↦ injR l_ndescr' *)
(* a descriptor l_descr' is currently stored at l_n -> CAS fails
try to help the on-going operation *)
......
......@@ -30,7 +30,7 @@ Record atomic_rdcss {Σ} `{!heapG Σ, !gcG Σ} := AtomicRdcss {
N ## gcN is_rdcss N γ v - is_gc_loc lm - gc_inv -
<<< (m n: Z), gc_mapsto lm #m rdcss_content γ n >>>
rdcss #lm v #m1 #n1 #n2 @((∖↑N)∖↑gcN)
<<< gc_mapsto lm #m rdcss_content γ (if decide (m = m1 n = n1) then n2 else n), RET #(bool_decide (n = n1)) >>>;
<<< gc_mapsto lm #m rdcss_content γ (if decide (m = m1 n = n1) then n2 else n), RET #n >>>;
get_spec N γ v:
N ## gcN gc_inv - is_rdcss N γ v -
<<< (n : Z), rdcss_content γ 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