lock.v 6.94 KB
Newer Older
1
From iris.proofmode Require Import tactics.
2
From iris.algebra Require Import excl.
3
From iris_logrel Require Export logrel.
4

5
Definition newlock : val := λ: <>, ref #false.
6
Definition acquire : val := rec: "acquire" "x" :=
7 8
  if: CAS "x" #false #true
  then #()
9 10
  else "acquire" "x".

11
Definition release : val := λ: "x", "x" <- #false.
12 13
Definition with_lock : val := λ: "e" "l" "x",
  acquire "l";;
14 15
  let: "v" := "e" "x" in
  release "l";; "v".
16 17 18

Definition LockType := Tref TBool.

Dan Frumin's avatar
Dan Frumin committed
19 20
Hint Unfold LockType : typeable.

21 22 23 24
Lemma newlock_type Γ : typed Γ newlock (TArrow TUnit LockType).
Proof. solve_typed. Qed.

Hint Resolve newlock_type : typeable.
25 26

Lemma acquire_type Γ : typed Γ acquire (TArrow LockType TUnit).
27
Proof. solve_typed. Qed.
28

29
Hint Resolve acquire_type : typeable.
30

31 32
Lemma release_type Γ : typed Γ release (TArrow LockType TUnit).
Proof. solve_typed. Qed.
33

Dan Frumin's avatar
Dan Frumin committed
34
Hint Resolve release_type : typeable.
35 36 37

Lemma with_lock_type Γ τ τ' :
  typed Γ with_lock (TArrow (TArrow τ τ') (TArrow LockType (TArrow τ τ'))).
38
Proof. solve_typed. Qed.
39

Dan Frumin's avatar
Dan Frumin committed
40 41
Hint Resolve with_lock_type : typeable.

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
Class lockG Σ := LockG { lock_tokG :> inG Σ (exclR unitC) }.
Definition lockΣ : gFunctors := #[GFunctor (exclR unitC)].

Instance subG_lockΣ {Σ} : subG lockΣ Σ  lockG Σ.
Proof. solve_inG. Qed.

Section lockG_rules.
  Context `{!lockG Σ, !logrelG Σ} (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, lk = #l  inv N (lock_inv γ l R))%I.

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

  Lemma locked_exclusive (γ : gname) : locked γ - locked γ - False.
  Proof. iIntros "H1 H2". by iDestruct (own_valid_2 with "H1 H2") as %?. Qed.

  Global Instance lock_inv_ne γ l : NonExpansive (lock_inv γ l).
  Proof. solve_proper. Qed.
  Global Instance is_lock_ne l : NonExpansive (is_lock γ l).
  Proof. solve_proper. Qed.

Dan Frumin's avatar
Dan Frumin committed
67
  Global Instance is_lock_persistent γ l R : Persistent (is_lock γ l R).
68
  Proof. apply _. Qed.
Dan Frumin's avatar
Dan Frumin committed
69
  Global Instance locked_timeless γ : Timeless (locked γ).
70 71
  Proof. apply _. Qed.

72
  Lemma bin_log_related_newlock_l (R : iProp Σ) Δ Γ K t τ :
73 74
    R -
    ( (lk : loc) γ, is_lock γ #lk R
75 76
      - ({Δ;Γ}  fill K #lk log t: τ)) -
    {Δ;Γ}  fill K (newlock #()) log t: τ.
77 78 79 80 81 82 83 84 85 86 87
  Proof.
    iIntros "HR Hlog".
    iApply bin_log_related_wp_l.
    rewrite -wp_fupd /newlock /=. unlock.
    wp_seq. wp_alloc l as "Hl".
    iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
    iMod (inv_alloc N _ (lock_inv γ l R) with "[-Hlog]") as "#?".
    { iIntros "!>". iExists false. by iFrame. }
    iModIntro. iApply "Hlog". iExists l. eauto.
  Qed.

88
  Lemma bin_log_related_release_l (R : iProp Σ) (lk : loc) γ Δ Γ K t τ :
89 90 91
    is_lock γ #lk R -
    locked γ -
    R -
92 93
    ({Δ;Γ}  fill K #() log t: τ) -
    {Δ;Γ}  fill K (release #lk) log t: τ.
94
  Proof.
95
    iIntros "Hlock Hlocked HR Hlog".
96 97 98 99 100 101 102 103 104 105 106 107
    iDestruct "Hlock" as (l) "[% #?]"; simplify_eq.
    unlock release. simpl.
    rel_let_l.
    rel_store_l_atomic.
    iInv N as (b) "[Hl _]" "Hclose".
    iModIntro. iExists _. iFrame.
    iNext. iIntros "Hl".
    iMod ("Hclose" with "[-Hlog]").
    { iNext. iExists false. by iFrame. }
    iApply "Hlog".
  Qed.

108
  Lemma bin_log_related_acquire_l (R : iProp Σ) (lk : loc) γ Δ Γ K t τ :
109
    is_lock γ #lk R -
110 111
    (locked γ - R - {Δ;Γ}  fill K #() log t: τ) -
    {Δ;Γ}  fill K (acquire #lk) log t: τ.
112
  Proof.
113
    iIntros "#Hlock Hlog".
114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137
    iLöb as "IH".
    unlock acquire. simpl.
    rel_rec_l.
    iDestruct "Hlock" as (l) "[% #?]". simplify_eq.
    rel_cas_l_atomic.
    iInv N as (b) "[Hl HR]" "Hclose".
    iModIntro. iExists _. iFrame.
    iSplit.
    - iIntros (?). iNext. iIntros "Hl".
      assert (b = true) as ->. { destruct b; congruence. }
      rel_if_l.
      iMod ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
      by iApply "IH".
    - iIntros (?). simplify_eq.
      iNext. iIntros "Hl".
      rel_if_l.
      iMod ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
      iDestruct "HR" as "[Hlocked HR]".
      iApply ("Hlog" with "Hlocked HR").
  Qed.

End lockG_rules.

Section lock_rules_r.
138
  Context `{logrelG Σ}.
139

140
  Variable (E : coPset).
141
  Variable (Δ : list (prodC valC valC -n> iProp Σ)).
142 143

  Lemma bin_log_related_newlock_r Γ K t τ 
144 145 146
    (Hcl : nclose specN  E) :
    ( l : loc, l ↦ₛ #false - {E;Δ;Γ}  t log fill K #l : τ) -
    {E;Δ;Γ}  t log fill K (newlock #()): τ.
147 148
  Proof.
    iIntros "Hlog".
149 150
    unfold newlock. unlock.
    rel_rec_r.
151 152
    rel_alloc_r as l "Hl".
    iApply ("Hlog" with "Hl").
153 154
  Qed.

155
  Lemma bin_log_related_newlock_l_simp Γ K t τ :
156 157
    ( l : loc, l ↦ᵢ #false - {Δ;Γ}  fill K #l log t : τ) -
    {Δ;Γ}  fill K (newlock #()) log t : τ.
158 159 160 161 162 163 164 165
  Proof.
    iIntros "Hlog".
    unfold newlock. unlock.
    rel_rec_l.
    rel_alloc_l as l "Hl".
    iApply ("Hlog" with "Hl").
  Qed.

166
  Global Opaque newlock.
167 168
  
  Transparent acquire. 
Dan Frumin's avatar
Dan Frumin committed
169
 
170
  Lemma bin_log_related_acquire_r Γ K l t τ
171
    (Hcl : nclose specN  E) :
172
    l ↦ₛ #false -
173 174
    (l ↦ₛ #true - {E;Δ;Γ}  t log fill K Unit : τ) -
    {E;Δ;Γ}  t log fill K (acquire #l) : τ.
175 176
  Proof.
    iIntros "Hl Hlog".
177
    unfold acquire. unlock.
178
    rel_rec_r.
179
    rel_cas_suc_r. simpl.
180
    rel_if_r.
181
    by iApply "Hlog".
182
  Qed.
183 184 185

  Lemma bin_log_related_acquire_suc_l Γ K l t τ :
    l ↦ᵢ #false -
186 187
    (l ↦ᵢ #true - {Δ;Γ}  fill K (#()) log t : τ) -
    {Δ;Γ}  fill K (acquire #l) log t : τ.
188 189 190 191 192 193 194 195 196 197 198 199 200 201 202
  Proof.
    iIntros "Hl Hlog".
    unfold acquire. unlock.
    rel_rec_l.
    rel_cas_l_atomic. iModIntro.
    iExists _; iFrame "Hl".
    iSplitR.
    { iIntros (Hfoo). congruence. }
    iIntros (_). iNext. iIntros "Hl".
    rel_if_l.
    by iApply "Hlog".
  Qed.

  Lemma bin_log_related_acquire_fail_l Γ K l t τ :
    l ↦ᵢ #true -
203 204
    (l ↦ᵢ #false - {Δ;Γ}  fill K (acquire #l) log t : τ) -
    {Δ;Γ}  fill K (acquire #l) log t : τ.
205 206 207 208 209 210 211 212 213 214 215 216 217 218
  Proof.
    iIntros "Hl Hlog".
    iLöb as "IH".
    unfold acquire. unlock.
    rel_rec_l.
    rel_cas_l_atomic. iModIntro.
    iExists _; iFrame "Hl".
    iSplitL; last first.
    { iIntros (Hfoo). congruence. }
    iIntros (_). iNext. iIntros "Hl".
    rel_if_l.
    iApply ("IH" with "Hl Hlog").
  Qed.

219 220
  Global Opaque acquire.

221
  Transparent release.
222
  Lemma bin_log_related_release_r Γ K l t τ (b : bool)
223
    (Hcl : nclose specN  E) :
224
    l ↦ₛ #b -
225 226
    (l ↦ₛ #false - {E;Δ;Γ}  t log fill K Unit : τ) -
    {E;Δ;Γ}  t log fill K (release #l) : τ.
227 228
  Proof.
    iIntros "Hl Hlog".
229
    unfold release. unlock.
230 231 232
    rel_rec_r.
    rel_store_r.
    by iApply "Hlog".
233 234
  Qed.

235
  Global Opaque release.
236
  
237
End lock_rules_r.