ticket_lock.v 6.84 KB
Newer Older
1 2 3 4
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.program_logic Require Import auth.
From iris.proofmode Require Import invariants.
Zhen Zhang's avatar
Zhen Zhang committed
5 6 7 8 9
From iris.heap_lang Require Import proofmode notation.
From iris.algebra Require Import gset.
Import uPred.

Definition wait_loop: val :=
Zhen Zhang's avatar
Zhen Zhang committed
10 11
  rec: "wait_loop" "x" "lock" :=
    let: "o" := !(Fst "lock") in
Zhen Zhang's avatar
Zhen Zhang committed
12 13
    if: "x" = "o"
      then #() (* my turn *)
Zhen Zhang's avatar
Zhen Zhang committed
14 15 16
      else "wait_loop" "x" "lock".

Definition newlock : val := λ: <>, ((* owner *) ref #0, (* next *) ref #0).
Zhen Zhang's avatar
Zhen Zhang committed
17 18

Definition acquire : val :=
Zhen Zhang's avatar
Zhen Zhang committed
19 20 21 22 23
  rec: "acquire" "lock" :=
    let: "n" := !(Snd "lock") in
    if: CAS (Snd "lock") "n" ("n" + #1)
      then wait_loop "n" "lock"
      else "acquire" "lock".
Zhen Zhang's avatar
Zhen Zhang committed
24 25

Definition release : val :=
Zhen Zhang's avatar
Zhen Zhang committed
26 27 28
  rec: "release" "lock" :=
    let: "o" := !(Fst "lock") in
    if: CAS (Fst "lock") "o" ("o" + #1)
Zhen Zhang's avatar
Zhen Zhang committed
29
      then #()
Zhen Zhang's avatar
Zhen Zhang committed
30
      else "release" "lock".
Zhen Zhang's avatar
Zhen Zhang committed
31 32 33

Global Opaque newlock acquire release wait_loop.

34
(** The CMRAs we need. *)
Zhen Zhang's avatar
Zhen Zhang committed
35
Class tlockG Σ := TlockG {
36 37
   tlock_G :> authG Σ (gset_disjUR nat);
   tlock_exclG  :> inG Σ (exclR unitC)
Zhen Zhang's avatar
Zhen Zhang committed
38
}.
39 40
Definition tlockΣ : gFunctors :=
  #[authΣ (gset_disjUR nat); GFunctor (constRF (exclR unitC))].
41

42 43
Instance subG_tlockΣ {Σ} : subG tlockΣ Σ  tlockG Σ.
Proof. intros [? [?%subG_inG _]%subG_inv]%subG_inv. split; apply _. Qed.
Zhen Zhang's avatar
Zhen Zhang committed
44 45

Section proof.
Zhen Zhang's avatar
Zhen Zhang committed
46
Context `{!heapG Σ, !tlockG Σ} (N : namespace) (HN: heapN  N).
Zhen Zhang's avatar
Zhen Zhang committed
47

48
Definition tickets_inv (n: nat) (gs: gset_disjUR nat) : iProp Σ :=
49
  (gs = GSet (seq_set 0 n))%I.
Zhen Zhang's avatar
Zhen Zhang committed
50

Zhen Zhang's avatar
Zhen Zhang committed
51 52 53 54 55
Definition lock_inv (γ1 γ2: gname) (lo ln: loc) (R : iProp Σ) : iProp Σ :=
  ( (o n: nat),
       lo  #o  ln  #n 
       auth_inv γ1 (tickets_inv n) 
       ((own γ2 (Excl ())   R)  auth_own γ1 (GSet {[ o ]})))%I.
Zhen Zhang's avatar
Zhen Zhang committed
56

Zhen Zhang's avatar
Zhen Zhang committed
57 58
Definition is_lock (l: val) (R: iProp Σ) : iProp Σ :=
  ( γ1 γ2 (lo ln: loc), heap_ctx  l = (#lo, #ln)%V  inv N (lock_inv γ1 γ2 lo ln R))%I.
Zhen Zhang's avatar
Zhen Zhang committed
59

Zhen Zhang's avatar
Zhen Zhang committed
60 61 62
Definition issued (l : val) (x: nat) (R : iProp Σ) : iProp Σ :=
  ( γ1 γ2 (lo ln: loc), heap_ctx  l = (#lo, #ln)%V  inv N (lock_inv γ1 γ2 lo ln R) 
                         auth_own γ1 (GSet {[ x ]}))%I.
Zhen Zhang's avatar
Zhen Zhang committed
63

Zhen Zhang's avatar
Zhen Zhang committed
64 65 66
Definition locked (l : val) (R : iProp Σ) : iProp Σ :=
  ( γ1 γ2 (lo ln: loc), heap_ctx  l = (#lo, #ln)%V  inv N (lock_inv γ1 γ2 lo ln R) 
                         own γ2 (Excl ()))%I.
Zhen Zhang's avatar
Zhen Zhang committed
67

Zhen Zhang's avatar
Zhen Zhang committed
68
Global Instance lock_inv_ne n γ1 γ2 lo ln: Proper (dist n ==> dist n) (lock_inv γ1 γ2 lo ln).
Zhen Zhang's avatar
Zhen Zhang committed
69 70 71 72 73 74 75 76 77
Proof. solve_proper. Qed.
Global Instance is_lock_ne n l: Proper (dist n ==> dist n) (is_lock l).
Proof. solve_proper. Qed.
Global Instance locked_ne n l: Proper (dist n ==> dist n) (locked l).
Proof. solve_proper. Qed.

Global Instance is_lock_persistent l R : PersistentP (is_lock l R).
Proof. apply _. Qed.

78
Lemma newlock_spec (R : iProp Σ) Φ :
Zhen Zhang's avatar
Zhen Zhang committed
79
  heap_ctx  R  ( l, is_lock l R - Φ l)  WP newlock #() {{ Φ }}.
Zhen Zhang's avatar
Zhen Zhang committed
80
Proof.
Zhen Zhang's avatar
Zhen Zhang committed
81 82
  iIntros "(#Hh & HR & HΦ)". rewrite /newlock.
  wp_seq. wp_alloc lo as "Hlo". wp_alloc ln as "Hln".
83 84
  iVs (own_alloc (Excl ())) as (γ2) "Hγ2"; first done.
  iVs (own_alloc_strong (Auth (Excl' ) ) {[ γ2 ]}) as (γ1) "[% Hγ1]"; first done.
Zhen Zhang's avatar
Zhen Zhang committed
85
  iVs (inv_alloc N _ (lock_inv γ1 γ2 lo ln R) with "[-HΦ]").
Zhen Zhang's avatar
Zhen Zhang committed
86 87 88 89 90 91
  { iNext. rewrite /lock_inv.
    iExists 0%nat, 0%nat.
    iFrame.
    iSplitL "Hγ1".
    { rewrite /auth_inv.
      iExists (GSet ).
92
      by iFrame. }
Zhen Zhang's avatar
Zhen Zhang committed
93
    iLeft.
94
    by iFrame. }
95
  iVsIntro.
Zhen Zhang's avatar
Zhen Zhang committed
96
  iApply "HΦ".
Zhen Zhang's avatar
Zhen Zhang committed
97
  iExists γ1, γ2, lo, ln.
Zhen Zhang's avatar
Zhen Zhang committed
98 99 100
  iSplit; by auto.
Qed.

101
Lemma wait_loop_spec l x R (Φ : val  iProp Σ) :
Zhen Zhang's avatar
Zhen Zhang committed
102
  issued l x R  ( l, locked l R - R - Φ #())  WP wait_loop #x l {{ Φ }}.
Zhen Zhang's avatar
Zhen Zhang committed
103
Proof.
Zhen Zhang's avatar
Zhen Zhang committed
104 105 106
  iIntros "[Hl HΦ]". iDestruct "Hl" as (γ1 γ2 lo ln) "(#? & % & #? & Ht)".
  iLöb as "IH". wp_rec. subst. wp_let. wp_proj. wp_bind (! _)%E.
  iInv N as (o n) "[Hlo [Hln Ha]]" "Hclose".
107 108
  wp_load. destruct (decide (x = o)) as [->|Hneq].
  - iDestruct "Ha" as "[Hainv [[Ho HR] | Haown]]".
Zhen Zhang's avatar
Zhen Zhang committed
109
    + iVs ("Hclose" with "[Hlo Hln Hainv Ht]").
110
      { iNext. iExists o, n. iFrame. eauto. }
Zhen Zhang's avatar
Zhen Zhang committed
111
      iVsIntro. wp_let. wp_op=>[_|[]] //.
112
      wp_if. iVsIntro.
Zhen Zhang's avatar
Zhen Zhang committed
113
      iApply ("HΦ" with "[-HR] HR"). iExists γ1, γ2, lo, ln; eauto.
Zhen Zhang's avatar
Zhen Zhang committed
114
    + iExFalso. iCombine "Ht" "Haown" as "Haown".
115
      iDestruct (auth_own_valid with "Haown") as % ?%gset_disj_valid_op.
Zhen Zhang's avatar
Zhen Zhang committed
116
      set_solver.
Zhen Zhang's avatar
Zhen Zhang committed
117
  - iVs ("Hclose" with "[Hlo Hln Ha]").
118
    { iNext. iExists o, n. by iFrame. }
Zhen Zhang's avatar
Zhen Zhang committed
119
    iVsIntro. wp_let. wp_op=>?; first omega.
120
    wp_if. by iApply ("IH" with "Ht").
Zhen Zhang's avatar
Zhen Zhang committed
121 122
Qed.

123
Lemma acquire_spec l R (Φ : val  iProp Σ) :
Zhen Zhang's avatar
Zhen Zhang committed
124
  is_lock l R  ( l, locked l R - R - Φ #())  WP acquire l {{ Φ }}.
Zhen Zhang's avatar
Zhen Zhang committed
125
Proof.
Zhen Zhang's avatar
Zhen Zhang committed
126 127 128 129
  iIntros "[Hl HΦ]". iDestruct "Hl" as (γ1 γ2 lo ln) "(#? & % & #?)".
  iLöb as "IH". wp_rec. wp_bind (! _)%E. subst. wp_proj.
  iInv N as (o n) "[Hlo [Hln Ha]]" "Hclose".
  wp_load. iVs ("Hclose" with "[Hlo Hln Ha]").
130
  { iNext. iExists o, n. by iFrame. }
Zhen Zhang's avatar
Zhen Zhang committed
131
  iVsIntro. wp_let. wp_proj. wp_op.
132
  wp_bind (CAS _ _ _).
Zhen Zhang's avatar
Zhen Zhang committed
133 134 135
  iInv N as (o' n') "[Hlo' [Hln' [Hainv Haown]]]" "Hclose".
  destruct (decide (#n' = #n))%V
    as [[= ->%Nat2Z.inj] | Hneq].
136 137 138 139 140 141
  - wp_cas_suc.
    iDestruct "Hainv" as (s) "[Ho %]"; subst.
    iVs (own_update with "Ho") as "Ho".
    { eapply auth_update_no_frag, (gset_alloc_empty_local_update n).
      rewrite elem_of_seq_set; omega. }
    iDestruct "Ho" as "[Hofull Hofrag]".
Zhen Zhang's avatar
Zhen Zhang committed
142
    iVs ("Hclose" with "[Hlo' Hln' Haown Hofull]").
143 144
    { rewrite gset_disj_union; last by apply (seq_set_S_disjoint 0).
      rewrite -(seq_set_S_union_L 0).
Zhen Zhang's avatar
Zhen Zhang committed
145
      iNext. iExists o', (S n)%nat.
146 147
      rewrite Nat2Z.inj_succ -Z.add_1_r.
      iFrame. iExists (GSet (seq_set 0 (S n))). by iFrame. }
Zhen Zhang's avatar
Zhen Zhang committed
148 149
    iVsIntro. wp_if.
    iApply (wait_loop_spec (#lo, #ln)).
150 151 152
    iSplitR "HΦ"; last by done.
    rewrite /issued /auth_own; eauto 10.
  - wp_cas_fail.
Zhen Zhang's avatar
Zhen Zhang committed
153
    iVs ("Hclose" with "[Hlo' Hln' Hainv Haown]").
154 155
    { iNext. iExists o', n'. by iFrame. }
    iVsIntro. wp_if. by iApply "IH".
Zhen Zhang's avatar
Zhen Zhang committed
156 157
Qed.

158
Lemma release_spec R l (Φ : val  iProp Σ):
Zhen Zhang's avatar
Zhen Zhang committed
159
  locked l R  R  Φ #()  WP release l {{ Φ }}.
Zhen Zhang's avatar
Zhen Zhang committed
160
Proof.
Zhen Zhang's avatar
Zhen Zhang committed
161 162 163 164
  iIntros "(Hl & HR & HΦ)"; iDestruct "Hl" as (γ1 γ2 lo ln) "(#? & % & #? & Hγ)".
  iLöb as "IH". wp_rec. subst. wp_proj. wp_bind (! _)%E.
  iInv N as (o n) "[Hlo [Hln Hr]]" "Hclose".
  wp_load. iVs ("Hclose" with "[Hlo Hln Hr]").
165
  { iNext. iExists o, n. by iFrame. }
166
  iVsIntro. wp_let. wp_bind (CAS _ _ _ ).
Zhen Zhang's avatar
Zhen Zhang committed
167 168 169 170
  wp_proj. wp_op.
  iInv N as (o' n') "[Hlo' [Hln' Hr]]" "Hclose".
  destruct (decide (#o' = #o))%V
    as [[= ->%Nat2Z.inj ] | Hneq].
171 172 173 174
  - wp_cas_suc.
    iDestruct "Hr" as "[Hainv [[Ho _] | Hown]]".
    + iExFalso. iCombine "Hγ" "Ho" as "Ho".
      iDestruct (own_valid with "#Ho") as %[].
Zhen Zhang's avatar
Zhen Zhang committed
175 176
    + iVs ("Hclose" with "[Hlo' Hln' HR Hγ Hainv]").
      { iNext. iExists (o + 1)%nat, n'%nat.
177 178 179
        iFrame. rewrite Nat2Z.inj_add.
        iFrame. iLeft; by iFrame. }
      iVsIntro. by wp_if.
Zhen Zhang's avatar
Zhen Zhang committed
180
  - wp_cas_fail. iVs ("Hclose" with "[Hlo' Hln' Hr]").
181 182
    { iNext. iExists o', n'. by iFrame. }
    iVsIntro. wp_if. by iApply ("IH" with "Hγ HR").
Zhen Zhang's avatar
Zhen Zhang committed
183 184 185 186
Qed.
End proof.

Typeclasses Opaque is_lock issued locked.