lock.v 3.33 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
From iris.program_logic Require Export global_functor.
From iris.proofmode Require Import invariants ghost_ownership.
From iris.heap_lang Require Import proofmode notation.
Import uPred.

Definition newlock : val := λ: <>, ref #false.
Definition acquire : val :=
  rec: "lock" "l" := if: CAS '"l" #false #true then #() else '"lock" '"l".
Definition release : val := λ: "l", '"l" <- #false.

(** The CMRA we need. *)
(* Not bundling heapG, as it may be shared with other users. *)
Class lockG Σ := SpawnG { lock_tokG :> inG heap_lang Σ (exclR unitC) }.
Definition lockGF : gFunctorList := [GFunctor (constRF (exclR unitC))].
Instance inGF_lockG `{H : inGFs heap_lang Σ lockGF} : lockG Σ.
Proof. destruct H. split. apply: inGF_inG. Qed.

Section proof.
Context {Σ : gFunctors} `{!heapG Σ, !lockG Σ}.
Context (heapN : namespace).
Local Notation iProp := (iPropG heap_lang Σ).

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 (l : loc) (R : iProp) : iProp :=
  ( N γ,  (heapN  N)  heap_ctx heapN  inv N (lock_inv γ l R))%I.

Definition locked (l : loc) (R : iProp) : iProp :=
  ( N γ,  (heapN  N)  heap_ctx heapN 
          inv N (lock_inv γ l R)  own γ (Excl ()))%I.

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.

Lemma newlock_spec N (R : iProp) Φ :
  heapN  N 
  (heap_ctx heapN  R  ( l, is_lock l R - Φ (LocV l)))
   WP newlock #() {{ Φ }}.
Proof.
  iIntros {?} "(#Hh&HR&HΦ)". rewrite /newlock.
  wp_seq. iApply wp_pvs. wp_alloc l as "Hl".
  iPvs (own_alloc (Excl ())) as {γ} "Hγ"; first done.
  iPvs (inv_alloc N _ (lock_inv γ l R)) "[HR Hl Hγ]" as "#?"; first done.
  { iNext. iExists false. by iFrame "Hl HR". }
  iPvsIntro; iApply "HΦ". iExists N, γ. by repeat iSplit.
Qed.

Lemma acquire_spec l R (Φ : val  iProp) :
  (is_lock l R  (locked l R - R - Φ #()))  WP acquire (%l) {{ Φ }}.
Proof.
  iIntros "[Hl HΦ]". iDestruct "Hl" as {N γ} "(%&#?&#?)".
  iLöb as "IH". wp_rec. wp_focus (CAS _ _ _)%E.
  iInv N as "Hinv". iDestruct "Hinv" as {b} "[Hl HR]"; destruct b.
  - wp_cas_fail. iSplitL "Hl".
    + iNext. iExists true. by iSplit.
    + wp_if. by iApply "IH".
  - wp_cas_suc. iDestruct "HR" as "[Hγ HR]". iSplitL "Hl".
    + iNext. iExists true. by iSplit.
    + wp_if. iPvsIntro. iApply "HΦ" "-[HR] HR". iExists N, γ. by repeat iSplit.
Qed.

Lemma release_spec R l (Φ : val  iProp) :
  (locked l R  R  (is_lock l R - Φ #()))  WP release (%l) {{ Φ }}.
Proof.
  iIntros "(Hl&HR&HΦ)"; iDestruct "Hl" as {N γ} "(%&#?&#?&Hγ)".
  rewrite /release. wp_let.
  iInv N as "Hinv". iDestruct "Hinv" as {b} "[Hl Hγ']"; destruct b.
  - wp_store. iSplitL "Hl HR Hγ".
    + iNext. iExists false. by iFrame "Hl HR Hγ".
    + iApply "HΦ". iExists N, γ. by repeat iSplit.
  - wp_store. iDestruct "Hγ'" as "[Hγ' _]".
    iCombine "Hγ" "Hγ'" as "Hγ". by iDestruct own_valid "Hγ" as "%".
Qed.
End proof.