counter.v 11.4 KB
Newer Older
1
From iris.proofmode Require Import tactics.
Robbert Krebbers's avatar
Robbert Krebbers committed
2
From iris.algebra Require Import auth.
3
From iris.base_logic Require Import lib.auth.
4
From iris_logrel.F_mu_ref_conc Require Export examples.lock.
5
From iris_logrel.F_mu_ref_conc Require Import tactics rel_tactics soundness_binary relational_properties.
6
From iris.program_logic Require Import adequacy.
7

8
9
From iris_logrel.F_mu_ref_conc Require Import hax.

10
Definition CG_increment : val := λ: "x" "l" <>,
11
  acquire "l";;
12
  "x" <- BinOp Add (#n 1) (! "x");;
13
  release "l".
14

15
Definition counter_read : val := λ: "x" <>, !"x".
16

17
18
19
20
Definition CG_counter : expr :=
  let: "l" := newlock in
  let: "x" := ref (#n 0) in
  (CG_increment "x" "l", counter_read "x").
21

22
Definition FG_increment : val := λ: "v", rec: "inc" <> :=
23
24
  Let "c" (!"v") (If (CAS "v" "c" (BinOp Add (#n 1) "c"))
                     (Unit)
25
                     ("inc" #())).
26
27

Definition FG_counter : expr := 
28
29
  let: "x" := Alloc (#n 0) in
  (FG_increment "x", counter_read "x").
Robbert Krebbers's avatar
Robbert Krebbers committed
30

31
Section CG_Counter.
Robbert Krebbers's avatar
Robbert Krebbers committed
32
  Context `{heapIG Σ, cfgSG Σ}.
Dan Frumin's avatar
Dan Frumin committed
33
  
34
  (* Coarse-grained increment *)  
35
  Lemma CG_increment_type Γ :
36
37
    typed Γ CG_increment (TArrow (Tref TNat) (TArrow LockType (TArrow TUnit TUnit))).
  Proof.
38
    unfold CG_increment. unlock.
39
    eauto 25 with typeable.
40
41
  Qed.

Dan Frumin's avatar
Dan Frumin committed
42
  Hint Resolve CG_increment_type : typeable.
43

44
  Lemma bin_log_related_CG_increment_r Γ K E1 E2 t τ x n l :
45
46
47
    nclose specN  E1 
    (x ↦ₛ (#nv n) - l ↦ₛ (#v false) -
    (x ↦ₛ (#nv S n) - l ↦ₛ (#v false) -
48
      ({E1,E2;Γ}  t log fill K (Lit Unit) : τ)) -
49
    {E1,E2;Γ}  t log fill K ((CG_increment $/ LocV x $/ LocV l) Unit)%E : τ)%I.
50
  Proof.
51
    iIntros (?) "Hx Hl Hlog".
52
    unfold CG_increment. unlock. simpl_subst/=.
53
    rel_rec_r.
54
55
    rel_bind_r (acquire #l).
    iApply (bin_log_related_acquire_r with "Hl"); eauto. iIntros "Hl". simpl.
56
    rel_rec_r.
57
58
59
    rel_load_r.
    rel_op_r.
    rel_store_r. simpl.
60
    rel_rec_r.
61
62
    iApply (bin_log_related_release_r with "Hl"); eauto.
    by iApply "Hlog".
63
64
  Qed.
 
65
66
  Lemma counter_read_type Γ :
    typed Γ counter_read (TArrow (Tref TNat) (TArrow TUnit TNat)).
67
  Proof.
68
    unfold counter_read. unlock.
Dan Frumin's avatar
Dan Frumin committed
69
    eauto 10 with typeable.
70
71
  Qed.

Dan Frumin's avatar
Dan Frumin committed
72
73
  Hint Resolve counter_read_type : typeable.

74
75
76
  Lemma CG_counter_type Γ :
    typed Γ CG_counter (TProd (TArrow TUnit TUnit) (TArrow TUnit TNat)).
  Proof.
Dan Frumin's avatar
Dan Frumin committed
77
78
    unfold CG_counter.
    eauto 15 with typeable.
79
80
  Qed.

Dan Frumin's avatar
Dan Frumin committed
81
82
  Hint Resolve CG_counter_type : typeable.

83
  (* Fine-grained increment *)
84
85
  Lemma FG_increment_type Γ :
    typed Γ FG_increment (TArrow (Tref TNat) (TArrow TUnit TUnit)).
86
  Proof.
87
    unfold FG_increment. unlock.
Dan Frumin's avatar
Dan Frumin committed
88
    eauto 20 with typeable.
89
90
  Qed.

Dan Frumin's avatar
Dan Frumin committed
91
92
  Hint Resolve FG_increment_type : typeable.

93
94
  Lemma bin_log_FG_increment_l Γ K E x n t τ :
    x ↦ᵢ (#nv n) -
95
96
    (x ↦ᵢ (#nv (S n)) - {E,E;Γ}  fill K (Lit Unit) log t : τ) -
    {E,E;Γ}  fill K (FG_increment (Loc x) Unit) log t : τ.
97
98
  Proof.
    iIntros "Hx Hlog".
Dan Frumin's avatar
Dan Frumin committed
99
    iApply bin_log_related_wp_l.
100
101
102
103
104
105
106
107
    wp_bind (FG_increment #x).
    unfold FG_increment. unlock.
    iApply wp_rec; eauto. 
    solve_closed. (* TODO: why is it not being solved automatically? *)
    iNext. simpl.
    iApply wp_value; eauto. simpl. by rewrite decide_left.
    iApply wp_rec; eauto. solve_closed. (* TODO: same comment here *)
    iNext. simpl.
108
109
    wp_bind (Load (Loc x)).
    iApply (wp_load with "[Hx]"); auto. iNext.
110
111
112
    iIntros "Hx".
    iApply wp_rec; eauto. solve_closed. (* TODO: same comment here *)
    iNext. simpl.
113
114
115
116
117
118
119
    wp_bind (BinOp _ _ _).
    iApply (wp_nat_binop). iNext. iModIntro. simpl.    
    wp_bind (CAS _ _ _).    
    iApply (wp_cas_suc with "[Hx]"); auto.
    iNext. iIntros "Hx".
    iApply wp_if_true. iNext.
    iApply wp_value; auto.
120
    by iApply "Hlog".
121
122
  Qed.

123
124
125
  Lemma FG_counter_type Γ :
    typed Γ FG_counter (TProd (TArrow TUnit TUnit) (TArrow TUnit TNat)).
  Proof.
Dan Frumin's avatar
Dan Frumin committed
126
127
    unfold FG_counter.
    eauto 15 with typeable.
128
129
  Qed.

Dan Frumin's avatar
Dan Frumin committed
130
  Hint Resolve FG_counter_type : typeable.
131

132
133
  Definition counterN : namespace := nroot .@ "counter".

134
135
136
  Definition counter_inv l cnt cnt' : iProp Σ :=
    ( n, l ↦ₛ (#v false)  cnt ↦ᵢ (#nv n)  cnt' ↦ₛ (#nv n))%I.

137
138
139
140
141
142
143
144
145

  Lemma bin_log_counter_read_r Γ E1 E2 K x n t τ
    (Hspec : nclose specN  E1) :
    x ↦ₛ (#nv n)
    - (x ↦ₛ (#nv n)
         - {E1,E2;Γ}  t log fill K (#n n)%E : τ)%I
    - {E1,E2;Γ}  t log fill K (lamsubst counter_read (LocV x) #())%E : τ.
  Proof.
    iIntros "Hx Hlog".
146
    unfold counter_read. unlock. simpl.
147
148
149
    rel_rec_r.
    rel_load_r.
    by iApply "Hlog".
150
151
  Qed.

152
153
154
155
156
157
158
  (* A logically atomic specification for
     a fine-grained increment with a baked in frame. *)
  (* Unfortunately, the precondition is not baked in the rule so you can only use it when your spatial context is empty *)
  Lemma bin_log_FG_increment_logatomic R Γ E1 E2 K x t τ  :
     (|={E1,E2}=>  n, x ↦ᵢ (#nv n)  R(n) 
       (( n, x ↦ᵢ (#nv n)  R(n)) ={E2,E1}= True) 
        ( m, x ↦ᵢ (#nv (S m))  R(m) - 
159
            {E2,E1;Γ}  fill K (Lit Unit) log t : τ))
160
    - ({E1,E1;Γ}  fill K ((FG_increment $/ LocV x) Unit)%E log t : τ).
161
  Proof.
162
    iIntros "#H".
163
    unfold FG_increment. unlock. simpl.
164
165
166
    iLöb as "IH".
    rel_rec_l.
    iPoseProof "H" as "H2". (* lolwhat *)
167
    rel_bind_l (Load #x).
168
169
    iApply (bin_log_related_load_l).
    iMod "H" as (n) "[Hx [HR Hrev]]".  iModIntro.
Dan Frumin's avatar
Dan Frumin committed
170
    iExists (#nv n). iFrame. iNext. iIntros "Hx".
171
    iDestruct "Hrev" as "[Hrev _]".
172
173
    iApply fupd_logrel.
    iMod ("Hrev" with "[HR Hx]").
174
    { iExists _. iFrame. } iModIntro. simpl.
175
176
    rel_rec_l.
    rel_op_l. simpl.
177
    rel_bind_l (CAS _ _ _).
178
    iApply (bin_log_related_cas_l); auto.
179
    iMod "H2" as (n') "[Hx [HR HQ]]". iModIntro. simpl.
180
    destruct (decide (n = n')); subst.
181
    - iExists (#nv n'). iFrame.
182
      iSplitR; eauto. { iDestruct 1 as %Hfoo. exfalso. done. }
Dan Frumin's avatar
Dan Frumin committed
183
      iIntros "_ !> Hx". simpl.
184
      iDestruct "HQ" as "[_ HQ]".
185
186
187
188
189
      iSpecialize ("HQ" $! n' with "[Hx HR]"). { iFrame. }
      iApply (bin_log_related_if_true_masked_l _ _ _ K); auto.   
    - iExists (#nv n'). iFrame. 
      iSplitL; eauto; last first.
      { iDestruct 1 as %Hfoo. exfalso. simplify_eq. }
Dan Frumin's avatar
Dan Frumin committed
190
      iIntros "_ !> Hx". simpl.
191
192
      iApply (bin_log_related_if_false_masked_l _ _ _ K); auto.
      iDestruct "HQ" as "[HQ _]".
193
      iMod ("HQ" with "[Hx HR]").
Dan Frumin's avatar
Dan Frumin committed
194
      { iExists _; iFrame. }
195
      iApply "IH".
Dan Frumin's avatar
Dan Frumin committed
196
  Qed.
197

198
199
200
201
202
203
  (* A similar atomic specification for the counter_read fn *)
  Lemma bin_log_counter_read_atomic_l R Γ E1 E2 K x t τ :
     (|={E1,E2}=>  n, x ↦ᵢ (#nv n)  R(n) 
       (( n, x ↦ᵢ (#nv n)  R(n)) ={E2,E1}= True) 
        ( m, x ↦ᵢ (#nv m)  R(m) -
            {E2,E1;Γ}  fill K (#n m) log t : τ))
204
    - {E1,E1;Γ}  fill K ((counter_read $/ LocV x) #())%E log t : τ.
205
206
  Proof.
    iIntros "#H".
207
    unfold counter_read. unlock. simpl.
208
    rel_rec_l.
209
210
    iApply (bin_log_related_load_l).
    iMod "H" as (n) "[Hx [HR Hfin]]". iModIntro.
Dan Frumin's avatar
Dan Frumin committed
211
    iExists _; iFrame "Hx". iNext.
212
    iIntros "Hx".
213
    iDestruct "Hfin" as "[_ Hfin]".
214
215
216
    iApply "Hfin". by iFrame.
  Qed.

217
  (* TODO: try to use with_lock rules *)
218
219
  Lemma FG_CG_increment_refinement l cnt cnt' Γ :
    inv counterN (counter_inv l cnt cnt') -
220
    Γ  FG_increment $/ LocV cnt log CG_increment $/ LocV cnt' $/ LocV l : TArrow TUnit TUnit.
221
222
  Proof.
    iIntros "#Hinv".
223
    iApply bin_log_related_arrow.
224
225
226
227
    { unfold FG_increment. unlock; simpl_subst. reflexivity. }
    { unfold CG_increment. unlock; simpl_subst. reflexivity. }
    { unfold FG_increment. unlock; simpl_subst/=. solve_closed. (* TODO: add a clause to the reflection mechanism that reifies a [lambdasubst] expression as a closed one *) }
    { unfold CG_increment. unlock; simpl_subst/=. solve_closed. }
228

229
    iAlways. iIntros (Δ [v v']) "[% %]"; simpl in *; subst. clear Δ.
230
231
    iApply (bin_log_FG_increment_logatomic (fun n => (l ↦ₛ (#v false))  cnt' ↦ₛ #nv n)%I _ _ _ [] cnt with "[Hinv]").
    iAlways.
232
    iInv counterN as ">Hcnt" "Hcl". iModIntro.
233
234
235
236
    iDestruct "Hcnt" as (n) "[Hl [Hcnt Hcnt']]".
    iExists n. iFrame. clear n.
    iSplit.
    - iDestruct 1 as (n) "[Hcnt [Hl Hcnt']]".
237
      iMod ("Hcl" with "[-]").
238
239
240
      { iNext. iExists _. iFrame. }
      done.
    - iIntros (m) "[Hcnt [Hl Hcnt']]".
241
      iApply (bin_log_related_CG_increment_r _ [] with "[Hcnt'] [Hl]"); auto. { solve_ndisj.  }
242
      iIntros "Hcnt' Hl".
243
      iMod ("Hcl" with "[-]").
244
245
      { iNext. iExists _. iFrame. }
      simpl.
246
      by rel_vals.
247
  Qed.
248

249
250
  Lemma counter_read_refinement l cnt cnt' Γ :
    inv counterN (counter_inv l cnt cnt') -
251
    Γ  counter_read $/ #cnt log counter_read $/ #cnt' : TArrow TUnit TNat.
252
253
  Proof.
    iIntros "#Hinv".
254
255
256
257
258
259
    iApply bin_log_related_arrow.
    { unfold counter_read. unlock. simpl. reflexivity. }
    { unfold counter_read. unlock. simpl. reflexivity. }
    { unfold counter_read. unlock. simpl. solve_closed. }
    { unfold counter_read. unlock. simpl. solve_closed. }
    iAlways. iIntros (Δ [v v']) "[% %]"; simpl in *; subst. clear Δ.
260
261
    iApply (bin_log_counter_read_atomic_l (fun n => (l ↦ₛ (#v false))  cnt' ↦ₛ #nv n)%I _ _ _ [] cnt with "[Hinv]").
    iAlways. iInv counterN as (n) "[>Hl [>Hcnt >Hcnt']]" "Hclose". 
262
    iModIntro. 
263
264
265
266
267
268
269
270
271
272
    iExists n. iFrame "Hcnt Hcnt' Hl". clear n.
    iSplit.
    - iDestruct 1 as (n) "(Hcnt & Hl & Hcnt')". iApply "Hclose".
      iNext. iExists n. by iFrame.
    - iIntros (m) "(Hcnt & Hl & Hcnt') /=".
      iApply (bin_log_counter_read_r _ _ _ [] with "Hcnt'").
      { solve_ndisj. }
      iIntros "Hcnt'".
      iMod ("Hclose" with "[Hl Hcnt Hcnt']"); simpl.
      { iNext. iExists _. by iFrame. }
273
      iApply bin_log_related_val; intros; simpl; eauto.
274
  Qed.
275

276
  Lemma FG_CG_counter_refinement :
277
      FG_counter log CG_counter : TProd (TArrow TUnit TUnit) (TArrow TUnit TNat).
278
  Proof.
279
280
281
282
    unfold FG_counter, CG_counter.
    rel_bind_r newlock.
    iApply (bin_log_related_newlock_r); auto; simpl.
    iIntros (l) "Hl".
283
284
    rel_rec_r.
    rel_alloc_r as cnt' "Hcnt'".
285
286
    rel_bind_l (Alloc _).
    iApply (bin_log_related_alloc_l); auto; simpl. iModIntro.
287
    iIntros (cnt) "Hcnt".
288

289
    rel_rec_l.
290
    rel_rec_r.
291
292
293
294
295
296
297

    (* establishing the invariant *)
    iAssert (counter_inv l cnt cnt')
      with "[Hl Hcnt Hcnt']" as "Hinv".
    { iExists _. by iFrame. }
    iMod (inv_alloc counterN with "[Hinv]") as "#Hinv"; trivial.

298
    iApply (bin_log_related_pair _ with "[]").
299
300
    - rel_rec_l.
      rel_rec_r.
301
      unfold CG_increment. unlock; simpl_subst/=.
302
      rel_rec_r.
303
      replace (λ: <>, acquire #l ;; #cnt' <- BinOp Add (Nat 1) (! #cnt');; release #l)%E
304
305
        with (CG_increment $/ LocV cnt' $/ LocV l)%E; last first.
      { unfold CG_increment. unlock; simpl_subst/=. reflexivity. }
306
307
308
309
      iApply (FG_CG_increment_refinement with "Hinv").
    - rel_rec_l.
      rel_rec_r.
      iApply (counter_read_refinement with "Hinv").
310
  Qed.
311

312
313
End CG_Counter.

314
Theorem counter_ctx_refinement :
315
    FG_counter ctx CG_counter :
Robbert Krebbers's avatar
Robbert Krebbers committed
316
         TProd (TArrow TUnit TUnit) (TArrow TUnit TNat).
317
Proof.
318
319
  set (Σ := #[invΣ ; gen_heapΣ loc val ; authΣ cfgUR ]).
  set (HG := HeapPreIG Σ _ _).
Dan Frumin's avatar
Dan Frumin committed
320
  eapply (logrel_ctxequiv Σ _).
321
322
323
324
  (* TODO: how to get rid of this bullshit with closed conditions? *)
  rewrite /FG_counter /CG_counter; try solve_closed.
  rewrite /FG_counter /CG_counter; try solve_closed.
  Transparent newlock. unfold newlock. solve_closed.
Dan Frumin's avatar
Dan Frumin committed
325
  intros. apply FG_CG_counter_refinement.
326
Qed.