From 5c19178aab7fa286bfffbad6b72b087e7efafba4 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 1 Oct 2021 14:33:54 -0400
Subject: [PATCH] adjust for framing not doing AsFractional any more
---
theories/logatom/conditional_increment/cinc.v | 24 ++++++++++++-------
theories/logatom/flat_combiner/flat.v | 2 +-
theories/logatom/rdcss/rdcss.v | 6 +++--
3 files changed, 21 insertions(+), 11 deletions(-)
diff --git a/theories/logatom/conditional_increment/cinc.v b/theories/logatom/conditional_increment/cinc.v
index aa5bee74..5d2901e5 100644
--- a/theories/logatom/conditional_increment/cinc.v
+++ b/theories/logatom/conditional_increment/cinc.v
@@ -300,10 +300,11 @@ Section conditional_counter.
{ iNext. iExists _. iFrame "Hp'". iRight. unfold done_state.
iFrame "#∗". iDestruct "Hl_ghost_inv" as (v) "Hl_ghost_inv".
iDestruct (mapsto_agree with "Hl_ghost Hl_ghost_inv") as %<-.
+ iCombine "Hl_ghost Hl_ghost_inv" as "Hl_ghost".
iSplitR "Hl"; iExists _; iFrame. }
iModIntro. iSplitR "HQ".
{ iNext. iDestruct "Hc" as "[Hc1 Hc2]".
- iExists l_new, _, (Quiescent n). iFrame. }
+ iExists l_new, _, (Quiescent n). iFrame. iSplitL "Hl_new"; done. }
wp_seq. iApply "HQ".
iApply state_done_extract_Q; done.
Qed.
@@ -346,7 +347,8 @@ Section conditional_counter.
wp_apply (wp_resolve with "Hp"); first done. wp_cmpxchg_fail.
iIntros "!>" (vs' ->) "Hp". iModIntro.
iSplitL "Done Hp". { iNext. iExists _. iFrame "#∗". } iModIntro.
- iSplitL "Hc Hrest Hl Hl'". { eauto 10 with iFrame. }
+ iCombine "Hl Hl'" as "Hl".
+ iSplitL "Hc Hrest Hl". { eauto 10 with iFrame. }
wp_seq. iApply "HQ".
iApply state_done_extract_Q; done.
Qed.
@@ -443,7 +445,8 @@ Section conditional_counter.
wp_load. destruct s as [n|f' n' p'].
- iDestruct "Hrest" as "(Hc' & Hv)".
iModIntro. iSplitR "AU Hl'".
- { iModIntro. iExists _, (q/2)%Qp, (Quiescent n). iFrame. }
+ { iModIntro. iExists _, (q/2)%Qp, (Quiescent n).
+ iCombine "Hl Hl''" as "Hl". iFrame. }
wp_let. wp_load. wp_match. wp_apply wp_new_proph; first done.
iIntros (l_ghost p') "Hp'".
wp_let. wp_alloc ly as "Hly".
@@ -471,7 +474,9 @@ Section conditional_counter.
iFrame. destruct (val_to_some_loc l_ghost); simpl; done. }
iModIntro. iDestruct "Hly" as "[Hly1 Hly2]". iSplitR "Hl' Token". {
(* close invariant *)
- iNext. iExists _, _, (Updating f n p'). eauto 10 with iFrame.
+ iNext. iExists _, _, (Updating f n p'). iFrame.
+ iSplitR "Hl"; last by eauto 10 with iFrame.
+ iSplitL "Hly1"; done.
}
wp_pures. wp_apply complete_spec; [done..|].
iIntros "Ht". iMod ("Ht" with "Token") as "Φ". wp_seq. by wp_lam.
@@ -486,7 +491,8 @@ Section conditional_counter.
iDestruct "Hrest" as (P Q l_ghost γ_t γ_s) "(#InvS & #P_AU & #Hgc)".
iSplitR "Hl' AU".
(* close invariant *)
- { iModIntro. iExists _, _, (Updating f' n' p'). iFrame. eauto 10 with iFrame. }
+ { iModIntro. iExists _, _, (Updating f' n' p'). iFrame.
+ iCombine "Hl Hl''" as "Hl". eauto 10 with iFrame. }
wp_let. wp_load. wp_match. wp_pures.
wp_apply complete_spec; [done..|].
iIntros "_". wp_seq. by iApply "IH".
@@ -507,8 +513,8 @@ Section conditional_counter.
iMod (inv_alloc counterN _ (counter_inv γ_n l_c)
with "[Hl_c Hl_n Hn●]") as "#InvC".
{ iNext. iDestruct "Hl_c" as "[Hl_c1 Hl_c2]".
- iDestruct "Hl_n" as "[??]".
- iExists l_n, (1/2)%Qp, (Quiescent 0). iFrame. }
+ iExists l_n, (1/2)%Qp, (Quiescent 0). iFrame.
+ rewrite Qp_half_half. done. }
iModIntro.
iApply ("HΦ" $! #l_c γ_n).
iSplitR; last by iFrame. iExists _. eauto with iFrame.
@@ -531,11 +537,13 @@ Section conditional_counter.
iMod ("Hclose" with "Hn◯") as "HΦ".
iModIntro. iSplitR "HΦ Hl'". {
iNext. iExists c, (q/2)%Qp, (Quiescent au_n). iFrame.
+ iSplitL "Hl"; done.
}
wp_let. wp_load. wp_match. iApply "HΦ".
- iDestruct "Hrest" as (P Q l_ghost γ_t γ_s) "(#InvS & #PAU & #Hgc)".
iModIntro. iSplitR "AU Hl'". {
- iNext. iExists c, (q/2)%Qp, (Updating _ _ p). eauto 10 with iFrame.
+ iNext. iExists c, (q/2)%Qp, (Updating _ _ p).
+ iCombine "Hl Hl''" as "Hl". eauto 10 with iFrame.
}
wp_let. wp_load. wp_pures. wp_bind (complete _ _ _ _ _)%E.
wp_apply complete_spec; [done..|].
diff --git a/theories/logatom/flat_combiner/flat.v b/theories/logatom/flat_combiner/flat.v
index 7c838969..d23a94eb 100644
--- a/theories/logatom/flat_combiner/flat.v
+++ b/theories/logatom/flat_combiner/flat.v
@@ -166,7 +166,7 @@ Section proof.
* iDestruct "Hp" as (? x5) ">(Hp & Hx & Hor & Ho4)".
wp_store. iDestruct (m_frag_agree' with "Hx Hx2") as "[Hx %]".
subst. rewrite Qp_div_2. iMod ("Hclose" with "[-HR Hor HΦ]").
- { iNext. iDestruct "Hp" as "[Hp1 Hp2]". iRight. iRight.
+ { iNext. iRight. iRight.
iRight. iExists _, v. iFrame. iExists Q. iFrame. }
iApply "HΦ". iFrame. done.
* iDestruct "Hp" as (? ?) "[? Hs]". iDestruct "Hs" as (?) "(_ & _ & _ & >Ho1' & _)".
diff --git a/theories/logatom/rdcss/rdcss.v b/theories/logatom/rdcss/rdcss.v
index ac2e0be3..6e4cf31a 100644
--- a/theories/logatom/rdcss/rdcss.v
+++ b/theories/logatom/rdcss/rdcss.v
@@ -622,7 +622,8 @@ Section rdcss.
iDestruct "Hm1'_unbox" as %Hm1'_unbox.
iSplitR "AU Hld2 Hld Hp".
(* close invariant, retain some permission to l_descr', so it can be read later *)
- { iModIntro. iExists (Updating l_descr' l_m' m1' n1' n2' p'). eauto 15 with iFrame. }
+ { iModIntro. iExists (Updating l_descr' l_m' m1' n1' n2' p').
+ iCombine "Hld1 Hld3" as "Hld". eauto 15 with iFrame. }
wp_pures.
wp_apply (complete_spec with "[] [] [] [] [] [$Hld2]"); [done..|].
iIntros "_". wp_seq. wp_pures.
@@ -670,7 +671,8 @@ Section rdcss.
- iDestruct "Hrest" as (q P Q tid_ghost γ_t γ_s γ_a)
"(% & [Hld [Hld' Hld'']] & #InvS & #PAU & #GC)".
iModIntro. iSplitR "AU Hld'".
- { iExists (Updating l_descr l_m m1 n1 n2 p). eauto 15 with iFrame. }
+ { iExists (Updating l_descr l_m m1 n1 n2 p).
+ iCombine "Hld Hld''" as "Hld". eauto 15 with iFrame. }
wp_match.
wp_apply (complete_spec with "[] [] [] [] [] [$Hld']"); [done..|].
iIntros "Ht". wp_seq. iApply "IH". iApply "AU".
--
GitLab