Library zoo_std.mutex

From zoo Require Import
  prelude.
From zoo.iris.base_logic Require Import
  excl.
From zoo.language Require Import
  notations.
From zoo.diaframe Require Import
  diaframe.
From zoo_std Require Export
  base
  mutex__code.
From zoo Require Import
  options.

Implicit Types b : bool.
Implicit Types l : location.
Implicit Types t fn : val.

Class MutexG Σ `{zoo_G : !ZooG Σ} :=
  { #[local] mutex_G :: ExclG Σ unitO
  }.

Definition mutex_Σ :=
  #[excl_Σ unitO
  ].
#[global] Instance subG_mutex_Σ Σ `{zoo_G : !ZooG Σ} :
  subG mutex_Σ Σ →
  MutexG Σ.

Section mutex_G.
  Context `{mutex_G : MutexG Σ}.

  #[local] Definition metadata :=
    gname.
  Implicit Types γ : metadata.

  #[local] Definition locked γ :=
    excl γ ().

  Definition mutex_init t b : iProp Σ :=
    ∃ l γ ,
    ⌜t = #l ⌝ ∗
    meta l nroot γ ∗
    l ↦ᵣ #b ∗
    if b then True else locked γ.

  #[local] Definition inv_inner l γ P : iProp Σ :=
    ∃ b ,
    l ↦ᵣ #b ∗
    match b with
    | true ⇒
        True
    | false ⇒
        locked γ ∗
        P
    end.
  Definition mutex_inv t P : iProp Σ :=
    ∃ l γ ,
    ⌜t = #l ⌝ ∗
    meta l nroot γ ∗
    inv nroot (inv_inner l γ P).

  Definition mutex_locked t : iProp Σ :=
    ∃ l γ ,
    ⌜t = #l ⌝ ∗
    meta l nroot γ ∗
    locked γ.

  #[global] Instance mutex_inv_contractive t :
    Contractive (mutex_inv t).
  #[global] Instance mutex_inv_ne t :
    NonExpansive (mutex_inv t).
  #[global] Instance mutex_inv_proper t :
    Proper ((≡) ==> (≡)) (mutex_inv t).

  #[global] Instance mutex_init_timeless t b :
    Timeless (mutex_init t b).
  #[global] Instance mutex_locked_timeless t :
    Timeless (mutex_locked t).

  #[global] Instance mutex_inv_persistent t P :
    Persistent (mutex_inv t P).

  Lemma mutex_init_exclusive t b1 b2 :
    mutex_init t b1 -∗
    mutex_init t b2 -∗
    False.
  Lemma mutex_init_to_inv {t b} P E :
    mutex_init t b -∗
    (if b then True else ▷ P ) ={E }=∗
    mutex_inv t P.

  Lemma mutex_locked_exclusive t :
    mutex_locked t -∗
    mutex_locked t -∗
    False.

  Lemma mutex ٠ create 𑁒 spec_init :
    {{{
      True
    }}}
      mutex ٠ create ()
    {{{
      t
    , RET t ;
      mutex_init t false
    }}}.
  Lemma mutex ٠ create 𑁒 spec P :
    {{{
      P
    }}}
      mutex ٠ create ()
    {{{
      t
    , RET t ;
      mutex_inv t P
    }}}.

  Lemma mutex ٠ create_lock 𑁒 spec_init :
    {{{
      True
    }}}
      mutex ٠ create_lock ()
    {{{
      t
    , RET t ;
      mutex_init t true ∗
      mutex_locked t
    }}}.
  Lemma mutex ٠ create_lock 𑁒 spec P :
    {{{
      True
    }}}
      mutex ٠ create_lock ()
    {{{
      t
    , RET t ;
      mutex_inv t P ∗
      mutex_locked t
    }}}.

  Lemma mutex ٠ lock 𑁒 spec t P :
    {{{
      mutex_inv t P
    }}}
      mutex ٠ lock t
    {{{
      RET ();
      mutex_locked t ∗
      P
    }}}.
  Lemma mutex ٠ lock 𑁒 spec_init t :
    {{{
      mutex_init t false
    }}}
      mutex ٠ lock t
    {{{
      RET ();
      mutex_init t true ∗
      mutex_locked t
    }}}.

  Lemma mutex ٠ unlock 𑁒 spec t P :
    {{{
      mutex_inv t P ∗
      mutex_locked t ∗
      P
    }}}
      mutex ٠ unlock t
    {{{
      RET ();
      True
    }}}.
  Lemma mutex ٠ unlock 𑁒 spec_init t :
    {{{
      mutex_init t true ∗
      mutex_locked t
    }}}
      mutex ٠ unlock t
    {{{
      RET ();
      mutex_init t false
    }}}.

  Lemma mutex ٠ synchronize 𑁒 spec t P :
    {{{
      mutex_inv t P
    }}}
      mutex ٠ synchronize t
    {{{
      RET ();
      True
    }}}.
  #[global] Instance mutex ٠ synchronize 𑁒 diaspec t P :
    DIASPEC
    {{
      mutex_inv t P
    }}
      mutex ٠ synchronize t
    {{
      RET ();
      True
    }}.

  Lemma mutex ٠ protect 𑁒 spec Ψ t P fn :
    {{{
      mutex_inv t P ∗
      ( mutex_locked t -∗
        P -∗
        WP fn () {{ v ,
          mutex_locked t ∗
          P ∗
          Ψ v
        }}
      )
    }}}
      mutex ٠ protect t fn
    {{{
      v
    , RET v ;
      Ψ v
    }}}.
End mutex_G.

From zoo_std Require
  mutex__opaque.

#[global] Opaque mutex_init.
#[global] Opaque mutex_inv.
#[global] Opaque mutex_locked.