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);
Please register or sign in to reply
 
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.
    • Please add some more comments explaining what is happening here... I think the point of this is just to implement the interface? It's confusing that the interface does not mention TaDA but the implementation does.

      It might also be worth saying how this relates to iris_heap_lang/lib/logatom_lock.v, since there's clearly some overlap.

Please register or sign in to reply
 
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.*)
Please register or sign in to reply
 
 
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