flock.v 1.41 KB
Newer Older
Léon Gondelman's avatar
Léon Gondelman committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44
From iris.heap_lang Require Export proofmode notation.
From iris.heap_lang Require Import spin_lock assert par.
From iris.algebra Require Import frac.
From iris.base_logic.lib Require Import fractional.

Section flock.
  Context `{heapG Σ, lockG Σ, spawnG Σ}.

  Definition is_flock (γ : gname) (π : frac) (b : bool)
             (l : val) (R : iProp Σ) : iProp Σ.
  Admitted.

  Lemma is_flock_op γ π1 π2 lk R :
    is_flock γ (π1 + π2) false lk R 
      is_flock γ π1 false lk R  is_flock γ π2 false lk R.
  Proof. Admitted.

  Global Instance is_flock_fractional γ lk R :
    Fractional (λ π, is_flock γ π false lk R).
  Proof. intros p q. apply is_flock_op. Qed.
  Global Instance is_flock_as_fractional γ π lk R :
    AsFractional (is_flock γ π false lk R) (λ π, is_flock γ π false lk R) π.
  Proof. split. done. apply _. Qed.

  Lemma newlock_cancel_spec (R : iProp Σ):
    {{{ R }}} newlock #() {{{ lk γ, RET lk; is_flock γ 1 false lk R }}}.
  Proof. Admitted.

  Lemma acquire_cancel_spec γ π lk R :
    {{{ is_flock γ π false lk R }}} acquire lk
    {{{ RET #(); is_flock γ π true lk R  R }}}.
  Proof. Admitted.

  Lemma release_cancel_spec γ π lk R :
    {{{ is_flock γ π true lk R  R }}} release lk
    {{{ RET #(); is_flock γ π false lk R }}}.
  Proof. Admitted.

  Lemma cancel_lock γ lk R :
    is_flock γ 1 false lk R ={}= R.
  Proof. Admitted.


End flock.