Commit fb95184a authored by Gaurav Parthasarathy's avatar Gaurav Parthasarathy

extract Q from match clause in the accepted state

parent 353e2900
......@@ -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. *)
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment