ticket_lock.v 13.3 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 199
     (|={,E}=>  o n : nat, lo ↦ᵢ #o  ln ↦ᵢ #n  issuedTickets γ n  R o 
       (( o n : nat, lo ↦ᵢ #o  ln ↦ᵢ #n  issuedTickets γ n  R o) ={E,}= True) 
200
        ( o 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 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245
  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 _]".
      iDestruct 1 as (n') "[Hln Ho]".
      iDestruct "Ho" as (o') "[Ho HR]".
      iApply "H".
      iExists _, _. iFrame.
    - iDestruct "Hrest" as "[H _]".
      iIntros (n') "[Hln Ho] HP".
      iDestruct "Ho" as (o') "[Ho [Hissued HR]]".
      iMod (issueNewTicket with "Hissued") as "[Hissued Hm]".
      iMod ("H" with "[-HP Hm]") as "_".
      { iExists _,_. iFrame. }
      rel_let_l. clear o n o'.
      rel_rec_l.
      iLöb as "IH".
      unlock wait_loop. simpl.
      rel_rec_l. rel_proj_l.
      rel_load_l_atomic.
      iMod "H2" as (o n) "(Hlo & Hln & Hissued & HR & Hrest)". iModIntro.
      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").
        { iFrame. }
      + iDestruct "Hrest" as "[H _]".
        iMod ("H" with "[-HP Hm]") as "_".
        { iExists _,_; iFrame. }
        rel_rec_l. iApply ("IH" with "HP Hm").
  Qed.

246 247
  Lemma acquire_refinement Δ Γ :
    {lockInt :: Δ; ⤉Γ}  acquire log lock.acquire : (TVar 0  Unit).
248 249 250 251 252 253 254 255 256 257 258 259
  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.
260
    openI.
261
    iModIntro. iExists _,_; iFrame.
262
    iSplitL "Hbticket Hl'".
263 264 265 266 267 268
    { iExists _. iFrame. }
    clear b o n.
    iSplit.
    - iDestruct 1 as (o' n') "(Hlo & Hln & Hissued & Hrest)".
      iDestruct "Hrest" as (b) "[Hl' Ht]".
      iApply ("Hcl" with "[-]").
269
      iNext. iExists _,_,_. by iFrame.
270 271 272 273 274 275 276 277
    - iIntros (o n) "(Hlo & Hln & Hissued & Ht & Hrest) _".
      iDestruct "Hrest" as (b) "[Hl' Ht']".
      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 "_".
278
      { iNext. iExists _,_,_; by iFrame. }
279 280 281
      iApply bin_log_related_unit.
  Qed.

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

  (* Releasing the lock *)
308
  Lemma wkincr_l x (n : nat) Δ Γ K t τ :
309
    x ↦ᵢ #n -
310 311
    (x ↦ᵢ #(n+1) - {Δ;Γ}  fill K Unit log t : τ) -
    ({Δ;Γ}  fill K (wkincr #x) log t : τ).
312 313 314 315 316 317 318 319 320 321 322 323 324
  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
     Postcondition λ_,  n, x ↦ᵢ n
 *)
325
  Lemma wkincr_atomic_l R1 R2 Δ Γ E K x t τ  :
326
    R2 -
327 328
     (|={,E}=>  n : nat, x ↦ᵢ #n  R1 n 
       (( n : nat, x ↦ᵢ #n  R1 n) ={E,}= True) 
329
        ( m, ( n : nat, x ↦ᵢ #n)  R1 m - R2 -
330 331
            {E;Δ;Γ}  fill K Unit log t : τ))
    - ({Δ;Γ}  fill K (wkincr #x) log t : τ).
332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349
  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.
    { iExists _. iFrame. }
    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.

350 351
  Lemma release_refinement Δ Γ :
    {(lockInt :: Δ); ⤉Γ}  release log lock.release : (TVar 0  Unit).
352 353 354 355 356
  Proof.
    unlock release.
    iApply bin_log_related_arrow_val; eauto.
    { by unlock lock.release. }
    iAlways. iIntros (? ?) "/= #Hl".
357
    iDestruct "Hl" as (lo ln γ l') "(% & % & Hin)". simplify_eq.
358 359 360 361 362 363 364
    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.
365
    openI.
366
    iModIntro. iExists _; iFrame.
367 368
    rewrite {1}/R. iSplitR "Hcl".
    { iExists _,_; by iFrame. } clear o n b.
369 370 371 372
    iSplit.
    - iDestruct 1 as (o) "[Hlo HR]".
      unfold R. iDestruct "HR" as (n b) "HR".
      iApply "Hcl".
373
      iNext. iExists _,_,_; by iFrame.
374 375 376 377 378 379 380
    - iIntros (?) "[Hlo HR] _".
      iDestruct "Hlo" as (o) "Hlo".
      unfold R. iDestruct "HR" as (n b) "(Hln & Hissued & Hl' & Hticket)".
      rel_apply_r (bin_log_related_release_r with "Hl'").
      { solve_ndisj. }
      iIntros "Hl'".
      iMod ("Hcl" with "[-]") as "_".
381
      { iNext. iExists _,_,_. by iFrame. }
382
      iApply bin_log_related_unit.
383 384
  Qed.

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

398
End refinement.