lock.v 3.17 KB
Newer Older
1
From iris.program_logic Require Export weakestpre.
2
3
From iris.heap_lang Require Export lang.
From iris.proofmode Require Import invariants tactics.
4
From iris.heap_lang Require Import proofmode notation.
5
From iris.algebra Require Import excl.
6
7
8

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

(** The CMRA we need. *)
(* Not bundling heapG, as it may be shared with other users. *)
16
Class lockG Σ := LockG { lock_tokG :> inG Σ (exclR unitC) }.
17
Definition lockΣ : gFunctors := #[GFunctor (constRF (exclR unitC))].
18

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

Section proof.
23
Context `{!heapG Σ, !lockG Σ} (N : namespace).
24

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

28
Definition is_lock (l : loc) (R : iProp Σ) : iProp Σ :=
29
  ( γ, heapN  N  heap_ctx  inv N (lock_inv γ l R))%I.
30

31
Definition locked (l : loc) (R : iProp Σ) : iProp Σ :=
32
33
  ( γ, heapN  N  heap_ctx 
        inv N (lock_inv γ l R)  own γ (Excl ()))%I.
34
35
36
37
38
39
40
41
42
43
44
45

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.
Global Instance locked_ne n l : Proper (dist n ==> dist n) (locked l).
Proof. solve_proper. Qed.

(** The main proofs. *)
Global Instance is_lock_persistent l R : PersistentP (is_lock l R).
Proof. apply _. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
46
Lemma locked_is_lock l R : locked l R  is_lock l R.
47
Proof. rewrite /is_lock. iDestruct 1 as (γ) "(?&?&?&_)"; eauto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
48

49
Lemma newlock_spec (R : iProp Σ) Φ :
50
  heapN  N 
51
  heap_ctx  R  ( l, is_lock l R - Φ #l)  WP newlock #() {{ Φ }}.
52
Proof.
53
  iIntros (?) "(#Hh & HR & HΦ)". rewrite /newlock /=.
54
  wp_seq. wp_alloc l as "Hl".
55
56
  iVs (own_alloc (Excl ())) as (γ) "Hγ"; first done.
  iVs (inv_alloc N _ (lock_inv γ l R) with "[-HΦ]") as "#?".
Robbert Krebbers's avatar
Robbert Krebbers committed
57
  { iIntros "!>". iExists false. by iFrame. }
58
  iVsIntro. iApply "HΦ". iExists γ; eauto.
59
60
Qed.

61
Lemma acquire_spec l R (Φ : val  iProp Σ) :
62
  is_lock l R  (locked l R - R - Φ #())  WP acquire #l {{ Φ }}.
63
Proof.
64
  iIntros "[Hl HΦ]". iDestruct "Hl" as (γ) "(%&#?&#?)".
65
  iLöb as "IH". wp_rec. wp_bind (CAS _ _ _)%E.
66
67
68
69
70
71
  iInv N as ([]) "[Hl HR]" "Hclose".
  - wp_cas_fail. iVs ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
    iVsIntro. wp_if. by iApply "IH".
  - wp_cas_suc. iDestruct "HR" as "[Hγ HR]".
    iVs ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
    iVsIntro. wp_if. iApply ("HΦ" with "[-HR] HR"). iExists γ; eauto.
72
73
Qed.

74
Lemma release_spec R l (Φ : val  iProp Σ) :
75
  locked l R  R  Φ #()  WP release #l {{ Φ }}.
76
Proof.
77
  iIntros "(Hl&HR&HΦ)"; iDestruct "Hl" as (γ) "(% & #? & #? & Hγ)".
78
  rewrite /release /=. wp_let. iInv N as (b) "[Hl _]" "Hclose".
79
  wp_store. iFrame "HΦ". iApply "Hclose". iNext. iExists false. by iFrame.
80
81
Qed.
End proof.