counter.v 13.1 KB
Newer Older
Amin Timany's avatar
Amin Timany committed
1
From iris.proofmode Require Import tactics.
Ralf Jung's avatar
Ralf Jung committed
2
From iris.algebra Require Import auth list.
Amin Timany's avatar
Amin Timany committed
3 4
From iris_examples.logrel.F_mu_ref_conc Require Export examples.lock.
From iris_examples.logrel.F_mu_ref_conc Require Import soundness_binary.
Amin Timany's avatar
Amin Timany committed
5 6 7
From iris.program_logic Require Import adequacy.

Definition CG_increment (x : expr) : expr :=
Amin Timany's avatar
Amin Timany committed
8
  Lam (Store x.[ren (+ 1)] (BinOp Add (#n 1) (Load x.[ren (+ 1)]))).
Amin Timany's avatar
Amin Timany committed
9 10 11 12 13 14

Definition CG_locked_increment (x l : expr) : expr :=
  with_lock (CG_increment x) l.
Definition CG_locked_incrementV (x l : expr) : val :=
  with_lockV (CG_increment x) l.

Amin Timany's avatar
Amin Timany committed
15 16
Definition counter_read (x : expr) : expr := Lam (Load x.[ren (+1)]).
Definition counter_readV (x : expr) : val := LamV (Load x.[ren (+1)]).
Amin Timany's avatar
Amin Timany committed
17 18 19 20

Definition CG_counter_body (x l : expr) : expr :=
  Pair (CG_locked_increment x l) (counter_read x).
Definition CG_counter : expr :=
Amin Timany's avatar
Amin Timany committed
21
  LetIn newlock (LetIn (Alloc (#n 0)) (CG_counter_body (Var 0) (Var 1))).
Amin Timany's avatar
Amin Timany committed
22 23

Definition FG_increment (x : expr) : expr :=
Amin Timany's avatar
Amin Timany committed
24 25 26 27 28 29
  Rec (LetIn
         (Load x.[ren (+2)]) (* read the counter *)
         (* try increment *)
         (If (CAS x.[ren (+3)] (Var 0) (BinOp Add (#n 1) (Var 0)))
             Unit (* increment succeeds we return unit *)
             (App (Var 1) (Var 2)) (* increment fails, we try again *))).
Amin Timany's avatar
Amin Timany committed
30 31 32
Definition FG_counter_body (x : expr) : expr :=
  Pair (FG_increment x) (counter_read x).
Definition FG_counter : expr :=
Amin Timany's avatar
Amin Timany committed
33
  LetIn (Alloc (#n 0)) (FG_counter_body (Var 0)).
Amin Timany's avatar
Amin Timany committed
34 35 36 37 38 39 40 41 42 43 44 45 46

Section CG_Counter.
  Context `{heapIG Σ, cfgSG Σ}.

  Notation D := (prodC valC valC -n> iProp Σ).
  Implicit Types Δ : listC D.

  (* Coarse-grained increment *)
  Lemma CG_increment_type x Γ :
    typed Γ x (Tref TNat) 
    typed Γ (CG_increment x) (TArrow TUnit TUnit).
  Proof.
    intros H1. repeat econstructor.
Amin Timany's avatar
Amin Timany committed
47 48
    - eapply (context_weakening [_]); eauto.
    - eapply (context_weakening [_]); eauto.
Amin Timany's avatar
Amin Timany committed
49 50 51 52 53 54
  Qed.

  Lemma CG_increment_closed (x : expr) :
    ( f, x.[f] = x)   f, (CG_increment x).[f] = CG_increment x.
  Proof. intros Hx f. unfold CG_increment. asimpl. rewrite ?Hx; trivial. Qed.

Amin Timany's avatar
Amin Timany committed
55 56
  Hint Rewrite CG_increment_closed : autosubst.

Amin Timany's avatar
Amin Timany committed
57 58 59 60
  Lemma CG_increment_subst (x : expr) f :
    (CG_increment x).[f] = CG_increment x.[f].
  Proof. unfold CG_increment; asimpl; trivial. Qed.

Amin Timany's avatar
Amin Timany committed
61 62
  Hint Rewrite CG_increment_subst : autosubst.

63
  Lemma steps_CG_increment E j K x n:
Amin Timany's avatar
Amin Timany committed
64
    nclose specN  E 
65
    spec_ctx  x ↦ₛ (#nv n)  j  fill K (App (CG_increment (Loc x)) Unit)
Amin Timany's avatar
Amin Timany committed
66 67 68
       |={E}=> j  fill K (Unit)  x ↦ₛ (#nv (S n)).
  Proof.
    iIntros (HNE) "[#Hspec [Hx Hj]]". unfold CG_increment.
Amin Timany's avatar
Amin Timany committed
69
    iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
70
    iMod (step_load _ j ((BinOpRCtx _ (#nv _) :: StoreRCtx (LocV _) :: K))
Amin Timany's avatar
Amin Timany committed
71
                    _ _ _ with "[Hj Hx]") as "[Hj Hx]"; eauto.
Amin Timany's avatar
Amin Timany committed
72
    { iFrame "Hspec Hj"; trivial. }
Amin Timany's avatar
Amin Timany committed
73
    simpl.
74
    iMod (do_step_pure _ _ ((StoreRCtx (LocV _)) :: K)  with "[$Hj]") as "Hj";
Amin Timany's avatar
Amin Timany committed
75
      eauto.
Amin Timany's avatar
Amin Timany committed
76
    simpl.
77
    iMod (step_store _ j K with "[$Hj $Hx]") as "[Hj Hx]"; eauto.
Amin Timany's avatar
Amin Timany committed
78
    iModIntro; iFrame.
Amin Timany's avatar
Amin Timany committed
79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108
  Qed.

  Global Opaque CG_increment.

  Lemma CG_locked_increment_to_val x l :
    to_val (CG_locked_increment x l) = Some (CG_locked_incrementV x l).
  Proof. by rewrite with_lock_to_val. Qed.

  Lemma CG_locked_increment_of_val x l :
    of_val (CG_locked_incrementV x l) = CG_locked_increment x l.
  Proof. by rewrite with_lock_of_val. Qed.

  Global Opaque CG_locked_incrementV.

  Lemma CG_locked_increment_type x l Γ :
    typed Γ x (Tref TNat) 
    typed Γ l LockType 
    typed Γ (CG_locked_increment x l) (TArrow TUnit TUnit).
  Proof.
    intros H1 H2. repeat econstructor.
    eapply with_lock_type; auto using CG_increment_type.
  Qed.

  Lemma CG_locked_increment_subst (x l : expr) f :
  (CG_locked_increment x l).[f] = CG_locked_increment x.[f] l.[f].
  Proof.
    unfold CG_locked_increment. simpl.
    rewrite with_lock_subst CG_increment_subst. asimpl; trivial.
  Qed.

Amin Timany's avatar
Amin Timany committed
109 110
  Hint Rewrite CG_locked_increment_subst : autosubst.

111
  Lemma steps_CG_locked_increment E j K x n l :
Amin Timany's avatar
Amin Timany committed
112
    nclose specN  E 
113
    spec_ctx  x ↦ₛ (#nv n)  l ↦ₛ (#v false)
Amin Timany's avatar
Amin Timany committed
114 115 116 117 118
       j  fill K (App (CG_locked_increment (Loc x) (Loc l)) Unit)
    ={E}= j  fill K Unit  x ↦ₛ (#nv S n)  l ↦ₛ (#v false).
  Proof.
    iIntros (HNE) "[#Hspec [Hx [Hl Hj]]]".
    iMod (steps_with_lock
119
            _ j K _ _ _ _ UnitV UnitV with "[$Hj Hx $Hl]") as "Hj"; eauto.
Ralf Jung's avatar
Ralf Jung committed
120
    - iIntros (K') "[#Hspec Hxj]".
Amin Timany's avatar
Amin Timany committed
121 122
      iApply steps_CG_increment; by try iFrame.
    - by iFrame.
Amin Timany's avatar
Amin Timany committed
123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138
  Qed.

  Global Opaque CG_locked_increment.

  Lemma counter_read_to_val x : to_val (counter_read x) = Some (counter_readV x).
  Proof. trivial. Qed.

  Lemma counter_read_of_val x : of_val (counter_readV x) = counter_read x.
  Proof. trivial. Qed.

  Global Opaque counter_readV.

  Lemma counter_read_type x Γ :
    typed Γ x (Tref TNat)  typed Γ (counter_read x) (TArrow TUnit TNat).
  Proof.
    intros H1. repeat econstructor.
Amin Timany's avatar
Amin Timany committed
139
    eapply (context_weakening [_]); trivial.
Amin Timany's avatar
Amin Timany committed
140 141 142 143 144 145
  Qed.

  Lemma counter_read_closed (x : expr) :
    ( f, x.[f] = x)   f, (counter_read x).[f] = counter_read x.
  Proof. intros H1 f. asimpl. unfold counter_read. by rewrite ?H1. Qed.

Amin Timany's avatar
Amin Timany committed
146 147
  Hint Rewrite counter_read_closed : autosubst.

Amin Timany's avatar
Amin Timany committed
148 149 150 151
  Lemma counter_read_subst (x: expr) f :
    (counter_read x).[f] = counter_read x.[f].
  Proof. unfold counter_read. by asimpl. Qed.

Amin Timany's avatar
Amin Timany committed
152 153
  Hint Rewrite counter_read_subst : autosubst.

154
  Lemma steps_counter_read E j K x n :
Amin Timany's avatar
Amin Timany committed
155
    nclose specN  E 
156
    spec_ctx  x ↦ₛ (#nv n)
Amin Timany's avatar
Amin Timany committed
157 158 159 160
                j  fill K (App (counter_read (Loc x)) Unit)
    ={E}= j  fill K (#n n)  x ↦ₛ (#nv n).
  Proof.
    intros HNE. iIntros "[#Hspec [Hx Hj]]". unfold counter_read.
Amin Timany's avatar
Amin Timany committed
161
    iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
162
    iAsimpl.
163
    iMod (step_load _ j K with "[$Hj Hx]") as "[Hj Hx]"; eauto.
Amin Timany's avatar
Amin Timany committed
164
    by iFrame.
Amin Timany's avatar
Amin Timany committed
165 166 167 168 169 170 171 172 173 174 175 176 177 178
  Qed.

  Opaque counter_read.

  Lemma CG_counter_body_type x l Γ :
    typed Γ x (Tref TNat) 
    typed Γ l LockType 
    typed Γ (CG_counter_body x l)
            (TProd (TArrow TUnit TUnit) (TArrow TUnit TNat)).
  Proof.
    intros H1 H2; repeat econstructor;
      eauto using CG_locked_increment_type, counter_read_type.
  Qed.

Amin Timany's avatar
Amin Timany committed
179 180 181 182 183
  Lemma CG_counter_body_subst (x l : expr) f :
    (CG_counter_body x l).[f] = CG_counter_body x.[f] l.[f].
  Proof. by asimpl. Qed.

  Hint Rewrite CG_counter_body_subst : autosubst.
Amin Timany's avatar
Amin Timany committed
184 185 186 187 188

  Lemma CG_counter_type Γ :
    typed Γ CG_counter (TProd (TArrow TUnit TUnit) (TArrow TUnit TNat)).
  Proof.
    econstructor; eauto using newlock_type.
Amin Timany's avatar
Amin Timany committed
189 190
    econstructor; first eauto using typed.
    apply CG_counter_body_type; eauto using typed.
Amin Timany's avatar
Amin Timany committed
191 192 193
  Qed.

  Lemma CG_counter_closed f : CG_counter.[f] = CG_counter.
Amin Timany's avatar
Amin Timany committed
194 195 196
  Proof. by asimpl. Qed.

  Hint Rewrite CG_counter_closed : autosubst.
Amin Timany's avatar
Amin Timany committed
197 198 199 200 201 202

  (* Fine-grained increment *)
  Lemma FG_increment_type x Γ :
    typed Γ x (Tref TNat) 
    typed Γ (FG_increment x) (TArrow TUnit TUnit).
  Proof.
Amin Timany's avatar
Amin Timany committed
203
    intros Hx. do 3 econstructor; eauto using typed.
Amin Timany's avatar
Amin Timany committed
204
    - eapply (context_weakening [_; _]); eauto.
Amin Timany's avatar
Amin Timany committed
205 206 207 208
    - econstructor; [| |repeat econstructor |].
      + constructor.
      + eapply (context_weakening [_; _; _]); eauto.
      + repeat constructor.
Amin Timany's avatar
Amin Timany committed
209 210
  Qed.

Amin Timany's avatar
Amin Timany committed
211 212 213 214 215
  Lemma FG_increment_subst (x : expr) f :
    (FG_increment x).[f] = FG_increment x.[f].
  Proof. rewrite /FG_increment. by asimpl. Qed.

  Hint Rewrite FG_increment_subst : autosubst.
Amin Timany's avatar
Amin Timany committed
216 217 218 219 220 221 222 223 224 225 226

  Lemma FG_counter_body_type x Γ :
    typed Γ x (Tref TNat) 
    typed Γ (FG_counter_body x)
            (TProd (TArrow TUnit TUnit) (TArrow TUnit TNat)).
  Proof.
    intros H1; econstructor.
    - apply FG_increment_type; trivial.
    - apply counter_read_type; trivial.
  Qed.

Amin Timany's avatar
Amin Timany committed
227 228 229 230 231
  Lemma FG_counter_body_subst (x : expr) f :
    (FG_counter_body x).[f] = FG_counter_body x.[f].
  Proof. rewrite /FG_counter_body /FG_increment. by asimpl. Qed.

  Hint Rewrite FG_counter_body_subst : autosubst.
Amin Timany's avatar
Amin Timany committed
232 233

  Lemma FG_counter_type Γ :
Amin Timany's avatar
Amin Timany committed
234
    Γ  FG_counter : (TProd (TArrow TUnit TUnit) (TArrow TUnit TNat)).
Amin Timany's avatar
Amin Timany committed
235 236
  Proof.
    econstructor; eauto using newlock_type, typed.
Amin Timany's avatar
Amin Timany committed
237
    apply FG_counter_body_type; by constructor.
Amin Timany's avatar
Amin Timany committed
238 239 240
  Qed.

  Lemma FG_counter_closed f : FG_counter.[f] = FG_counter.
Amin Timany's avatar
Amin Timany committed
241 242 243
  Proof. by asimpl. Qed.

  Hint Rewrite FG_counter_closed : autosubst.
Amin Timany's avatar
Amin Timany committed
244 245 246 247 248 249

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

  Lemma FG_CG_counter_refinement :
    []  FG_counter log CG_counter : TProd (TArrow TUnit TUnit) (TArrow TUnit TNat).
  Proof.
250
    iIntros (Δ [|??] ?) "#(Hspec & HΓ)"; iIntros (j K) "Hj"; last first.
Amin Timany's avatar
Amin Timany committed
251 252 253 254
    { iDestruct (interp_env_length with "HΓ") as %[=]. }
    iClear "HΓ". cbn -[FG_counter CG_counter].
    rewrite ?empty_env_subst /CG_counter /FG_counter.
    iApply fupd_wp.
255
    iMod (steps_newlock _ j (LetInCtx _ :: K) with "[$Hj]")
Amin Timany's avatar
Amin Timany committed
256
      as (l) "[Hj Hl]"; eauto.
Amin Timany's avatar
Amin Timany committed
257 258 259
    simpl.
    iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
    iAsimpl.
260
    iMod (step_alloc _ j (LetInCtx _ :: K) with "[$Hj]")
Amin Timany's avatar
Amin Timany committed
261
      as (cnt') "[Hj Hcnt']"; eauto.
Amin Timany's avatar
Amin Timany committed
262 263 264 265
    simpl.
    iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
    iAsimpl.
    iApply (wp_bind (fill [LetInCtx _])).
Amin Timany's avatar
Amin Timany committed
266 267 268 269 270 271 272 273 274
    iApply wp_wand_l. iSplitR; [iModIntro; iIntros (v) "Hv"; iExact "Hv"|].
    iApply (wp_alloc); trivial; iFrame "#"; iModIntro; iNext; iIntros (cnt) "Hcnt /=".
    (* establishing the invariant *)
    iAssert (( n, l ↦ₛ (#v false)  cnt ↦ᵢ (#nv n)  cnt' ↦ₛ (#nv n) )%I)
      with "[Hl Hcnt Hcnt']" as "Hinv".
    { iExists _. by iFrame. }
    iApply fupd_wp.
    iMod (inv_alloc counterN with "[Hinv]") as "#Hinv"; [iNext; iExact "Hinv"|].
    (* splitting increment and read *)
Robbert Krebbers's avatar
Robbert Krebbers committed
275
    iApply wp_pure_step_later; trivial. iModIntro. iNext. iAsimpl.
Amin Timany's avatar
Amin Timany committed
276 277 278 279 280 281 282 283 284 285
    iApply wp_value; auto.
    iExists (PairV (CG_locked_incrementV _ _) (counter_readV _)); simpl.
    rewrite CG_locked_increment_of_val counter_read_of_val.
    iFrame "Hj".
    iExists (_, _), (_, _); simpl; repeat iSplit; trivial.
    - (* refinement of increment *)
      iAlways. clear j K. iIntros (v) "#Heq". iIntros (j K) "Hj".
      rewrite CG_locked_increment_of_val /=.
      destruct v; iDestruct "Heq" as "[% %]"; simplify_eq/=.
      iLöb as "Hlat".
Robbert Krebbers's avatar
Robbert Krebbers committed
286
      iApply wp_pure_step_later; trivial. iAsimpl. iNext.
Amin Timany's avatar
Amin Timany committed
287
      (* fine-grained reads the counter *)
Amin Timany's avatar
Amin Timany committed
288
      iApply (wp_bind (fill [LetInCtx _]));
Amin Timany's avatar
Amin Timany committed
289 290 291 292 293 294 295
        iApply wp_wand_l; iSplitR; [iIntros (v) "Hv"; iExact "Hv"|].
      iApply wp_atomic; eauto.
      iInv counterN as (n) ">[Hl [Hcnt Hcnt']]" "Hclose".
      iApply (wp_load with "[Hcnt]"); [iNext; by iFrame|].
      iModIntro. iNext. iIntros "Hcnt".
      iMod ("Hclose" with "[Hl Hcnt Hcnt']").
      { iNext. iExists _. iFrame "Hl Hcnt Hcnt'". }
Robbert Krebbers's avatar
Robbert Krebbers committed
296
      iApply wp_pure_step_later; trivial. iAsimpl. iModIntro. iNext.
Amin Timany's avatar
Amin Timany committed
297 298 299 300 301 302 303 304 305 306 307 308 309 310
      (* fine-grained performs increment *)
      iApply (wp_bind (fill [CasRCtx (LocV _) (NatV _); IfCtx _ _]));
        iApply wp_wand_l; iSplitR; [iIntros (v) "Hv"; iExact "Hv"|].
      iApply wp_pure_step_later; auto. iApply wp_value.
      iNext.
      iApply (wp_bind (fill [IfCtx _ _]));
        iApply wp_wand_l; iSplitR; [iIntros (v) "Hv"; iExact "Hv"|].
      iApply wp_atomic; eauto.
      iInv counterN as (n') ">[Hl [Hcnt Hcnt']]" "Hclose".
      (* performing CAS *)
      destruct (decide (n = n')) as [|Hneq]; subst.
      + (* CAS succeeds *)
        (* In this case, we perform increment in the coarse-grained one *)
        iMod (steps_CG_locked_increment
311
                _ _ _ _ _ _ _ with "[Hj Hl Hcnt']") as "[Hj [Hcnt' Hl]]".
Amin Timany's avatar
Amin Timany committed
312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355
        { iFrame "Hspec Hcnt' Hl Hj"; trivial. }
        iApply (wp_cas_suc with "[Hcnt]"); auto.
        iModIntro. iNext. iIntros "Hcnt".
        iMod ("Hclose" with "[Hl Hcnt Hcnt']").
        { iNext. iExists _. iFrame "Hl Hcnt Hcnt'"; trivial. }
        simpl.
        iApply wp_pure_step_later; trivial.
        iModIntro. iNext. iApply wp_value; trivial.
        iExists UnitV; iFrame; auto.
      + (* CAS fails *)
        (* In this case, we perform a recursive call *)
        iApply (wp_cas_fail _ _ _ (#nv n') with "[Hcnt]"); auto;
        [inversion 1; subst; auto | ].
        iModIntro. iNext. iIntros "Hcnt".
        iMod ("Hclose" with "[Hl Hcnt Hcnt']").
        { iNext. iExists _; iFrame "Hl Hcnt Hcnt'". }
        iApply wp_pure_step_later; trivial. iModIntro. iNext. by iApply "Hlat".
    - (* refinement of read *)
      iAlways. clear j K. iIntros (v) "#Heq". iIntros (j K) "Hj".
      rewrite ?counter_read_of_val.
      iDestruct "Heq" as "[% %]"; destruct v; simplify_eq/=.
      Transparent counter_read.
      unfold counter_read.
      iApply wp_pure_step_later; trivial. simpl.
      iNext.
      iApply wp_atomic; eauto.
      iInv counterN as (n) ">[Hl [Hcnt Hcnt']]" "Hclose".
      iMod (steps_counter_read with "[Hj Hcnt']") as "[Hj Hcnt']"; first by solve_ndisj.
      { by iFrame "Hspec Hcnt' Hj". }
      iApply (wp_load with "[Hcnt]"); eauto.
      iModIntro. iNext. iIntros "Hcnt".
      iMod ("Hclose" with "[Hl Hcnt Hcnt']").
      { iNext. iExists _; iFrame "Hl Hcnt Hcnt'". }
      iExists (#nv _); eauto.
      Unshelve. solve_ndisj.
  Qed.
End CG_Counter.

Theorem counter_ctx_refinement :
  []  FG_counter ctx CG_counter :
         TProd (TArrow TUnit TUnit) (TArrow TUnit TNat).
Proof.
  set (Σ := #[invΣ ; gen_heapΣ loc val ; GFunctor (authR cfgUR) ]).
  set (HG := soundness_unary.HeapPreIG Σ _ _).
Amin Timany's avatar
Amin Timany committed
356
  eapply (binary_soundness Σ _); auto using FG_counter_type, CG_counter_type.
Amin Timany's avatar
Amin Timany committed
357 358
  intros. apply FG_CG_counter_refinement.
Qed.