spin_lock.v 3.85 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 10
Definition newlock : val := λ: <>, ref #false.
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 17 18 19 20 21 22 23

(** 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 (constRF (exclR unitC))].

Instance subG_lockΣ {Σ} : subG lockΣ Σ  lockG Σ.
Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.

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 32 33

  Definition locked (γ : gname): iProp Σ := own γ (Excl ()).

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 38 39 40 41 42 43 44 45 46 47

  Global Instance lock_inv_ne n γ l : Proper (dist n ==> dist n) (lock_inv γ l).
  Proof. solve_proper. Qed.
  Global Instance is_lock_ne n l : Proper (dist n ==> dist n) (is_lock γ l).
  Proof. solve_proper. Qed.

  (** The main proofs. *)
  Global Instance is_lock_persistent γ l R : PersistentP (is_lock γ l R).
  Proof. apply _. Qed.
  Global Instance locked_timeless γ : TimelessP (locked γ).
  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 /=.
52
    wp_seq. 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) "[% #?]"; subst.
64
    wp_rec. iInv N as ([]) "[Hl HR]" "Hclose".
65
    - wp_cas_fail. iMod ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
66
      iModIntro. iApply ("HΦ" $! false). done.
67
    - wp_cas_suc. iDestruct "HR" as "[Hγ HR]".
68
      iMod ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
69
      iModIntro. rewrite /locked. 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) "[% #?]"; subst.
86
    rewrite /release /=. wp_let. iInv N as (b) "[Hl _]" "Hclose".
87
    wp_store. iApply "HΦ". iApply "Hclose". iNext. iExists false. by iFrame.
88
  Qed.
Zhen Zhang's avatar
Zhen Zhang committed
89 90
End proof.

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

93 94 95
Definition 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 |}.