counter.v 10.5 KB
Newer Older
1
From iris.proofmode Require Import tactics.
2 3
From iris_logrel Require Export logrel.
From iris_logrel.examples Require Import lock.
4

5
Definition CG_increment : val := λ: "x" "l" <>,
6
  acquire "l";;
7
  "x" <- #1 + !"x";;
8
  release "l".
9

10
Definition counter_read : val := λ: "x" <>, !"x".
11

Dan Frumin's avatar
Dan Frumin committed
12
Definition CG_counter : val := λ: <>,
13 14
  let: "l" := newlock #() in
  let: "x" := ref #0 in
15
  (CG_increment "x" "l", counter_read "x").
16

17
Definition FG_increment : val := λ: "v", rec: "inc" <> :=
Dan Frumin's avatar
Dan Frumin committed
18
  let: "c" := !"v" in
19 20 21
  if: CAS "v" "c" (#1 + "c")
  then #()
  else "inc" #().
22

Dan Frumin's avatar
Dan Frumin committed
23
Definition FG_counter : val := λ: <>,
24
  let: "x" := ref #0 in
25
  (FG_increment "x", counter_read "x").
Robbert Krebbers's avatar
Robbert Krebbers committed
26

27
Section CG_Counter.
28
  Context `{logrelG Σ}.
29
  Variable (Δ : list (prodC valC valC -n> iProp Σ)).
Robbert Krebbers's avatar
Robbert Krebbers committed
30

31
  (* Coarse-grained increment *)  
32
  Lemma CG_increment_type Γ :
33
    typed Γ CG_increment (TArrow (Tref TNat) (TArrow LockType (TArrow TUnit TUnit))).
Dan Frumin's avatar
Dan Frumin committed
34
  Proof. solve_typed. Qed.
35

Dan Frumin's avatar
Dan Frumin committed
36
  Hint Resolve CG_increment_type : typeable.
37

38
  Lemma bin_log_related_CG_increment_r Γ K E1 E2 t τ (x l : loc) (n : nat) :
39
    nclose specN  E1 
Robbert Krebbers's avatar
Robbert Krebbers committed
40 41 42 43
    (x ↦ₛ # n - l ↦ₛ #false -
    (x ↦ₛ # (S n) - l ↦ₛ #false -
      ({E1,E2;Δ;Γ}  t log fill K #() : τ)) -
    {E1,E2;Δ;Γ}  t log fill K ((CG_increment $/ (LitV (Loc x)) $/ LitV (Loc l)) #()) : τ)%I.
44
  Proof.
45
    iIntros (?) "Hx Hl Hlog".
46
    unfold CG_increment. unlock. simpl_subst/=.
Dan Frumin's avatar
Dan Frumin committed
47
    rel_seq_r.
Dan Frumin's avatar
Dan Frumin committed
48 49
    rel_apply_r (bin_log_related_acquire_r with "Hl"); eauto.
    iIntros "Hl".
50
    rel_rec_r.
51 52
    rel_load_r.
    rel_op_r.
Dan Frumin's avatar
Dan Frumin committed
53
    rel_store_r.
54
    rel_rec_r.
Dan Frumin's avatar
Dan Frumin committed
55
    rel_apply_r (bin_log_related_release_r with "Hl"); eauto.
56
    by iApply "Hlog".
57 58
  Qed.
 
59 60
  Lemma counter_read_type Γ :
    typed Γ counter_read (TArrow (Tref TNat) (TArrow TUnit TNat)).
Dan Frumin's avatar
Dan Frumin committed
61
  Proof. solve_typed. Qed.
62

Dan Frumin's avatar
Dan Frumin committed
63 64
  Hint Resolve counter_read_type : typeable.

65
  Lemma CG_counter_type Γ :
Dan Frumin's avatar
Dan Frumin committed
66 67
    typed Γ CG_counter (TArrow TUnit (TProd (TArrow TUnit TUnit) (TArrow TUnit TNat))).
  Proof. solve_typed. Qed.
68

Dan Frumin's avatar
Dan Frumin committed
69 70
  Hint Resolve CG_counter_type : typeable.

71
  (* Fine-grained increment *)
72 73
  Lemma FG_increment_type Γ :
    typed Γ FG_increment (TArrow (Tref TNat) (TArrow TUnit TUnit)).
Dan Frumin's avatar
Dan Frumin committed
74
  Proof. solve_typed. Qed.
75

Dan Frumin's avatar
Dan Frumin committed
76 77
  Hint Resolve FG_increment_type : typeable.

Robbert Krebbers's avatar
Robbert Krebbers committed
78 79 80
  Lemma bin_log_FG_increment_l Γ K E x (n : nat) t τ :
    x ↦ᵢ #n -
    (x ↦ᵢ # (S n) - {E,E;Δ;Γ}  fill K #() log t : τ) -
81
    {E,E;Δ;Γ}  fill K (FG_increment #x #()) log t : τ.
82 83
  Proof.
    iIntros "Hx Hlog".
Dan Frumin's avatar
Dan Frumin committed
84
    iApply bin_log_related_wp_l.
85 86
    wp_bind (FG_increment #x).
    unfold FG_increment. unlock.
Dan Frumin's avatar
Dan Frumin committed
87 88 89 90
    wp_rec.
    wp_rec.
    wp_load.
    wp_rec.
Dan Frumin's avatar
Dan Frumin committed
91
    wp_binop.
92 93 94
    wp_bind (CAS _ _ _).    
    iApply (wp_cas_suc with "[Hx]"); auto.
    iNext. iIntros "Hx".
Dan Frumin's avatar
Dan Frumin committed
95
    wp_if.
96
    by iApply "Hlog".
97 98
  Qed.

99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115
  Lemma bin_log_FG_increment_r Γ K E1 E2 t τ (x : loc) (n : nat) :
    nclose specN  E1 
    (x ↦ₛ # n -
    (x ↦ₛ #(S n) -
      {E1,E2;Δ;Γ}  t log fill K #() : τ) -
    {E1,E2;Δ;Γ}  t log fill K ((FG_increment $/ (LitV (Loc x))) #()) : τ)%I.
  Proof.
    iIntros (?) "Hx Hlog".
    unfold FG_increment. unlock. simpl_subst/=.
    rel_seq_r.
    rel_load_r; rel_seq_r.
    rel_op_r.
    rel_cas_suc_r.
    rel_if_r.
    by iApply "Hlog".
  Qed.

116
  Lemma FG_counter_type Γ :
Dan Frumin's avatar
Dan Frumin committed
117 118
    typed Γ FG_counter (TArrow TUnit (TProd (TArrow TUnit TUnit) (TArrow TUnit TNat))).
  Proof. solve_typed. Qed.
119

Dan Frumin's avatar
Dan Frumin committed
120
  Hint Resolve FG_counter_type : typeable.
121

122 123
  Definition counterN : namespace := nroot .@ "counter".

124
  Definition counter_inv l cnt cnt' : iProp Σ :=
Robbert Krebbers's avatar
Robbert Krebbers committed
125
    ( n : nat, l ↦ₛ #false  cnt ↦ᵢ #n  cnt' ↦ₛ #n)%I.
126

Robbert Krebbers's avatar
Robbert Krebbers committed
127
  Lemma bin_log_counter_read_r Γ E1 E2 K x (n : nat) t τ
128
    (Hspec : nclose specN  E1) :
Robbert Krebbers's avatar
Robbert Krebbers committed
129 130
    x ↦ₛ #n -
    (x ↦ₛ #n - {E1,E2;Δ;Γ}  t log fill K #n : τ) -
131
    {E1,E2;Δ;Γ}  t log fill K ((counter_read $/ LitV (Loc x)) #()) : τ.
132 133
  Proof.
    iIntros "Hx Hlog".
134
    unfold counter_read. unlock. simpl.
135 136 137
    rel_rec_r.
    rel_load_r.
    by iApply "Hlog".
138 139
  Qed.

140 141 142
  (* 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 *)
143 144
  Lemma bin_log_FG_increment_logatomic R P Γ E1 E2 K x t τ  :
    P -
Robbert Krebbers's avatar
Robbert Krebbers committed
145 146
     (|={E1,E2}=>  n : nat, x ↦ᵢ #n  R n 
       (( n : nat, x ↦ᵢ #n  R n) ={E2,E1}= True) 
147
        ( m, x ↦ᵢ # (S m)  R m - P -
Robbert Krebbers's avatar
Robbert Krebbers committed
148
            {E2,E1;Δ;Γ}  fill K #() log t : τ))
149
    - ({E1,E1;Δ;Γ}  fill K ((FG_increment $/ LitV (Loc x)) #()) log t : τ).
150
  Proof.
151
    iIntros "HP #H".
152
    iLöb as "IH".
153
    rewrite {2}/FG_increment. unlock. simpl.
154 155
    rel_rec_l.
    iPoseProof "H" as "H2". (* lolwhat *)
Dan Frumin's avatar
Dan Frumin committed
156
    rel_load_l_atomic.
157
    iMod "H" as (n) "[Hx [HR Hrev]]".  iModIntro.
Robbert Krebbers's avatar
Robbert Krebbers committed
158
    iExists #n. iFrame. iNext. iIntros "Hx".
159
    iDestruct "Hrev" as "[Hrev _]".
160 161
    iApply fupd_logrel.
    iMod ("Hrev" with "[HR Hx]").
162
    { iExists _. iFrame. } iModIntro. simpl.
163
    rel_rec_l.
164
    rel_op_l.
Dan Frumin's avatar
Dan Frumin committed
165
    rel_cas_l_atomic.
166
    iMod "H2" as (n') "[Hx [HR HQ]]". iModIntro. simpl.
167
    destruct (decide (n = n')); subst.
Robbert Krebbers's avatar
Robbert Krebbers committed
168
    - iExists #n'. iFrame.
169
      iSplitR; eauto. { iDestruct 1 as %Hfoo. exfalso. done. }
Dan Frumin's avatar
Dan Frumin committed
170
      iIntros "_ !> Hx". simpl.
171
      iDestruct "HQ" as "[_ HQ]".
172
      iSpecialize ("HQ" $! n' with "[Hx HR]"). { iFrame. }
173
      rel_if_true_l. by iApply "HQ".
Robbert Krebbers's avatar
Robbert Krebbers committed
174
    - iExists #n'. iFrame. 
175 176
      iSplitL; eauto; last first.
      { iDestruct 1 as %Hfoo. exfalso. simplify_eq. }
Dan Frumin's avatar
Dan Frumin committed
177
      iIntros "_ !> Hx". simpl.
Dan Frumin's avatar
Dan Frumin committed
178
      rel_if_false_l.
179
      iDestruct "HQ" as "[HQ _]".
180
      iMod ("HQ" with "[Hx HR]").
Dan Frumin's avatar
Dan Frumin committed
181
      { iExists _; iFrame. }
182
      rewrite /FG_increment. unlock. simpl.
183
      by iApply "IH".
Dan Frumin's avatar
Dan Frumin committed
184
  Qed.
185

186 187
  (* A similar atomic specification for the counter_read fn *)
  Lemma bin_log_counter_read_atomic_l R Γ E1 E2 K x t τ :
Robbert Krebbers's avatar
Robbert Krebbers committed
188 189 190 191
     (|={E1,E2}=>  n : nat, x ↦ᵢ #n  R n 
       (( n : nat, x ↦ᵢ #n  R n) ={E2,E1}= True) 
        ( m : nat, x ↦ᵢ #m  R m -
            {E2,E1;Δ;Γ}  fill K #m log t : τ))
192
    - {E1,E1;Δ;Γ}  fill K ((counter_read $/ LitV (Loc x)) #()) log t : τ.
193 194
  Proof.
    iIntros "#H".
195
    unfold counter_read. unlock. simpl.
196
    rel_rec_l.
Dan Frumin's avatar
Dan Frumin committed
197
    rel_load_l_atomic.
198
    iMod "H" as (n) "[Hx [HR Hfin]]". iModIntro.
Dan Frumin's avatar
Dan Frumin committed
199
    iExists _; iFrame "Hx". iNext.
200
    iIntros "Hx".
201
    iDestruct "Hfin" as "[_ Hfin]".
202 203 204
    iApply "Hfin". by iFrame.
  Qed.

205
  (* TODO: try to use with_lock rules *)
206 207
  Lemma FG_CG_increment_refinement l cnt cnt' Γ :
    inv counterN (counter_inv l cnt cnt') -
208
    {,;Δ;Γ}  FG_increment $/ LitV (Loc cnt) log CG_increment $/ LitV (Loc cnt') $/ LitV (Loc l) : TArrow TUnit TUnit.
209 210
  Proof.
    iIntros "#Hinv".
211
    iApply bin_log_related_arrow_val.
212 213 214 215
    { 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. }
216

217
    iAlways. iIntros (v v') "[% %]"; simpl in *; subst.
218
    iApply (bin_log_FG_increment_logatomic (fun n => (l ↦ₛ #false)  cnt' ↦ₛ #n)%I True%I _ _ _ [] cnt with "[Hinv]"); auto.
219
    iAlways.
220
    iInv counterN as ">Hcnt" "Hcl". iModIntro.
221 222 223 224
    iDestruct "Hcnt" as (n) "[Hl [Hcnt Hcnt']]".
    iExists n. iFrame. clear n.
    iSplit.
    - iDestruct 1 as (n) "[Hcnt [Hl Hcnt']]".
225
      iMod ("Hcl" with "[-]").
226 227
      { iNext. iExists _. iFrame. }
      done.
228
    - iIntros (m) "[Hcnt [Hl Hcnt']] _".
229
      iApply (bin_log_related_CG_increment_r _ [] with "[Hcnt'] [Hl]"); auto. { solve_ndisj.  }
230
      iIntros "Hcnt' Hl".
231
      iMod ("Hcl" with "[-]").
232 233
      { iNext. iExists _. iFrame. }
      simpl.
234
      by rel_vals.
235
  Qed.
236

237 238
  Lemma counter_read_refinement l cnt cnt' Γ :
    inv counterN (counter_inv l cnt cnt') -
239
    {,;Δ;Γ}  counter_read $/ LitV (Loc cnt) log counter_read $/ LitV (Loc cnt') : TArrow TUnit TNat.
240 241
  Proof.
    iIntros "#Hinv".
242
    iApply bin_log_related_arrow_val.
243 244 245 246
    { 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. }
247
    iAlways. iIntros (v v') "[% %]"; simpl in *; subst.
Robbert Krebbers's avatar
Robbert Krebbers committed
248
    iApply (bin_log_counter_read_atomic_l (fun n => (l ↦ₛ #false)  cnt' ↦ₛ #n)%I _ _ _ [] cnt with "[Hinv]").
249
    iAlways. iInv counterN as (n) "[>Hl [>Hcnt >Hcnt']]" "Hclose". 
250
    iModIntro. 
251 252 253 254 255 256 257 258 259 260
    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. }
261
      rel_vals. simpl. eauto.
262
  Qed.
263

264
  Lemma FG_CG_counter_refinement :
265
    {,;Δ;}  FG_counter log CG_counter :
Dan Frumin's avatar
Dan Frumin committed
266
          TArrow TUnit (TProd (TArrow TUnit TUnit) (TArrow TUnit TNat)).
267
  Proof.
268
    unfold FG_counter, CG_counter.
Dan Frumin's avatar
Dan Frumin committed
269
    iApply bin_log_related_arrow; try by (unlock; eauto).
270
    iAlways. iIntros (? ?) "/= ?"; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
271
    unlock. rel_rec_l. rel_rec_r.
Dan Frumin's avatar
Dan Frumin committed
272
    rel_apply_r bin_log_related_newlock_r; auto.
273
    iIntros (l) "Hl".
274 275
    rel_rec_r.
    rel_alloc_r as cnt' "Hcnt'".
Dan Frumin's avatar
Dan Frumin committed
276
    rel_alloc_l as cnt "Hcnt". simpl.
277

278
    rel_rec_l.
279
    rel_rec_r.
280 281 282 283 284 285 286

    (* 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.

287
    iApply (bin_log_related_pair _ with "[]").
288
    - rel_rec_l.
289
      unfold CG_increment. unlock.
290 291
      rel_rec_r.
      rel_rec_r.
292 293
      replace (λ: <>, acquire # l ;; #cnt' <- #1 + (! #cnt');; release # l)%E
        with (CG_increment $/ LitV (Loc cnt') $/ LitV (Loc l))%E; last first.
294
      { unfold CG_increment. unlock; simpl_subst/=. reflexivity. }
295 296 297 298
      iApply (FG_CG_increment_refinement with "Hinv").
    - rel_rec_l.
      rel_rec_r.
      iApply (counter_read_refinement with "Hinv").
299
  Qed.
300 301
End CG_Counter.

302
Theorem counter_ctx_refinement :
303
    FG_counter ctx CG_counter :
Dan Frumin's avatar
Dan Frumin committed
304
         TArrow TUnit (TProd (TArrow TUnit TUnit) (TArrow TUnit TNat)).
305
Proof.
306 307
  eapply (logrel_ctxequiv logrelΣ); [solve_closed.. | intros ].
  apply FG_CG_counter_refinement.
308
Qed.