spec.v 1.54 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42
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 Herlihy-Wing queues. *)
Record atomic_hwq {Σ} `{!heapG Σ} := AtomicHWQ {
  (* -- operations -- *)
  new_queue : val;
  enqueue : val;
  dequeue : val;
  (* -- other data -- *)
  name : Type;
  name_eqdec : EqDecision name;
  name_countable : Countable name;
  (* -- predicates -- *)
  is_hwq (N : namespace) (sz : nat) (γ : name) (v : val) : iProp Σ;
  hwq_content (γ : name) (ls : list loc) : iProp Σ;
  (* -- predicate properties -- *)
  is_hwq_persistent N sz γ v : Persistent (is_hwq N sz γ v);
  hwq_content_timeless γ ls : Timeless (hwq_content γ ls);
  hwq_content_exclusive γ ls1 ls2 :
    hwq_content γ ls1 - hwq_content γ ls2 - False;
  (* -- operation specs -- *)
  new_queue_spec N (sz : nat) :
    0 < sz 
    {{{ True }}}
      new_queue #sz
    {{{ v γ, RET v; is_hwq N sz γ v  hwq_content γ [] }}};
  enqueue_spec N (sz : nat) (γ : name) (q : val) (l : loc) :
    is_hwq N sz γ q -
    <<<  (ls : list loc), hwq_content γ ls >>>
      enqueue q #l @   N
    <<< hwq_content γ (ls ++ [l]), RET #() >>>;
  dequeue_spec N (sz : nat) (γ : name) (q : val) :
    is_hwq N sz γ q -
    <<<  (ls : list loc), hwq_content γ ls >>>
      dequeue q @   N
    <<<  (l : loc) ls', ls = l :: ls'  hwq_content γ ls', RET #l >>>;
}.
Arguments atomic_hwq _ {_}.

Existing Instances is_hwq_persistent hwq_content_timeless.