counter.v 9.95 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 8 9 10
  let: "n" := !"x" in
  "x" <- #1 + "n";;
  release "l";;
  "n".
11

12
Definition counter_read : val := λ: "x" <>, !"x".
13

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

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

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

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

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

Dan Frumin's avatar
Dan Frumin committed
38
  Hint Resolve CG_increment_type : typeable.
39

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

  Lemma bin_log_counter_read_r Γ E1 E2 K x (n : nat) t τ
    (Hspec : nclose specN  E1) :
    x ↦ₛ #n -
    (x ↦ₛ #n - {E1,E2;Δ;Γ}  t log fill K #n : τ) -
    {E1,E2;Δ;Γ}  t log fill K ((counter_read $/ LitV (Loc x)) #()) : τ.
  Proof.
    iIntros "Hx Hlog".
    unfold counter_read. unlock. simpl.
    rel_rec_r.
    rel_load_r.
73
    by iApply "Hlog".
74 75
  Qed.
 
76 77
  Lemma counter_read_type Γ :
    typed Γ counter_read (TArrow (Tref TNat) (TArrow TUnit TNat)).
Dan Frumin's avatar
Dan Frumin committed
78
  Proof. solve_typed. Qed.
79

Dan Frumin's avatar
Dan Frumin committed
80 81
  Hint Resolve counter_read_type : typeable.

82
  Lemma CG_counter_type Γ :
83
    typed Γ CG_counter (TArrow TUnit (TProd (TArrow TUnit TNat) (TArrow TUnit TNat))).
Dan Frumin's avatar
Dan Frumin committed
84
  Proof. solve_typed. Qed.
85

Dan Frumin's avatar
Dan Frumin committed
86 87
  Hint Resolve CG_counter_type : typeable.

88
  (* Fine-grained increment *)
89
  Lemma FG_increment_type Γ :
90
    typed Γ FG_increment (TArrow (Tref TNat) (TArrow TUnit TNat)).
Dan Frumin's avatar
Dan Frumin committed
91
  Proof. solve_typed. Qed.
92

Dan Frumin's avatar
Dan Frumin committed
93 94
  Hint Resolve FG_increment_type : typeable.

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

112
  Lemma FG_counter_type Γ :
113
    typed Γ FG_counter (TArrow TUnit (TProd (TArrow TUnit TNat) (TArrow TUnit TNat))).
Dan Frumin's avatar
Dan Frumin committed
114
  Proof. solve_typed. Qed.
115

Dan Frumin's avatar
Dan Frumin committed
116
  Hint Resolve FG_counter_type : typeable.
117

118 119
  Definition counterN : namespace := nroot .@ "counter".

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

123 124 125
  (* 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 *)
126 127
  Lemma bin_log_FG_increment_logatomic R P Γ E1 E2 K x t τ  :
    P -
Robbert Krebbers's avatar
Robbert Krebbers committed
128 129
     (|={E1,E2}=>  n : nat, x ↦ᵢ #n  R n 
       (( n : nat, x ↦ᵢ #n  R n) ={E2,E1}= True) 
130
        ( m, x ↦ᵢ # (S m)  R m - P -
131
            {E2,E1;Δ;Γ}  fill K #m log t : τ))
132
    - ({E1;Δ;Γ}  fill K ((FG_increment $/ LitV (Loc x)) #()) log t : τ).
133
  Proof.
134
    iIntros "HP #H".
135
    iLöb as "IH".
136
    rewrite {2}/FG_increment. unlock. simpl.
137 138
    rel_rec_l.
    iPoseProof "H" as "H2". (* lolwhat *)
Dan Frumin's avatar
Dan Frumin committed
139
    rel_load_l_atomic.
140
    iMod "H" as (n) "[Hx [HR Hrev]]".  iModIntro.
Robbert Krebbers's avatar
Robbert Krebbers committed
141
    iExists #n. iFrame. iNext. iIntros "Hx".
142
    iDestruct "Hrev" as "[Hrev _]".
143 144
    iMod ("Hrev" with "[HR Hx]") as "_".
    { iExists _. iFrame. } simpl.
145
    rel_rec_l.
146
    rel_op_l.
Dan Frumin's avatar
Dan Frumin committed
147
    rel_cas_l_atomic.
148
    iMod "H2" as (n') "[Hx [HR HQ]]". iModIntro. simpl.
149
    destruct (decide (n = n')); subst.
Robbert Krebbers's avatar
Robbert Krebbers committed
150
    - iExists #n'. iFrame.
151
      iSplitR; eauto. { iDestruct 1 as %Hfoo. exfalso. done. }
Dan Frumin's avatar
Dan Frumin committed
152
      iIntros "_ !> Hx". simpl.
153
      iDestruct "HQ" as "[_ HQ]".
154
      iSpecialize ("HQ" $! n' with "[Hx HR]"). { iFrame. }
155
      rel_if_true_l. by iApply "HQ".
Robbert Krebbers's avatar
Robbert Krebbers committed
156
    - iExists #n'. iFrame. 
157 158
      iSplitL; eauto; last first.
      { iDestruct 1 as %Hfoo. exfalso. simplify_eq. }
Dan Frumin's avatar
Dan Frumin committed
159
      iIntros "_ !> Hx". simpl.
Dan Frumin's avatar
Dan Frumin committed
160
      rel_if_false_l.
161
      iDestruct "HQ" as "[HQ _]".
162
      iMod ("HQ" with "[Hx HR]").
Dan Frumin's avatar
Dan Frumin committed
163
      { iExists _; iFrame. }
164
      rewrite /FG_increment. unlock. simpl.
165
      by iApply "IH".
Dan Frumin's avatar
Dan Frumin committed
166
  Qed.
167

168
  (* A similar atomic specification for the counter_read fn *)
169 170
  Lemma bin_log_counter_read_atomic_l R P Γ E1 E2 K x t τ :
    P -
Robbert Krebbers's avatar
Robbert Krebbers committed
171 172
     (|={E1,E2}=>  n : nat, x ↦ᵢ #n  R n 
       (( n : nat, x ↦ᵢ #n  R n) ={E2,E1}= True) 
173
        ( m : nat, x ↦ᵢ #m  R m - P -
Robbert Krebbers's avatar
Robbert Krebbers committed
174
            {E2,E1;Δ;Γ}  fill K #m log t : τ))
175
    - {E1;Δ;Γ}  fill K ((counter_read $/ LitV (Loc x)) #()) log t : τ.
176
  Proof.
177
    iIntros "HP #H".
178
    unfold counter_read. unlock. simpl.
179
    rel_rec_l.
Dan Frumin's avatar
Dan Frumin committed
180
    rel_load_l_atomic.
181
    iMod "H" as (n) "[Hx [HR Hfin]]". iModIntro.
Dan Frumin's avatar
Dan Frumin committed
182
    iExists _; iFrame "Hx". iNext.
183
    iIntros "Hx".
184
    iDestruct "Hfin" as "[_ Hfin]".
185
    iApply ("Hfin" with "[Hx HR] HP"). by iFrame.
186 187
  Qed.

188 189
  Lemma FG_CG_increment_refinement l cnt cnt' Γ :
    inv counterN (counter_inv l cnt cnt') -
190
    {Δ;Γ}  FG_increment #cnt log CG_increment #cnt' #l : TArrow TUnit TNat.
191 192
  Proof.
    iIntros "#Hinv".
193 194 195 196 197 198
    rel_rec_l.
    unlock CG_increment.
    do 2 rel_rec_r.
    replace (λ: <>, acquire #l;; let: "n" := ! #cnt' in #cnt' <- #1 + "n";; release #l;; "n")%E
        with (CG_increment $/ LitV (Loc cnt') $/ LitV (Loc l))%E; last first.
    { unlock CG_increment. by simpl_subst/=. }
199
    iApply bin_log_related_arrow_val.
200 201 202 203
    { 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. }
204

205 206 207 208 209 210 211 212
    iAlways. iIntros (v v') "[% %]"; simplify_eq/=.
    rel_apply_l
      (bin_log_FG_increment_logatomic
              (fun n => (l ↦ₛ #false)  cnt' ↦ₛ #n)%I
              True%I); first done.
    iAlways. iInv counterN as ">Hcnt" "Hcl". iModIntro.
    iDestruct "Hcnt" as (n) "(Hl & Hcnt & Hcnt')".
    iExists _; iFrame. clear n.
213
    iSplit.
214 215 216 217 218 219
    - iDestruct 1 as (n) "(Hcnt & Hl & Hcnt')".
      iApply ("Hcl" with "[-]").
      iNext. iExists _. iFrame.
    - iIntros (m) "(Hcnt & Hl & Hcnt') _".
      rel_apply_r (bin_log_related_CG_increment_r with "Hcnt' Hl").
      { solve_ndisj. }
220
      iIntros "Hcnt' Hl".
221
      iMod ("Hcl" with "[-]").
222 223
      { iNext. iExists _. iFrame. }      
      by iApply bin_log_related_nat.
224
  Qed.
225

226 227
  Lemma counter_read_refinement l cnt cnt' Γ :
    inv counterN (counter_inv l cnt cnt') -
228 229
    {Δ;Γ}  counter_read #cnt log counter_read #cnt' : TArrow TUnit TNat.
  Proof.    
230
    iIntros "#Hinv".
231
    rel_rec_l. rel_rec_r.
232
    iApply bin_log_related_arrow_val.
233 234 235 236
    { 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. }
237

238
    iAlways. iIntros (v v') "[% %]"; simpl in *; subst.
239 240 241 242
    rel_apply_l
      (bin_log_counter_read_atomic_l
         (fun n => (l ↦ₛ #false)  cnt' ↦ₛ #n)%I
         True%I); first done.
243
    iAlways. iInv counterN as (n) "[>Hl [>Hcnt >Hcnt']]" "Hclose". 
244
    iModIntro. 
245 246 247 248
    iExists n. iFrame "Hcnt Hcnt' Hl". clear n.
    iSplit.
    - iDestruct 1 as (n) "(Hcnt & Hl & Hcnt')". iApply "Hclose".
      iNext. iExists n. by iFrame.
249 250
    - iIntros (m) "(Hcnt & Hl & Hcnt') _ /=".
      rel_apply_r (bin_log_counter_read_r with "Hcnt'").
251 252 253 254
      { solve_ndisj. }
      iIntros "Hcnt'".
      iMod ("Hclose" with "[Hl Hcnt Hcnt']"); simpl.
      { iNext. iExists _. by iFrame. }
255
      by iApply bin_log_related_nat.
256
  Qed.
257

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

272
    rel_rec_l.
273
    rel_rec_r.
274 275 276 277 278 279 280

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

281 282 283
    iApply bin_log_related_pair.
    - iApply (FG_CG_increment_refinement with "Hinv").
    - iApply (counter_read_refinement with "Hinv").
284
  Qed.
285 286
End CG_Counter.

287
Theorem counter_ctx_refinement :
288
    FG_counter ctx CG_counter :
289
         TArrow TUnit (TProd (TArrow TUnit TNat) (TArrow TUnit TNat)).
290
Proof.
291 292
  eapply (logrel_ctxequiv logrelΣ); [solve_closed.. | intros ].
  apply FG_CG_counter_refinement.
293
Qed.