From fb95184a89588c7daf52ce0e695008c71fa74b91 Mon Sep 17 00:00:00 2001
From: Gaurav Parthasarathy <gauravp@student.ethz.ch>
Date: Mon, 8 Jul 2019 15:13:16 +0200
Subject: [PATCH] extract Q from match clause in the accepted state
---
theories/logatom/rdcss/rdcss.v | 8 ++++----
1 file changed, 4 insertions(+), 4 deletions(-)
diff --git a/theories/logatom/rdcss/rdcss.v b/theories/logatom/rdcss/rdcss.v
index 27a30a5..85a975a 100644
--- a/theories/logatom/rdcss/rdcss.v
+++ b/theories/logatom/rdcss/rdcss.v
@@ -186,10 +186,10 @@ Section rdcss.
(* After the prophecy said we are going to win the race, we commit and run the AU,
switching from [pending] to [accepted]. *)
Definition accepted_state Q (proph_winner : option proph_id) (p_ghost_winner : proph_id) :=
- ((∃ vs, proph p_ghost_winner vs) ∗
+ ((∃ vs, proph p_ghost_winner vs) ∗ Q ∗
match proph_winner with
None => True
- | Some p => ⌜p = p_ghost_winner⌠∗ Q
+ | Some p => ⌜p = p_ghost_winnerâŒ
end)%I.
(* The same thread then wins the CmpXchg and moves from [accepted] to [done].
@@ -342,7 +342,7 @@ Section rdcss.
wp_apply (wp_resolve with "Hp"); first done. wp_cmpxchg_suc.
iIntros (vs'' ->) "Hp'". simpl.
(* Update to Done. *)
- iDestruct "Accepted" as "[Hp_phost_inv [HEq Q]]".
+ iDestruct "Accepted" as "[Hp_phost_inv [Q Heq]]".
iMod (own_update with "Hs") as "Hs".
{ apply (cmra_update_exclusive (Cinr (to_agree ()))). done. }
iDestruct "Hs" as "#Hs'". iModIntro.
@@ -378,7 +378,7 @@ Section rdcss.
iIntros (vs'' ->). simpl.
iDestruct "State" as "[Pending | Accepted]".
+ iDestruct "Pending" as "[_ [Hvs _]]". iDestruct "Hvs" as %Hvs. by inversion Hvs.
- + iDestruct "Accepted" as "[_ [Hvs _]]". iDestruct "Hvs" as %Hvs. by inversion Hvs.
+ + iDestruct "Accepted" as "[_ [_ Hvs]]". iDestruct "Hvs" as %Hvs. by inversion Hvs.
}
(* So, we know our protocol is [Done]. *)
(* It must be that (state_to_val s) ≠(InjRV l_descr) because we are in the failing thread. *)
--
GitLab