modular_incr.v 9.44 KB
Newer Older
1
2
3
4
5
6
7
(* Modular Specifications for Concurrent Modules. *)

From iris.program_logic Require Export hoare weakestpre.
From iris.heap_lang Require Export lang proofmode notation.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import agree frac frac_auth.

Ralf Jung's avatar
Ralf Jung committed
8
From iris.bi.lib Require Import fractional.
9
10
11

From iris.heap_lang.lib Require Import par.

Robbert Krebbers's avatar
Robbert Krebbers committed
12
Definition cntCmra : cmraT := (prodR fracR (agreeR (leibnizO Z))).
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41

Class cntG Σ := CntG { CntG_inG :> inG Σ cntCmra }.
Definition cntΣ : gFunctors := #[GFunctor cntCmra ].

Instance subG_cntΣ {Σ} : subG cntΣ Σ  cntG Σ.
Proof. solve_inG. Qed.

Definition newcounter : val :=
  λ: "m", ref "m".

Definition read : val := λ: "ℓ", !"ℓ".

Definition incr: val :=
  rec: "incr" "l" :=
     let: "oldv" := !"l" in
     if: CAS "l" "oldv" ("oldv" + #1)
       then "oldv" (* return old value if success *)
       else "incr" "l".

Definition wk_incr : val :=
    λ: "l", let: "n" := !"l" in
            "l" <- "n" + #1.

Section cnt_model.
  Context `{!cntG Σ}.

  Definition makeElem (q : Qp) (m : Z) : cntCmra := (q, to_agree m).

  Notation "γ ⤇[ q ] m" := (own γ (makeElem q m))
Ralf Jung's avatar
Ralf Jung committed
42
    (at level 20, q at level 50, format "γ ⤇[ q ]  m") : bi_scope.
43
  Notation "γ ⤇½ m" := (own γ (makeElem (1/2) m))
Ralf Jung's avatar
Ralf Jung committed
44
    (at level 20, format "γ ⤇½  m") : bi_scope.
45
46
47
48
49
50
51
52
53

  Global Instance makeElem_fractional γ m: Fractional (λ q, γ [q] m)%I.
  Proof.
    intros p q. rewrite /makeElem.
    rewrite -own_op; f_equiv.
    split; first done.
    by rewrite /= agree_idemp.
  Qed.

54
  Global Instance makeElem_as_fractional γ m q:
55
56
57
58
59
60
61
    AsFractional (own γ (makeElem q m)) (λ q, γ [q] m)%I q.
  Proof.
    split. done. apply _.
  Qed.

  Global Instance makeElem_Exclusive m: Exclusive (makeElem 1 m).
  Proof.
62
    intros [y ?] [H _]. apply (exclusive_l _ _ H).
63
64
65
66
67
  Qed.

  Lemma makeElem_op p q n:
    makeElem p n  makeElem q n  makeElem (p + q) n.
  Proof.
68
    rewrite /makeElem; split; first done.
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
    by rewrite /= agree_idemp.
  Qed.

  Lemma makeElem_eq γ p q (n m : Z):
    γ [p] n - γ [q] m - n = m.
  Proof.
    iIntros "H1 H2".
    iDestruct (own_valid_2 with "H1 H2") as %HValid.
    destruct HValid as [_ H2].
    iIntros "!%"; by apply agree_op_invL'.
  Qed.

  Lemma makeElem_entail γ p q (n m : Z):
    γ [p] n - γ [q] m - γ [p + q] n.
  Proof.
    iIntros "H1 H2".
    iDestruct (makeElem_eq with "H1 H2") as %->.
    iCombine "H1" "H2" as "H".
    by rewrite makeElem_op.
  Qed.
89

90
91
92
93
94
95
96
97
  Lemma makeElem_update γ (n m k : Z):
    γ ⤇½ n - γ ⤇½ m == γ [1] k.
  Proof.
    iIntros "H1 H2".
    iDestruct (makeElem_entail with "H1 H2") as "H".
    rewrite Qp_div_2.
    iApply (own_update with "H"); by apply cmra_update_exclusive.
  Qed.
98
End cnt_model.
99
100

Notation "γ ⤇[ q ] m" := (own γ (makeElem q m))
Ralf Jung's avatar
Ralf Jung committed
101
  (at level 20, q at level 50, format "γ ⤇[ q ]  m") : bi_scope.
102
Notation "γ ⤇½ m" := (own γ (makeElem (1/2) m))
Ralf Jung's avatar
Ralf Jung committed
103
  (at level 20, format "γ ⤇½  m") : bi_scope.
104
105
106

Section cnt_spec.
  Context `{!heapG Σ, !cntG Σ} (N : namespace).
107

108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
  Definition cnt_inv  γ := ( (m : Z),   #m  γ ⤇½ m)%I.

  Definition Cnt ( : loc) (γ : gname) : iProp Σ :=
    inv (N .@ "internal") (cnt_inv  γ).

  Lemma Cnt_alloc (E : coPset) (m : Z) ( : loc):
    (  #m) ={E}=  γ, Cnt  γ  γ ⤇½ m.
  Proof.
    iIntros "Hpt".
    iMod (own_alloc (makeElem 1 m)) as (γ) "[Hown1 Hown2]"; first done.
    iMod (inv_alloc (N.@ "internal") _ (cnt_inv  γ)%I with "[Hpt Hown1]") as "#HInc".
    { iExists _; iFrame. }
    iModIntro; iExists _; iFrame "# Hown2".
  Qed.

  Theorem newcounter_spec (E : coPset) (m : Z):
    (N .@ "internal")  E 
    {{{ True }}} newcounter #m @ E {{{ ( : loc), RET #;  γ, Cnt  γ  γ ⤇½ m}}}.
  Proof.
    iIntros (Hsubset Φ) "#Ht HΦ".
128
    rewrite -wp_fupd.
129
130
131
132
133
134
135
    wp_lam.
    wp_alloc  as "Hl".
    iApply "HΦ".
    by iApply Cnt_alloc.
  Qed.

  Theorem read_spec (γ : gname) (E : coPset) (P : iProp Σ) (Q : Z  iProp Σ) ( : loc):
136
    (N .@ "internal")  E 
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
    ( m, (γ ⤇½ m  P ={E  (N .@ "internal")}=> γ ⤇½ m  Q m)) 
    {{{ Cnt  γ  P}}} read # @ E {{{ (m : Z), RET #m; Cnt  γ  Q m }}}.
  Proof.
    iIntros (Hsubset) "#HVS".
    iIntros (Φ) "!# [#HInc HP] HCont".
    wp_rec.
    rewrite /Cnt.
    iInv (N .@ "internal") as (m) "[>Hpt >Hown]" "HClose".
    iMod ("HVS" $! m with "[Hown HP]") as "[Hown HQ]"; first by iFrame.
    wp_load.
    iMod ("HClose" with "[Hpt Hown]") as "_".
    { iNext; iExists _; iFrame. }
    iApply "HCont".
    iModIntro.
    iFrame.
    done.
153
  Qed.
154
155

  Theorem incr_spec (γ : gname) (E : coPset) (P : iProp Σ) (Q : Z  iProp Σ) ( : loc):
156
    (N .@ "internal")  E 
157
158
159
160
    ( (n : Z), γ ⤇½ n  P  ={E  (N .@ "internal")}=> γ ⤇½ (n+1)  Q n) 
    {{{ Cnt  γ  P }}} incr # @ E {{{ (m : Z), RET #m; Cnt  γ  Q m}}}.
  Proof.
    iIntros (Hsubset) "#HVS".
Ralf Jung's avatar
Ralf Jung committed
161
    iIntros (Φ) "!# [#HInc HP] HCont".
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
    iLöb as "IH".
    wp_rec.
    wp_bind (! _)%E.
    iInv (N .@ "internal") as (m) "[>Hpt >Hown]" "HClose".
    wp_load.
    iMod ("HClose" with "[Hpt Hown]") as "_".
    { iNext; iExists _; iFrame. }
    iModIntro.
    wp_let.
    wp_op.
    wp_bind (CAS _ _ _)%E.
    iInv (N .@ "internal") as (m') "[>Hpt >Hown]" "HClose".
    destruct (decide (m = m')); simplify_eq.
    - wp_cas_suc.
      iMod ("HVS" $! m' with "[Hown HP]") as "[Hown HQ]"; first iFrame.
      iMod ("HClose" with "[Hpt Hown]") as "_".
      { iNext; iExists _; iFrame. }
      iModIntro.
      wp_if.
Ralf Jung's avatar
Ralf Jung committed
181
      iApply "HCont"; by iFrame.
182
183
184
185
186
    - wp_cas_fail.
      iMod ("HClose" with "[Hpt Hown]") as "_".
      { iNext; iExists _; iFrame. }
      iModIntro.
      wp_if.
Ralf Jung's avatar
Ralf Jung committed
187
      iApply ("IH" with "HP HCont").
188
189
190
191
192
193
194
195
  Qed.

  Theorem wk_incr_spec (γ : gname) (E : coPset) (P Q : iProp Σ) ( : loc) (n : Z) (q : Qp):
    (N .@ "internal")  E 
    (γ ⤇½ n  γ [q] n  P ={E  (N .@ "internal")}=> γ ⤇½ (n+1)  Q) -
    {{{ Cnt  γ  γ [q] n  P}}} wk_incr # @ E {{{ RET #(); Cnt  γ  Q}}}.
  Proof.
    iIntros (Hsubset) "#HVS".
Ralf Jung's avatar
Ralf Jung committed
196
    iIntros (Φ) "!# [#HInc [Hγ HP]] HCont".
197
198
199
200
    wp_lam.
    wp_bind (! _)%E.
    iInv (N .@ "internal") as (m) "[>Hpt >Hown]" "HClose".
    wp_load.
201
    iDestruct (makeElem_eq with "Hγ Hown") as %->.
202
203
204
205
206
207
208
209
210
211
212
    iMod ("HClose" with "[Hpt Hown]") as "_".
    { iNext; iExists _; iFrame. }
    iModIntro.
    wp_let.
    wp_op.
    iInv (N .@ "internal") as (k) "[>Hpt >Hown]" "HClose".
    iDestruct (makeElem_eq with "Hγ Hown") as %->.
    iMod ("HVS" with "[$Hown $HP $Hγ]") as "[Hown HQ]".
    wp_store.
    iMod ("HClose" with "[Hpt Hown]") as "_".
    { iNext; iExists _; iFrame. }
213
    iModIntro.
Ralf Jung's avatar
Ralf Jung committed
214
    iApply "HCont"; by iFrame.
215
  Qed.
216

217
218
219
220
221
222
223
  Theorem wk_incr_spec' (γ : gname) (E : coPset) (P Q : iProp Σ) ( : loc) (n : Z) (q : Qp):
    (N .@ "internal")  E 
    (γ ⤇½ n  γ [q] n  P ={E  (N .@ "internal")}=> γ ⤇½ (n+1)   γ [q] (n + 1)  Q) -
    {{{ Cnt  γ  γ [q] n  P}}} wk_incr # @ E {{{ RET #(); Cnt  γ   γ [q] (n + 1)  Q}}}.
  Proof.
    iIntros (Hsubset) "#HVS".
    iApply wk_incr_spec; done.
224
Qed.
225
226
227
228
229
230
231

End cnt_spec.
Global Opaque newcounter incr read wk_incr.

Section incr_twice.
  Context `{!heapG Σ, !cntG Σ} (N : namespace).
  Definition incr_twice : val := λ: "ℓ", incr "ℓ" ;; incr "ℓ".
232

233
234
235
  Theorem incr_twice_spec (γ : gname) (E : coPset) (P : iProp Σ) (Q Q' : Z  iProp Σ) ( : loc):
    (N .@ "internal")  E 
    ( (n : Z), (γ ⤇½ n  P  ={E  (N .@ "internal")}=> γ ⤇½ (n+1)  Q n))
236
      -
237
238
239
240
241
242
      ( (n : Z), γ ⤇½ n  ( m, Q m)  ={E  (N .@ "internal")}=> γ ⤇½ (n+1)  Q' n)
      -
      {{{ Cnt N  γ  P }}} incr_twice # @ E {{{ (m : Z), RET #m; Cnt N  γ  Q' m}}}.
  Proof.
    iIntros (?) "#HVS1 #HVS2 !#".
    iIntros (Φ) "HPre HΦ".
243
    wp_lam. wp_bind (incr _)%E.
244
245
    wp_apply (incr_spec with "HVS1 HPre"); auto.
    iIntros (m) "[HCnt HPre]".
246
    wp_seq.
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
    wp_apply (incr_spec with "HVS2 [$HCnt HPre]"); auto.
  Qed.
End incr_twice.

Section example_1.
  Context `{!heapG Σ, !spawnG Σ, !cntG Σ} (N : namespace).

  Definition incr_2 : val :=
    λ: "x",
       let: "l" := newcounter "x" in
       incr "l" ||| incr "l";;
       read "l".

  (* Prove that incr is safe w.r.t. data race. TODO: prove a stronger post-condition *)
  Lemma incr_2_safe:
     (x: Z), (WP incr_2 #x {{ _, True }})%I.
  Proof.
    iIntros (x).
    rewrite /incr_2 /=.
    wp_lam.
    wp_bind (newcounter _)%E.
    wp_apply newcounter_spec; auto; iIntros () "H".
    iDestruct "H" as (γ) "[#HInc Hown2]".
    iMod (inv_alloc (N.@ "external") _ (m, own γ (makeElem (1/2) m))%I with "[Hown2]") as "#Hinv".
    { iNext; iExists _; iFrame. }
    iDestruct (incr_spec N γ  True%I (λ _, True)%I with "[]") as "#HIncr"; eauto.
    { iIntros (n) "!# [Hown _]".
      iInv (N .@ "external") as (m) ">Hownm" "H2".
      iMod (makeElem_update _ _ _ (n + 1) with "Hown Hownm") as "[Hown Hown']".
      iMod ("H2" with "[Hown]") as "_".
      { iExists _; iFrame. }
      iModIntro; iFrame.
    }
    wp_let.
    wp_bind (_ ||| _)%E.
282
    let tac := iApply ("HIncr" with "[$HInc]"); iNext; by iIntros (?) "_" in
Ralf Jung's avatar
Ralf Jung committed
283
    wp_apply (wp_par (λ _, True%I) (λ _, True%I)); [tac | tac | ].
284
    { iIntros (v1 v2) "_ !>".
285
      wp_seq.
286
287
288
289
290
      wp_apply (read_spec _ _ _ True%I (λ _, True%I)); auto.
      iIntros (n) "!# [Hown _] !>"; by iFrame.
    }
  Qed.
End example_1.