Commit b2c331e6 authored by Marianna Rapoport's avatar Marianna Rapoport

Stop requiring prophecy variables to be mapped to Some location in the invariant

parent 4501f1e0
......@@ -457,6 +457,24 @@ Section cond_counter.
(** Definition of the invariant *)
Definition val_to_some_loc l :=
match l with
| Some (LitV (LitLoc l')) => Some l'
| _ => None
end.
Inductive abstract_state : Set :=
| injl : Z abstract_state
| injr : Z proph abstract_state.
Definition repr (abs : abstract_state) : val :=
match abs with
| injl n =>
InjLV #n
| injr n p =>
InjRV (#n, #p)
end.
Definition own_token γ_t := (own γ_t token)%I.
Definition used_up l γ_h :=
......@@ -466,30 +484,28 @@ Section cond_counter.
(P own γ_h (half_history_frag H) Some l = head H
p Some #l_ghost own γ_n ( Excl' n))%I.
Definition pending_state_wrong_proph P H (n : Z) (p : proph) (l : loc) (γ_h γ_n : gname) :=
(P own γ_h (half_history_frag H) Some l = head H
( v, p v val_to_some_loc v = None) own γ_n ( Excl' n))%I.
Definition accepted_state Q H (p : proph) (l l_ghost : loc) (γ_h : gname) :=
(Q own γ_h (half_history_frag H) Some l = head H
l_ghost {1/2} - p Some #l_ghost)%I.
Definition accepted_state_wrong_proph H (p : proph) (l l_ghost : loc) (γ_h : gname) :=
(own γ_h (half_history_frag H) Some l = head H
l_ghost {1/2} - v, p v val_to_some_loc v = None)%I.
Definition done_state Q (l l_ghost : loc) (γ_t γ_h : gname) :=
((Q own_token γ_t) l_ghost - used_up l γ_h)%I.
Definition state_inv P Q p n (l l_ghost : loc) H (γ_h γ_n γ_t : gname) : iProp Σ :=
(pending_state P H n p l l_ghost γ_h γ_n
pending_state_wrong_proph P H n p l γ_h γ_n
accepted_state Q H p l l_ghost γ_h
accepted_state_wrong_proph H p l l_ghost γ_h
done_state Q l l_ghost γ_t γ_h)%I.
Inductive abstract_state : Set :=
| injl : Z abstract_state
| injr : Z proph abstract_state.
Definition repr (abs : abstract_state) : val :=
match abs with
| injl n =>
InjLV #n
| injr n p =>
InjRV (#n, #p)
end.
Definition pau P Q γs :=
( P - AU << (b : bool) (n : Z), counter_content γs (b, n) >> @ ∖↑N,
<< counter_content γs (b, (if b then n + 1 else n)), COMM Q >>)%I.
......@@ -503,7 +519,6 @@ Section cond_counter.
own γ_b ( Excl' b)
v (p : proph),
l {q} (repr v)
( v (p : proph), p v - (l : loc), v = Some #l)
(( (n : Z) , v = injl n own γ_h (half_history_frag H) own γ_n ( Excl' n))
( (n : Z) (p : proph) l_ghost, v = injr n p
P Q γ_t, inv stateN (state_inv P Q p n l l_ghost H γ_h γ_n γ_t)
......@@ -574,19 +589,23 @@ Section cond_counter.
wp_alloc l_new as "Hl_new".
wp_bind (CAS _ _ _ _ _)%E.
iInv counterN as (b3 l3 H3 q3) "[>Hf [>Hc [>H● [>H◯ [>Hlh3 [>Heq [Hb● Hrest]]]]]]]".
iDestruct "Hrest" as (v' p') "[Hl3' [#Hp Hrest]]".
iDestruct "Hrest" as (v' p') "[Hl3' Hrest]".
iDestruct "Heq" as %[Heq'' Hd'].
iDestruct ((nodup_fresh_loc _ _ _ Hd') with "Hl_new Hlh3") as %Hd''.
(* we must assert that l = l3 because we're the succeeding thread *)
destruct (decide (l3 = l)) as [<- | Hnl].
** (* to apply CAS, we need the prophecy variable, and for that we need
to open the state invariant *)
iInv stateN as "[Pending | [Accepted | Done]]".
iInv stateN as "[Pending | [Pending_wp | [Accepted | [Accepted_wp | Done]]]]".
*** (* Pending: contradiction *)
iDestruct "Pending" as "[_ >[_ [_ [_ Hn●']]]]".
iCombine "Hn●" "Hn●'" as "Contra".
iDestruct (own_valid with "Contra") as %Contra. inversion Contra.
*** (* Accepted *)
*** (* Pending (wrong proph): contradiction *)
iDestruct "Pending_wp" as "[_ [_ >[_ [_ Hn●']]]]".
iCombine "Hn●" "Hn●'" as "Contra".
iDestruct (own_valid with "Contra") as %Contra. inversion Contra.
*** (* Accepted: CAS and update to Done *)
iDestruct "Accepted" as "[Q >[Hh◯ [Heq' [Hl_ghost_inv Hp']]]]".
iDestruct (sync_histories with "H◯ Hh◯") as %->.
wp_apply (wp_cas_suc_proph with "[Hc Hp']");
......@@ -604,7 +623,7 @@ Section cond_counter.
iDestruct (extract_snapshot with "H◯'") as "#Hs".
iSplitL "Hl_ghost_inv Hl_ghost Q".
(* update state to Done *)
{ iNext. iRight. iRight.
{ iNext. repeat iRight.
iDestruct "Hl_ghost_inv" as (v'') "Hl_ghost''".
iDestruct (mapsto_agree with "Hl_ghost Hl_ghost''") as %<-.
iCombine "Hl_ghost" "Hl_ghost''" as "Hl_ghost'".
......@@ -627,38 +646,63 @@ Section cond_counter.
eauto 10 with iFrame. }
iApply wp_fupd. wp_seq.
iApply "HQ". iModIntro. iIntros "Ht".
iInv stateN as "[Pending | [Accepted | Done]]".
iInv stateN as "[Pending | [Pending_wp | [Accepted | [Accepted_wp | Done]]]]".
**** (* Pending: contradiction *)
iDestruct "Pending" as "[_ >[Hh◯ _]]".
iInv counterN as (b5 l5 H5 q5) "[>Hf [>Hc [>H● [>H◯ [Hlh3 [>Heq [Hb● Hrest]]]]]]]".
iDestruct (sync_histories with "H◯ Hh◯") as %->.
by iDestruct (sync_snapshot with "H● Hs") as %?%suffix_cons_not.
**** (* Pending (wrong proph): contradiction *)
iDestruct "Pending_wp" as "[_ >[Hh◯ _]]".
iInv counterN as (b5 l5 H5 q5) "[>Hf [>Hc [>H● [>H◯ [Hlh3 [>Heq [Hb● Hrest]]]]]]]".
iDestruct (sync_histories with "H◯ Hh◯") as %->.
by iDestruct (sync_snapshot with "H● Hs") as %?%suffix_cons_not.
**** (* Accepted: contradiction *)
iDestruct "Accepted" as "[_ [>Hh◯ _]]".
iInv counterN as (b5 l5 H5 q5) "[>Hf [>Hc [>H● [>H◯ [Hlh3 [>Heq [Hb● Hrest]]]]]]]".
iDestruct (sync_histories with "H◯ Hh◯") as %->.
by iDestruct (sync_snapshot with "H● Hs") as %?%suffix_cons_not.
**** (* Accepted (wrong proph): contradiction *)
iDestruct "Accepted_wp" as "[>Hh◯ _]".
iInv counterN as (b5 l5 H5 q5) "[>Hf [>Hc [>H● [>H◯ [Hlh3 [>Heq [Hb● Hrest]]]]]]]".
iDestruct (sync_histories with "H◯ Hh◯") as %->.
by iDestruct (sync_snapshot with "H● Hs") as %?%suffix_cons_not.
**** (* Done *)
iDestruct "Done" as "[QT [>Hlghost Usedup]]".
iModIntro. iDestruct (later_intro with "Ht") as "Ht".
iDestruct (later_or with "QT") as "[Q | T]"; last first.
{ iCombine "Ht" "T" as "Contra". iDestruct (own_valid with "Contra") as "#Contra'".
iSplitL; try iModIntro; try iNext; iDestruct "Contra'" as %Contra; inversion Contra. }
iSplitR "Q"; last done. iNext. iRight. iRight. iFrame.
iSplitR "Q"; last done. iNext. repeat iRight. iFrame.
*** (* Accepted (wrong proph): CAS and contradiction *)
iDestruct "Accepted_wp" as ">[Hh◯ [Heq' [Hl_ghost_inv Hp']]]".
iDestruct (sync_histories with "H◯ Hh◯") as %->.
iDestruct "Hp'" as (v) "[Hp' Heq'']". iDestruct "Heq''" as %Heq'.
wp_apply (wp_cas_suc_proph with "[Hc Hp']");
[ by left | done | by iFrame | ..].
iIntros "[_ Heq]". iDestruct "Heq" as %->. inversion Heq'.
*** (* Done: contradiction *)
iDestruct "Done" as "[QT [>Hlghost Usedup]]".
iDestruct "Hlghost" as (v) "Hlghost".
by iDestruct (mapsto_valid_2 with "Hl_ghost Hlghost") as %?.
** (* we are the succeeding thread, so CAS can't fail: contradiction *)
iInv stateN as "[Pending | [Accepted | Done]]".
iInv stateN as "[Pending | [Pending_wp | [Accepted | [Accepted_wp | Done]]]]".
*** (* Pending: contradiction *)
iDestruct "Pending" as "[_ >[_ [_ [_ Hn●']]]]".
iCombine "Hn●'" "Hn●" as "Contra".
iDestruct (own_valid with "Contra") as %Contra. inversion Contra.
*** (* Pending (wrong proph): contradiction *)
iDestruct "Pending_wp" as "[_ >[_ [_ [_ Hn●']]]]".
iCombine "Hn●'" "Hn●" as "Contra".
iDestruct (own_valid with "Contra") as %Contra. inversion Contra.
*** (* Accepted: contradiction *)
iDestruct "Accepted" as "[_ >[Hh◯ _]]".
iDestruct (sync_histories with "Hh◯ H◯") as %->. rewrite <- Heq'' in Heq.
by inversion Heq.
*** (* Accepted (wrong proph): contradiction *)
iDestruct "Accepted_wp" as ">[Hh◯ _]".
iDestruct (sync_histories with "Hh◯ H◯") as %->. rewrite <- Heq'' in Heq.
by inversion Heq.
*** (* Done: contradiction *)
wp_apply (wp_cas_fail with "Hc"); [ done | by intros [=] | by left | .. ].
iDestruct "Done" as "[_ [Hlghost _]]".
......@@ -687,15 +731,25 @@ Section cond_counter.
iDestruct (sync_snapshot with "H● Hs1") as %H12.
destruct (decide (l2 = l)) as [<- | Hn].
* (* CAS succeeds: contradiction (b/c we're failing thread) *)
iInv stateN as "[Pending | [Accepted | Done]]".
iInv stateN as "[Pending | [Pending_wp | [Accepted | [Accepted_wp | Done]]]]".
** (* Pending: contradiction *)
iDestruct "Pending" as "[P >[Hh◯ [Heq' [Hp' Hn●']]]]".
wp_apply (wp_cas_suc_proph with "[Hc Hp']"); [ by left | done | by iFrame | ..].
iIntros "[Hc Contra]". iDestruct "Contra" as %[=->]. done.
** (* Pending (wrong proph): contradiction *)
iDestruct "Pending_wp" as "[P >[Hh◯ [Heq' [Hp' Hn●']]]]".
iDestruct "Hp'" as (v) "[Hp' Heq'']". iDestruct "Heq''" as %Heq'.
wp_apply (wp_cas_suc_proph with "[Hc Hp']"); [ by left | done | by iFrame | ..].
iIntros "[Hc Contra]". iDestruct "Contra" as %[=->]. done.
** (* Accepted: contradiction *)
iDestruct "Accepted" as "[Q >[Hh◯ [Heq' [Hl_ghost_inv Hp']]]]".
wp_apply (wp_cas_suc_proph with "[Hc Hp']"); [ by left | done | by iFrame | ..].
iIntros "[Hc Contra]". iDestruct "Contra" as %[=->]. done.
** (* Accepted (wrong proph): contradiction *)
iDestruct "Accepted_wp" as ">[Hh◯ [Heq' [Hl_ghost_inv Hp']]]".
iDestruct "Hp'" as (v) "[Hp' Heq'']". iDestruct "Heq''" as %Heq'.
wp_apply (wp_cas_suc_proph with "[Hc Hp']"); [ by left | done | by iFrame | ..].
iIntros "[Hc Contra]". iDestruct "Contra" as %[=->]. done.
** (* Done : contradiction *)
iDestruct "Done" as "[QT [>Hlghost Usedup]]".
iDestruct "Usedup" as (H') "[Hs >Usedup]". iDestruct "Usedup" as %[Hin' Hn].
......@@ -717,7 +771,7 @@ Section cond_counter.
wp_seq. iApply "HQ". iIntros "Ht".
iInv counterN as (b3 l3 H3 q3) "[>Hf [>Hc [>H● [>H◯ [Hlh [>Heq [Hb● Hrest]]]]]]]".
iDestruct "Heq" as %[Heq'' Hd''].
iInv stateN as "[Pending | [Accepted | Done]]".
iInv stateN as "[Pending | [Pending_wp | [Accepted | [Accepted_wp | Done]]]]".
** (* Pending: contradiction *)
iDestruct "Pending" as "[_ >[Hh◯ [Heq' _]]]".
iDestruct "Heq'" as %Heq'''.
......@@ -725,6 +779,13 @@ Section cond_counter.
iDestruct (sync_snapshot with "H● Hs") as %Hs.
rewrite <- Heq'' in Heq'''. inversion Heq'''; subst.
exfalso. by eapply (nodup_suffix_contradiction _ _ _ _ _ _ Heq Heq').
** (* Pending (wrong proph): contradiction *)
iDestruct "Pending_wp" as "[_ >[Hh◯ [Heq' _]]]".
iDestruct "Heq'" as %Heq'''.
iDestruct (sync_histories with "H◯ Hh◯") as %->.
iDestruct (sync_snapshot with "H● Hs") as %Hs.
rewrite <- Heq'' in Heq'''. inversion Heq'''; subst.
exfalso. by eapply (nodup_suffix_contradiction _ _ _ _ _ _ Heq Heq').
** (* Accepted: contradiction *)
iDestruct "Accepted" as "[_ >[Hh◯ [Heq' _]]]".
iDestruct "Heq'" as %Heq'''.
......@@ -732,10 +793,17 @@ Section cond_counter.
iDestruct (sync_snapshot with "H● Hs") as %Hs.
rewrite <- Heq'' in Heq'''. inversion Heq'''; subst l3.
exfalso. by eapply (nodup_suffix_contradiction _ _ _ _ _ _ Heq Heq').
** (* Accepted (wrong proph): contradiction *)
iDestruct "Accepted_wp" as ">[Hh◯ [Heq' _]]".
iDestruct "Heq'" as %Heq'''.
iDestruct (sync_histories with "H◯ Hh◯") as %->.
iDestruct (sync_snapshot with "H● Hs") as %Hs.
rewrite <- Heq'' in Heq'''. inversion Heq'''; subst l3.
exfalso. by eapply (nodup_suffix_contradiction _ _ _ _ _ _ Heq Heq').
** (* Done *)
iDestruct "Done" as "[[Q | >T] Hrest']".
*** iModIntro.
iSplitL "Ht Hrest'"; first by (iNext; iRight; iRight; iFrame).
iSplitL "Ht Hrest'"; first by (iNext; repeat iRight; iFrame).
iModIntro. iSplitR "Q".
{ iNext. iExists _, _, _, _. eauto 10 with iFrame. }
done.
......@@ -763,14 +831,13 @@ Section cond_counter.
(* open outer invariant to read `f` *)
iInv counterN as (b1 l1 H1 q1) "[>Hf [>Hc [>H● [>H◯ [Hlh1 [>Heq [Hb● Hrest]]]]]]]".
iDestruct "Heq" as %[Heq Hd].
iDestruct "Hrest" as (v1 p1) "[[Hl1 Hl1'] [#Hp Hrest]]".
iDestruct "Hrest" as (v1 p1) "[[Hl1 Hl1'] Hrest]".
wp_load.
iDestruct "Hp" as "#Hp".
(* two different proofs depending on whether we are succeeding thread *)
destruct (decide (l_ghost_inv = l_ghost)) as [-> | Hnl].
- (* we are the succeeding thread *)
(* we need to move from pending to accepted. *)
iInv stateN as "[Pending | [Accepted | Done]]".
iInv stateN as "[Pending | [Pending_wp | [Accepted | [Accepted_wp | Done]]]]".
+ (* Pending: update to accepted *)
iDestruct "Pending" as "[P >[Hh◯ [Heq [Hp' Hn●]]]]". iDestruct "Heq" as %Heq'.
iDestruct ("PAU" with "P") as ">AU".
......@@ -786,7 +853,29 @@ Section cond_counter.
iMod ("Hclose" with "[Hn◯ Hb◯]") as "Q"; first by iFrame.
(* close state inv *)
iModIntro. iSplitL "Q H◯ Hl_ghost' Hp'".
{ iNext. iRight. iLeft. iFrame. iSplit; first done. by iExists _. }
{ iNext. iRight. iRight. iLeft. iFrame. iSplit; first done. by iExists _. }
(* close outer inv *)
iModIntro. iSplitR "Hl_ghost'2 HQ Hn●".
{ iNext. iExists _, _, _, _. iFrame. iSplit; first done. iExists _, p. eauto with iFrame. }
destruct b2; wp_if; [ wp_op | .. ];
iApply ((complete_succeeding_thread_pending _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ Heq)
with "InvC InvS PAU Hl_ghost'2 HQ Hn●").
+ (* Pending (wrong proph): update to accepted (wrong proph) *)
iDestruct "Pending_wp" as "[P >[Hh◯ [Heq [Hp' Hn●]]]]". iDestruct "Heq" as %Heq'.
iDestruct ("PAU" with "P") as ">AU".
(* open AU, sync flag and counter *)
iMod "AU" as (b2 n2) "[CC [_ Hclose]]".
iDestruct "CC" as "[Hb◯ Hn◯]". simpl.
iDestruct (sync_flag_values with "Hb● Hb◯") as %->.
iDestruct (sync_counter_values with "Hn● Hn◯") as %->.
iDestruct (sync_histories with "H◯ Hh◯") as %->.
rewrite <- Heq in Heq'. inversion_clear Heq'; subst.
iMod (update_counter_value _ _ _ (if b2 then n2 + 1 else n2) with "Hn● Hn◯")
as "[Hn● Hn◯]".
iMod ("Hclose" with "[Hn◯ Hb◯]") as "Q"; first by iFrame.
(* close state inv *)
iModIntro. iSplitL "Q H◯ Hl_ghost' Hp'".
{ iNext. iRight. iRight. iRight. iLeft. iFrame. iSplit; first done. by iExists _. }
(* close outer inv *)
iModIntro. iSplitR "Hl_ghost'2 HQ Hn●".
{ iNext. iExists _, _, _, _. iFrame. iSplit; first done. iExists _, p. eauto with iFrame. }
......@@ -798,6 +887,11 @@ Section cond_counter.
iDestruct "Hl_ghost_inv" as (v) "Hlghost".
iCombine "Hl_ghost'" "Hl_ghost'2" as "Hl_ghost'".
by iDestruct (mapsto_valid_2 with "Hlghost Hl_ghost'") as %?.
+ (* Accepted (wrong proph): contradiction *)
iDestruct "Accepted_wp" as ">[Hh◯ [Heq' [Hl_ghost_inv Hp']]]".
iDestruct "Hl_ghost_inv" as (v) "Hlghost".
iCombine "Hl_ghost'" "Hl_ghost'2" as "Hl_ghost'".
by iDestruct (mapsto_valid_2 with "Hlghost Hl_ghost'") as %?.
+ (* Done: contradiction *)
iDestruct "Done" as "[QT [>Hlghost Usedup]]".
iDestruct "Hlghost" as (v) "Hlghost".
......@@ -807,16 +901,26 @@ Section cond_counter.
(* extract history and assert that it contains l *)
iDestruct (extract_snapshot with "H◯") as "#Hs1".
iAssert (|={ counterN}=> (In l H1 own γ_h (full_history_auth H1)))%I with "[H●]" as "Hin". {
iInv stateN as "[Pending | [Accepted | Done]]".
iInv stateN as "[Pending | [Pending_wp | [Accepted | [Accepted_wp | Done]]]]".
- (* Pending *)
iDestruct "Pending" as "[H1 >[Hh◯ [Heq' H2]]]".
iDestruct (sync_snapshot with "H● Hh◯") as %Hs1. iDestruct "Heq'" as %Heq'.
iModIntro. iSplitR "H●". { iNext. iLeft. iFrame. done. }
iModIntro. iFrame. iPureIntro. by eapply suffix_in_head.
- (* Pending (wrong proph) *)
iDestruct "Pending_wp" as "[H1 >[Hh◯ [Heq' [Hp' Hn●]]]]".
iDestruct (sync_snapshot with "H● Hh◯") as %Hs1. iDestruct "Heq'" as %Heq'.
iModIntro. iSplitR "H●". { iNext. iRight. iLeft. iFrame. done. }
iModIntro. iFrame. iPureIntro. by eapply suffix_in_head.
- (* Accepted *)
iDestruct "Accepted" as "[H1 >[Hh◯ [Heq' H2]]]".
iDestruct (sync_snapshot with "H● Hh◯") as %Hs1. iDestruct "Heq'" as %Heq'.
iModIntro. iSplitR "H●". { iNext. iRight. iLeft. iFrame. done. }
iModIntro. iSplitR "H●". { iNext. iRight. iRight. iLeft. iFrame. done. }
iModIntro. iFrame. iPureIntro. by eapply suffix_in_head.
- (* Accepted (wrong proph) *)
iDestruct "Accepted_wp" as ">[Hh◯ [Heq' H2]]".
iDestruct (sync_snapshot with "H● Hh◯") as %Hs1. iDestruct "Heq'" as %Heq'.
iModIntro. iSplitR "H●". { iNext. iRight. iRight. iRight. iLeft. iFrame. done. }
iModIntro. iFrame. iPureIntro. by eapply suffix_in_head.
- (* Pending *)
iDestruct "Done" as "[QT [>Hlghost Usedup]]".
......@@ -824,7 +928,7 @@ Section cond_counter.
iMod (intuitionistically_elim with "Hs") as "Hs".
iDestruct (sync_snapshot with "H● Hs") as %Hs'.
iModIntro. iSplitR "H●".
{ iNext. iRight. iRight. iFrame. iExists _. iSplit; last by iPureIntro.
{ iNext. repeat iRight. iFrame. iExists _. iSplit; last by iPureIntro.
iDestruct "Hs" as "#Hs". iModIntro. iApply "Hs". }
iModIntro. iSplit; last done.
iPureIntro. by eapply suffix_in.
......@@ -836,7 +940,7 @@ Section cond_counter.
iSplit; first done.
iDestruct "Hrest" as "[Hrest1 | Hrest2]"; iExists _, p; eauto 10 with iFrame. }
(* two equal proofs depending on value of b1 *)
destruct b1 as [-> | Hn]; wp_if; [ wp_op | ..];
destruct b1 as [? | ?]; wp_if; [ wp_op | ..];
iApply ((complete_failing_thread _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ Heq Hin Hnl)
with "InvC InvS PAU Hs1 HQ").
Qed.
......@@ -857,7 +961,7 @@ Section cond_counter.
iApply wp_atomic_intro. iIntros (Φ) "AU". iLöb as "IH".
repeat (wp_lam; wp_proj). wp_lam. wp_bind (!_)%E.
iInv counterN as (b' l' H' q) "[>Hf [>Hc [>H● [>H◯ [Hlh [>Heq [>Hb● Hrest]]]]]]]".
iDestruct "Hrest" as (v p) "[>[Hl' Hl'2] [#Hp InvC_rest]]".
iDestruct "Hrest" as (v p) "[>[Hl' Hl'2] InvC_rest]".
wp_load.
destruct v as [n' | n'].
- (* l' ↦ injL *)
......@@ -879,7 +983,7 @@ Section cond_counter.
wp_cas_suc.
(* We need to update the half history with `ly`.
For that we will need to get the second half of the history *)
iDestruct "Hrest" as (v _) "[Hl'2 [_ [InjL | InjR]]]";
iDestruct "Hrest" as (v _) "[Hl'2 [InjL | InjR]]";
iPoseProof (mapsto_agree with "Hl' Hl'2") as "#Heq"; last first.
{ (* injR: contradiction *)
iDestruct "InjR" as (???) "[Heq' InjR_rest]".
......@@ -888,25 +992,39 @@ Section cond_counter.
iDestruct "InjL" as (n'') "[Heq' [H◯' Hn●]]".
iDestruct "Heq'" as %->. simpl. iDestruct "Heq" as %[=<-].
iPoseProof ((update_history _ _ ly) with "H● H◯ H◯'") as ">[H● [H◯' H◯'']]".
iPoseProof ("Hp" with "Hp'") as "#Heq". iDestruct "Heq" as %[v' ->].
iDestruct (laterable with "AU") as (AU_later) "[AU #AU_back]".
iDestruct (own_alloc token) as ">Ht"; first by apply auth_auth_valid.
iDestruct "Ht" as (γ_t) "Token".
iMod (inv_alloc stateN _ (state_inv AU_later _ _ _ _ _ _ _ _ γ_t)
destruct (val_to_some_loc l_ghost) eqn:H.
* destruct l_ghost as [l_ghost|]; last by inversion H.
destruct l_ghost; inversion H. destruct l0; inversion H. subst.
iMod (inv_alloc stateN _ (state_inv AU_later _ _ _ _ _ _ _ _ γ_t)
with "[AU H◯' Hp' Hn●]") as "#Hinv".
{ iNext. iLeft. iFrame. done.
(* if we don't require in [counter_inv] that all prophecy variables
are mapped to [Some] value, the problem will come up here *) }
iModIntro. iDestruct "Hly" as "[Hly1 Hly2]". iSplitR "Hl' Token". {
{ iNext. iLeft. iFrame. done. }
iModIntro. iDestruct "Hly" as "[Hly1 Hly2]". iSplitR "Hl' Token". {
(* close invariant *)
iModIntro. iExists _, _, _, _.
iFrame. iSplitL "Hly1"; first by eauto. iSplit; first by iPureIntro.
iExists (injr n' p'), p'. iFrame. iSplit; first done. iRight.
iExists (injr n' p'), p'. iFrame. iRight.
iExists _, _, _. iSplit; first done. iExists _, _, _. iSplit; done.
}
wp_if.
wp_apply complete_spec; [iExists _, _, _, _, _; eauto | done | done | done | ..].
iIntros "Ht". iMod ("Ht" with "Token") as "Φ". wp_seq. by wp_seq.
}
wp_if.
wp_apply complete_spec; [iExists _, _, _, _, _; eauto | done | done | done | ..].
iIntros "Ht". iMod ("Ht" with "Token") as "Φ". wp_seq. by wp_seq.
* iMod (inv_alloc stateN _ (state_inv AU_later _ _ _ ly l' _ _ _ γ_t)
with "[AU H◯' Hp' Hn●]") as "#Hinv".
{ iNext. iRight. iLeft. iFrame. iSplit; first done.
iExists _; by iFrame. }
iModIntro. iDestruct "Hly" as "[Hly1 Hly2]". iSplitR "Hl' Token". {
(* close invariant *)
iModIntro. iExists _, _, _, _.
iFrame. iSplitL "Hly1"; first by eauto. iSplit; first by iPureIntro.
iExists (injr n' p'), p'. iFrame. iRight.
iExists _, _, _. iSplit; first done. iExists _, _, _. iSplit; done.
}
wp_if.
wp_apply complete_spec; [iExists _, _, _, _, _; eauto | done | done | done | ..].
iIntros "Ht". iMod ("Ht" with "Token") as "Φ". wp_seq. by wp_seq.
+ (* CAS fails: closing invariant and invoking IH *)
wp_cas_fail.
iModIntro. iSplitR "Hl' AU".
......@@ -926,7 +1044,6 @@ Section cond_counter.
{ iModIntro. iExists _, _, _, _. iFrame.
iExists _, p.
iSplitL "Hl'2"; first done.
iSplit; first done.
iRight. eauto 10 with iFrame. }
wp_let. wp_load.
wp_match. repeat wp_proj.
......
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