Skip to content
Snippets Groups Projects

two more styles of lock spec

Open William Mansky requested to merge wmansky/examples:master into master
3 unresolved threads
2 files
+ 217
0
Compare changes
  • Side-by-side
  • Inline
Files
2
+ 108
0
 
From iris.proofmode Require Import proofmode.
 
From iris.base_logic.lib Require Export invariants ghost_var.
 
From iris.bi.lib Require Import fractional.
 
From iris.heap_lang Require Import proofmode primitive_laws notation atomic_heap.
 
From iris.prelude Require Import options.
 
 
(** Deallocatable lock with share, operations are atomic. *)
 
Structure atomic_lock `{!heapGS Σ} := AtomicLock {
 
(** * Operations *)
 
newlock : val;
 
acquire : val;
 
release : val;
 
freelock : 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 (f: Qp) (γ: name) (lock: val) (R: iProp Σ) : iProp Σ;
 
locked (γ: name) : iProp Σ;
 
(** * General properties of the predicates *)
 
is_lock_ne f γ lk : Contractive (is_lock f γ lk);
 
is_lock_persistent γ lk R : Fractional (fun f => is_lock f γ lk R);
 
is_lock_iff f γ lk R1 R2 :
 
is_lock f γ lk R1 -∗ (R1 R2) -∗ is_lock f γ lk R2;
 
locked_timeless γ : Timeless (locked γ);
 
locked_exclusive γ : locked γ -∗ locked γ -∗ False;
 
(** * Program specs *)
 
newlock_spec (R : iProp Σ) :
 
{{{ R }}} newlock #() {{{ lk γ, RET lk; is_lock 1 γ lk R }}};
 
acquire_spec f γ (lk : val) R :
 
<<{ is_lock f γ lk R }>> acquire lk @ <<{ is_lock f γ lk R locked γ R | RET #() }>>;
 
release_spec f γ lk R :
 
{{{ is_lock f γ lk R locked γ R }}} release lk {{{ RET #(); is_lock f γ lk R }}};
 
freelock_spec γ lk (R : iProp Σ) :
 
{{{ is_lock 1 γ lk R R }}} freelock #() {{{ RET #(); R }}}
 
}.
 
 
Inductive state := Free | Locked.
 
 
Class lockG Σ := LockG { lock_tokG : ghost_varG Σ state }.
 
Local Existing Instance lock_tokG.
 
Definition lockΣ : gFunctors := #[ghost_varΣ state].
 
Global Instance subG_lockΣ {Σ} : subG lockΣ Σ lockG Σ.
 
Proof. solve_inG. Qed.
 
 
Section tada.
 
Context `{!heapGS Σ, !lockG Σ} (l : atomic_lock).
 
 
Record tada_lock_name := TadaLockName {
 
tada_lock_name_state : gname;
 
tada_lock_name_lock : l.(name);
 
}.
 
 
Definition tada_is_lock (γ : tada_lock_name) (lk : val) : iProp Σ :=
 
l.(is_lock) 1 γ.(tada_lock_name_lock) lk
 
(ghost_var γ.(tada_lock_name_state) (1/4) Free).
 
Definition tada_lock_state (γ : tada_lock_name) (lk : val) (s : state) : iProp Σ :=
 
tada_is_lock γ lk ghost_var γ.(tada_lock_name_state) (3/4) s
 
if s is Locked then
 
l.(locked) γ.(tada_lock_name_lock) ghost_var γ.(tada_lock_name_state) (1/4) Locked
 
else True.
 
 
(* Global Instance tada_is_lock_persistent γ lk : Persistent (tada_is_lock γ lk).
 
Proof. apply _. Qed. *)
 
(* Global Instance tada_lock_state_timeless γ s : Timeless (tada_lock_state γ lk s).
 
Proof. destruct s; apply _. Qed.*)
 
 
Lemma tada_lock_state_exclusive γ lk s1 s2 :
 
tada_lock_state γ lk s1 -∗ tada_lock_state γ lk s2 -∗ False.
 
Proof.
 
iIntros "[_ [Hvar1 _]] [_ [Hvar2 _]]".
 
iDestruct (ghost_var_valid_2 with "Hvar1 Hvar2") as %[Hval _].
 
exfalso. done.
 
Qed.
 
 
Lemma newlock_tada_spec :
 
{{{ True }}}
 
l.(newlock) #()
 
{{{ lk γ, RET lk; tada_lock_state γ lk Free }}}.
 
Proof.
 
iIntros (Φ) "_ HΦ".
 
iMod (ghost_var_alloc Free) as (γvar) "Hvar".
 
rewrite -Qp.three_quarter_quarter.
 
iDestruct "Hvar" as "[Hvar1 Hvar2]".
 
wp_apply (l.(newlock_spec) with "Hvar2").
 
iIntros (lk γlock) "Hlock".
 
iApply ("HΦ" $! lk (TadaLockName _ _)).
 
iFrame.
 
Qed.
 
 
Lemma acquire_tada_spec γ (lk : val) :
 
⊢<<{ s, tada_lock_state γ lk s }>>
 
l.(acquire) lk @
 
<<{ tada_lock_state γ lk Locked | RET #() }>>.
 
Proof.
 
iIntros "%Φ AU".
 
iApply fupd_wp.
 
Abort.
 
 
Lemma release_tada_spec γ (lk : val) :
 
⊢<<{ tada_lock_state γ lk Locked }>>
 
l.(release) lk @
 
<<{ tada_lock_state γ lk Free | RET #() }>>.
 
Proof.
 
Abort.
 
 
End tada.
Loading