atomic_snapshot.v 15.2 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14
From iris.algebra Require Import excl auth gmap agree.
From iris.heap_lang Require Export lifting notation.
From iris.base_logic.lib Require Export invariants.
From iris.program_logic Require Export atomic.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation par.
From iris.bi.lib Require Import fractional.
From iris_examples.logatom.snapshot Require Import spec.
Set Default Proof Using "Type".

(** Specifying snapshots with histories
    Implementing atomic pair snapshot data structure from Sergey et al. (ESOP 2015) *)


15
(*
16 17
     newPair v :=
       ref (ref (v, 0))
18
 *)
19 20 21
Definition new_snapshot : val :=
  λ: "v",
    ref (ref ("v", #0)).
22 23

(*
24
    write xp x :=
25 26 27 28 29 30
      let xp1 = !xp in
      let v   = (!xp1).2
      let xp2 = ref (x, v + 1)
      if CAS xp xp1 xp2
        then ()
        else writeX (xp, yp) x
31
 *)
32 33
Definition write : val :=
  rec: "write" "xp" "x" :=
34 35 36 37 38
    let: "xp1"  := !"xp"                  in
    let: "v"    := Snd (!"xp1")           in
    let: "xp2"  := ref ("x", "v" + #1)    in
    if: CAS "xp" "xp1" "xp2"
    then #()
39
    else "write" "xp" "x".
40 41

(*
42 43
    read xp :=
      (!!xp).1
44
 *)
45 46 47
Definition read : val :=
  λ: "xp",
    Fst !(!"xp").
48 49

(*
50 51 52 53
    read_with xp l :=
      let (x, v)  = !!xp in
      let y       = !l in
      let (_, v') = !!xp in
54 55 56
      if v = v'
        then (x, y)
        else readPair l
57
 *)
58 59 60 61 62 63 64
Definition read_with_proph : val :=
  rec: "readPair" "xp" "l" :=
    let: "proph"  := NewProph in
    let: "x"  := ! !"xp" in
    let: "y"  := !"l" in
    let: "x'" := ! !"xp" in
    let: "v_eq"   := Snd "x" = Snd "x'" in
65 66
    resolve_proph: "proph" to: "v_eq" ;;
    if: "v_eq"
67 68
    then (Fst "x", "y")
    else  "readPair" "xp" "l".
69 70 71 72


(** The CMRA & functor we need. *)

73
Definition timestampUR := gmapUR Z $ agreeR valO.
74 75

Class atomic_snapshotG Σ := AtomicSnapshotG {
76
                                atomic_snapshot_stateG :> inG Σ $ authR $ optionUR $ exclR $ valO;
77 78 79
                                atomic_snapshot_timestampG :> inG Σ $ authR $ timestampUR
}.
Definition atomic_snapshotΣ : gFunctors :=
80
  #[GFunctor (authR $ optionUR $ exclR $ valO); GFunctor (authR timestampUR)].
81 82 83 84 85 86 87

Instance subG_atomic_snapshotΣ {Σ} : subG atomic_snapshotΣ Σ  atomic_snapshotG Σ.
Proof. solve_inG. Qed.

Section atomic_snapshot.

  Context {Σ} `{!heapG Σ, !atomic_snapshotG Σ}.
88 89 90 91 92

  Variable N: namespace.

  Definition gmap_to_UR T : timestampUR := to_agree <$> T.

93
  Definition snapshot_inv γ1 γ2 l1 : iProp Σ :=
94
    ( q (l1':loc) (T : gmap Z val) x (t : Z),
95 96 97 98
      (* we add the q to make the l1' map fractional. that way,
         we can take a fraction of the l1' map out of the invariant
         and do a case analysis on whether the pointer is the same
         throughout invariant openings *)
99 100
      l1  #l1'  l1' {q} (x, #t) 
         own γ1 ( Excl' x)  own γ2 ( gmap_to_UR T) 
101 102 103
         T !! t = Some x 
         forall (t' : Z), t'  dom (gset Z) T  (t' <= t)%Z)%I.

104 105
  Definition is_snapshot (γs: gname * gname) (p : val) :=
    ( (l1 : loc), p = #l1%V  inv N (snapshot_inv γs.1 γs.2 l1))%I.
106

107
  Global Instance is_snapshot_persistent γs p : Persistent (is_snapshot γs p) := _.
108

109 110
  Definition snapshot_content (γs : gname * gname) (a : val) :=
    (own γs.1 ( Excl' a))%I.
111

112
  Global Instance snapshot_content_timeless γs a : Timeless (snapshot_content γs a) := _.
113

114 115
  Lemma snapshot_content_exclusive γs a1 a2 :
    snapshot_content γs a1 - snapshot_content γs a2 - False.
116
  Proof.
117
    iIntros "H1 H2". iDestruct (own_valid_2 with "H1 H2") as %[].
118 119 120 121
  Qed.

  Definition new_timestamp t v : gmap Z val := {[ t := v ]}.

122
  Lemma new_snapshot_spec (v : val) :
123
      {{{ True }}}
124 125
        new_snapshot v
      {{{ γs p, RET p; is_snapshot γs p  snapshot_content γs v }}}.
126
  Proof.
127
    iIntros (Φ _) "Hx". rewrite /new_snapshot. wp_lam.
128 129 130 131
    repeat (wp_proj; wp_let).
    iApply wp_fupd.
    wp_alloc lx' as "Hlx'".
    wp_alloc lx as "Hlx".
132
    set (Excl' v) as p.
133
    iMod (own_alloc ( p   p)) as (γ1) "[Hx⚫ Hx◯]". {
134
      rewrite /p. apply auth_both_valid. split; done.
135
    }
136
    set (new_timestamp 0 v) as t.
137
    iMod (own_alloc ( gmap_to_UR t   gmap_to_UR t)) as (γ2) "[Ht⚫ Ht◯]". {
138
      rewrite /t /new_timestamp. apply auth_both_valid.
139 140
      split; first done. rewrite /gmap_to_UR map_fmap_singleton. apply singleton_valid. done.
    }
141 142 143
    wp_pures. iApply ("Hx" $! (γ1, γ2)).
    iMod (inv_alloc N _ (snapshot_inv γ1 γ2 _) with "[-Hx◯ Ht◯]") as "#Hinv". {
      iNext. rewrite /snapshot_inv. iExists _, _, _, _, 0. iFrame.
144 145 146
      iPureIntro. split; first done. intros ?. subst t. rewrite /new_timestamp dom_singleton.
      rewrite elem_of_singleton. lia.
    }
147
    iModIntro. rewrite /is_snapshot /snapshot_content. iFrame. iExists _.
148
    iSplitL; first done. done.
149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165
  Qed.

 Lemma excl_update γ n' n m :
    own γ ( (Excl' n)) - own γ ( (Excl' m)) ==
      own γ ( (Excl' n'))  own γ ( (Excl' n')).
  Proof.
    iIntros "Hγ● Hγ◯".
    iMod (own_update_2 _ _ _ ( Excl' n'   Excl' n') with "Hγ● Hγ◯") as "[$$]".
    { by apply auth_update, option_local_update, exclusive_local_update. }
    done.
  Qed.

  Lemma excl_sync γ n m :
    own γ ( (Excl' n)) - own γ ( (Excl' m)) - m = n.
  Proof.
    iIntros "Hγ● Hγ◯".
    iDestruct (own_valid_2 with "Hγ● Hγ◯") as
166
        %[H%Excl_included%leibniz_equiv _]%auth_both_valid.
167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196
    done.
  Qed.

  Lemma timestamp_dupl γ T:
    own γ ( T) == own γ ( T)  own γ ( T).
  Proof.
    iIntros "Ht". iApply own_op. iApply (own_update with "Ht").
    apply auth_update_alloc. apply local_update_unital_discrete => f Hv. rewrite left_id => <-.
    split; first done. apply core_id_dup. apply _.
  Qed.

  Lemma timestamp_update γ (T : gmap Z val) (t : Z) x :
    T !! t = None 
    own γ ( gmap_to_UR T) == own γ ( gmap_to_UR (<[ t := x ]> T)).
  Proof.
    iIntros (HT) "Ht".
    set (<[ t := x ]> T) as T'.
    iDestruct (own_update _ _ ( gmap_to_UR T'   gmap_to_UR {[ t := x ]}) with "Ht") as "Ht". {
      apply auth_update_alloc. rewrite /T' /gmap_to_UR map_fmap_singleton. rewrite fmap_insert.
      apply alloc_local_update; last done. rewrite lookup_fmap HT. done.
    }
    iMod (own_op with "Ht") as "[Ht● Ht◯]". iModIntro. iFrame.
  Qed.

  Lemma timestamp_sub γ (T1 T2 : gmap Z val):
    own γ ( gmap_to_UR T1)  own γ ( gmap_to_UR T2) -
    forall t x, T2 !! t = Some x  T1 !! t = Some x.
  Proof.
    iIntros "[Hγ⚫ Hγ◯]".
    iDestruct (own_valid_2 with "Hγ⚫ Hγ◯") as
197
        %[H Hv]%auth_both_valid. iPureIntro. intros t x HT2.
198 199 200 201 202 203 204 205
    pose proof (iffLR (lookup_included (gmap_to_UR T2) (gmap_to_UR T1)) H t) as Ht.
    rewrite !lookup_fmap HT2 /= in Ht.
    destruct (is_Some_included _ _ Ht) as [? [t2 [Ht2 ->]]%fmap_Some_1]; first by eauto.
    revert Ht.
    rewrite Ht2 Some_included_total to_agree_included. fold_leibniz.
    by intros ->.
  Qed.

206 207 208 209
  Lemma write_spec γ (x2: val) p :
      is_snapshot γ p  -
      <<<  x : val, snapshot_content γ x >>>
        write p x2
210
        @ ⊤∖↑N
211
      <<< snapshot_content γ x2, RET #() >>>.
212
  Proof.
213 214
    iIntros "Hx". iIntros (Φ) "AU". iLöb as "IH".
    iDestruct "Hx" as (l1 ->) "#Hinv". wp_pures. wp_lam. wp_pures.
215 216
    (* first read *)
    (* open invariant *)
217
    wp_bind (!_)%E. iInv N as (q l1' T x v') "[Hl1 [Hl1' [Hx⚫ Htime]]]".
218 219 220 221
      wp_load.
      iDestruct "Hl1'" as "[Hl1'frac1 Hl1'frac2]".
      iModIntro. iSplitR "AU Hl1'frac2".
      (* close invariant *)
222
      { iNext. rewrite /snapshot_inv. eauto 10 with iFrame. }
223 224 225 226 227 228
    wp_let. wp_bind (!_)%E. clear T.
    wp_load. wp_proj. wp_let. wp_op. wp_alloc l1'new as "Hl1'new".
    wp_let.
    (* CAS *)
    wp_bind (CAS _ _ _)%E.
    (* open invariant *)
229
    iInv N as (q' l1'' T x' v'') ">[Hl1 [Hl1'' [Hx⚫ [Ht● Ht]]]]".
230 231 232 233 234
    iDestruct "Ht" as %[Ht Hvt].
    destruct (decide (l1'' = l1')) as [-> | Hn].
    - wp_cas_suc.
      iDestruct (mapsto_agree with "Hl1'frac2 Hl1''") as %[= -> ->]. iClear "Hl1'frac2".
      (* open AU *)
235 236
      iMod "AU" as (xv) "[Hx [_ Hclose]]".
        (* update snapshot ghost state to (x2, y') *)
237 238
        iDestruct (excl_sync with "Hx⚫ Hx") as %[= ->].
        iMod (excl_update _ x2 with "Hx⚫ Hx") as "[Hx⚫ Hx◯]".
239
        (* close AU *)
240
        iMod ("Hclose" with "Hx◯") as "HΦ".
241 242 243 244 245 246
      (* update timestamp *)
      iMod (timestamp_update _ T (v'' + 1)%Z x2 with "[Ht●]") as "Ht".
      { eapply (not_elem_of_dom (D:=gset Z) T). intros Hd. specialize (Hvt _ Hd). omega. }
      { done. }
      (* close invariant *)
      iModIntro. iSplitR "HΦ".
247
      + iNext. rewrite /snapshot_inv.
248
        set (<[ v'' + 1 := x2]> T) as T'.
249
        iExists 1%Qp, l1'new, T', x2, (v'' + 1).
250 251 252 253 254 255 256 257 258 259 260 261
        iFrame.
        iPureIntro. split.
        * apply: lookup_insert.
        * intros ? Hv. destruct (decide (t' = (v'' + 1)%Z)) as [-> | Hn]; first done.
          assert (dom (gset Z) T' = {[(v'' + 1)%Z]}  dom (gset Z) T) as Hd. {
            apply leibniz_equiv. rewrite dom_insert. done.
          }
          rewrite Hd in Hv. clear Hd. apply elem_of_union in Hv.
          destruct Hv as [Hv%elem_of_singleton_1 | Hv]; first done.
          specialize (Hvt _ Hv). lia.
      + wp_if. done.
    - wp_cas_fail. iModIntro. iSplitR "AU".
262 263
      + iNext. rewrite /snapshot_inv. eauto 10 with iFrame.
      + wp_if. iApply "IH"; last eauto. rewrite /is_snapshot. eauto.
264 265
  Qed.

266 267 268 269
  Lemma read_spec γ p :
    is_snapshot γ p -
    <<<  v : val, snapshot_content γ v >>>
      read p
270
      @ ⊤∖↑N
271
    <<< snapshot_content γ v, RET v >>>.
272
  Proof.
273 274
    iIntros "Hx". iIntros (Φ) "AU".
    iDestruct "Hx" as (l1 ->) "#Hinv".
275
    wp_lam. wp_bind (! #l1)%E.
276
    (* open invariant for 1st read *)
277
    iInv N as (q l1' T x v') ">[Hl1 [Hl1' [Hx⚫ Htime]]]".
278 279
      wp_load.
      iDestruct "Hl1'" as "[Hl1' Hl1'frac]".
280
      iMod "AU" as (xv) "[Hx [_ Hclose]]".
281
      iDestruct (excl_sync with "Hx⚫ Hx") as %[= ->].
282
      iMod ("Hclose" with "Hx") as "HΦ".
283 284
      (* close invariant *)
      iModIntro. iSplitR "HΦ Hl1'". {
285
        iNext. unfold snapshot_inv. eauto 7 with iFrame.
286
      }
287
    iApply wp_fupd. wp_load. wp_pures. eauto.
288 289
  Qed.

290
  Definition prophecy_to_bool (v : list (val * val)) : bool :=
291
    match v with
292 293
    | (_, LitV (LitBool b)) :: _ => b
    | _                          => false
294 295
    end.

296 297 298 299
  Lemma read_with_spec γ p (l : loc) :
    is_snapshot γ p -
    <<<  v1 v2 : val, snapshot_content γ v1  l  v2 >>>
       read_with_proph p #l
300
       @ ⊤∖↑N
301
    <<< snapshot_content γ v1  l  v2, RET (v1, v2) >>>.
302
  Proof.
303 304 305 306
    iIntros "Hx". iIntros (Φ) "AU". iLöb as "IH". wp_lam. wp_pures.
    (* ************ new prophecy ********** *)
    wp_apply wp_new_proph; first done.
    iIntros (proph_val proph) "Hpr".
307 308
    wp_pures.
    (* ************ 1st readX ********** *)
309
    iDestruct "Hx" as (l1 ->) "#Hinv". wp_bind (! #l1)%E.
310
    (* open invariant for 1st read *)
311
    iInv N as (q_x1 l1' T_x x1 v_x1) ">[Hl1 [Hl1' [Hx⚫ [Ht_x Htime_x]]]]".
312 313 314
      iDestruct "Htime_x" as %[Hlookup_x Hdom_x].
      wp_load.
      iDestruct "Hl1'" as "[Hl1' Hl1'frac]".
315 316
      iMod "AU" as (xv yv) "[[Hx Hy] [Hclose _]]".
      iDestruct (excl_sync with "Hx⚫ Hx") as %[= ->].
317
      iMod ("Hclose" with "[$Hx $Hy]") as "AU".
318 319 320
      (* duplicate timestamp T_x1 *)
      iMod (timestamp_dupl with "Ht_x") as "[Ht_x1⚫ Ht_x1◯]".
      (* close invariant *)
321 322
      iModIntro. iSplitR "AU Hl1' Ht_x1◯ Hpr". {
        iNext. unfold snapshot_inv. eauto 8 with iFrame.
323 324 325 326
      }
    wp_load. wp_let.
    (* ************ readY ********** *)
    repeat (wp_lam; wp_pures). wp_bind (!_)%E.
327
    iInv N as (q_y l1'_y T_y x_y v_y) ">[Hl1 [Hl1'_y [Hx⚫ [Ht_y Htime_y]]]]".
328 329
    iDestruct "Htime_y" as %[Hlookup_y Hdom_y].
    (* linearization point *)
330 331 332
    clear yv.
    iMod "AU" as (xv yv) "[[Hx Hy] Hclose]".
    wp_load.
333
    rewrite /snapshot_content.
334
    iDestruct (excl_sync with "Hx⚫ Hx") as %[= ->].
335
    destruct (prophecy_to_bool proph_val) eqn:Hproph.
336 337
    - (* prophecy value is predicting that timestamp has not changed, so we commit *)
      (* committing AU *)
338
      iMod ("Hclose" with "[$Hx $Hy]") as "HΦ".
339 340 341 342 343
      (* duplicate timestamp T_y *)
      iMod (timestamp_dupl with "Ht_y") as "[Ht_y● Ht_y◯]".
      (* show that T_x <= T_y *)
      iDestruct (timestamp_sub with "[Ht_y● Ht_x1◯]") as "#Hs"; first by iFrame.
      iDestruct "Hs" as %Hs.
344
      iModIntro. iModIntro.
345 346
      (* closing invariant *)
      iSplitR "HΦ Hl1' Ht_x1◯ Ht_y◯ Hpr".
347
      { iNext. unfold snapshot_inv. eauto 10 with iFrame. }
348 349 350 351
      wp_let.
      (* ************ 2nd readX ********** *)
      repeat (wp_lam; wp_pures). wp_bind (! #l1)%E.
      (* open invariant *)
352
      iInv N as (q_x2 l1'_x2 T_x2 x2 v_x2) ">[Hl1 [Hl1'_x2 [Hx⚫ [Ht_x2 Htime_x2]]]]".
353 354 355 356 357 358 359
      iDestruct "Htime_x2" as %[Hlookup_x2 Hdom_x2].
      iDestruct "Hl1'_x2" as "[Hl1'_x2 Hl1'_x2_frag]".
      wp_load.
      (* show that T_y <= T_x2 *)
      iDestruct (timestamp_sub with "[Ht_x2 Ht_y◯]") as "#Hs'"; first by iFrame.
      iDestruct "Hs'" as %Hs'.
      iModIntro. iSplitR "HΦ Hl1'_x2_frag Hpr". {
360
        iNext. unfold snapshot_inv. eauto 8 with iFrame.
361
      }
362 363
      wp_load. wp_pures.
      case_bool_decide; wp_apply (wp_resolve_proph with "Hpr");
364
        iIntros (vs') "[Eq _]"; iDestruct "Eq" as %->; wp_seq; wp_if.
365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381
      + inversion H; subst; clear H. wp_pures.
        assert (v_x2 = v_y) as ->. {
          assert (v_x2 <= v_y) as vneq. {
            apply Hdom_y.
            eapply (iffRL (elem_of_dom T_y _)). eauto using mk_is_Some.
          }
          assert (v_y <= v_x2) as vneq'. {
            apply Hdom_x2.
            eapply (iffRL (elem_of_dom T_x2 _)). eauto using mk_is_Some.
          }
          apply Z.le_antisymm; auto.
        }
        assert (x1 = x_y) as ->. {
          specialize (Hs _ _ Hlookup_x). rewrite Hs in Hlookup_y. inversion Hlookup_y. done.
        }
        done.
      + inversion Hproph.
382 383
    - (* prophecy value is predicting that timestamp has not changed, so we abort *)
      iDestruct "Hclose" as "[Hclose _]". iMod ("Hclose" with "[$Hx $Hy]") as "AU".
384
      iModIntro. iModIntro.
385 386
      (* closing invariant *)
      iSplitR "AU Hpr".
387
      { iNext. unfold snapshot_inv. eauto 10 with iFrame. }
388 389
      wp_let.
      (* ************ 2nd readX ********** *)
390
      wp_bind (! #l1)%E.
391
      (* open invariant *)
392
      iInv N as (q_x2 l1'_x2 T_x2 x2 v_x2) "[Hl1 [Hl1'_x2 [Hx⚫ [Ht_x2 Htime_x2]]]]".
393 394 395
      iDestruct "Hl1'_x2" as "[Hl1'_x2 Hl1'_x2_frag]".
      wp_load.
      iModIntro. iSplitR "AU Hl1'_x2_frag Hpr". {
396
        iNext. unfold snapshot_inv. eauto 8 with iFrame.
397
      }
398
      wp_load. wp_pures.
399
      wp_apply (wp_resolve_proph with "Hpr").
400
      iIntros (vs') "[Heq _]"; iDestruct "Heq" as %->.
401 402
      case_bool_decide.
      + inversion H; subst; clear H. inversion Hproph.
403
      + wp_seq. wp_if. iApply "IH"; rewrite /is_snapshot; eauto.
404 405 406 407
  Qed.

End atomic_snapshot.

408
Program Definition atomic_snapshot `{!heapG Σ, atomic_snapshotG Σ} :
409
  spec.atomic_snapshot Σ :=
410 411 412 413 414
  {| spec.new_snapshot_spec := new_snapshot_spec;
     spec.write_spec := write_spec;
     spec.read_spec := read_spec;
     spec.read_with_spec := read_with_spec;
     spec.snapshot_content_exclusive := snapshot_content_exclusive |}.
415

416
Typeclasses Opaque snapshot_content is_snapshot.