Commit dc62b1b1 authored by Gaurav Parthasarathy's avatar Gaurav Parthasarathy

changed data name to rdcss

parent c90f27aa
Pipeline #17624 canceled with stage
This diff is collapsed.
......@@ -6,7 +6,7 @@ Set Default Proof Using "Type".
(** A general logically atomic interface for conditional increment. *)
Record atomic_rdcss_minor {Σ} `{!heapG Σ} := AtomicRdcss {
(* -- operations -- *)
new_data: val;
new_rdcss : val;
rdcss_minor: val;
set_value: val;
get : val;
......@@ -15,36 +15,36 @@ Record atomic_rdcss_minor {Σ} `{!heapG Σ} := AtomicRdcss {
name_eqdec : EqDecision name;
name_countable : Countable name;
(* -- predicates -- *)
is_data (N : namespace) (γs : name) (v : val) : iProp Σ;
data_content (γs : name) (m n : Z) : iProp Σ;
is_rdcss (N : namespace) (γs : name) (v : val) : iProp Σ;
rdcss_content (γs : name) (m n : Z) : iProp Σ;
(* -- predicate properties -- *)
is_data_persistent N γs v : Persistent (is_data N γs v);
data_content_timeless γs f c : Timeless (data_content γs f c);
data_content_exclusive γs f1 c1 f2 c2 :
data_content γs f1 c1 - data_content γs f2 c2 - False;
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;
(* -- operation specs -- *)
new_data_spec N :
new_rdcss_spec N :
{{{ True }}}
new_data #()
{{{ ctr γs, RET ctr ; is_data N γs ctr data_content γs 0 0 }}};
new_rdcss #()
{{{ ctr γs, RET ctr ; is_rdcss N γs ctr rdcss_content γs 0 0 }}};
rdcss_minor_spec N γs v (m1 n1 n2 : Z):
is_data N γs v -
<<< (m n: Z), data_content γs m n >>>
is_rdcss N γs v -
<<< (m n: Z), rdcss_content γs m n >>>
rdcss_minor v #m1 #n1 #n2 @∖↑N
<<< data_content γs m (if decide (m = m1 n = n1) then n2 else n), RET if decide (n = n1) then #true else #false >>>;
<<< rdcss_content γs m (if decide (m = m1 n = n1) then n2 else n), RET if decide (n = n1) then #true else #false >>>;
set_value_spec N γs v (new_m: Z) :
is_data N γs v -
<<< (m n : Z), data_content γs m n >>>
is_rdcss N γs v -
<<< (m n : Z), rdcss_content γs m n >>>
set_value v #new_m @∖↑N
<<< data_content γs new_m n, RET #() >>>;
<<< rdcss_content γs new_m n, RET #() >>>;
get_spec N γs v:
is_data N γs v -
<<< (m n : Z), data_content γs m n >>>
is_rdcss N γs v -
<<< (m n : Z), rdcss_content γs m n >>>
get v @∖↑N
<<< data_content γs m n, RET #n >>>;
<<< rdcss_content γs m n, RET #n >>>;
}.
Arguments atomic_rdcss_minor _ {_}.
Existing Instances
is_data_persistent data_content_timeless
is_rdcss_persistent rdcss_content_timeless
name_countable name_eqdec.
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