Commit 61c1f103 authored by Gaurav Parthasarathy's avatar Gaurav Parthasarathy

made rdcss_inner an actual closure (all the arguments remain the same)

parent 04407ae9
Pipeline #17830 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(l_descr, l_m, l_n, m1, n1, n2)
(rec: rdcss_inner(_)
match r with
InjL n =>
if n = n1 then
......@@ -88,12 +88,12 @@ Definition get : val :=
else
(* CAS failed, hence we could linearize at the CAS *)
#false
| InjR l_descr =>
| InjR l_descr_other =>
let (l_m', m1', n1', n2', p') := !l_descr in
complete(l_descr, l_m', l_n, m1', n1', n2', p') ;;
rdcss(l_m, l_n, m1, n1, n2)
complete(l_descr_other, l_m', l_n, m1', n1', n2', p') ;;
rdcss_inner(_)
end
)(l_descr, l_m, l_n, m1, n1, n2)
)(#())
*)
Definition rdcss: val :=
λ: "l_m" "l_n" "m1" "n1" "n2",
......@@ -102,7 +102,7 @@ Definition rdcss: val :=
let: "l_descr" := ref ("l_m", "m1", "n1", "n2", "p") in
(* start rdcss computation with allocated descriptor *)
(
rec: "rdcss_inner" "l_descr" "l_m" "l_n" "m1" "n1" "n2" :=
rec: "rdcss_inner" "_":=
let: "r" := (CAS "l_n" (InjL "n1") (InjR "l_descr")) in
match: "r" with
InjL "n" =>
......@@ -123,9 +123,9 @@ Definition rdcss: val :=
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" "l_descr" "l_m" "l_n" "m1" "n1" "n2"
"rdcss_inner" #()
end
) "l_descr" "l_m" "l_n" "m1" "n1" "n2".
) #().
(** ** Proof setup *)
......
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