Library iris.heap_lang.lib.rw_lock

From iris.base_logic.lib Require Export invariants.
From Require Export fractional.
From iris.heap_lang Require Import proofmode notation.
From iris.prelude Require Import options.

A general interface for a reader-writer lock.
All parameters are implicit, since it is expected that there is only one heapGS_gen in scope that could possibly apply.
Only one instance of this class should ever be in scope. To write a library that is generic over the lock, just add a `{!rwlock} implicit parameter around the code and `{!rwlockG Σ} around the proofs. To use a particular lock instance, use Local Existing Instance <rwlock instance>.
When writing an instance of this class, please take care not to shadow the class projections (e.g., either use Local Definition newlock or avoid the name newlock altogether), and do not register an instance -- just make it a Definition that others can register later.
Class rwlock := RwLock {


Ghost state

The assumptions about Σ
  rwlockG : gFunctors Type;
lock_name is used to associate reader_locked and writer_locked with is_rw_lock
  lock_name : Type;


No namespace N parameter because we only expose program specs, which anyway have the full mask.

General properties of the predicates

Program specs

  newlock_spec `{!heapGS_gen hlc Σ} {L : rwlockG Σ} (Φ : Qp iProp Σ) `{!AsFractional P Φ 1} :
    {{{ P }}}
      newlock #()
    {{{ lk γ, RET lk; is_rw_lock (L:=L) γ lk Φ }}};
  acquire_reader_spec `{!heapGS_gen hlc Σ} {L : rwlockG Σ} γ lk Φ :
    {{{ is_rw_lock (L:=L) γ lk Φ }}}
      acquire_reader lk
    {{{ q, RET #(); reader_locked (L:=L) γ q Φ q }}};
  release_reader_spec `{!heapGS_gen hlc Σ} {L : rwlockG Σ} γ lk Φ q :
    {{{ is_rw_lock (L:=L) γ lk Φ reader_locked (L:=L) γ q Φ q }}}
      release_reader lk
    {{{ RET #(); True }}};
  acquire_writer_spec `{!heapGS_gen hlc Σ} {L : rwlockG Σ} γ lk Φ :
    {{{ is_rw_lock (L:=L) γ lk Φ }}}
      acquire_writer lk
    {{{ RET #(); writer_locked (L:=L) γ Φ 1%Qp }}};
  release_writer_spec `{!heapGS_gen hlc Σ} {L : rwlockG Σ} γ lk Φ :
    {{{ is_rw_lock (L:=L) γ lk Φ writer_locked (L:=L) γ Φ 1%Qp }}}
      release_writer lk
    {{{ RET #(); True }}};

Global Arguments newlock : simpl never.
Global Arguments acquire_reader : simpl never.
Global Arguments release_reader : simpl never.
Global Arguments acquire_writer : simpl never.
Global Arguments release_writer : simpl never.
Global Arguments is_rw_lock : simpl never.
Global Arguments reader_locked : simpl never.
Global Arguments writer_locked : simpl never.

Existing Class rwlockG.
Global Hint Mode rwlockG + + : typeclass_instances.
Global Hint Extern 0 (rwlockG _) ⇒ progress simpl : typeclass_instances.

Global Instance is_rw_lock_contractive `{!heapGS_gen hlc Σ, !rwlock, !rwlockG Σ} γ lk n :
  Proper (pointwise_relation _ (dist_later n) ==> dist n) (is_rw_lock γ lk).
  assert (Contractive (is_rw_lock γ lk : (Qp -d> iPropO Σ) _)) as Hcontr.
  { apply (uPred.contractive_internal_eq (M:=iResUR Σ)); iIntros (Φ1 Φ2) "#HΦ".
    rewrite discrete_fun_equivI.
    iApply plainly.prop_ext_2; iIntros "!>"; iSplit; iIntros "H";
      iApply (is_rw_lock_iff with "H");
      iIntros "!> !>" (q); iRewrite ("HΦ" $! q); auto. }
  intros Φ1 Φ2 . apply Hcontr. dist_later_intro. apply .

Global Instance is_rw_lock_proper `{!heapGS_gen hlc Σ, !rwlock, !rwlockG Σ} γ lk :
  Proper (pointwise_relation _ (≡) ==> (≡)) (is_rw_lock γ lk).
  intros Φ1 Φ2 . apply equiv_distn. apply is_rw_lock_contractiveq.
  dist_later_intro. apply equiv_dist, .