counter.v 9.17 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

Dan Frumin committed
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

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

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

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

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

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

Dan Frumin committed
38
  Hint Resolve CG_increment_type : typeable.
39

40 41
  Lemma bin_log_related_CG_increment_r Γ K E t τ (x l : loc) (n : nat) :
    nclose specN  E 
42 43
    (x ↦ₛ # n - l ↦ₛ #false -
    (x ↦ₛ # (S n) - l ↦ₛ #false -
44
      ({E;Δ;Γ}  t log fill K #n : τ)) -
45
    {E;Δ;Γ}  t log fill K (CG_increment #x #l) : τ)%I.
46
  Proof.
47
    iIntros (?) "Hx Hl Hlog".
48
    unfold CG_increment. unlock. simpl_subst/=.
Dan Frumin committed
49
    repeat rel_rec_r.
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.
56
    rel_store_r.
57
    rel_rec_r.
Dan Frumin committed
58
    rel_apply_r (bin_log_related_release_r with "Hl"); eauto.
59 60 61 62
    iIntros "Hl". rel_seq_r.
    by iApply ("Hlog" with "Hx Hl").
  Qed.

63 64
  Lemma bin_log_counter_read_r Γ E K x (n : nat) t τ
    (Hspec : nclose specN  E) :
65
    x ↦ₛ #n -
66 67
    (x ↦ₛ #n - {E;Δ;Γ}  t log fill K #n : τ) -
    {E;Δ;Γ}  t log fill K ((counter_read $/ LitV (Loc x)) #()) : τ.
68 69 70 71 72
  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)).
78
  Proof. solve_typed. Qed.
79

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))).
84
  Proof. solve_typed. Qed.
85

Dan Frumin committed
86 87
  Hint Resolve CG_counter_type : typeable.

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

Dan Frumin committed
93 94
  Hint Resolve FG_increment_type : typeable.

95 96
  Lemma bin_log_related_FG_increment_r Γ K E t τ (x : loc) (n : nat) :
    nclose specN  E 
97 98
    (x ↦ₛ # n -
    (x ↦ₛ #(S n) -
99
      {E;Δ;Γ}  t log fill K #n : τ) -
100
    {E;Δ;Γ}  t log fill K (FG_increment #x) : τ)%I.
101 102
  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))).
114
  Proof. solve_typed. Qed.
115

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 Σ :=
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
  Lemma bin_log_FG_increment_logatomic R P Γ E K x t τ  :
127
    P -
128 129
     (|={,E}=>  n : nat, x ↦ᵢ #n  R n 
       (( n : nat, x ↦ᵢ #n  R n) ={E,}= True) 
130
        ( m, x ↦ᵢ # (S m)  R m - P -
131
            {E;Δ;Γ}  fill K #m log t : τ))
132
    - ({Δ;Γ}  fill K (FG_increment #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 committed
139
    rel_load_l_atomic.
140
    iMod "H" as (n) "[Hx [HR Hrev]]".  iModIntro.
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 committed
147
    rel_cas_l_atomic.
148
    iMod "H2" as (n') "[Hx [HR HQ]]". iModIntro. simpl.
149
    destruct (decide (n = n')); subst.
150
    - iExists #n'. iFrame.
151
      iSplitR; eauto. { iDestruct 1 as %Hfoo. exfalso. done. }
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".
156
    - iExists #n'. iFrame. 
157 158
      iSplitL; eauto; last first.
      { iDestruct 1 as %Hfoo. exfalso. simplify_eq. }
Dan Frumin committed
159
      iIntros "_ !> Hx". simpl.
Dan Frumin committed
160
      rel_if_false_l.
161
      iDestruct "HQ" as "[HQ _]".
162
      iMod ("HQ" with "[Hx HR]").
Dan Frumin committed
163
      { iExists _; iFrame. }
164
      rewrite /FG_increment. unlock. simpl.
165
      by iApply "IH".
Dan Frumin committed
166
  Qed.
167

168
  (* A similar atomic specification for the counter_read fn *)
169
  Lemma bin_log_counter_read_atomic_l R P Γ E K x t τ :
170
    P -
171 172
     (|={,E}=>  n : nat, x ↦ᵢ #n  R n 
       (( n : nat, x ↦ᵢ #n  R n) ={E,}= True) 
173
        ( m : nat, x ↦ᵢ #m  R m - P -
174 175
            {E;Δ;Γ}  fill K #m log t : τ))
    - {Δ;Γ}  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 committed
180
    rel_load_l_atomic.
181
    iMod "H" as (n) "[Hx [HR Hfin]]". iModIntro.
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') -
Dan Frumin committed
190
    {Δ;Γ}  FG_increment #cnt log CG_increment #cnt' #l : TNat.
191 192
  Proof.
    iIntros "#Hinv".
193 194 195 196 197 198 199
    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.
200
    iSplit.
201 202 203 204 205 206
    - 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. }
207
      iIntros "Hcnt' Hl".
208
      iMod ("Hcl" with "[-]").
209 210
      { iNext. iExists _. iFrame. }      
      by iApply bin_log_related_nat.
211
  Qed.
212

213 214
  Lemma counter_read_refinement l cnt cnt' Γ :
    inv counterN (counter_inv l cnt cnt') -
215 216
    {Δ;Γ}  counter_read #cnt log counter_read #cnt' : TArrow TUnit TNat.
  Proof.    
217
    iIntros "#Hinv".
218
    rel_rec_l. rel_rec_r.
219
    iApply bin_log_related_arrow_val.
220 221 222 223
    { 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. }
224

225
    iAlways. iIntros (v v') "[% %]"; simpl in *; subst.
226 227 228 229
    rel_apply_l
      (bin_log_counter_read_atomic_l
         (fun n => (l ↦ₛ #false)  cnt' ↦ₛ #n)%I
         True%I); first done.
230
    iAlways. iInv counterN as (n) "[>Hl [>Hcnt >Hcnt']]" "Hclose". 
231
    iModIntro. 
232 233 234 235
    iExists n. iFrame "Hcnt Hcnt' Hl". clear n.
    iSplit.
    - iDestruct 1 as (n) "(Hcnt & Hl & Hcnt')". iApply "Hclose".
      iNext. iExists n. by iFrame.
236 237
    - iIntros (m) "(Hcnt & Hl & Hcnt') _ /=".
      rel_apply_r (bin_log_counter_read_r with "Hcnt'").
238 239 240 241
      { solve_ndisj. }
      iIntros "Hcnt'".
      iMod ("Hclose" with "[Hl Hcnt Hcnt']"); simpl.
      { iNext. iExists _. by iFrame. }
242
      by iApply bin_log_related_nat.
243
  Qed.
244

245
  Lemma FG_CG_counter_refinement :
246
    {Δ;}  FG_counter log CG_counter :
247
          TArrow TUnit (TProd (TArrow TUnit TNat) (TArrow TUnit TNat)).
248
  Proof.
249
    unfold FG_counter, CG_counter.
250
    iApply bin_log_related_arrow; try by (unlock; eauto).
251
    iAlways. iIntros (? ?) "/= ?"; simplify_eq/=.
252
    unlock. rel_rec_l. rel_rec_r.
Dan Frumin committed
253
    rel_apply_r bin_log_related_newlock_r; auto.
254
    iIntros (l) "Hl".
255 256
    rel_rec_r.
    rel_alloc_r as cnt' "Hcnt'".
257
    rel_alloc_l as cnt "Hcnt". simpl.
258

259
    rel_rec_l.
260
    rel_rec_r.
261 262 263 264 265 266 267

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

268
    iApply bin_log_related_pair.
Dan Frumin committed
269 270 271
    - iApply bin_log_related_arrow; eauto.
      iAlways. iIntros (??) "_". rel_seq_l; rel_seq_r.
      iApply (FG_CG_increment_refinement with "Hinv").
272
    - iApply (counter_read_refinement with "Hinv").
273
  Qed.
274 275
End CG_Counter.

276
Theorem counter_ctx_refinement :
277
    FG_counter ctx CG_counter :
278
         TArrow TUnit (TProd (TArrow TUnit TNat) (TArrow TUnit TNat)).
279
Proof.
280 281
  eapply (logrel_ctxequiv logrelΣ); [solve_closed.. | intros ].
  apply FG_CG_counter_refinement.
282
Qed.