counter.v 8.93 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 26 27
Definition wkincr : val := λ: "l",
  "l" <- !"l" + #1.

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

32
Section CG_Counter.
33
  Context `{logrelG Σ}.
34
  Variable (Δ : list (prodC valC valC -n> iProp Σ)).
35

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

Dan Frumin committed
41
  Hint Resolve CG_increment_type : typeable.
42

43 44
  Lemma bin_log_related_CG_increment_r Γ K E t τ (x l : loc) (n : nat) :
    nclose specN  E 
45 46
    (x ↦ₛ # n - l ↦ₛ #false -
    (x ↦ₛ # (S n) - l ↦ₛ #false -
47
      ({E;Δ;Γ}  t log fill K #n : τ)) -
48
    {E;Δ;Γ}  t log fill K (CG_increment #x #l) : τ)%I.
49
  Proof.
50
    iIntros (?) "Hx Hl Hlog".
51
    unfold CG_increment. unlock. simpl_subst/=.
Dan Frumin committed
52
    repeat rel_rec_r.
Dan Frumin committed
53 54
    rel_apply_r (bin_log_related_acquire_r with "Hl"); eauto.
    iIntros "Hl".
55
    rel_rec_r.
56
    rel_load_r.
57
    rel_let_r.
58
    rel_op_r.
59
    rel_store_r.
60
    rel_rec_r.
Dan Frumin committed
61
    rel_apply_r (bin_log_related_release_r with "Hl"); eauto.
62 63 64 65
    iIntros "Hl". rel_seq_r.
    by iApply ("Hlog" with "Hx Hl").
  Qed.

66 67
  Lemma bin_log_counter_read_r Γ E K x (n : nat) t τ
    (Hspec : nclose specN  E) :
68
    x ↦ₛ #n -
69 70
    (x ↦ₛ #n - {E;Δ;Γ}  t log fill K #n : τ) -
    {E;Δ;Γ}  t log fill K ((counter_read $/ LitV (Loc x)) #()) : τ.
71 72 73 74 75
  Proof.
    iIntros "Hx Hlog".
    unfold counter_read. unlock. simpl.
    rel_rec_r.
    rel_load_r.
76
    by iApply "Hlog".
77 78
  Qed.
 
79 80
  Lemma counter_read_type Γ :
    typed Γ counter_read (TArrow (Tref TNat) (TArrow TUnit TNat)).
81
  Proof. solve_typed. Qed.
82

Dan Frumin committed
83 84
  Hint Resolve counter_read_type : typeable.

85
  Lemma CG_counter_type Γ :
86
    typed Γ CG_counter (TArrow TUnit (TProd (TArrow TUnit TNat) (TArrow TUnit TNat))).
87
  Proof. solve_typed. Qed.
88

Dan Frumin committed
89 90
  Hint Resolve CG_counter_type : typeable.

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

Dan Frumin committed
96 97
  Hint Resolve FG_increment_type : typeable.

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

115
  Lemma FG_counter_type Γ :
116
    typed Γ FG_counter (TArrow TUnit (TProd (TArrow TUnit TNat) (TArrow TUnit TNat))).
117
  Proof. solve_typed. Qed.
118

Dan Frumin committed
119
  Hint Resolve FG_counter_type : typeable.
120

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

123
  Definition counter_inv l cnt cnt' : iProp Σ :=
124
    ( n : nat, l ↦ₛ #false  cnt ↦ᵢ #n  cnt' ↦ₛ #n)%I.
125

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

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

185 186
  Lemma FG_CG_increment_refinement l cnt cnt' Γ :
    inv counterN (counter_inv l cnt cnt') -
Dan Frumin committed
187
    {Δ;Γ}  FG_increment #cnt log CG_increment #cnt' #l : TNat.
188 189
  Proof.
    iIntros "#Hinv".
190 191 192 193 194 195
    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')".
196
    iExists _; iFrame.
197
    iSplit.
198
    - iIntros "(Hcnt & Hl & Hcnt')".
199 200
      iApply ("Hcl" with "[-]").
      iNext. iExists _. iFrame.
201
    - iIntros "(Hcnt & Hl & Hcnt') _".
202 203
      rel_apply_r (bin_log_related_CG_increment_r with "Hcnt' Hl").
      { solve_ndisj. }
204
      iIntros "Hcnt' Hl".
205
      iMod ("Hcl" with "[-]").
206 207
      { iNext. iExists _. iFrame. }      
      by iApply bin_log_related_nat.
208
  Qed.
209

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

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

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

256
    rel_rec_l.
257
    rel_rec_r.
258 259 260 261 262 263 264

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

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

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