spec.v 1.73 KB
Newer Older
1 2 3
From stdpp Require Import namespaces.
From iris.heap_lang Require Export lifting notation.
From iris.program_logic Require Export atomic.
4
From iris_examples.logatom.lib Require Export gc.
5 6 7 8 9 10 11 12 13 14 15 16 17 18
Set Default Proof Using "Type".

(** A general logically atomic interface for conditional increment. *)
Record atomic_rdcss {Σ} `{!heapG Σ, !gcG Σ} := AtomicRdcss {
  (* -- operations -- *)
  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) (v : val) : iProp Σ;
19
  rdcss_content (γ : name) (n : val) : iProp Σ;
20 21 22 23 24
  (* -- predicate properties -- *)
  is_rdcss_persistent N γ v : Persistent (is_rdcss N γ v);
  rdcss_content_timeless γ n : Timeless (rdcss_content γ n);
  rdcss_content_exclusive γ n1 n2 : rdcss_content γ n1 - rdcss_content γ n2 - False;
  (* -- operation specs -- *)
25
  new_rdcss_spec N (init_v : val):
26 27
    N ## gcN  gc_inv -
    {{{ True }}}
28 29 30 31 32 33 34
        new_rdcss init_v
    {{{ ln γ, RET ln ; is_rdcss N γ ln  rdcss_content γ init_v }}};
  rdcss_spec N γ v (lm : loc) (m1 n1 n2 : val):
    val_is_unboxed m1  val_is_unboxed (InjLV n1)  is_rdcss N γ v -
    <<<  (m n: val), gc_mapsto lm m  rdcss_content γ n >>>
        rdcss #lm v m1 n1 n2 @((∖↑N)∖↑gcN)
    <<< gc_mapsto lm m  rdcss_content γ (if decide (m = m1  n = n1) then n2 else n), RET n >>>;
35 36
  get_spec N γ v:
    is_rdcss N γ v -
37
    <<<  (n : val), rdcss_content γ n >>>
38
        get v @(∖↑N)
39
    <<< rdcss_content γ n, RET n >>>;
40 41 42 43 44 45 46 47
}.
Arguments atomic_rdcss _ {_} {_}.


Existing Instances
  is_rdcss_persistent rdcss_content_timeless
  name_countable name_eqdec.