Commit c3aaa5db authored by Gaurav Parthasarathy's avatar Gaurav Parthasarathy

minor changes as suggested by merge request discussion

parent dadcdd18
Pipeline #17702 failed with stage
......@@ -28,7 +28,7 @@ Set Default Proof Using "Type".
(*
new_rdcss() :=
let lln = ref (injL 0) in
let lln = ref ( ref(injL 0) ) in
let lm = ref false in
ref (lm, lln)
*)
......@@ -54,9 +54,9 @@ Definition set_value : val :=
*)
Definition complete : val :=
λ: "lln" "lm" "ln" "m1" "n1" "n2" "p",
let: "l_ghost" := ref #() in
let: "n_new" := (if: !"lm" = "m1" then "n2" else "n1") in
Resolve (CAS "lln" "ln" (ref (InjL "n_new"))) "p" "l_ghost" ;; #().
let: "l_ghost" := ref #() in
let: "n_new" := (if: !"lm" = "m1" then "n2" else "n1") in
Resolve (CAS "lln" "ln" (ref (InjL "n_new"))) "p" "l_ghost" ;; #().
(*
get(rdcss_data) :=
......@@ -625,7 +625,7 @@ Section rdcss.
End rdcss.
Definition atomic_rdcss `{!heapG Σ, rdcssG Σ} :
Definition atomic_rdcss `{!heapG Σ, !rdcssG Σ} :
spec.atomic_rdcss Σ :=
{| spec.new_rdcss_spec := new_rdcss_spec;
spec.rdcss_spec := rdcss_spec;
......
......@@ -20,8 +20,7 @@ Record atomic_rdcss {Σ} `{!heapG Σ} := AtomicRdcss {
(* -- predicate properties -- *)
is_rdcss_persistent N γs v : Persistent (is_rdcss N γs v);
rdcss_content_timeless γs f c : Timeless (rdcss_content γs f c);
rdcss_content_exclusive γs f1 c1 f2 c2 :
rdcss_content γs f1 c1 - rdcss_content γs f2 c2 - False;
rdcss_content_exclusive γs f1 c1 f2 c2 : rdcss_content γs f1 c1 - rdcss_content γs f2 c2 - False;
(* -- operation specs -- *)
new_rdcss_spec N :
{{{ True }}}
......
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