spin_lock.v 4 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
48
49
50
51
52
53
54
55
56
57
58
59

  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.

  Lemma newlock_spec (R : iProp Σ) Φ :
    heapN  N 
    heap_ctx  R  ( lk γ, is_lock γ lk R - Φ lk)  WP newlock #() {{ Φ }}.
  Proof.
    iIntros (?) "(#Hh & HR & HΦ)". rewrite /newlock /=.
    wp_seq. wp_alloc l as "Hl".
    iVs (own_alloc (Excl ())) as (γ) "Hγ"; first done.
    iVs (inv_alloc N _ (lock_inv γ l R) with "[-HΦ]") as "#?".
    { iIntros "!>". iExists false. by iFrame. }
    iVsIntro. iApply "HΦ". iExists l. eauto.
  Qed.

60
61
62
  Lemma try_acquire_spec γ lk R (Φ: val  iProp Σ) :
    is_lock γ lk R  ((locked γ - R - Φ #true)  Φ #false)
     WP try_acquire lk {{ Φ }}.
63
  Proof.
64
65
    iIntros "[#Hl HΦ]". iDestruct "Hl" as (l) "(% & #? & % & #?)". subst.
    wp_rec. iInv N as ([]) "[Hl HR]" "Hclose".
66
    - wp_cas_fail. iVs ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
67
      iVsIntro. iDestruct "HΦ" as "[_ HΦ]". iApply "HΦ".
68
69
    - wp_cas_suc. iDestruct "HR" as "[Hγ HR]".
      iVs ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
70
71
72
73
74
75
76
77
78
79
      iVsIntro. iDestruct "HΦ" as "[HΦ _]". rewrite /locked. by iApply ("HΦ" with "Hγ HR").
  Qed.

  Lemma acquire_spec γ lk R (Φ : val  iProp Σ) :
    is_lock γ lk R  (locked γ - R - Φ #())  WP acquire lk {{ Φ }}.
  Proof.
    iIntros "[#Hl HΦ]". iLöb as "IH". wp_rec. wp_bind (try_acquire _).
    iApply try_acquire_spec. iFrame "#". iSplit.
    - iIntros "Hlked HR". wp_if. iVsIntro. iApply ("HΦ" with "Hlked HR").
    - wp_if. iApply ("IH" with "HΦ").
80
81
82
83
84
85
86
87
88
89
  Qed.

  Lemma release_spec γ lk R (Φ : val  iProp Σ) :
    is_lock γ lk R  locked γ  R  Φ #()  WP release lk {{ Φ }}.
  Proof.
    iIntros "(Hlock & Hlocked & HR & HΦ)".
    iDestruct "Hlock" as (l) "(% & #? & % & #?)". subst.
    rewrite /release /=. wp_let. iInv N as (b) "[Hl _]" "Hclose".
    wp_store. iFrame "HΦ". iApply "Hclose". iNext. iExists false. by iFrame.
  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 |}.