lock.v 1.35 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
From iris.heap_lang Require Export lifting notation.
2
From iris.base_logic.lib Require Export invariants.
Zhen Zhang's avatar
Zhen Zhang committed
3

4 5 6 7 8 9 10 11 12 13 14 15 16 17
Structure lock Σ `{!heapG Σ} := Lock {
  (* -- operations -- *)
  newlock : val;
  acquire : val;
  release : val;
  (* -- predicates -- *)
  (* name is used to associate locked with is_lock *)
  name : Type;
  is_lock (N: namespace) (γ: name) (lock: val) (R: iProp Σ) : iProp Σ;
  locked (γ: name) : iProp Σ;
  (* -- general properties -- *)
  is_lock_ne N γ lk n: Proper (dist n ==> dist n) (is_lock N γ lk);
  is_lock_persistent N γ lk R : PersistentP (is_lock N γ lk R);
  locked_timeless γ : TimelessP (locked γ);
18
  locked_exclusive γ : locked γ - locked γ - False;
19
  (* -- operation specs -- *)
20
  newlock_spec N (R : iProp Σ) :
21
    {{{ R }}} newlock #() {{{ lk γ, RET lk; is_lock N γ lk R }}};
22
  acquire_spec N γ lk R :
23
    {{{ is_lock N γ lk R }}} acquire lk {{{ RET #(); locked γ  R }}};
24
  release_spec N γ lk R :
25
    {{{ is_lock N γ lk R  locked γ  R }}} release lk {{{ RET #(); True }}}
26
}.
Zhen Zhang's avatar
Zhen Zhang committed
27 28 29 30 31 32 33 34 35 36 37

Arguments newlock {_ _} _.
Arguments acquire {_ _} _.
Arguments release {_ _} _.
Arguments is_lock {_ _} _ _ _ _ _.
Arguments locked {_ _} _ _.

Existing Instances is_lock_ne is_lock_persistent locked_timeless.

Instance is_lock_proper Σ `{!heapG Σ} (L: lock Σ) N lk R:
  Proper (() ==> ()) (is_lock L N lk R) := ne_proper _.
38