lock.v 3.16 KB
Newer Older
1 2 3 4 5 6 7
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 :=
Robbert Krebbers's avatar
Robbert Krebbers committed
8 9
  rec: "acquire" "l" :=
    if: CAS '"l" #false #true then #() else '"acquire" '"l".
10
Definition release : val := λ: "l", '"l" <- #false.
11
Global Opaque newlock acquire release.
12 13 14

(** The CMRA we need. *)
(* Not bundling heapG, as it may be shared with other users. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
15
Class lockG Σ := LockG { lock_tokG :> inG heap_lang Σ (exclR unitC) }.
16 17 18 19 20 21 22 23 24 25 26 27 28
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 :=
29
  ( N γ, heapN  N  heap_ctx heapN  inv N (lock_inv γ l R))%I.
30 31

Definition locked (l : loc) (R : iProp) : iProp :=
32
  ( N γ, heapN  N  heap_ctx heapN 
33 34 35 36 37 38 39 40 41 42 43 44 45
          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.

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 {N γ} "(?&?&?&_)"; eauto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
48

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

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

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