lock.v 10.2 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.
Dan Frumin's avatar
Dan Frumin committed
6
Definition acquire : val := rec: "acquire" "x" :=
7 8
  if: CAS "x" #false #true
  then #()
Dan Frumin's avatar
Dan Frumin committed
9 10
  else "acquire" "x".

11
Definition release : val := λ: "x", "x" <- #false.
12 13
Definition with_lock : val := λ: "e" "l" "x",
  acquire "l";;
Dan Frumin's avatar
Dan Frumin committed
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.

Dan Frumin's avatar
Dan Frumin committed
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).
Dan Frumin's avatar
Dan Frumin committed
27
Proof. solve_typed. Qed.
28

Dan Frumin's avatar
Dan Frumin committed
29
Hint Resolve acquire_type : typeable.
30

Dan Frumin's avatar
Dan Frumin committed
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 τ τ'))).
Dan Frumin's avatar
Dan Frumin committed
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 72 73 74
  Proof. apply _. Qed.

  Lemma bin_log_related_newlock_l (R : iProp Σ) Δ Γ E K t τ :
    R -
    ( (lk : loc) γ, is_lock γ #lk R
75 76
      - ({E;Δ;Γ}  fill K #lk log t: τ)) -
    {E;Δ;Γ}  fill K (newlock #()) log t: τ.
77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92
  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.

  Lemma bin_log_related_release_l (R : iProp Σ) (lk : loc) γ Δ Γ E K t τ :
    N  E 
    is_lock γ #lk R -
    locked γ -
    R -
93 94
    ({E;Δ;Γ}  fill K #() log t: τ) -
    {E;Δ;Γ}  fill K (release #lk) log t: τ.
95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111
  Proof.
    iIntros (?) "Hlock Hlocked HR Hlog".
    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.

  Lemma bin_log_related_acquire_l (R : iProp Σ) (lk : loc) γ Δ Γ E K t τ :
    N  E 
    is_lock γ #lk R -
112 113
    (locked γ - R - {E;Δ;Γ}  fill K #() log t: τ) -
    {E;Δ;Γ}  fill K (acquire #lk) log t: τ.
114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139
  Proof.
    iIntros (?) "#Hlock Hlog".
    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.
140
  Context `{logrelG Σ}.
141

142
  Variable (E1 E2 : coPset).
143
  Variable (Δ : list (prodC valC valC -n> iProp Σ)).
144 145 146

  Lemma steps_newlock ρ j K
    (Hcl : nclose specN  E1) :
147 148
    spec_ctx ρ - j  fill K (newlock #())
    ={E1}=  l : loc, j  fill K (of_val #l)  l ↦ₛ #false.
149
  Proof.
150
    iIntros "#Hspec Hj".
Dan Frumin's avatar
Dan Frumin committed
151 152
    unfold newlock. unlock.
    tp_rec j. simpl.
153 154
    tp_alloc j as l "Hl". tp_normalise j.
    by iExists _; iFrame.
155 156
  Qed.

157 158
  Lemma bin_log_related_newlock_r Γ K t τ 
    (Hcl : nclose specN  E1) :
159 160
    ( l : loc, l ↦ₛ #false - {E1,E2;Δ;Γ}  t log fill K #l : τ) -
    {E1,E2;Δ;Γ}  t log fill K (newlock #()): τ.
161 162
  Proof.
    iIntros "Hlog".
Dan Frumin's avatar
Dan Frumin committed
163 164
    unfold newlock. unlock.
    rel_rec_r.
165 166
    rel_alloc_r as l "Hl".
    iApply ("Hlog" with "Hl").
167 168
  Qed.

169
  Lemma bin_log_related_newlock_l_simp Γ K t τ :
170 171
    ( l : loc, l ↦ᵢ #false - {E1;Δ;Γ}  fill K #l log t : τ) -
    {E1;Δ;Γ}  fill K (newlock #()) log t : τ.
Dan Frumin's avatar
Dan Frumin committed
172 173 174 175 176 177 178 179
  Proof.
    iIntros "Hlog".
    unfold newlock. unlock.
    rel_rec_l.
    rel_alloc_l as l "Hl".
    iApply ("Hlog" with "Hl").
  Qed.

180
  Global Opaque newlock.
181 182
  
  Transparent acquire. 
183 184
  Lemma steps_acquire ρ j K l
    (Hcl : nclose specN  E1) :
185 186
    spec_ctx ρ - l ↦ₛ #false - j  fill K (acquire #l)
    ={E1}= j  fill K (Lit Unit)  l ↦ₛ #true.
187
  Proof.
188
    iIntros "#Hspec Hl Hj". 
Dan Frumin's avatar
Dan Frumin committed
189
    unfold acquire. unlock.
190
    tp_rec j.
191
    tp_cas_suc j. simpl.
192
    tp_if_true j.
193
    by iFrame.
194
  Qed.
195
  
196 197
  Lemma bin_log_related_acquire_r Γ K l t τ
    (Hcl : nclose specN  E1) :
198 199 200
    l ↦ₛ #false -
    (l ↦ₛ #true - {E1,E2;Δ;Γ}  t log fill K (Lit Unit) : τ) -
    {E1,E2;Δ;Γ}  t log fill K (acquire #l) : τ.
201 202
  Proof.
    iIntros "Hl Hlog".
Dan Frumin's avatar
Dan Frumin committed
203
    unfold acquire. unlock.
204
    rel_rec_r.
205
    rel_cas_suc_r. simpl.
206
    rel_if_r.
207
    by iApply "Hlog".
208
  Qed.
Dan Frumin's avatar
Dan Frumin committed
209 210 211

  Lemma bin_log_related_acquire_suc_l Γ K l t τ :
    l ↦ᵢ #false -
212 213
    (l ↦ᵢ #true - {E1;Δ;Γ}  fill K (#()) log t : τ) -
    {E1;Δ;Γ}  fill K (acquire #l) log t : τ.
Dan Frumin's avatar
Dan Frumin committed
214 215 216 217 218 219 220 221 222 223 224 225 226 227 228
  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 -
229 230
    (l ↦ᵢ #false - {E1;Δ;Γ}  fill K (acquire #l) log t : τ) -
    {E1;Δ;Γ}  fill K (acquire #l) log t : τ.
Dan Frumin's avatar
Dan Frumin committed
231 232 233 234 235 236 237 238 239 240 241 242 243 244
  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.

245 246
  Global Opaque acquire.

247
  Transparent release.
248
  Lemma steps_release ρ j K l (b : bool)
249
    (Hcl : nclose specN  E1) :
250
    spec_ctx ρ - l ↦ₛ #b - j  fill K (release #l)
251
    ={E1}= j  fill K #()  l ↦ₛ #false.
252
  Proof.
Dan Frumin's avatar
Dan Frumin committed
253
    iIntros "#Hspec Hl Hj". unfold release. unlock.
254
    tp_rec j.
255
    tp_store j.
256
    by iFrame.
257 258
  Qed.

259
  Lemma bin_log_related_release_r Γ K l t τ (b : bool)
260
    (Hcl : nclose specN  E1) :
261 262 263
    l ↦ₛ #b -
    (l ↦ₛ #false - {E1,E2;Δ;Γ}  t log fill K (Lit Unit) : τ) -
    {E1,E2;Δ;Γ}  t log fill K (release #l) : τ.
264 265
  Proof.
    iIntros "Hl Hlog".
Dan Frumin's avatar
Dan Frumin committed
266
    unfold release. unlock.
267 268 269
    rel_rec_r.
    rel_store_r.
    by iApply "Hlog".
270 271
  Qed.

272
  Global Opaque release.
273

274
  Lemma steps_with_lock ρ j K e ev l P Q v w:
275
    to_val e = Some ev 
276
    ( K', spec_ctx ρ - P - j  fill K' (App e (of_val w))
277 278
            ={E1}= j  fill K' (of_val v)  Q) 
    (nclose specN  E1) 
279 280 281
    spec_ctx ρ - P - l ↦ₛ #false -
    j  fill K (with_lock e #l w)
    ={E1}= j  fill K (of_val v)  Q  l ↦ₛ #false.
282
  Proof.
283
    iIntros (Hev Hpf ?) "#Hspec HP Hl Hj".
Dan Frumin's avatar
Dan Frumin committed
284
    unfold with_lock. unlock.
285 286
    tp_rec j.
    tp_rec j.
287
    tp_rec j.
288
    tp_bind j (App acquire (# l)).
Dan Frumin's avatar
Dan Frumin committed
289
    tp_apply j steps_acquire with "Hl" as "Hl".
290
    tp_rec j.
291
    tp_bind j (App e _).
292
    iMod (Hpf with "Hspec HP Hj") as "[Hj HQ]". 
293
    tp_normalise j.
294
    tp_rec j; eauto using to_of_val.
295
    tp_bind j (App release _).    
Dan Frumin's avatar
Dan Frumin committed
296
    tp_apply j steps_release with "Hl" as "Hl".
297
    tp_normalise j.
298
    tp_rec j.
299
    by iFrame.
300
  Qed.
301
  
302
  Lemma bin_log_related_with_lock_r Γ K Q e ev ew cl v w l t τ :
303
    (to_val e = Some cl) 
304 305
    (to_val ev = Some v) 
    (to_val ew = Some w) 
306
    (nclose specN  E1) 
307 308
    ( K, (Q - {E1,E2;Δ;Γ}  t log fill K ev : τ) -
        {E1,E2;Δ;Γ}  t log fill K (App e ew) : τ) -
309 310 311
    l ↦ₛ #false -
    (Q - l ↦ₛ #false - {E1,E2;Δ;Γ}  t log fill K ev : τ) -
    {E1,E2;Δ;Γ}  t log fill K (with_lock e #l ew) : τ.
312
  Proof.
313 314 315
    iIntros (????) "HA Hl Hlog".
    rel_bind_r (with_lock e).
    unfold with_lock. unlock. (*TODO: unlock here needed *)
316
    iApply (bin_log_related_rec_r); eauto. simpl_subst.
317
    rel_bind_r (App _ (# l)).
318 319
    iApply (bin_log_related_rec_r); eauto. simpl_subst.
    iApply (bin_log_related_rec_r); eauto. simpl_subst.
320
    rel_bind_r (App acquire (# l)).
321
    iApply (bin_log_related_acquire_r Γ (_ :: K) l with "Hl"); auto.
322
    iIntros "Hl". simpl.
323
    iApply (bin_log_related_rec_r); eauto. simpl_subst/=.
324
    rel_bind_r (App e ew).
325
    iApply "HA". iIntros "HQ". simpl.
326
    iApply (bin_log_related_rec_r); eauto. simpl_subst.
327 328
    rel_bind_r (App release _).
    iApply (bin_log_related_release_r with "Hl"); eauto.
329
    iIntros "Hl". simpl.
330
    iApply (bin_log_related_rec_r); eauto. simpl_subst.
331 332 333
    iApply ("Hlog" with "HQ Hl").
  Qed.

334
End lock_rules_r.