ticket_lock.v 13.2 KB
Newer Older
1
From iris.proofmode Require Import tactics.
Dan Frumin's avatar
Dan Frumin committed
2
From iris.algebra Require Export auth gset excl.
3
From iris.base_logic Require Import auth.
4
From iris_logrel Require Export logrel examples.lock examples.counter.
5 6 7 8 9 10 11 12 13 14

Definition wait_loop: val :=
  rec: "wait_loop" "x" "lk" :=
    if: "x" = !(Fst "lk")
      then #() (* my turn *)
      else "wait_loop" "x" "lk".

Definition newlock : val :=
  λ: <>, ((* owner *) ref #0, (* next *) ref #0).

15
Definition acquire : val := λ: "lk",
Dan Frumin's avatar
Dan Frumin committed
16
  let: "n" := FG_increment (Snd "lk") in
17
  wait_loop "n" "lk".
18

19 20 21
Definition wkincr : val := λ: "l",
  "l" <- !"l" + #1.
Definition release : val := λ: "lk", wkincr (Fst "lk").
22

23
Definition LockType : type := ref TNat × ref TNat.
24 25 26

Hint Unfold LockType : typeable.

27
Lemma newlock_type Γ : typed Γ newlock (Unit  LockType).
28 29 30 31
Proof. solve_typed. Qed.

Hint Resolve newlock_type : typeable.

32
Lemma acquire_type Γ : typed Γ acquire (LockType  TUnit).
33 34 35 36 37 38
Proof.
  unlock acquire wait_loop.
  econstructor; cbn; solve_typed.
  econstructor; cbn; solve_typed.
  econstructor; cbn; solve_typed.
Qed.
39 40 41

Hint Resolve acquire_type : typeable.

42
Lemma release_type Γ : typed Γ release (LockType  TUnit).
43
Proof. unlock release wkincr. solve_typed. Qed.
44 45 46

Hint Resolve release_type : typeable.

47 48
Definition lockT : type := : (Unit  TVar 0) × (TVar 0  Unit) × (TVar 0  Unit).
Lemma ticket_lock_typed Γ : typed Γ (Pack (newlock, acquire, release)) lockT.
49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66
Proof.
  apply TPack with LockType.
  asimpl. solve_typed.
Qed.

Class tlockG Σ :=
  tlock_G :> authG Σ (gset_disjUR nat).
Definition tlockΣ : gFunctors :=
  #[ authΣ (gset_disjUR nat) ].

Definition lockPool := gset ((loc * loc * gname) * loc).
Definition lockPoolR := gsetUR ((loc * loc * gname) * loc).

Class lockPoolG Σ :=
  lockPool_inG :> authG Σ lockPoolR.
Section refinement.
  Context `{logrelG Σ, tlockG Σ, lockPoolG Σ}.

67
  (** * Basic abstractions around the concrete RA *)
68

69 70 71 72
  (** ticket with the id `n` *)
  Definition ticket (γ : gname) (n : nat) := own γ ( GSet {[ n ]}).
  (** total number of issued tickets is `n` *)
  Definition issuedTickets (γ : gname) (n : nat) := own γ ( GSet (seq_set 0 n)).
73

74 75 76 77 78 79
  Lemma ticket_nondup γ n : ticket γ n - ticket γ n - False.
  Proof.
    iIntros "Ht1 Ht2".
    iDestruct (own_valid_2 with "Ht1 Ht2") as %?%gset_disj_valid_op.
    set_solver.
  Qed.
80

81 82
  Lemma newIssuedTickets : (|==>  γ, issuedTickets γ 0)%I.
  Proof. iMod (own_alloc ( (GSet ))) as (γ) "Hγ"; [done|eauto]. Qed.
83

84 85 86
  Lemma issueNewTicket γ m :
    issuedTickets γ m ==
    issuedTickets γ (S m)  ticket γ m.
87
  Proof.
88 89 90 91 92 93
    iIntros "Hseq".
    iMod (own_update with "Hseq") as "[Hseq Hticket]".
    { eapply auth_update_alloc.
      eapply (gset_disj_alloc_empty_local_update _ {[ m ]}).
      apply (seq_set_S_disjoint 0). }
    rewrite -(seq_set_S_union_L 0).
94 95 96
    by iFrame.
  Qed.

97 98 99 100 101
  Instance ticket_timeless γ n : Timeless (ticket γ n).
  Proof. apply _. Qed.
  Instance issuedTickets_timeless γ n : Timeless (issuedTickets γ n).
  Proof. apply _. Qed.

102
  Opaque ticket issuedTickets.
103 104 105 106 107 108 109 110 111 112 113 114

  (** * Invariants and abstracts for them *)
  Definition lockInv (lo ln : loc) (γ : gname) (l' : loc) : iProp Σ :=
    ( (o n : nat) (b : bool), lo ↦ᵢ #o  ln ↦ᵢ #n
    issuedTickets γ n  l' ↦ₛ #b
    if b then ticket γ o else True)%I.

  Instance ifticket_timeless (b : bool) γ o : Timeless (if b then ticket γ o else True%I).
  Proof. destruct b; apply _. Qed.
  Instance lockInv_timeless lo ln γ l' : Timeless (lockInv lo ln γ l').
  Proof. apply _. Qed.

115
  Definition N := logrelN.@"locked".
116

117
  Program Definition lockInt := λne vv,
118 119
    ( (lo ln : loc) (γ : gname) (l' : loc),
        vv.1 = (#lo, #ln)%V  vv.2 = #l'⌝
120
       inv N (lockInv lo ln γ l'))%I.
121
  Next Obligation. solve_proper. Qed.
122 123
  
  Instance lockInt_persistent ww : Persistent (lockInt ww).
124 125
  Proof. apply _. Qed.

126
  (** * Refinement proofs *)
127

128
  Local Ltac openI :=
129
    iInv N as (o n b) ">(Hlo & Hln & Hissued & Hl' & Hbticket)" "Hcl".
130
  Local Ltac closeI := iMod ("Hcl" with "[-]") as "_";
131
    first by (iNext; iExists _,_,_; iFrame).
132

133
  (* Allocating a new lock *)
134 135
  Lemma newlock_refinement Δ Γ:
    {(lockInt:: Δ); ⤉Γ}  newlock log lock.newlock : (Unit  TVar 0).
136 137 138 139 140
  Proof.
    unlock newlock.
    iApply bin_log_related_arrow_val; eauto.
    { by unlock lock.newlock. }
    iAlways. iIntros (? ?) "/= [% %]"; simplify_eq.
141
    (* Reducing to a value on the LHS *)
142 143
    rel_let_l.
    rel_alloc_l as lo "Hlo".
144 145
    rel_alloc_l as ln "Hln".
    (* Reducing to a value on the RHS *)
146 147 148
    rel_apply_r bin_log_related_newlock_r.
    { solve_ndisj. }
    iIntros (l') "Hl'".
149 150
    (* Establishing the invariant *)
    iMod newIssuedTickets as (γ) "Hγ".
151
    iMod (inv_alloc N _ (lockInv lo ln γ l') with "[-]") as "#Hinv".
152 153 154
    { iNext. iExists _,_,_. iFrame. }
    rel_vals. iModIntro. iAlways.
    iExists _,_,_,_. iFrame "Hinv". eauto.
155 156 157
  Qed.

  (* Acquiring a lock *)
158
  (* helper lemma *)
159
  Lemma wait_loop_refinement Δ Γ (lo ln : loc) γ (l' : loc) (m : nat) :
160
    inv N (lockInv lo ln γ l') -
161
    ticket γ m -
162
    {(lockInt :: Δ); ⤉Γ} 
163 164
      wait_loop #m (#lo, #ln) log lock.acquire #l' : TUnit.
  Proof.
165
    iIntros "#Hinv Hticket".
166 167
    rel_rec_l.
    iLöb as "IH".
168
    unlock {2}wait_loop. simpl.
169 170
    rel_let_l. rel_proj_l.
    rel_load_l_atomic.
171
    openI.
172 173 174 175 176 177
    iModIntro. iExists _; iFrame; iNext.
    iIntros "Hlo".
    rel_op_l.
    case_decide; subst; rel_if_l.
    (* Whether the ticket is called out *)
    - destruct b.
178
      { iDestruct (ticket_nondup with "Hticket Hbticket") as %[]. }
179 180 181
      rel_apply_r (bin_log_related_acquire_r with "Hl'").
      { solve_ndisj. }
      iIntros "Hl'".
182
      closeI.
183 184
      iApply bin_log_related_unit.
    - iMod ("Hcl" with "[-Hticket]") as "_".
185
      { iNext. iExists _,_,_; by iFrame. }
186
      rel_rec_l.
187
      unlock wait_loop. simpl_subst/=. by iApply "IH".
188 189
  Qed.

190 191 192 193 194 195
  (** Logically atomic spec for `acquire`.
      Parameter type: nat
      Precondition:
        λo,  n, lo ↦ᵢ o  ln ↦ᵢ n  issuedTickets γ n
      Postcondition:
        λo,  n, lo ↦ᵢ o  ln ↦ᵢ n  issuedTickets γ n  ticket γ o *)
196
  Lemma acquire_l_logatomic R P γ Δ Γ E K lo ln t τ :
197
    P -
198
     (|={,E}=>  o n : nat, lo ↦ᵢ #o  ln ↦ᵢ #n  issuedTickets γ n  R o 
199 200
       ( o : nat, ( n : nat, lo ↦ᵢ #o  ln ↦ᵢ #n  issuedTickets γ n  R o) ={E,}= True) 
        ( o : nat, ( n : nat, lo ↦ᵢ #o  ln ↦ᵢ #n  issuedTickets γ n  ticket γ o  R o) - P -
201 202
            {E;Δ;Γ}  fill K #() log t : τ))
    - ({Δ;Γ}  fill K (acquire (#lo, #ln)) log t : τ).
203 204 205 206 207 208 209 210 211 212 213 214 215
  Proof.
    iIntros "HP #H".
    rewrite /acquire. unlock. simpl.
    rel_rec_l. rel_proj_l.
    rel_apply_l (bin_log_FG_increment_logatomic _ (fun n : nat =>  o : nat, lo ↦ᵢ #o  issuedTickets γ n  R o)%I P%I with "HP").
    iAlways.
    iPoseProof "H" as "H2".
    iMod "H" as (o n) "(Hlo & Hln & Hissued & HR & Hrest)". iModIntro.
    iExists _; iFrame.
    iSplitL "Hlo HR".
    { iExists _. iFrame. }
    iSplit.
    - iDestruct "Hrest" as "[H _]".
216
      iIntros "[Hln Ho]".
217 218
      iDestruct "Ho" as (o') "[Ho HR]".
      iApply "H".
219
      iExists _. iFrame.
220
    - iDestruct "Hrest" as "[H _]".
221
      iIntros "[Hln Ho] HP".
222 223 224
      iDestruct "Ho" as (o') "[Ho [Hissued HR]]".
      iMod (issueNewTicket with "Hissued") as "[Hissued Hm]".
      iMod ("H" with "[-HP Hm]") as "_".
225 226
      { iExists _. iFrame. } clear o o'.
      rel_let_l. rel_rec_l.
227 228 229 230
      iLöb as "IH".
      unlock wait_loop. simpl.
      rel_rec_l. rel_proj_l.
      rel_load_l_atomic.
231
      iMod "H2" as (o n') "(Hlo & Hln & Hissued & HR & Hrest)". iModIntro.
232 233 234 235 236 237
      iExists _. iFrame. iNext. iIntros "Hlo".
      rel_op_l.
      case_decide; subst; rel_if_l.
      (* Whether the ticket is called out *)
      + iDestruct "Hrest" as "[_ H]".
        iApply ("H" with "[-HP] HP").
238
        { iExists _. iFrame. }
239 240
      + iDestruct "Hrest" as "[H _]".
        iMod ("H" with "[-HP Hm]") as "_".
241
        { iExists _. iFrame. }
242 243 244
        rel_rec_l. iApply ("IH" with "HP Hm").
  Qed.

245 246
  Lemma acquire_refinement Δ Γ :
    {lockInt :: Δ; ⤉Γ}  acquire log lock.acquire : (TVar 0  Unit).
247 248 249 250 251 252 253 254 255 256 257 258
  Proof.
    iApply bin_log_related_arrow_val; eauto.
    { by unlock acquire. }
    { by unlock lock.acquire. }
    iAlways. iIntros (? ?) "/= #Hl".
    iDestruct "Hl" as (lo ln γ l') "(% & % & Hin)". simplify_eq/=.
    rel_apply_l (acquire_l_logatomic
                   (fun o =>  (b : bool),
                             l' ↦ₛ #b 
                             if b then ticket γ o else True)%I
                   True%I γ); first done.
    iAlways.
259
    openI.
260
    iModIntro. iExists _,_; iFrame.
261
    iSplitL "Hbticket Hl'".
262 263 264
    { iExists _. iFrame. }
    clear b o n.
    iSplit.
265
    - iIntros (o). iDestruct 1 as (n) "(Hlo & Hln & Hissued & Hrest)".
266 267
      iDestruct "Hrest" as (b) "[Hl' Ht]".
      iApply ("Hcl" with "[-]").
268
      iNext. iExists _,_,_. by iFrame.
269 270
    - iIntros (o). iDestruct 1 as (n) "(Hlo & Hln & Hissued & Ht & Hrest)".
      iIntros "_". iDestruct "Hrest" as (b) "[Hl' Ht']".
271 272 273 274 275 276
      destruct b.
      { iDestruct (ticket_nondup with "Ht Ht'") as %[]. }
      rel_apply_r (bin_log_related_acquire_r with "Hl'").
      { solve_ndisj. }
      iIntros "Hl'".
      iMod ("Hcl" with "[-]") as "_".
277
      { iNext. iExists _,_,_; by iFrame. }
278 279 280
      iApply bin_log_related_unit.
  Qed.

281 282
  Lemma acquire_refinement_direct Δ Γ :
    {(lockInt :: Δ); ⤉Γ}  acquire log lock.acquire : (TVar 0  Unit).
283 284 285 286 287
  Proof.
    unlock acquire; simpl.
    iApply bin_log_related_arrow_val; eauto.
    { by unlock lock.acquire. }
    iAlways. iIntros (? ?) "/= #Hl".
288
    iDestruct "Hl" as (lo ln γ l') "(% & % & Hin)". simplify_eq.
289
    rel_let_l. repeat rel_proj_l.
290
    rel_apply_l (bin_log_FG_increment_logatomic _ (issuedTickets γ)%I True%I); first done.
291
    iAlways.
292
    openI.
293 294
    iModIntro. iExists _; iFrame.
    iSplit.
295
    - iIntros "[Hln ?]".
296
      iApply ("Hcl" with "[-]").
297
      iNext. iExists _,_,_; by iFrame.
298
    - iIntros "[Hln Hissued] _".
299 300
      iMod (issueNewTicket with "Hissued") as "[Hissued Hm]".
      iMod ("Hcl" with "[-Hm]") as "_".
301
      { iNext. iExists _,_,_; by iFrame. }
302
      rel_let_l.
303 304 305 306
      by iApply wait_loop_refinement.
  Qed.

  (* Releasing the lock *)
307
  Lemma wkincr_l x (n : nat) Δ Γ K t τ :
308
    x ↦ᵢ #n -
309 310
    (x ↦ᵢ #(n+1) - {Δ;Γ}  fill K Unit log t : τ) -
    ({Δ;Γ}  fill K (wkincr #x) log t : τ).
311 312 313 314 315 316 317 318 319 320 321
  Proof.
    iIntros "Hx Hlog".
    unlock wkincr. rel_rec_l.
    rel_load_l. rel_op_l. rel_store_l.
    by iApply "Hlog".
  Qed.

  (* Logically atomic specification for wkincr,
     cf wkIncr specification from (da Rocha Pinto, Dinsdale-Young, Gardner)
     Parameter type: nat
     Precondition: λn, x ↦ᵢ n
322
     Postcondition λ_,  n, x ↦ᵢ (n+1)
323
 *)
324
  Lemma wkincr_atomic_l R1 R2 Δ Γ E K x t τ  :
325
    R2 -
326
     (|={,E}=>  n : nat, x ↦ᵢ #n  R1 n 
327 328
       (x ↦ᵢ #n  R1 n ={E,}= True) 
        (( n : nat, x ↦ᵢ #(n + 1))  R1 n - R2 -
329 330
            {E;Δ;Γ}  fill K Unit log t : τ))
    - ({Δ;Γ}  fill K (wkincr #x) log t : τ).
331 332 333 334 335 336 337 338 339
  Proof.
    iIntros "HR2 #H".
    unlock wkincr.
    rel_rec_l.
    iPoseProof "H" as "H2".
    rel_load_l_atomic.
    iMod "H" as (n) "[Hx [HR1 [Hrev _]]]". iModIntro.
    iExists _; iFrame. iNext. iIntros "Hx".
    iMod ("Hrev" with "[HR1 Hx]") as "_"; simpl.
340
    { iFrame. }
341 342 343 344 345 346 347 348
    rel_op_l.
    rel_store_l_atomic.
    iMod "H2" as (m) "[Hx [HR1 [_ Hmod]]]". iModIntro.
    iExists _; iFrame. iNext. iIntros "Hx".
    iApply ("Hmod" with "[$HR1 Hx] HR2").
    iExists _; iFrame.
  Qed.

349 350
  Lemma release_refinement Δ Γ :
    {(lockInt :: Δ); ⤉Γ}  release log lock.release : (TVar 0  Unit).
351 352 353 354 355
  Proof.
    unlock release.
    iApply bin_log_related_arrow_val; eauto.
    { by unlock lock.release. }
    iAlways. iIntros (? ?) "/= #Hl".
356
    iDestruct "Hl" as (lo ln γ l') "(% & % & Hin)". simplify_eq.
357 358 359 360 361 362 363
    rel_let_l. rel_proj_l.
    pose (R := fun (o : nat) =>
                 ( (n : nat) (b : bool), ln ↦ᵢ #n
                  issuedTickets γ n  l' ↦ₛ #b
                  if b then ticket γ o else True)%I).
    rel_apply_l (wkincr_atomic_l R True%I); first done.
    iAlways.
364
    openI.
365
    iModIntro. iExists _; iFrame.
366
    rewrite {1}/R. iSplitR "Hcl".
367
    { iExists _,_; by iFrame. }
368
    iSplit.
369 370
    - iIntros "[Hlo HR]".
      unfold R. iDestruct "HR" as (n' b') "HR".
371
      iApply "Hcl".
372
      iNext. iExists _,_,_; by iFrame.
373 374 375
    - iIntros "[Hlo HR] _".
      iDestruct "Hlo" as (o') "Hlo".
      unfold R. iDestruct "HR" as (n' b') "(Hln & Hissued & Hl' & Hticket)".
376 377 378 379
      rel_apply_r (bin_log_related_release_r with "Hl'").
      { solve_ndisj. }
      iIntros "Hl'".
      iMod ("Hcl" with "[-]") as "_".
380
      { iNext. iExists _,_,_. by iFrame. }
381
      iApply bin_log_related_unit.
382 383
  Qed.

384 385 386
  Lemma ticket_lock_refinement Γ :
    Γ  Pack (newlock, acquire, release)
      log
387
        Pack (lock.newlock, lock.acquire, lock.release) : lockT.
388 389
  Proof.
    iIntros (Δ).
390
    iApply (bin_log_related_pack lockInt).
391
    repeat iApply bin_log_related_pair.
392
    - by iApply newlock_refinement.
393
    - by iApply acquire_refinement_direct.
394
    - by iApply release_refinement.
395
  Qed.
396

397
End refinement.