Commit 19e774cb authored by Gaurav Parthasarathy's avatar Gaurav Parthasarathy

complete now only takes the descriptor and B location as arguments

parent f3ca2f8f
......@@ -38,13 +38,22 @@ Definition new_rdcss : val :=
let: "l_n" := ref (InjL #0) in "l_n".
(*
complete(l_descr, l_n, l_m, m1, n1, n2, p) :=
complete(l_descr, l_n) :=
let (l_m, m1, n1, n2, p) := !l_descr in
(* data = (l_m, m1, n1, n2, p) *)
let l_ghost = ref #() in
let n_new = (if !l_m = m1 then n1 else n2) in
Resolve (CAS l_n (InjR l_descr) (ref (InjL n_new))) p l_ghost ;; #().
Resolve (CAS l_n (InjR l_descr) (ref (InjL n_new))) p l_ghost ; #().
*)
Definition complete : val :=
λ: "l_descr" "l_m" "l_n" "m1" "n1" "n2" "p",
λ: "l_descr" "l_n",
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: "l_ghost" := ref #() in
let: "n_new" := (if: !"l_m" = "m1" then "n2" else "n1") in
Resolve (CAS "l_n" (InjR "l_descr") (InjL "n_new")) "p" "l_ghost" ;; #().
......@@ -54,8 +63,7 @@ Definition complete : val :=
match: !l_n with
| injL n => n
| injR (l_descr) =>
let (l_m, m1, n1, n2, p) = !l_descr
complete(l_n, l_m, l_descr, m1, n1, n2, p);
complete(l_descr, l_n);
get(l_n)
end.
*)
......@@ -64,14 +72,7 @@ Definition get : val :=
match: !"l_n" with
InjL "n" => "n"
| InjR "l_descr" =>
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" ;;
complete "l_descr" "l_n" ;;
"get" "l_n"
end.
......@@ -79,18 +80,16 @@ Definition get : val :=
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
(rec: rdcss_inner()
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) ;; n1
complete(l_descr, l_n) ; n1
else
(* CAS failed, hence we could linearize at the CAS *)
n
| InjR l_descr_other =>
let (l_m', m1', n1', n2', p') := !l_descr_other in
complete(l_descr_other, l_m', l_n, m1', n1', n2', p') ;;
complete(l_descr_other, l_n) ;
rdcss_inner()
end
)()
......@@ -101,31 +100,23 @@ Definition rdcss: val :=
let: "p" := NewProph in
let: "l_descr" := ref ("l_m", "m1", "n1", "n2", "p") in
(* start rdcss computation with allocated descriptor *)
(
rec: "rdcss_inner" "_":=
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" ;; "n1"
else
(* CAS failed, hence we could linearize at the CAS *)
"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
(* 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" #()
end
) #().
( rec: "rdcss_inner" "_" :=
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_n" ;; "n1"
else
(* CAS failed, hence we could linearize at the CAS *)
"n"
| InjR "l_descr_other" =>
(* a descriptor from a different operation was read, try to help and then restart *)
complete "l_descr_other" "l_n" ;;
"rdcss_inner" #()
end
) #().
(** ** Proof setup *)
......@@ -415,19 +406,20 @@ Section rdcss.
this request, then you get [Q]. But we also try to complete other
thread's requests, which is why we cannot ask for the token
as a precondition. *)
Lemma complete_spec (l_n l_m l_descr : loc) (m1 n1 n2 : Z) (p : proph_id) γ_n γ_t γ_s l_ghost_inv P Q :
Lemma complete_spec (l_n l_m l_descr : loc) (m1 n1 n2 : Z) (p : proph_id) γ_n γ_t γ_s l_ghost_inv P Q q:
N ## gcN
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 -
is_gc_loc l_m -
gc_inv -
{{{ True }}}
complete #l_descr #l_m #l_n #m1 #n1 #n2 #p
{{{ l_descr {q} (#l_m, #m1, #n1, #n2, #p) }}}
complete #l_descr #l_n
{{{ RET #(); (own_token γ_t ={}= (Q #n1)) }}}.
Proof.
iIntros (Hdisj) "#InvC #InvS #PAU #isGC #InvGC".
iModIntro. iIntros (Φ) "_ HQ". wp_lam. wp_pures.
iModIntro. iIntros (Φ) "Hld HQ". wp_lam. wp_let.
wp_bind (! _)%E. wp_load. iClear "Hld". wp_pures.
wp_alloc l_ghost as "[Hl_ghost' Hl_ghost'2]". wp_pures.
wp_bind (! _)%E.
(* open outer invariant *)
......@@ -540,14 +532,14 @@ Section rdcss.
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".
iModIntro. iDestruct "Hld" as "[Hld1 [Hld2 Hld3]]". iSplitR "Hld2 Token".
{ (* close outer invariant *)
iNext. iExists (Updating l_descr l_m m1 n n2 p').
iNext. iCombine "Hld1 Hld3" as "Hld1". 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..|].
wp_if. wp_apply (complete_spec with "[] [] [] [] [] [$Hld2]");[ done..|].
iIntros "Ht". iMod ("Ht" with "Token") as "Φ". by wp_seq.
+ (* values do not match -> CAS fails
we can commit here *)
......@@ -569,12 +561,10 @@ Section rdcss.
(* extract state invariant *)
iDestruct "Hrest" as (q P Q l_ghost γ_t γ_s) "([Hld1 [Hld2 Hld3]] & #InvS & #P_AU & #P_GC)".
iSplitR "AU Hld2 Hld Hp'".
(* close invariant, retain some permission to l_descr', so that we can read it later *)
(* close invariant, retain some permission to l_descr', so it can be read 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..|].
wp_let. wp_match.
wp_apply (complete_spec with "[] [] [] [] [] [$Hld2]"); [done..|].
iIntros "_". wp_seq. wp_pures.
iApply ("IH" with "AU Hp' Hld").
Qed.
......@@ -623,8 +613,8 @@ Section rdcss.
iModIntro. iSplitR "AU Hld'". {
iNext. iExists (Updating l_descr lm m1 n1 n2 p). eauto 11 with iFrame.
}
wp_match. wp_load. wp_pures. wp_bind (complete _ _ _ _ _ _ _)%E.
wp_apply complete_spec; [done..|].
wp_match.
wp_apply (complete_spec with "[] [] [] [] [] [$Hld']"); [done..|].
iIntros "Ht". wp_seq. iApply "IH". iApply "AU".
Qed.
......
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