-
Notifications
You must be signed in to change notification settings - Fork 2
/
spin_lock.v
96 lines (80 loc) · 3.74 KB
/
spin_lock.v
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
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation.
From iris.algebra Require Import excl.
From iris.heap_lang.lib Require Import lock.
Set Default Proof Using "Type".
Definition newlock : val := λ: <>, ref #false.
Definition try_acquire : val := λ: "l", CAS "l" #false #true.
Definition acquire : val :=
rec: "acquire" "l" := if: try_acquire "l" then #() else "acquire" "l".
Definition release : val := λ: "l", "l" <- #false.
(** The CMRA we need. *)
(* Not bundling heapG, as it may be shared with other users. *)
Class lockG Σ := LockG { lock_tokG :> inG Σ (exclR unitC) }.
Definition lockΣ : gFunctors := #[GFunctor (exclR unitC)].
Instance subG_lockΣ {Σ} : subG lockΣ Σ → lockG Σ.
Proof. solve_inG. Qed.
Section proof.
Context `{!heapG Σ, !lockG Σ} (N : namespace).
Definition lock_inv (γ : gname) (l : loc) (R : iProp Σ) : iProp Σ :=
(∃ b : bool, l ↦ #b ∗ if b then True else own γ (Excl ()) ∗ R)%I.
Definition is_lock (γ : gname) (lk : val) (R : iProp Σ) : iProp Σ :=
(∃ l: loc, ⌜lk = #l⌝ ∧ inv N (lock_inv γ l R))%I.
Definition locked (γ : gname) : iProp Σ := own γ (Excl ()).
Lemma locked_exclusive (γ : gname) : locked γ -∗ locked γ -∗ False.
Proof. iIntros "H1 H2". by iDestruct (own_valid_2 with "H1 H2") as %?. Qed.
Global Instance lock_inv_ne γ l : NonExpansive (lock_inv γ l).
Proof. solve_proper. Qed.
Global Instance is_lock_ne γ l : NonExpansive (is_lock γ l).
Proof. solve_proper. Qed.
(** The main proofs. *)
Global Instance is_lock_persistent γ l R : Persistent (is_lock γ l R).
Proof. apply _. Qed.
Global Instance locked_timeless γ : Timeless (locked γ).
Proof. apply _. Qed.
Lemma newlock_spec (R : iProp Σ):
{{{ R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}}.
Proof.
iIntros (Φ) "HR HΦ". rewrite -wp_fupd /newlock /=.
wp_lam. wp_alloc l as "Hl".
iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
iMod (inv_alloc N _ (lock_inv γ l R) with "[-HΦ]") as "#?".
{ iIntros "!>". iExists false. by iFrame. }
iModIntro. iApply "HΦ". iExists l. eauto.
Qed.
Lemma try_acquire_spec γ lk R :
{{{ is_lock γ lk R }}} try_acquire lk
{{{ b, RET #b; if b is true then locked γ ∗ R else True }}}.
Proof.
iIntros (Φ) "#Hl HΦ". iDestruct "Hl" as (l ->) "#Hinv".
wp_rec. iInv N as ([]) "[Hl HR]".
- wp_cas_fail. iModIntro. iSplitL "Hl"; first (iNext; iExists true; eauto).
iApply ("HΦ" $! false). done.
- wp_cas_suc. iDestruct "HR" as "[Hγ HR]".
iModIntro. iSplitL "Hl"; first (iNext; iExists true; eauto).
rewrite /locked. by iApply ("HΦ" $! true with "[$Hγ $HR]").
Qed.
Lemma acquire_spec γ lk R :
{{{ is_lock γ lk R }}} acquire lk {{{ RET #(); locked γ ∗ R }}}.
Proof.
iIntros (Φ) "#Hl HΦ". iLöb as "IH". wp_rec.
wp_apply (try_acquire_spec with "Hl"). iIntros ([]).
- iIntros "[Hlked HR]". wp_if. iApply "HΦ"; iFrame.
- iIntros "_". wp_if. iApply ("IH" with "[HΦ]"). auto.
Qed.
Lemma release_spec γ lk R :
{{{ is_lock γ lk R ∗ locked γ ∗ R }}} release lk {{{ RET #(); True }}}.
Proof.
iIntros (Φ) "(Hlock & Hlocked & HR) HΦ".
iDestruct "Hlock" as (l ->) "#Hinv".
rewrite /release /=. wp_let. iInv N as (b) "[Hl _]".
wp_store. iSplitR "HΦ"; last by iApply "HΦ".
iModIntro. iNext. iExists false. by iFrame.
Qed.
End proof.
Typeclasses Opaque is_lock locked.
Canonical Structure spin_lock `{!heapG Σ, !lockG Σ} : lock Σ :=
{| lock.locked_exclusive := locked_exclusive; lock.newlock_spec := newlock_spec;
lock.acquire_spec := acquire_spec; lock.release_spec := release_spec |}.