Library iris.heap_lang.lib.lock

From iris.base_logic.lib Require Export invariants.
From iris.heap_lang Require Import primitive_laws notation.
Set Default Proof Using "Type".

Structure lock Σ `{!heapG Σ} := Lock {
  

Operations

  newlock : val;
  acquire : val;
  release : val;
  

Predicates

name is used to associate locked with is_lock
  name : Type;
  
No namespace N parameter because we only expose program specs, which anyway have the full mask.
  is_lock (γ: name) (lock: val) (R: iProp Σ) : iProp Σ;
  locked (γ: name) : iProp Σ;
  

General properties of the predicates

Program specs

  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 }}}
}.

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 Σ) γ lk:
  Proper ((≡) ==> (≡)) (is_lock L γ lk) := ne_proper _.