lock.v 1.54 KB
Newer Older
1
From iris.base_logic.lib Require Export invariants.
2
From iris.heap_lang Require Export lifting notation.
3
Set Default Proof Using "Type".
Zhen Zhang's avatar
Zhen Zhang committed
4

5
Structure lock Σ `{!heapG Σ} := Lock {
Robbert Krebbers's avatar
Robbert Krebbers committed
6
  (** * Operations *)
7 8 9
  newlock : val;
  acquire : val;
  release : val;
Robbert Krebbers's avatar
Robbert Krebbers committed
10 11
  (** * Predicates *)
  (** [name] is used to associate locked with [is_lock] *)
12
  name : Type;
Robbert Krebbers's avatar
Robbert Krebbers committed
13 14
  (** No namespace [N] parameter because we only expose program specs, which
  anyway have the full mask. *)
15
  is_lock (γ: name) (lock: val) (R: iProp Σ) : iProp Σ;
16
  locked (γ: name) : iProp Σ;
Robbert Krebbers's avatar
Robbert Krebbers committed
17
  (** * General properties of the predicates *)
18 19 20 21
  is_lock_ne γ lk : Contractive (is_lock γ lk);
  is_lock_persistent γ lk R : Persistent (is_lock γ lk R);
  is_lock_iff γ lk R1 R2 :
    is_lock γ lk R1 -   (R1  R2) - is_lock γ lk R2;
22
  locked_timeless γ : Timeless (locked γ);
23
  locked_exclusive γ : locked γ - locked γ - False;
Robbert Krebbers's avatar
Robbert Krebbers committed
24
  (** * Program specs *)
25 26 27 28 29 30
  newlock_spec (R : iProp Σ) :
    {{{ R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}};
  acquire_spec γ lk R :
    {{{ is_lock γ lk R }}} acquire lk {{{ RET #(); locked γ  R }}};
  release_spec γ lk R :
    {{{ is_lock γ lk R  locked γ  R }}} release lk {{{ RET #(); True }}}
31
}.
Zhen Zhang's avatar
Zhen Zhang committed
32 33 34 35

Arguments newlock {_ _} _.
Arguments acquire {_ _} _.
Arguments release {_ _} _.
36
Arguments is_lock {_ _} _ _ _ _.
Zhen Zhang's avatar
Zhen Zhang committed
37 38 39 40
Arguments locked {_ _} _ _.

Existing Instances is_lock_ne is_lock_persistent locked_timeless.

41 42
Instance is_lock_proper Σ `{!heapG Σ} (L: lock Σ) γ lk:
  Proper (() ==> ()) (is_lock L γ lk) := ne_proper _.