Commit 4b06b748 authored by Gaurav Parthasarathy's avatar Gaurav Parthasarathy

Added first refinement of cinc to rdcss_minor.

    Now both the left and right reference point to an integer. rdcss_minor takes as input the pair of references and three values (m1, n1, n2). It atomically does the following:

    If the left value equals m1 and the right value equals n1, then the right value is updated to n2.
This diff is collapsed.
From stdpp Require Import namespaces.
From iris.heap_lang Require Export lifting notation.
From iris.program_logic Require Export atomic.
Set Default Proof Using "Type".
(** A general logically atomic interface for conditional increment. *)
Record atomic_rdcss_minor {Σ} `{!heapG Σ} := AtomicRdcss {
(* -- operations -- *)
new_data: val;
rdcss_minor: val;
set_value: val;
get : val;
(* -- other data -- *)
name : Type;
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 Σ;
(* -- 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;
(* -- operation specs -- *)
new_data_spec N :
{{{ True }}}
new_data #()
{{{ ctr γs, RET ctr ; is_data N γs ctr data_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 >>>
rdcss_minor v #m1 #n1 #n2 @∖↑N
<<< data_content γs m (if decide (m = m1 n = n1) then n2 else n), RET #() >>>;
set_value_spec N γs v (new_m: Z) :
is_data N γs v -
<<< (m n : Z), data_content γs m n >>>
set_value v #new_m @∖↑N
<<< data_content γs new_m n, RET #() >>>;
get_spec N γs v:
is_data N γs v -
<<< (m n : Z), data_content γs m n >>>
get v @∖↑N
<<< data_content γs m n, RET #n >>>;
Arguments atomic_rdcss_minor _ {_}.
Existing Instances
is_data_persistent data_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