spin_lock.v 4.24 KB
Newer Older
1 2
From iris.proofmode Require Import tactics.
From iris.algebra Require Import excl.
Zhen Zhang's avatar
Zhen Zhang committed
3 4 5 6
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang.lib Require Import lock.
7
Set Default Proof Using "Type".
Zhen Zhang's avatar
Zhen Zhang committed
8

9
Definition newlock : val := λ: <>, ref #false.
10
Definition try_acquire : val := λ: "l", CAS "l" #false #true.
Zhen Zhang's avatar
Zhen Zhang committed
11
Definition acquire : val :=
12 13
  rec: "acquire" "l" := if: try_acquire "l" then #() else "acquire" "l".
Definition release : val := λ: "l", "l" <- #false.
Zhen Zhang's avatar
Zhen Zhang committed
14 15 16

(** The CMRA we need. *)
(* Not bundling heapG, as it may be shared with other users. *)
17 18
Class lockG Σ := LockG { lock_tokG :> inG Σ (exclR unitO) }.
Definition lockΣ : gFunctors := #[GFunctor (exclR unitO)].
Zhen Zhang's avatar
Zhen Zhang committed
19 20

Instance subG_lockΣ {Σ} : subG lockΣ Σ  lockG Σ.
21
Proof. solve_inG. Qed.
Zhen Zhang's avatar
Zhen Zhang committed
22 23

Section proof.
24 25
  Context `{!heapG Σ, !lockG Σ}.
  Let N := nroot .@ "spin_lock".
26 27

  Definition lock_inv (γ : gname) (l : loc) (R : iProp Σ) : iProp Σ :=
28
    ( b : bool, l  #b  if b then True else own γ (Excl ())  R)%I.
29 30

  Definition is_lock (γ : gname) (lk : val) (R : iProp Σ) : iProp Σ :=
31
    ( l: loc, lk = #l  inv N (lock_inv γ l R))%I.
32

Ralf Jung's avatar
style  
Ralf Jung committed
33
  Definition locked (γ : gname) : iProp Σ := own γ (Excl ()).
34

35 36
  Lemma locked_exclusive (γ : gname) : locked γ - locked γ - False.
  Proof. iIntros "H1 H2". by iDestruct (own_valid_2 with "H1 H2") as %?. Qed.
37

38
  Global Instance lock_inv_ne γ l : NonExpansive (lock_inv γ l).
39
  Proof. solve_proper. Qed.
40 41
  Global Instance is_lock_contractive γ l : Contractive (is_lock γ l).
  Proof. solve_contractive. Qed.
42 43

  (** The main proofs. *)
44
  Global Instance is_lock_persistent γ l R : Persistent (is_lock γ l R).
45
  Proof. apply _. Qed.
46
  Global Instance locked_timeless γ : Timeless (locked γ).
47 48
  Proof. apply _. Qed.

49 50 51 52 53 54 55 56 57 58
  Lemma is_lock_iff γ lk R1 R2 :
    is_lock γ lk R1 -   (R1  R2) - is_lock γ lk R2.
  Proof.
    iDestruct 1 as (l ->) "#Hinv"; iIntros "#HR".
    iExists l; iSplit; [done|]. iApply (inv_iff with "Hinv").
    iIntros "!> !#"; iSplit; iDestruct 1 as (b) "[Hl H]";
      iExists b; iFrame "Hl"; destruct b;
      first [done|iDestruct "H" as "[$ ?]"; by iApply "HR"].
  Qed.

59
  Lemma newlock_spec (R : iProp Σ):
60
    {{{ R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}}.
61
  Proof.
62
    iIntros (Φ) "HR HΦ". rewrite -wp_fupd /newlock /=.
Ralf Jung's avatar
Ralf Jung committed
63
    wp_lam. wp_alloc l as "Hl".
64 65
    iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
    iMod (inv_alloc N _ (lock_inv γ l R) with "[-HΦ]") as "#?".
66
    { iIntros "!>". iExists false. by iFrame. }
67
    iModIntro. iApply "HΦ". iExists l. eauto.
68 69
  Qed.

70 71
  Lemma try_acquire_spec γ lk R :
    {{{ is_lock γ lk R }}} try_acquire lk
72
    {{{ b, RET #b; if b is true then locked γ  R else True }}}.
73
  Proof.
74
    iIntros (Φ) "#Hl HΦ". iDestruct "Hl" as (l ->) "#Hinv".
Ralf Jung's avatar
Ralf Jung committed
75 76
    wp_rec. wp_bind (CmpXchg _ _ _). iInv N as ([]) "[Hl HR]".
    - wp_cmpxchg_fail. iModIntro. iSplitL "Hl"; first (iNext; iExists true; eauto).
77
      wp_pures. iApply ("HΦ" $! false). done.
Ralf Jung's avatar
Ralf Jung committed
78
    - wp_cmpxchg_suc. iDestruct "HR" as "[Hγ HR]".
79
      iModIntro. iSplitL "Hl"; first (iNext; iExists true; eauto).
80
      rewrite /locked. wp_pures. by iApply ("HΦ" $! true with "[$Hγ $HR]").
81 82
  Qed.

83
  Lemma acquire_spec γ lk R :
84
    {{{ is_lock γ lk R }}} acquire lk {{{ RET #(); locked γ  R }}}.
85
  Proof.
Ralf Jung's avatar
Ralf Jung committed
86 87
    iIntros (Φ) "#Hl HΦ". iLöb as "IH". wp_rec.
    wp_apply (try_acquire_spec with "Hl"). iIntros ([]).
88
    - iIntros "[Hlked HR]". wp_if. iApply "HΦ"; iFrame.
89
    - iIntros "_". wp_if. iApply ("IH" with "[HΦ]"). auto.
90 91
  Qed.

92
  Lemma release_spec γ lk R :
93
    {{{ is_lock γ lk R  locked γ  R }}} release lk {{{ RET #(); True }}}.
94
  Proof.
Ralf Jung's avatar
Ralf Jung committed
95
    iIntros (Φ) "(Hlock & Hlocked & HR) HΦ".
96
    iDestruct "Hlock" as (l ->) "#Hinv".
97
    rewrite /release /=. wp_lam. iInv N as (b) "[Hl _]".
Ralf Jung's avatar
Ralf Jung committed
98
    wp_store. iSplitR "HΦ"; last by iApply "HΦ".
99
    iModIntro. iNext. iExists false. by iFrame.
100
  Qed.
Zhen Zhang's avatar
Zhen Zhang committed
101 102
End proof.

Ralf Jung's avatar
Ralf Jung committed
103 104
Typeclasses Opaque is_lock locked.

105
Canonical Structure spin_lock `{!heapG Σ, !lockG Σ} : lock Σ :=
106 107
  {| lock.locked_exclusive := locked_exclusive; lock.is_lock_iff := is_lock_iff;
     lock.newlock_spec := newlock_spec;
108
     lock.acquire_spec := acquire_spec; lock.release_spec := release_spec |}.