Commit bbf33b66 authored by Rodolphe Lepigre's avatar Rodolphe Lepigre Committed by Ralf Jung

Modification of the RDCSS example to use meta tokens

(and some cleanup)
parent d731cb31
This diff is collapsed.
......@@ -17,39 +17,33 @@ Record atomic_rdcss {Σ} `{!heapG Σ, !gcG Σ} := AtomicRdcss {
new_rdcss : val;
rdcss: val;
get : val;
(* -- other data -- *)
name : Type;
name_eqdec : EqDecision name;
name_countable : Countable name;
(* -- predicates -- *)
is_rdcss (N : namespace) (γ : name) (l_n : loc) : iProp Σ;
rdcss_content (γ : name) (n : val) : iProp Σ;
is_rdcss (N : namespace) (l_n : loc) : iProp Σ;
rdcss_state (N : namespace) (l_n : loc) (n : val) : iProp Σ;
(* -- predicate properties -- *)
is_rdcss_persistent N γ l_n : Persistent (is_rdcss N γ l_n);
rdcss_content_timeless γ n : Timeless (rdcss_content γ n);
rdcss_content_exclusive γ n1 n2 : rdcss_content γ n1 - rdcss_content γ n2 - False;
is_rdcss_persistent N l_n : Persistent (is_rdcss N l_n);
rdcss_state_timeless N l_n n : Timeless (rdcss_state N l_n n);
rdcss_state_exclusive N l_n n1 n2 :
rdcss_state N l_n n1 - rdcss_state N l_n n2 - False;
(* -- operation specs -- *)
new_rdcss_spec N (n : val):
N ## gcN gc_inv -
{{{ True }}}
new_rdcss n
{{{ l_n γ, RET #l_n ; is_rdcss N γ l_n rdcss_content γ n }}};
rdcss_spec N γ (l_n l_m : loc) (m1 n1 n2 : val):
{{{ l_n, RET #l_n ; is_rdcss N l_n rdcss_state N l_n n }}};
rdcss_spec N (l_n l_m : loc) (m1 n1 n2 : val):
val_is_unboxed m1
val_is_unboxed (InjLV n1)
is_rdcss N γ l_n -
<<< (m n: val), gc_mapsto l_m m rdcss_content γ n >>>
is_rdcss N l_n -
<<< (m n: val), gc_mapsto l_m m rdcss_state N l_n n >>>
rdcss #l_m #l_n m1 n1 n2 @((∖↑N)∖↑gcN)
<<< gc_mapsto l_m m rdcss_content γ (if decide (m = m1 n = n1) then n2 else n), RET n >>>;
get_spec N γ (l_n : loc):
is_rdcss N γ l_n -
<<< (n : val), rdcss_content γ n >>>
<<< gc_mapsto l_m m rdcss_state N l_n (if decide (m = m1 n = n1) then n2 else n), RET n >>>;
get_spec N (l_n : loc):
is_rdcss N l_n -
<<< (n : val), rdcss_state N l_n n >>>
get #l_n @(∖↑N)
<<< rdcss_content γ n, RET n >>>;
<<< rdcss_state N l_n n, RET n >>>;
}.
Arguments atomic_rdcss _ {_} {_}.
Existing Instances
is_rdcss_persistent rdcss_content_timeless
name_countable name_eqdec.
Existing Instances is_rdcss_persistent rdcss_state_timeless.
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