Commit ea7f7b7b authored by Gaurav Parthasarathy's avatar Gaurav Parthasarathy

small fix to rdcss description

parent 61c1f103
Pipeline #17831 canceled with stage
......@@ -80,7 +80,7 @@ Definition get : val :=
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(_)
(rec: rdcss_inner()
match r with
InjL n =>
if n = n1 then
......@@ -89,11 +89,11 @@ Definition get : val :=
(* CAS failed, hence we could linearize at the CAS *)
#false
| InjR l_descr_other =>
let (l_m', m1', n1', n2', p') := !l_descr in
let (l_m', m1', n1', n2', p') := !l_descr_other in
complete(l_descr_other, l_m', l_n, m1', n1', n2', p') ;;
rdcss_inner(_)
rdcss_inner()
end
)(#())
)()
*)
Definition rdcss: val :=
λ: "l_m" "l_n" "m1" "n1" "n2",
......
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