ticket_lock.v 6.85 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.
81
  iIntros "(#Hh & HR & HΦ)". rewrite /newlock /=.
Zhen Zhang's avatar
Zhen Zhang committed
82
  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. }
119
120
    iVsIntro. wp_let. wp_op=>[[/Nat2Z.inj //]|?].
    wp_if. iApply ("IH" with "Ht"). by iExact "HΦ".
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
  iInv N as (o' n') "[Hlo' [Hln' [Hainv Haown]]]" "Hclose".
134
  destruct (decide (#n' = #n))%V as [[= ->%Nat2Z.inj] | Hneq].
135
136
137
138
139
140
  - 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
141
    iVs ("Hclose" with "[Hlo' Hln' Haown Hofull]").
142
143
    { 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
144
      iNext. iExists o', (S n)%nat.
145
146
      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
147
148
    iVsIntro. wp_if.
    iApply (wait_loop_spec (#lo, #ln)).
149
150
151
    iSplitR "HΦ"; last by done.
    rewrite /issued /auth_own; eauto 10.
  - wp_cas_fail.
Zhen Zhang's avatar
Zhen Zhang committed
152
    iVs ("Hclose" with "[Hlo' Hln' Hainv Haown]").
153
154
    { iNext. iExists o', n'. by iFrame. }
    iVsIntro. wp_if. by iApply "IH".
Zhen Zhang's avatar
Zhen Zhang committed
155
156
Qed.

157
Lemma release_spec R l (Φ : val  iProp Σ):
Zhen Zhang's avatar
Zhen Zhang committed
158
  locked l R  R  Φ #()  WP release l {{ Φ }}.
Zhen Zhang's avatar
Zhen Zhang committed
159
Proof.
Zhen Zhang's avatar
Zhen Zhang committed
160
161
162
163
  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]").
164
  { iNext. iExists o, n. by iFrame. }
165
  iVsIntro. wp_let. wp_bind (CAS _ _ _ ).
Zhen Zhang's avatar
Zhen Zhang committed
166
167
  wp_proj. wp_op.
  iInv N as (o' n') "[Hlo' [Hln' Hr]]" "Hclose".
168
  destruct (decide (#o' = #o))%V as [[= ->%Nat2Z.inj ] | Hneq].
169
170
171
172
  - 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
173
174
    + iVs ("Hclose" with "[Hlo' Hln' HR Hγ Hainv]").
      { iNext. iExists (o + 1)%nat, n'%nat.
175
176
177
        iFrame. rewrite Nat2Z.inj_add.
        iFrame. iLeft; by iFrame. }
      iVsIntro. by wp_if.
Zhen Zhang's avatar
Zhen Zhang committed
178
  - wp_cas_fail. iVs ("Hclose" with "[Hlo' Hln' Hr]").
179
180
    { iNext. iExists o', n'. by iFrame. }
    iVsIntro. wp_if. by iApply ("IH" with "Hγ HR").
Zhen Zhang's avatar
Zhen Zhang committed
181
182
183
184
Qed.
End proof.

Typeclasses Opaque is_lock issued locked.