Commit d76c337b authored by Gaurav Parthasarathy's avatar Gaurav Parthasarathy

changed order of arguments, added comments on implementation

parent f9e04141
......@@ -14,6 +14,20 @@ Set Default Proof Using "Type".
(** * Implementation of the functions. *)
(* 1) l_m corresponds to the A location in the paper and can differ when helping another thread
in the same RDCSS instance.
2) l_n corresponds to the B location in the paper and identifies a single RDCSS instance.
3) Values stored at the B location have type
Int + Ref (Ref * Int * Int * Int * Proph)
3.1) If the value is injL n, then no operation is on-going and the logical state is n.
3.2) If the value is injR (Ref (l_m', m1', n1', n2', p)), then an operation is on-going
with corresponding A location l_m'. The reference pointing to the tuple of values
corresponds to the descriptor in the paper. We use the name l_descr for the
such a descriptor reference.
*)
(*
new_rdcss() :=
let l_n = ref ( ref(injL 0) ) in
......@@ -24,13 +38,13 @@ Definition new_rdcss : val :=
let: "l_n" := ref (InjL #0) in "l_n".
(*
complete(l_n, l_m, l_descr, m1, n1, n2, p) :=
complete(l_descr, l_n, 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 ;; #().
*)
Definition complete : val :=
λ: "l_n" "l_m" "l_descr" "m1" "n1" "n2" "p",
λ: "l_descr" "l_m" "l_n" "m1" "n1" "n2" "p",
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" ;; #().
......@@ -57,7 +71,7 @@ Definition get : val :=
let: "n1" := Snd (Fst (Fst ("data"))) in
let: "n2" := Snd (Fst ("data")) in
let: "p" := Snd ("data") in
complete "l_n" "l_m" "l_descr" "m1" "n1" "n2" "p" ;;
complete "l_descr" "l_m" "l_n" "m1" "n1" "n2" "p" ;;
"get" "l_n"
end.
......@@ -79,15 +93,15 @@ rdcss(l_n, l_m, m1, n1, n2) :=
end.
*)
Definition rdcss: val :=
rec: "rdcss" "l_n" "l_m" "m1" "n1" "n2" :=
rec: "rdcss" "l_m" "l_n" "m1" "n1" "n2" :=
match: !"l_n" with
InjL "n" =>
if: "n" = "n1" then
let: "p" := NewProph in
let: "l_descr" := ref ("l_m", "m1", "n1", "n2", "p") in
if: (CAS "l_n" (InjL "n1") (InjR "l_descr")) = (InjL "n1") then
complete "l_n" "l_m" "l_descr" "m1" "n1" "n2" "p" ;; #true
else "rdcss" "l_n" "l_m" "m1" "n1" "n2"
complete "l_descr" "l_m" "l_n" "m1" "n1" "n2" "p" ;; #true
else "rdcss" "l_m" "l_n" "m1" "n1" "n2"
else #false
| InjR "l_descr" =>
let: "data" := !"l_descr" in
......@@ -97,8 +111,8 @@ Definition rdcss: val :=
let: "n1'" := Snd (Fst (Fst ("data"))) in
let: "n2'" := Snd (Fst ("data")) in
let: "p'" := Snd ("data") in
complete "l_n" "l_m'" "l_descr" "m1'" "n1'" "n2'" "p'" ;;
"rdcss" "l_n" "l_m" "m1" "n1" "n2"
complete "l_descr" "l_m'" "l_n" "m1'" "n1'" "n2'" "p'" ;;
"rdcss" "l_m" "l_n" "m1" "n1" "n2"
end.
(** ** Proof setup *)
......@@ -309,7 +323,7 @@ Section rdcss.
}
(* So, we are [Accepted]. Now we can show that (InjRV l_descr) = (state_to_val s), because
while a [state] protocol is not [done], it owns enough of
the [counter] protocol to ensure that does not move anywhere else. *)
the [rdcss] protocol to ensure that does not move anywhere else. *)
destruct s as [n' |ld' lm' m1' n1' n2' p'].
{ simpl. iDestruct (mapsto_agree with "Hln Hln'") as %Heq. inversion Heq. }
iDestruct (mapsto_agree with "Hln Hln'") as %[= ->].
......@@ -404,7 +418,7 @@ Section rdcss.
is_gc_loc l_m -
gc_inv -
{{{ True }}}
complete #l_n #l_m #l_descr #m1 #n1 #n2 #p
complete #l_descr #l_m #l_n #m1 #n1 #n2 #p
{{{ RET #(); (own_token γ_t ={}= (Q #true)) }}}.
Proof.
iIntros (Hdisj) "#InvC #InvS #PAU #isGC #InvGC".
......@@ -484,7 +498,7 @@ Section rdcss.
Lemma rdcss_spec γ_n v (l_m: loc) (m1 n1 n2: Z) :
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 v #l_m #m1 #n1 #n2 @((∖↑N)∖↑gcN)
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)) >>>.
Proof.
iIntros (Hdisj) "#InvC #GC #InvGC". iDestruct "InvC" as (l_n) "[Heq InvC]".
......
......@@ -29,7 +29,7 @@ Record atomic_rdcss {Σ} `{!heapG Σ, !gcG Σ} := AtomicRdcss {
rdcss_spec N γ v lm (m1 n1 n2 : Z):
N ## gcN is_rdcss N γ v - is_gc_loc lm - gc_inv -
<<< (m n: Z), gc_mapsto lm #m rdcss_content γ n >>>
rdcss v #lm #m1 #n1 #n2 @((∖↑N)∖↑gcN)
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)) >>>;
get_spec N γ v:
N ## gcN gc_inv - is_rdcss N γ v -
......
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