spin_lock.v 3.79 KB
Newer Older
Zhen Zhang's avatar
Zhen Zhang committed
1 2
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
3
From iris.proofmode Require Import tactics.
Zhen Zhang's avatar
Zhen Zhang committed
4 5 6
From iris.heap_lang Require Import proofmode notation.
From iris.algebra Require Import excl.
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 26
  Context `{!heapG Σ, !lockG Σ} (N : namespace).

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

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

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

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

37
  Global Instance lock_inv_ne γ l : NonExpansive (lock_inv γ l).
38
  Proof. solve_proper. Qed.
39
  Global Instance is_lock_ne γ l : NonExpansive (is_lock γ l).
40 41 42
  Proof. solve_proper. Qed.

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

48
  Lemma newlock_spec (R : iProp Σ):
49
    {{{ R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}}.
50
  Proof.
51
    iIntros (Φ) "HR HΦ". rewrite -wp_fupd /newlock /=.
Ralf Jung's avatar
Ralf Jung committed
52
    wp_lam. wp_alloc l as "Hl".
53 54
    iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
    iMod (inv_alloc N _ (lock_inv γ l R) with "[-HΦ]") as "#?".
55
    { iIntros "!>". iExists false. by iFrame. }
56
    iModIntro. iApply "HΦ". iExists l. eauto.
57 58
  Qed.

59 60
  Lemma try_acquire_spec γ lk R :
    {{{ is_lock γ lk R }}} try_acquire lk
61
    {{{ b, RET #b; if b is true then locked γ  R else True }}}.
62
  Proof.
63
    iIntros (Φ) "#Hl HΦ". iDestruct "Hl" as (l ->) "#Hinv".
64
    wp_rec. wp_bind (CompareExchange _ _ _). iInv N as ([]) "[Hl HR]".
65
    - wp_cas_fail. iModIntro. iSplitL "Hl"; first (iNext; iExists true; eauto).
66
      wp_pures. iApply ("HΦ" $! false). done.
67
    - wp_cas_suc. iDestruct "HR" as "[Hγ HR]".
68
      iModIntro. iSplitL "Hl"; first (iNext; iExists true; eauto).
69
      rewrite /locked. wp_pures. by iApply ("HΦ" $! true with "[$Hγ $HR]").
70 71
  Qed.

72
  Lemma acquire_spec γ lk R :
73
    {{{ is_lock γ lk R }}} acquire lk {{{ RET #(); locked γ  R }}}.
74
  Proof.
Ralf Jung's avatar
Ralf Jung committed
75 76
    iIntros (Φ) "#Hl HΦ". iLöb as "IH". wp_rec.
    wp_apply (try_acquire_spec with "Hl"). iIntros ([]).
77
    - iIntros "[Hlked HR]". wp_if. iApply "HΦ"; iFrame.
78
    - iIntros "_". wp_if. iApply ("IH" with "[HΦ]"). auto.
79 80
  Qed.

81
  Lemma release_spec γ lk R :
82
    {{{ is_lock γ lk R  locked γ  R }}} release lk {{{ RET #(); True }}}.
83
  Proof.
Ralf Jung's avatar
Ralf Jung committed
84
    iIntros (Φ) "(Hlock & Hlocked & HR) HΦ".
85
    iDestruct "Hlock" as (l ->) "#Hinv".
86
    rewrite /release /=. wp_lam. iInv N as (b) "[Hl _]".
Ralf Jung's avatar
Ralf Jung committed
87
    wp_store. iSplitR "HΦ"; last by iApply "HΦ".
88
    iModIntro. iNext. iExists false. by iFrame.
89
  Qed.
Zhen Zhang's avatar
Zhen Zhang committed
90 91
End proof.

Ralf Jung's avatar
Ralf Jung committed
92 93
Typeclasses Opaque is_lock locked.

94
Canonical Structure spin_lock `{!heapG Σ, !lockG Σ} : lock Σ :=
95 96
  {| lock.locked_exclusive := locked_exclusive; lock.newlock_spec := newlock_spec;
     lock.acquire_spec := acquire_spec; lock.release_spec := release_spec |}.