spin_lock.v 3.89 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 7 8
From iris.heap_lang Require Import proofmode notation.
From iris.algebra Require Import excl.
From iris.heap_lang.lib Require Import lock.

Definition newlock : val := λ: <>, ref #false.
9
Definition try_acquire : val := λ: "l", CAS "l" #false #true.
Zhen Zhang's avatar
Zhen Zhang committed
10
Definition acquire : val :=
11
  rec: "acquire" "l" := if: try_acquire "l" then #() else "acquire" "l".
Zhen Zhang's avatar
Zhen Zhang committed
12
Definition release : val := λ: "l", "l" <- #false.
13
Global Opaque newlock try_acquire acquire release.
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 27 28 29 30 31 32 33 34
  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, heapN  N  heap_ctx  lk = #l  inv N (lock_inv γ l R))%I.

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

  Lemma locked_exclusive (γ : gname) : locked γ  locked γ  False.
35
  Proof. rewrite /locked own_valid_2. by iIntros (?). 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
    heapN  N 
50
    {{{ heap_ctx  R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}}.
51
  Proof.
Ralf Jung's avatar
Ralf Jung committed
52
    iIntros (? Φ) "[#Hh HR] HΦ". rewrite -wp_fupd /newlock /=.
53
    wp_seq. wp_alloc l as "Hl".
54 55
    iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
    iMod (inv_alloc N _ (lock_inv γ l R) with "[-HΦ]") as "#?".
56
    { iIntros "!>". iExists false. by iFrame. }
57
    iModIntro. iApply "HΦ". iExists l. eauto.
58 59
  Qed.

60 61
  Lemma try_acquire_spec γ lk R :
    {{{ is_lock γ lk R }}} try_acquire lk
62
    {{{ b, RET #b; if b is true then locked γ  R else True }}}.
63
  Proof.
Ralf Jung's avatar
Ralf Jung committed
64
    iIntros (Φ) "#Hl HΦ". iDestruct "Hl" as (l) "(% & #? & % & #?)". subst.
65
    wp_rec. iInv N as ([]) "[Hl HR]" "Hclose".
66
    - wp_cas_fail. iMod ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
67
      iModIntro. iApply ("HΦ" $! false). done.
68
    - wp_cas_suc. iDestruct "HR" as "[Hγ HR]".
69
      iMod ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
70
      iModIntro. rewrite /locked. by iApply ("HΦ" $! true with "[$Hγ $HR]").
71 72
  Qed.

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

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

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