ticket_lock.v 7.51 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
From iris.heap_lang Require Import proofmode notation.
From iris.algebra Require Import gset.
7
From iris.heap_lang.lib Require Export lock.
Zhen Zhang's avatar
Zhen Zhang committed
8
9
10
Import uPred.

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

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

Definition acquire : val :=
Zhen Zhang's avatar
Zhen Zhang committed
20
21
22
23
24
  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
25
26

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

Global Opaque newlock acquire release wait_loop.

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

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

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

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

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

Zhen Zhang's avatar
Zhen Zhang committed
58
59
60
61
62
63
64
65
66
67
68
69
70
  Definition is_lock (γs: gname * gname) (l: val) (R: iProp Σ) : iProp Σ :=
    ( (lo ln: loc),
       heapN  N  heap_ctx 
       l = (#lo, #ln)%V  inv N (lock_inv (fst γs) (snd γs) lo ln R))%I.

  Definition issued (γs: gname * gname) (l : val) (x: nat) (R : iProp Σ) : iProp Σ :=
    ( (lo ln: loc),
       heapN  N  heap_ctx 
       l = (#lo, #ln)%V  inv N (lock_inv (fst γs) (snd γs) lo ln R) 
       auth_own (fst γs) (GSet {[ x ]}))%I.

  Definition locked (γs: gname * gname) : iProp Σ := own (snd γs) (Excl ())%I.

71
72
  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
73
74
75
76
77
78
79
80
81
  Proof. solve_proper. Qed.
  Global Instance is_lock_ne γs n l : Proper (dist n ==> dist n) (is_lock γs l).
  Proof. solve_proper. Qed.
  Global Instance is_lock_persistent γs l R : PersistentP (is_lock γs l R).
  Proof. apply _. Qed.
  Global Instance locked_timeless γs : TimelessP (locked γs).
  Proof. apply _. Qed.

  Lemma locked_exclusive (γs: gname * gname) : (locked γs  locked γs  False)%I.
82
  Proof. rewrite /locked -own_op own_valid. by iIntros (?). Qed.
Zhen Zhang's avatar
Zhen Zhang committed
83
84

  Lemma newlock_spec (R : iProp Σ) Φ :
85
86
    heapN  N 
    heap_ctx  R  ( lk γs, is_lock γs lk R - Φ lk)  WP newlock #() {{ Φ }}.
Zhen Zhang's avatar
Zhen Zhang committed
87
  Proof.
88
    iIntros (HN) "(#Hh & HR & HΦ)". rewrite /newlock /=.
Zhen Zhang's avatar
Zhen Zhang committed
89
90
91
92
93
94
95
96
97
98
99
100
101
    wp_seq. wp_alloc lo as "Hlo". wp_alloc ln as "Hln".
    iVs (own_alloc (Excl ())) as (γ2) "Hγ2"; first done.
    iVs (own_alloc_strong (Auth (Excl' ) ) {[ γ2 ]}) as (γ1) "[% Hγ1]"; first done.
    iVs (inv_alloc N _ (lock_inv γ1 γ2 lo ln R) with "[-HΦ]").
    - iNext. rewrite /lock_inv.
      iExists 0%nat, 0%nat.
      iFrame.
      iSplitL "Hγ1".
      + rewrite /auth_inv.
        iExists (GSet ).
        by iFrame.
      + iLeft. by iFrame.
    - iVsIntro.
102
      iApply ("HΦ" $! (#lo, #ln)%V (γ1, γ2)).
Zhen Zhang's avatar
Zhen Zhang committed
103
104
105
106
      iExists lo, ln.
      iSplit; by eauto.
  Qed.

107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
  Lemma wait_loop_spec γs l x R (Φ : val  iProp Σ) :
    issued γs l x R  (locked γs - R - Φ #())  WP wait_loop #x l {{ Φ }}.
  Proof.
    iIntros "[Hl HΦ]". iDestruct "Hl" as (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".
    wp_load. destruct (decide (x = o)) as [->|Hneq].
    - iDestruct "Ha" as "[Hainv [[Ho HR] | Haown]]".
      + iVs ("Hclose" with "[Hlo Hln Hainv Ht]").
        { iNext. iExists o, n. iFrame. eauto. }
        iVsIntro. wp_let. wp_op=>[_|[]] //.
        wp_if. iVsIntro.
        iApply ("HΦ" with "[-HR] HR"). eauto.
      + iExFalso. iCombine "Ht" "Haown" as "Haown".
        iDestruct (auth_own_valid with "Haown") as % ?%gset_disj_valid_op.
        set_solver.
    - iVs ("Hclose" with "[Hlo Hln Ha]").
      { iNext. iExists o, n. by iFrame. }
      iVsIntro. wp_let. wp_op=>[[/Nat2Z.inj //]|?].
      wp_if. iApply ("IH" with "Ht"). by iExact "HΦ".
  Qed.

  Lemma acquire_spec γs l R (Φ : val  iProp Σ) :
    is_lock γs l R  (locked γs - R - Φ #())  WP acquire l {{ Φ }}.
  Proof.
    iIntros "[Hl HΦ]". iDestruct "Hl" as (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]").
136
    { iNext. iExists o, n. by iFrame. }
137
138
139
140
141
142
143
    iVsIntro. wp_let. wp_proj. wp_op.
    wp_bind (CAS _ _ _).
    iInv N as (o' n') "[Hlo' [Hln' [Hainv Haown]]]" "Hclose".
    destruct (decide (#n' = #n))%V as [[= ->%Nat2Z.inj] | Hneq].
    - wp_cas_suc.
      iDestruct "Hainv" as (s) "[Ho %]"; subst.
      iVs (own_update with "Ho") as "Ho".
144
      { eapply auth_update_no_frag, (gset_disj_alloc_empty_local_update n).
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
        rewrite elem_of_seq_set; omega. }
      iDestruct "Ho" as "[Hofull Hofrag]".
      iVs ("Hclose" with "[Hlo' Hln' Haown Hofull]").
      { rewrite gset_disj_union; last by apply (seq_set_S_disjoint 0).
        rewrite -(seq_set_S_union_L 0).
        iNext. iExists o', (S n)%nat.
        rewrite Nat2Z.inj_succ -Z.add_1_r.
        iFrame. iExists (GSet (seq_set 0 (S n))). by iFrame. }
      iVsIntro. wp_if.
      iApply (wait_loop_spec γs (#lo, #ln)).
      iSplitR "HΦ"; last by auto.
      rewrite /issued /auth_own; eauto 10.
    - wp_cas_fail.
      iVs ("Hclose" with "[Hlo' Hln' Hainv Haown]").
      { iNext. iExists o', n'. by iFrame. }
      iVsIntro. wp_if. by iApply "IH".
  Qed.

  Lemma release_spec γs l R (Φ : val  iProp Σ):
    is_lock γs l R  locked γs  R  Φ #()  WP release l {{ Φ }}.
  Proof.
    iIntros "(Hl & Hγ & HR & HΦ)". iDestruct "Hl" as (lo ln) "(% & #? & % & #?)".
    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]").
    { iNext. iExists o, n. by iFrame. }
    iVsIntro. wp_let. wp_bind (CAS _ _ _ ).
    wp_proj. wp_op.
    iInv N as (o' n') "[Hlo' [Hln' Hr]]" "Hclose".
    destruct (decide (#o' = #o))%V as [[= ->%Nat2Z.inj ] | Hneq].
    - wp_cas_suc.
      iDestruct "Hr" as "[Hainv [[Ho _] | Hown]]".
      + iExFalso. iCombine "Hγ" "Ho" as "Ho".
        iDestruct (own_valid with "#Ho") as %[].
      + iVs ("Hclose" with "[Hlo' Hln' HR Hγ Hainv]").
        { iNext. iExists (o + 1)%nat, n'%nat.
          iFrame. rewrite Nat2Z.inj_add.
          iFrame. iLeft; by iFrame. }
        iVsIntro. by wp_if.
    - wp_cas_fail. iVs ("Hclose" with "[Hlo' Hln' Hr]").
      { iNext. iExists o', n'. by iFrame. }
      iVsIntro. wp_if. by iApply ("IH" with "Hγ HR").
  Qed.
Zhen Zhang's avatar
Zhen Zhang committed
188
189
190
End proof.

Typeclasses Opaque is_lock issued locked.
Zhen Zhang's avatar
Zhen Zhang committed
191

192
193
194
Definition ticket_lock `{!heapG Σ, !tlockG Σ} : lock Σ :=
  {| lock.locked_exclusive := locked_exclusive; lock.newlock_spec := newlock_spec;
     lock.acquire_spec := acquire_spec; lock.release_spec := release_spec |}.