ticket_lock.v 13.7 KB
Newer Older
Dan Frumin's avatar
Dan Frumin committed
1
From iris.proofmode Require Import tactics.
Dan Frumin's avatar
Dan Frumin committed
2
From iris.algebra Require Export auth gset excl.
Dan Frumin's avatar
Dan Frumin committed
3
From iris.base_logic Require Import auth.
4
From iris_logrel Require Export logrel examples.lock examples.counter.
Dan Frumin's avatar
Dan Frumin committed
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".
Dan Frumin's avatar
Dan Frumin committed
18

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

23
Definition LockType : type := ref TNat × ref TNat.
Dan Frumin's avatar
Dan Frumin committed
24 25 26

Hint Unfold LockType : typeable.

27
Lemma newlock_type Γ : typed Γ newlock (Unit  LockType).
Dan Frumin's avatar
Dan Frumin committed
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.
Dan Frumin's avatar
Dan Frumin committed
39 40 41

Hint Resolve acquire_type : typeable.

42
Lemma release_type Γ : typed Γ release (LockType  TUnit).
43
Proof. unlock release wkincr. solve_typed. Qed.
Dan Frumin's avatar
Dan Frumin committed
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.
Dan Frumin's avatar
Dan Frumin committed
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 *)
Dan Frumin's avatar
Dan Frumin committed
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)).
Dan Frumin's avatar
Dan Frumin committed
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.
Dan Frumin's avatar
Dan Frumin committed
80

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

84 85 86
  Lemma issueNewTicket γ m :
    issuedTickets γ m ==
    issuedTickets γ (S m)  ticket γ m.
Dan Frumin's avatar
Dan Frumin committed
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).
Dan Frumin's avatar
Dan Frumin committed
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.@(lo,ln,l')) (lockInv lo ln γ l'))%I.
121
  Next Obligation. solve_proper. Qed.
122 123 124 125 126 127 128 129
  
  (* Program Definition lockInt (γp : gname) := λne vv, *)
  (*   ( (lo ln : loc) (γ : gname) (l' : loc), *)
  (*       vv.1 = (#lo, #ln)%V  vv.2 = #l'⌝ *)
  (*      inPool γp lo ln γ l')%I. *)
  (* Next Obligation. solve_proper. Qed. *)

  Instance lockInt_persistent ww : Persistent (lockInt ww).
130 131
  Proof. apply _. Qed.

132
  (** * Refinement proofs *)
133

134 135
  Local Ltac openI N := 
    iInv N as (o n b) ">(Hlo & Hln & Hissued & Hl' & Hbticket)" "Hcl".
136
  Local Ltac closeI := iMod ("Hcl" with "[-]") as "_";
137
    first by (iNext; iExists _,_,_; iFrame).
138

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

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

196 197 198 199 200 201
  (** 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 *)
202 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 246 247 248 249 250 251
  Lemma acquire_l_logatomic R P γ Δ Γ E1 E2 K lo ln t τ :
    P -
     (|={E1,E2}=>  o n : nat, lo ↦ᵢ #o  ln ↦ᵢ #n  issuedTickets γ n  R o 
       (( o n : nat, lo ↦ᵢ #o  ln ↦ᵢ #n  issuedTickets γ n  R o) ={E2,E1}= True) 
        ( o n : nat, lo ↦ᵢ #o  ln ↦ᵢ #n  issuedTickets γ n  ticket γ o  R o - P -
            {E2,E1;Δ;Γ}  fill K #() log t : τ))
    - ({E1;Δ;Γ}  fill K (acquire (#lo, #ln)) log t : τ).
  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.

252 253
  Lemma acquire_refinement Δ Γ :
    {lockInt :: Δ; ⤉Γ}  acquire log lock.acquire : (TVar 0  Unit).
254 255 256 257 258 259 260 261 262 263 264 265
  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.
266
    openI (N.@(lo, ln, l')).
267
    iModIntro. iExists _,_; iFrame.
268
    iSplitL "Hbticket Hl'".
269 270 271 272 273 274
    { 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 "[-]").
275
      iNext. iExists _,_,_. by iFrame.
276 277 278 279 280 281 282 283
    - 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 "_".
284
      { iNext. iExists _,_,_; by iFrame. }
285 286 287
      iApply bin_log_related_unit.
  Qed.

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

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

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

Dan Frumin's avatar
Dan Frumin committed
391 392 393
  Lemma ticket_lock_refinement Γ :
    Γ  Pack (newlock, acquire, release)
      log
394
        Pack (lock.newlock, lock.acquire, lock.release) : lockT.
Dan Frumin's avatar
Dan Frumin committed
395 396
  Proof.
    iIntros (Δ).
397
    iApply (bin_log_related_pack _ lockInt).
Dan Frumin's avatar
Dan Frumin committed
398
    repeat iApply bin_log_related_pair.
399
    - by iApply newlock_refinement.
400
    - by iApply acquire_refinement_direct.
401
    - by iApply release_refinement.
Dan Frumin's avatar
Dan Frumin committed
402
  Qed.
Dan Frumin's avatar
Dan Frumin committed
403

Dan Frumin's avatar
Dan Frumin committed
404
End refinement.