From 45ad940f90bbb05c5c1459dd4fc9ee09742169b7 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 12 Jun 2019 16:42:46 +0200
Subject: [PATCH] restructure snapshot to not actually have a protocol on the y
location
---
theories/logatom/snapshot/atomic_snapshot.v | 305 ++++++++++----------
1 file changed, 147 insertions(+), 158 deletions(-)
diff --git a/theories/logatom/snapshot/atomic_snapshot.v b/theories/logatom/snapshot/atomic_snapshot.v
index 026750bd..2fa4f266 100644
--- a/theories/logatom/snapshot/atomic_snapshot.v
+++ b/theories/logatom/snapshot/atomic_snapshot.v
@@ -11,44 +11,27 @@ Set Default Proof Using "Type".
(** Specifying snapshots with histories
Implementing atomic pair snapshot data structure from Sergey et al. (ESOP 2015) *)
-(** The CMRA & functor we need. *)
-
-Definition timestampUR := gmapUR Z $ agreeR valC.
-
-Class atomic_snapshotG Σ := AtomicSnapshotG {
- atomic_snapshot_stateG :> inG Σ $ authR $ optionUR $ exclR $ prodC valC valC;
- atomic_snapshot_timestampG :> inG Σ $ authR $ timestampUR
-}.
-Definition atomic_snapshotΣ : gFunctors :=
- #[GFunctor (authR $ optionUR $ exclR $ prodC valC valC); GFunctor (authR timestampUR)].
-Instance subG_atomic_snapshotΣ {Σ} : subG atomic_snapshotΣ Σ → atomic_snapshotG Σ.
-Proof. solve_inG. Qed.
-
-Section atomic_snapshot.
-
- Context {Σ} `{!heapG Σ, !atomic_snapshotG Σ}.
-
- (*
+(*
newPair x y :=
(ref (ref (x, 0)), ref y)
- *)
- Definition newPair : val :=
- λ: "args",
- let: "x" := Fst "args" in
- let: "y" := Snd "args" in
- (ref (ref ("x", #0)), ref "y").
-
- (*
+ *)
+Definition newPair : val :=
+ λ: "args",
+ let: "x" := Fst "args" in
+ let: "y" := Snd "args" in
+ (ref (ref ("x", #0)), ref "y").
+
+(*
writeY (xp, yp) y :=
yp <- y
- *)
- Definition writeY : val :=
- λ: "args",
- let: "p" := Fst "args" in
- Snd "p" <- Snd "args".
+ *)
+Definition writeY : val :=
+ λ: "args",
+ let: "p" := Fst "args" in
+ Snd "p" <- Snd "args".
- (*
+(*
writeX (xp, yp) x :=
let xp1 = !xp in
let v = (!xp1).2
@@ -56,34 +39,34 @@ Section atomic_snapshot.
if CAS xp xp1 xp2
then ()
else writeX (xp, yp) x
- *)
- Definition writeX : val :=
- rec: "writeX" "args" :=
- let: "p" := Fst "args" in
- let: "x" := Snd "args" in
- let: "xp" := Fst "p" in
- let: "xp1" := !"xp" in
- let: "v" := Snd (!"xp1") in
- let: "xp2" := ref ("x", "v" + #1) in
- if: CAS "xp" "xp1" "xp2"
- then #()
- else "writeX" "args".
-
- (*
+ *)
+Definition writeX : val :=
+ rec: "writeX" "args" :=
+ let: "p" := Fst "args" in
+ let: "x" := Snd "args" in
+ let: "xp" := Fst "p" in
+ let: "xp1" := !"xp" in
+ let: "v" := Snd (!"xp1") in
+ let: "xp2" := ref ("x", "v" + #1) in
+ if: CAS "xp" "xp1" "xp2"
+ then #()
+ else "writeX" "args".
+
+(*
readX (xp, yp) :=
!!xp
- *)
- Definition readX : val :=
- λ: "p",
- let: "xp" := Fst "p" in
- !(!"xp").
-
- Definition readY : val :=
- λ: "p",
- let: "yp" := Snd "p" in
- !"yp".
-
- (*
+ *)
+Definition readX : val :=
+ λ: "p",
+ let: "xp" := Fst "p" in
+ !(!"xp").
+
+Definition readY : val :=
+ λ: "p",
+ let: "yp" := Snd "p" in
+ !"yp".
+
+(*
readPair l :=
let (x, v) = readX l in
let y = readY l in
@@ -91,58 +74,77 @@ Section atomic_snapshot.
if v = v'
then (x, y)
else readPair l
- *)
- Definition readPair : val :=
- rec: "readPair" "l" :=
- let: "x" := readX "l" in
- let: "y" := readY "l" in
- let: "x'" := readX "l" in
- if: Snd "x" = Snd "x'"
- then (Fst "x", Fst "y")
- else "readPair" "l".
-
- Definition readPair_proph : val :=
- rec: "readPair" "l" :=
- let: "xv1" := readX "l" in
- let: "proph" := NewProph in
- let: "y" := readY "l" in
- let: "xv2" := readX "l" in
- let: "v2" := Snd "xv2" in
- let: "v_eq" := Snd "xv1" = "v2" in
- resolve_proph: "proph" to: "v_eq" ;;
- if: "v_eq"
- then (Fst "xv1", "y")
- else "readPair" "l".
+ *)
+Definition readPair : val :=
+ rec: "readPair" "l" :=
+ let: "x" := readX "l" in
+ let: "y" := readY "l" in
+ let: "x'" := readX "l" in
+ if: Snd "x" = Snd "x'"
+ then (Fst "x", Fst "y")
+ else "readPair" "l".
+
+Definition readPair_proph : val :=
+ rec: "readPair" "l" :=
+ let: "xv1" := readX "l" in
+ let: "proph" := NewProph in
+ let: "y" := readY "l" in
+ let: "xv2" := readX "l" in
+ let: "v2" := Snd "xv2" in
+ let: "v_eq" := Snd "xv1" = "v2" in
+ resolve_proph: "proph" to: "v_eq" ;;
+ if: "v_eq"
+ then (Fst "xv1", "y")
+ else "readPair" "l".
+
+
+(** The CMRA & functor we need. *)
+
+Definition timestampUR := gmapUR Z $ agreeR valC.
+
+Class atomic_snapshotG Σ := AtomicSnapshotG {
+ atomic_snapshot_stateG :> inG Σ $ authR $ optionUR $ exclR $ valC;
+ atomic_snapshot_timestampG :> inG Σ $ authR $ timestampUR
+}.
+Definition atomic_snapshotΣ : gFunctors :=
+ #[GFunctor (authR $ optionUR $ exclR $ valC); GFunctor (authR timestampUR)].
+
+Instance subG_atomic_snapshotΣ {Σ} : subG atomic_snapshotΣ Σ → atomic_snapshotG Σ.
+Proof. solve_inG. Qed.
+
+Section atomic_snapshot.
+
+ Context {Σ} `{!heapG Σ, !atomic_snapshotG Σ}.
Variable N: namespace.
Definition gmap_to_UR T : timestampUR := to_agree <$> T.
- Definition pair_inv γ1 γ2 l1 l2 : iProp Σ :=
- (∃ q (l1':loc) (T : gmap Z val) x y (t : Z),
+ Definition pair_inv γ1 γ2 l1 : iProp Σ :=
+ (∃ q (l1':loc) (T : gmap Z val) x (t : Z),
(* 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 *)
- l1 ↦ #l1' ∗ l1' ↦{q} (x, #t) ∗ l2 ↦ y ∗
- own γ1 (◠Excl' (x, y)) ∗ own γ2 (◠gmap_to_UR T) ∗
+ l1 ↦ #l1' ∗ l1' ↦{q} (x, #t) ∗
+ own γ1 (◠Excl' x) ∗ own γ2 (◠gmap_to_UR T) ∗
⌜T !! t = Some x⌠∗
⌜forall (t' : Z), t' ∈ dom (gset Z) T → (t' <= t)%ZâŒ)%I.
- Definition is_pair (γs: gname * gname) (p : val) :=
- (∃ (l1 l2 : loc), ⌜p = (#l1, #l2)%V⌠∗ inv N (pair_inv γs.1 γs.2 l1 l2))%I.
+ Definition is_pair (γs: gname * gname * loc) (p : val) :=
+ (∃ (l1 : loc), ⌜p = (#l1, #γs.2)%V⌠∗ inv N (pair_inv γs.1.1 γs.1.2 l1))%I.
Global Instance is_pair_persistent γs p : Persistent (is_pair γs p) := _.
- Definition pair_content (γs : gname * gname) (a : val * val) :=
- (own γs.1 (◯ Excl' a))%I.
+ Definition pair_content (γs : gname * gname * loc) (a : val * val) :=
+ (own γs.1.1 (◯ Excl' a.1) ∗ γs.2 ↦ a.2)%I.
Global Instance pair_content_timeless γs a : Timeless (pair_content γs a) := _.
Lemma pair_content_exclusive γs a1 a2 :
pair_content γs a1 -∗ pair_content γs a2 -∗ False.
Proof.
- iIntros "H1 H2". iDestruct (own_valid_2 with "H1 H2") as %[].
+ iIntros "[H1 _] [H2 _]". iDestruct (own_valid_2 with "H1 H2") as %[].
Qed.
Definition new_timestamp t v : gmap Z val := {[ t := v ]}.
@@ -152,14 +154,14 @@ Section atomic_snapshot.
newPair (v1, v2)%V
{{{ γs p, RET p; is_pair γs p ∗ pair_content γs (v1, v2) }}}.
Proof.
- iIntros (Φ _) "Hp". rewrite /newPair. wp_lam.
+ iIntros (Φ _) "Hx". rewrite /newPair. wp_lam.
repeat (wp_proj; wp_let).
iApply wp_fupd.
+ wp_alloc ly as "Hly".
wp_alloc lx' as "Hlx'".
wp_alloc lx as "Hlx".
- wp_alloc ly as "Hly".
- set (Excl' (v1, v2)) as p.
- iMod (own_alloc (◠p ⋅ ◯ p)) as (γ1) "[Hp⚫ Hp◯]". {
+ set (Excl' v1) as p.
+ iMod (own_alloc (◠p ⋅ ◯ p)) as (γ1) "[Hx⚫ Hx◯]". {
rewrite /p. apply auth_both_valid. split; done.
}
set (new_timestamp 0 v1) as t.
@@ -167,14 +169,14 @@ Section atomic_snapshot.
rewrite /t /new_timestamp. apply auth_both_valid.
split; first done. rewrite /gmap_to_UR map_fmap_singleton. apply singleton_valid. done.
}
- wp_pures. iApply ("Hp" $! (γ1, γ2)).
- iMod (inv_alloc N _ (pair_inv γ1 γ2 _ _) with "[-Hp◯ Ht◯]") as "#Hinv". {
- iNext. rewrite /pair_inv. iExists _, _, _, _, _. iExists 0. iFrame.
+ wp_pures. iApply ("Hx" $! (γ1, γ2, ly)).
+ iMod (inv_alloc N _ (pair_inv γ1 γ2 _) with "[-Hx◯ Ht◯ Hly]") as "#Hinv". {
+ iNext. rewrite /pair_inv. iExists _, _, _, _, 0. iFrame.
iPureIntro. split; first done. intros ?. subst t. rewrite /new_timestamp dom_singleton.
rewrite elem_of_singleton. lia.
}
- iModIntro. iSplitR. rewrite /is_pair. repeat (iExists _). iSplitL; eauto.
- rewrite /pair_content. rewrite /p. iApply "Hpâ—¯".
+ iModIntro. rewrite /is_pair /pair_content. iFrame. iExists _.
+ iSplitL; first done. done.
Qed.
Lemma excl_update γ n' n m :
@@ -239,20 +241,15 @@ Section atomic_snapshot.
@ ⊤∖↑N
<<< pair_content γ (x, y2), RET #() >>>.
Proof.
- iIntros "Hp". iIntros (Φ) "AU".
- iDestruct "Hp" as (l1 l2 ->) "#Hinv". wp_pures.
+ iIntros "Hx". iIntros (Φ) "AU".
+ iDestruct "Hx" as (l1 ->) "#Hinv". wp_pures.
wp_lam. wp_pures.
iApply wp_fupd.
- iInv N as (q l1' T x) "Hinvp".
- iDestruct "Hinvp" as (y v') "[Hl1 [Hl1' [Hl2 [Hpâš« Htime]]]]".
+ iMod "AU" as (xv yv) "[[Hx Hy] [_ Hclose]]".
wp_store.
- iMod "AU" as (xv yv) "[Hpair [_ Hclose]]".
- rewrite /pair_content.
- iDestruct (excl_sync with "Hpâš« Hpair") as %[= -> ->].
- iMod (excl_update _ (x, y2) with "Hpâš« Hpair") as "[Hpâš« Hpâ—¯]".
- iMod ("Hclose" with "Hp◯") as "HΦ".
- iModIntro. iSplitR "HΦ"; last done.
- iNext. unfold pair_inv. eauto 7 with iFrame.
+ iMod ("Hclose" with "[Hx Hy]") as "HΦ".
+ { rewrite /pair_content. iFrame. }
+ eauto.
Qed.
Lemma writeX_spec γ (x2: val) p :
@@ -262,12 +259,11 @@ Section atomic_snapshot.
@ ⊤∖↑N
<<< pair_content γ (x2, y), RET #() >>>.
Proof.
- iIntros "Hp". iIntros (Φ) "AU". iLöb as "IH".
- iDestruct "Hp" as (l1 l2 ->) "#Hinv". wp_pures. wp_lam. wp_pures.
+ iIntros "Hx". iIntros (Φ) "AU". iLöb as "IH".
+ iDestruct "Hx" as (l1 ->) "#Hinv". wp_pures. wp_lam. wp_pures.
(* first read *)
(* open invariant *)
- wp_bind (!_)%E. iInv N as (q l1' T x) "Hinvp".
- iDestruct "Hinvp" as (y v') "[Hl1 [Hl1' [Hl2 [Hpâš« Htime]]]]".
+ wp_bind (!_)%E. iInv N as (q l1' T x v') "[Hl1 [Hl1' [Hxâš« Htime]]]".
wp_load.
iDestruct "Hl1'" as "[Hl1'frac1 Hl1'frac2]".
iModIntro. iSplitR "AU Hl1'frac2".
@@ -279,19 +275,19 @@ Section atomic_snapshot.
(* CAS *)
wp_bind (CAS _ _ _)%E.
(* open invariant *)
- iInv N as (q' l1'' T x') ">Hinvp".
- iDestruct "Hinvp" as (y' v'') "[Hl1 [Hl1'' [Hl2 [Hpâš« [Htâ— Ht]]]]]".
+ iInv N as (q' l1'' T x' v'') ">[Hl1 [Hl1'' [Hxâš« [Htâ— Ht]]]]".
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 *)
- iMod "AU" as (xv yv) "[Hpair [_ Hclose]]".
+ iMod "AU" as (xv yv) "[[Hx Hy] [_ Hclose]]".
(* update pair ghost state to (x2, y') *)
- iDestruct (excl_sync with "Hpâš« Hpair") as %[= -> ->].
- iMod (excl_update _ (x2, y') with "Hpâš« Hpair") as "[Hpâš« Hpâ—¯]".
+ iDestruct (excl_sync with "Hxâš« Hx") as %[= ->].
+ iMod (excl_update _ x2 with "Hxâš« Hx") as "[Hxâš« Hxâ—¯]".
(* close AU *)
- iMod ("Hclose" with "Hp◯") as "HΦ".
+ iMod ("Hclose" with "[Hx◯ Hy]") as "HΦ".
+ { rewrite /pair_content. iFrame. }
(* 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. }
@@ -300,7 +296,7 @@ Section atomic_snapshot.
iModIntro. iSplitR "HΦ".
+ iNext. rewrite /pair_inv.
set (<[ v'' + 1 := x2]> T) as T'.
- iExists 1%Qp, l1'new, T', x2, y', (v'' + 1).
+ iExists 1%Qp, l1'new, T', x2, (v'' + 1).
iFrame.
iPureIntro. split.
* apply: lookup_insert.
@@ -324,19 +320,15 @@ Section atomic_snapshot.
@ ⊤∖↑N
<<< pair_content γ (v1, v2), RET v2 >>>.
Proof.
- iIntros "Hp". iIntros (Φ) "AU".
- iDestruct "Hp" as (l1 l2 ->) "#Hinv".
+ iIntros "Hx". iIntros (Φ) "AU".
+ iDestruct "Hx" as (l1 ->) "#Hinv".
repeat (wp_lam; wp_proj). wp_let.
iApply wp_fupd.
- iInv N as (q l1' T x) "Hinvp".
- iDestruct "Hinvp" as (y v') "[Hl1 [Hl1' [Hl2 [Hpâš« Htime]]]]".
+ iMod "AU" as (xv yv) "[[Hx Hy] [_ Hclose]]".
wp_load.
- iMod "AU" as (xv yv) "[Hpair [_ Hclose]]".
rewrite /pair_content.
- iDestruct (excl_sync with "Hpâš« Hpair") as %[= -> ->].
- iMod ("Hclose" with "Hpair") as "HΦ".
- iModIntro. iSplitR "HΦ"; last done.
- iNext. unfold pair_inv. eauto 7 with iFrame.
+ iMod ("Hclose" with "[$Hx $Hy]") as "HΦ".
+ iModIntro. done.
Qed.
Lemma readX_spec γ p :
@@ -346,23 +338,22 @@ Section atomic_snapshot.
@ ⊤∖↑N
<<< ∃ (t: Z), pair_content γ (v1, v2), RET (v1, #t) >>>.
Proof.
- iIntros "Hp". iIntros (Φ) "AU".
- iDestruct "Hp" as (l1 l2 ->) "#Hinv".
+ iIntros "Hx". iIntros (Φ) "AU".
+ iDestruct "Hx" as (l1 ->) "#Hinv".
repeat (wp_lam; wp_proj). wp_let. wp_bind (! #l1)%E.
(* open invariant for 1st read *)
- iInv N as (q l1' T x) ">Hinvp".
- iDestruct "Hinvp" as (y v') "[Hl1 [Hl1' [Hl2 [Hpâš« Htime]]]]".
+ iInv N as (q l1' T x v') ">[Hl1 [Hl1' [Hxâš« Htime]]]".
wp_load.
iDestruct "Hl1'" as "[Hl1' Hl1'frac]".
- iMod "AU" as (xv yv) "[Hpair [_ Hclose]]".
- iDestruct (excl_sync with "Hpâš« Hpair") as %[= -> ->].
- iMod ("Hclose" with "Hpair") as "HΦ".
+ iMod "AU" as (xv yv) "[[Hx Hy] [_ Hclose]]".
+ iDestruct (excl_sync with "Hxâš« Hx") as %[= ->].
+ iMod ("Hclose" with "[Hx Hy]") as "HΦ".
+ { rewrite /pair_content. iFrame. }
(* close invariant *)
iModIntro. iSplitR "HΦ Hl1'". {
iNext. unfold pair_inv. eauto 7 with iFrame.
}
- iApply wp_fupd. clear T y.
- wp_load. eauto.
+ iApply wp_fupd. wp_load. eauto.
Qed.
Definition prophecy_to_bool (v : list (val * val)) : bool :=
@@ -378,20 +369,20 @@ Section atomic_snapshot.
@ ⊤∖↑N
<<< pair_content γ (v1, v2), RET (v1, v2) >>>.
Proof.
- iIntros "Hp". iIntros (Φ) "AU". iLöb as "IH".
+ iIntros "Hx". iIntros (Φ) "AU". iLöb as "IH".
wp_pures.
(* ************ 1st readX ********** *)
- iDestruct "Hp" as (l1 l2 ->) "#Hinv". repeat (wp_lam; wp_pures).
+ iDestruct "Hx" as (l1 ->) "#Hinv". repeat (wp_lam; wp_pures).
wp_bind (! #l1)%E.
(* open invariant for 1st read *)
- iInv N as (q_x1 l1' T_x x1) ">Hinvp".
- iDestruct "Hinvp" as (y_x1 v_x1) "[Hl1 [Hl1' [Hl2 [Hpâš« [Ht_x Htime_x]]]]]".
+ iInv N as (q_x1 l1' T_x x1 v_x1) ">[Hl1 [Hl1' [Hxâš« [Ht_x Htime_x]]]]".
iDestruct "Htime_x" as %[Hlookup_x Hdom_x].
wp_load.
iDestruct "Hl1'" as "[Hl1' Hl1'frac]".
- iMod "AU" as (xv yv) "[Hpair [Hclose _]]".
- iDestruct (excl_sync with "Hpâš« Hpair") as %[= -> ->].
- iMod ("Hclose" with "Hpair") as "AU".
+ iMod "AU" as (xv yv) "[[Hx Hy] [Hclose _]]".
+ iDestruct (excl_sync with "Hxâš« Hx") as %[= ->].
+ iMod ("Hclose" with "[Hx Hy]") as "AU".
+ { rewrite /pair_content. iFrame. }
(* duplicate timestamp T_x1 *)
iMod (timestamp_dupl with "Ht_x") as "[Ht_x1âš« Ht_x1â—¯]".
(* close invariant *)
@@ -405,24 +396,24 @@ Section atomic_snapshot.
wp_let.
(* ************ readY ********** *)
repeat (wp_lam; wp_pures). wp_bind (!_)%E.
- iInv N as (q_y l1'_y T_y x_y) ">Hinvp".
- iDestruct "Hinvp" as (y_y v_y) "[Hl1 [Hl1'_y [Hl2 [Hpâš« [Ht_y Htime_y]]]]]".
+ iInv N as (q_y l1'_y T_y x_y v_y) ">[Hl1 [Hl1'_y [Hxâš« [Ht_y Htime_y]]]]".
iDestruct "Htime_y" as %[Hlookup_y Hdom_y].
- wp_load.
(* linearization point *)
- iMod "AU" as (xv yv) "[Hpair Hclose]".
+ clear yv.
+ iMod "AU" as (xv yv) "[[Hx Hy] Hclose]".
+ wp_load.
rewrite /pair_content.
- iDestruct (excl_sync with "Hpâš« Hpair") as %[= -> ->].
+ iDestruct (excl_sync with "Hxâš« Hx") as %[= ->].
destruct (prophecy_to_bool proph_val) eqn:Hproph.
- (* prophecy value is predicting that timestamp has not changed, so we commit *)
(* committing AU *)
- iMod ("Hclose" with "Hpair") as "HΦ".
+ iMod ("Hclose" with "[$Hx $Hy]") as "HΦ".
(* 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.
- iModIntro.
+ iModIntro. iModIntro.
(* closing invariant *)
iSplitR "HΦ Hl1' Ht_x1◯ Ht_y◯ Hpr".
{ iNext. unfold pair_inv. eauto 10 with iFrame. }
@@ -430,8 +421,7 @@ Section atomic_snapshot.
(* ************ 2nd readX ********** *)
repeat (wp_lam; wp_pures). wp_bind (! #l1)%E.
(* open invariant *)
- iInv N as (q_x2 l1'_x2 T_x2 x2) ">Hinvp".
- iDestruct "Hinvp" as (y_x2 v_x2) "[Hl1 [Hl1'_x2 [Hl2 [Hpâš« [Ht_x2 Htime_x2]]]]]".
+ iInv N as (q_x2 l1'_x2 T_x2 x2 v_x2) ">[Hl1 [Hl1'_x2 [Hxâš« [Ht_x2 Htime_x2]]]]".
iDestruct "Htime_x2" as %[Hlookup_x2 Hdom_x2].
iDestruct "Hl1'_x2" as "[Hl1'_x2 Hl1'_x2_frag]".
wp_load.
@@ -461,8 +451,8 @@ Section atomic_snapshot.
}
done.
+ inversion Hproph.
- - iDestruct "Hclose" as "[Hclose _]". iMod ("Hclose" with "Hpair") as "AU".
- iModIntro.
+ - iDestruct "Hclose" as "[Hclose _]". iMod ("Hclose" with "[$Hx $Hy]") as "AU".
+ iModIntro. iModIntro.
(* closing invariant *)
iSplitR "AU Hpr".
{ iNext. unfold pair_inv. eauto 10 with iFrame. }
@@ -470,8 +460,7 @@ Section atomic_snapshot.
(* ************ 2nd readX ********** *)
repeat (wp_lam; wp_proj). wp_let. wp_bind (! #l1)%E.
(* open invariant *)
- iInv N as (q_x2 l1'_x2 T_x2 x2) ">Hinvp".
- iDestruct "Hinvp" as (y_x2 v_x2) "[Hl1 [Hl1'_x2 [Hl2 [Hpâš« [Ht_x2 Htime_x2]]]]]".
+ iInv N as (q_x2 l1'_x2 T_x2 x2 v_x2) "[Hl1 [Hl1'_x2 [Hxâš« [Ht_x2 Htime_x2]]]]".
iDestruct "Hl1'_x2" as "[Hl1'_x2 Hl1'_x2_frag]".
wp_load.
iModIntro. iSplitR "AU Hl1'_x2_frag Hpr". {
--
GitLab