Commit d3f1f876 authored by Marianna Rapoport's avatar Marianna Rapoport
Browse files

Pass over Ralf's comments on Commit 851f05c2

parent a655f886
......@@ -490,11 +490,14 @@ Definition state_upd_used_proph_id (f: gset proph_id → gset proph_id) (σ: sta
{| heap := σ.(heap); used_proph_id := f σ.(used_proph_id) |}.
Arguments state_upd_used_proph_id _ !_ /.
Local Notation NONEV := (InjLV (LitV LitUnit)) (only parsing).
Local Notation SOMEV x := (InjRV x) (only parsing).
(** We extend CAS to support atomic resolution of prophecy variables as follows:
[CAS p e1 e1 pv1 pv2]
where [pv1] and [pv2] are values of type [option (proph * val)].
If [CAS p e1 e2] succeeds, and if [pv1 = Some (p, v)], we atomically resolve the
prophecy variable [p] to [v]. If the [CAS] fails, we do the same of [pv2]:
prophecy variable [p] to [v]. If the [CAS] fails, we do the same with [pv2]:
[let b = CAS p e1 e2 ;;
match (if b then pv1 else pv2) with
......@@ -504,12 +507,14 @@ Arguments state_upd_used_proph_id _ !_ /.
The following function takes a value and extracts its encoding
of an optional prophecy-value pair.
If [extract_proph_resolve] returns [None], it indicates an invalid encoding,
whereas [Some None] means that it's a valid encoding of no pair.
*)
Definition extract_proph_resolve (v : val) : option (option (proph_id * val)) :=
match v with
| InjLV (LitV LitUnit) =>
| NONEV =>
Some None
| InjRV (PairV (LitV (LitProphecy p)) v') =>
| SOMEV (PairV (LitV (LitProphecy p)) v') =>
Some (Some (p, v'))
| _ =>
None
......@@ -554,7 +559,7 @@ Inductive head_step : expr → state → list observation → expr → state →
(Val $ LitV $ LitLoc l) (state_upd_heap <[l:=v]> σ)
[]
| LoadS l v σ :
σ.(heap) !! l = Some v
σ.(heap) !! l = Some v
head_step (Load (Val $ LitV $ LitLoc l)) σ [] (of_val v) σ []
| StoreS l v σ :
is_Some (σ.(heap) !! l)
......@@ -562,21 +567,23 @@ Inductive head_step : expr → state → list observation → expr → state →
[]
(Val $ LitV LitUnit) (state_upd_heap <[l:=v]> σ)
[]
| CasFailS l v1 v2 v3 v4 pv pvs vl σ :
extract_proph_resolve v4 = Some pv
| CasFailS l v1 v2 p1 p2 pv pvs vl σ :
is_Some (extract_proph_resolve p1)
extract_proph_resolve p2 = Some pv
pvs = option_list pv
σ.(heap) !! l = Some vl vl v1
vals_cas_compare_safe vl v1
head_step (CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) (Val v3) (Val v4)) σ
head_step (CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) (Val p1) (Val p2)) σ
pvs
(Val $ LitV $ LitBool false) σ
[]
| CasSucS l v1 v2 v3 v4 pv pvs σ :
extract_proph_resolve v3 = Some pv
| CasSucS l v1 v2 p1 p2 pv pvs σ :
extract_proph_resolve p1 = Some pv
is_Some (extract_proph_resolve p2)
pvs = option_list pv
σ.(heap) !! l = Some v1
vals_cas_compare_safe v1 v1
head_step (CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) (Val v3) (Val v4)) σ
head_step (CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) (Val p1) (Val p2)) σ
pvs
(Val $ LitV $ LitBool true) (state_upd_heap <[l:=v2]> σ)
[]
......
......@@ -32,22 +32,24 @@ Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
*or* [v] to be unboxed. However, by writing it this way the [val_is_unboxed]
is outside the atomic triple, which makes it much easier to use -- and the
spec is still good enough for all our applications. *)
cas_spec (l : loc) (w1 w2 w3 w4 : val) :
extract_proph_resolve w3 = Some None
extract_proph_resolve w4 = Some None
cas_spec (l : loc) (w1 w2 p1 p2 : val) :
extract_proph_resolve p1 = Some None
extract_proph_resolve p2 = Some None
val_is_unboxed w1
<<< v, mapsto l 1 v >>> cas #l w1 w2 w3 w4 @
<<< v, mapsto l 1 v >>> cas #l w1 w2 p1 p2 @
<<< if decide (v = w1) then mapsto l 1 w2 else mapsto l 1 v,
RET #(if decide (v = w1) then true else false) >>>;
cas_suc_proph_spec (l : loc) (w1 w2 w3 w4 w : val) v (p : proph_id) :
extract_proph_resolve w3 = Some (Some (p, w))
cas_suc_proph_spec (l : loc) (w1 w2 p1 p2 w : val) v (p : proph_id) :
extract_proph_resolve p1 = Some (Some (p, w))
is_Some (extract_proph_resolve p2)
val_is_unboxed w1
<<< mapsto l 1 w1 proph p v >>> cas #l w1 w2 w3 w4 @
<<< mapsto l 1 w1 proph p v >>> cas #l w1 w2 p1 p2 @
<<< mapsto l 1 w2 v = Some w, RET #true>>>;
cas_fail_proph_spec (l : loc) (w1 w2 w3 w4 w : val) v (p : proph_id) :
extract_proph_resolve w4 = Some (Some (p, w))
cas_fail_proph_spec (l : loc) (w1 w2 p1 p2 w : val) v (p : proph_id) :
is_Some (extract_proph_resolve p1)
extract_proph_resolve p2 = Some (Some (p, w))
val_is_unboxed w1
<<< v', v' w1 mapsto l 1 v' proph p v >>> cas #l w1 w2 w3 w4 @
<<< v', v' w1 mapsto l 1 v' proph p v >>> cas #l w1 w2 p1 p2 @
<<< mapsto l 1 v' v = Some w, RET #false>>>;
}.
Arguments atomic_heap _ {_}.
......@@ -67,6 +69,8 @@ Notation "! e" := (load e) : expr_scope.
Notation "e1 <- e2" := (store e1 e2) : expr_scope.
Notation CAS e1 e2 e3 e4 e5 := (cas e1 e2 e3 e4 e5).
Notation "'cas:' e1 ',' e2 ',' e3" := (cas e1 e2 e3 NONEV NONEV)
(at level 200, e1, e2, e3 at level 200) : expr_scope.
End notation.
......@@ -107,12 +111,12 @@ Section proof.
wp_store. iMod ("Hclose" with "H↦") as "HΦ". by iApply "HΦ".
Qed.
Lemma primitive_cas_spec (l : loc) (w1 w2 w3 w4: val) :
extract_proph_resolve w3 = Some None
extract_proph_resolve w4 = Some None
Lemma primitive_cas_spec (l : loc) (w1 w2 p1 p2 : val) :
extract_proph_resolve p1 = Some None
extract_proph_resolve p2 = Some None
val_is_unboxed w1
<<< (v : val), l v >>>
primitive_cas #l w1 w2 w3 w4 @
primitive_cas #l w1 w2 p1 p2 @
<<< if decide (v = w1) then l w2 else l v,
RET #(if decide (v = w1) then true else false) >>>.
Proof.
......@@ -122,27 +126,29 @@ Section proof.
iMod ("Hclose" with "H↦") as "HΦ"; by iApply "HΦ".
Qed.
Lemma primitive_cas_suc_proph_spec (l : loc) (w1 w2 w3 w4 w : val) v (p : proph_id) :
extract_proph_resolve w3 = Some (Some (p, w))
Lemma primitive_cas_suc_proph_spec (l : loc) (w1 w2 p1 p2 w : val) v (p : proph_id) :
extract_proph_resolve p1 = Some (Some (p, w))
is_Some (extract_proph_resolve p2)
val_is_unboxed w1
<<< l w1 proph p v >>>
primitive_cas #l w1 w2 w3 w4 @
primitive_cas #l w1 w2 p1 p2 @
<<< l w2 v = Some w, RET #true>>>.
Proof.
iIntros (?? Q Φ) "? AU". wp_lam. repeat wp_let.
iIntros (??? Q Φ) "? AU". wp_lam. repeat wp_let.
iMod "AU" as "[[H↦ Hp] [_ Hclose]]".
wp_apply (wp_cas_suc_proph with "[H↦ Hp]"); eauto with iFrame; first by left.
iIntros "H". iMod ("Hclose" with "H") as "HΦ". by iApply "HΦ".
Qed.
Lemma primitive_cas_fail_proph_spec (l : loc) (w1 w2 w3 w4 w : val) v (p : proph_id) :
extract_proph_resolve w4 = Some (Some (p, w))
Lemma primitive_cas_fail_proph_spec (l : loc) (w1 w2 p1 p2 w : val) v (p : proph_id) :
is_Some (extract_proph_resolve p1)
extract_proph_resolve p2 = Some (Some (p, w))
val_is_unboxed w1
<<< v', v' w1 l v' proph p v >>>
primitive_cas #l w1 w2 w3 w4 @
primitive_cas #l w1 w2 p1 p2 @
<<< l v' v = Some w, RET #false>>>.
Proof.
iIntros (? ? Q Φ) "? AU". wp_lam. repeat wp_let.
iIntros (??? Q Φ) "? AU". wp_lam. repeat wp_let.
iMod "AU" as (v') "[(Hn & H↦ & Hp) [_ Hclose]]". iDestruct "Hn" as %Hn.
wp_apply (wp_cas_fail_proph with "[H↦ Hp]"); eauto with iFrame; first by right.
iIntros "H". iMod ("Hclose" with "H") as "HΦ". by iApply "HΦ".
......
......@@ -32,12 +32,7 @@ Section cond_counter.
else CAS(c, x, ref (injL n), Some (p, l_ghost), None)
*)
Definition complete : val :=
λ: "args",
let: "c" := Fst $ Fst $ Fst $ Fst "args" in
let: "f" := Snd $ Fst $ Fst $ Fst "args" in
let: "x" := Snd $ Fst $ Fst "args" in
let: "n" := Snd $ Fst "args" in
let: "p" := Snd "args" in
λ: "c" "f" "x" "n" "p",
let: "l_ghost" := ref #() in
CAS "c" "x" (ref (InjL (if: !"f" then "n" + #1 else "n"))) (SOME ("p", "l_ghost")) NONE ;;
#().
......@@ -57,20 +52,18 @@ Section cond_counter.
cinc(c, f)
*)
Definition cinc : val :=
rec: "cinc" "args" :=
let: "c" := Fst "args" in
let: "f" := Snd "args" in
rec: "cinc" "c" "f" :=
let: "x" := !"c" in
match: !"x" with
InjL "n" =>
let: "p" := new prophecy in
let: "y" := ref (InjR ("n", "p")) in
if: cas: "c", "x", "y"
then complete ("c", "f", "y", "n", "p") ;; Skip
else "cinc" ("c", "f")
then complete "c" "f" "y" "n" "p" ;; Skip
else "cinc" "c" "f"
| InjR "args'" =>
(complete ("c", "f", "x", Fst "args'", Snd "args'") ;;
"cinc" ("c", "f"))
(complete "c" "f" "x" (Fst "args'") (Snd "args'") ;;
"cinc" "c" "f")
end.
(** * Proving a spec for [cinc] *)
......@@ -370,9 +363,8 @@ Section cond_counter.
Proof.
iIntros "H1 H2". iCombine "H1" "H2" as "H". iPoseProof (own_valid with "H") as "H".
iDestruct "H" as %H. iPureIntro. destruct H as [[_ Hl1%agree_op_inv] _].
apply to_val_eq.
(* TODO (MR) use agree_equivI *)
Admitted.
apply to_val_eq. by apply to_agree_inj, leibniz_equiv in Hl1.
Qed.
Lemma add_half_histories (H : list loc) γ_h :
own γ_h (half_history_frag H) -
......@@ -465,7 +457,7 @@ Section cond_counter.
Inductive abstract_state : Set :=
| injl : Z abstract_state
| injr : Z proph abstract_state.
| injr : Z proph_id abstract_state.
Definition repr (abs : abstract_state) : val :=
match abs with
......@@ -480,21 +472,21 @@ Section cond_counter.
Definition used_up l γ_h :=
( H, own γ_h (hist_snapshot H) In l H Some l head H)%I.
Definition pending_state P H (n : Z) (p : proph) (l l_ghost : loc) (γ_h γ_n : gname) :=
Definition pending_state P H (n : Z) (p : proph_id) (l l_ghost : loc) (γ_h γ_n : gname) :=
(P own γ_h (half_history_frag H) Some l = head H
p Some #l_ghost own γ_n ( Excl' n))%I.
proph 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) :=
Definition pending_state_wrong_proph P H (n : Z) (p : proph_id) (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.
( v, proph 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) :=
Definition accepted_state Q H (p : proph_id) (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.
l_ghost {1/2} - proph p (Some #l_ghost))%I.
Definition accepted_state_wrong_proph H (p : proph) (l l_ghost : loc) (γ_h : gname) :=
Definition accepted_state_wrong_proph H (p : proph_id) (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.
l_ghost {1/2} - v, proph 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.
......@@ -517,10 +509,10 @@ Section cond_counter.
([ list] l' H, q v, l' {q} v)
Some l = head H NoDup H
own γ_b ( Excl' b)
v (p : proph),
v (p : proph_id),
l {q} (repr v)
(( (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
( (n : Z) (p : proph_id) l_ghost, v = injr n p
P Q γ_t, inv stateN (state_inv P Q p n l l_ghost H γ_h γ_n γ_t)
pau P Q (γ_h, γ_b, γ_n))))%I.
......@@ -583,7 +575,7 @@ Section cond_counter.
l_ghost {1 / 2} #() -
((own_token γ_t ={}= Q) - Φ #()) -
own γ_n ( Excl' n) -
WP CAS #c_l #l (ref InjL #n) (InjR (#p, #l_ghost)) (InjL #());; #() {{ v, Φ v }}.
WP CAS #c_l #l (ref InjLV #n) (InjRV (#p, #l_ghost)) (InjLV #());; #() {{ v, Φ v }}.
Proof.
iIntros (Heq) "#InvC #InvS PAU Hl_ghost HQ Hn●".
wp_alloc l_new as "Hl_new".
......@@ -609,7 +601,7 @@ Section cond_counter.
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']");
[ by left | done | by iFrame | ..].
[ by left | done | by eauto | by iFrame | ..].
(* show that l3 ≠ l_new *)
destruct H as [|l3' H]; inversion Heq; subst l3'.
destruct (decide (l3 = l_new)) as [-> | Hn].
......@@ -679,7 +671,7 @@ Section cond_counter.
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 | ..].
[ by left | done | by eauto | by iFrame | ..].
iIntros "[_ Heq]". iDestruct "Heq" as %->. inversion Heq'.
*** (* Done: contradiction *)
iDestruct "Done" as "[QT [>Hlghost Usedup]]".
......@@ -704,13 +696,12 @@ Section cond_counter.
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 | .. ].
wp_apply (wp_cas_fail with "Hc"); [ naive_solver | naive_solver | naive_solver | naive_solver | ..].
iDestruct "Done" as "[_ [Hlghost _]]".
iDestruct "Hlghost" as (?) "Hlghost".
by iDestruct (mapsto_valid_2 with "Hlghost Hl_ghost") as %?.
Qed.
(** The part of [complete] for the failing thread *)
Lemma complete_failing_thread γ_h γ_b γ_n γ_t f_l c_l l1 l H1 H P Q p m n l_ghost_inv l_ghost Φ :
......@@ -722,7 +713,7 @@ Section cond_counter.
pau P Q (γ_h, γ_b, γ_n) -
own γ_h (hist_snapshot H1) -
((own_token γ_t ={}= Q) - Φ #()) -
WP CAS #c_l #l (ref InjL #n) (InjR (#p, #l_ghost)) (InjL #());; #() {{ v, Φ v }}.
WP CAS #c_l #l (ref InjLV #n) (InjRV (#p, #l_ghost)) (InjLV #());; #() {{ v, Φ v }}.
Proof.
iIntros (Heq Hin Hnl) "#InvC #InvS PAU #Hs1 HQ".
wp_alloc l_new as "Hlnew". wp_bind (CAS _ _ _ _ _)%E.
......@@ -734,21 +725,25 @@ Section cond_counter.
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 | ..].
wp_apply (wp_cas_suc_proph with "[Hc Hp']");
[ by left | done | by eauto | 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 | ..].
wp_apply (wp_cas_suc_proph with "[Hc Hp']");
[ by left | done | by eauto | 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 | ..].
wp_apply (wp_cas_suc_proph with "[Hc Hp']");
[ by left | done | by eauto | 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 | ..].
wp_apply (wp_cas_suc_proph with "[Hc Hp']");
[ by left | done | by eauto | by iFrame | ..].
iIntros "[Hc Contra]". iDestruct "Contra" as %[=->]. done.
** (* Done : contradiction *)
iDestruct "Done" as "[QT [>Hlghost Usedup]]".
......@@ -771,63 +766,41 @@ 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 | [Pending_wp | [Accepted | [Accepted_wp | Done]]]]".
** (* Pending: contradiction *)
iDestruct "Pending" 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').
** (* 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'''.
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').
** (* 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; repeat iRight; iFrame).
iModIntro. iSplitR "Q".
{ iNext. iExists _, _, _, _. eauto 10 with iFrame. }
done.
*** iModIntro. iCombine "T" "Ht" as "Contra". iDestruct (own_valid with "Contra") as %Contra.
inversion Contra.
iInv stateN as "[Pending | [Pending_wp | [Accepted | [Accepted_wp | Done]]]]";
[ iDestruct "Pending" as "[_ >[Hh◯ [Heq' _]]]" |
iDestruct "Pending_wp" as "[_ >[Hh◯ [Heq' _]]]" |
iDestruct "Accepted" as "[_ >[Hh◯ [Heq' _]]]" |
iDestruct "Accepted_wp" as ">[Hh◯ [Heq' _]]" | ..];
try (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')).
iDestruct "Done" as "[[Q | >T] Hrest']".
** iModIntro.
iSplitL "Ht Hrest'"; first by (iNext; repeat iRight; iFrame).
iModIntro. iSplitR "Q".
{ iNext. iExists _, _, _, _. eauto 10 with iFrame. }
done.
** iModIntro. iCombine "T" "Ht" as "Contra". iDestruct (own_valid with "Contra") as %Contra.
inversion Contra.
Qed.
(** ** Proof of [complete] *)
Lemma complete_spec e (c f l : loc) H (n : Z) (p : proph) γs γ_t l_ghost_inv P Q :
IntoVal e (#c, #f, #l, #n, #p)
Lemma complete_spec (c f l : loc) H (n : Z) (p : proph_id) γs γ_t l_ghost_inv P Q :
is_counter γs (#f, #c) -
inv stateN (state_inv P Q p n l l_ghost_inv H γs.1.1 γs.2 γ_t) -
pau P Q γs -
{{{ True }}}
complete e
complete #c #f #l #n #p
{{{ RET #(); own_token γ_t ={}= Q }}}.
Proof.
iIntros (<-) "#InvC #InvS #PAU". destruct γs as [[γ_h γ_b] γ_n].
iIntros "#InvC #InvS #PAU". destruct γs as [[γ_h γ_b] γ_n].
iDestruct "InvC" as (??? f_l c_l [[=<-<-<-][=->->]]) "#InvC".
iModIntro. iIntros (Φ) "_ HQ".
repeat (wp_lam; repeat wp_proj).
wp_alloc l_ghost as "[Hl_ghost' Hl_ghost'2]". wp_let. wp_bind (!_)%E. simpl.
iModIntro. iIntros (Φ) "_ HQ". wp_lam. repeat wp_let.
wp_alloc l_ghost as "[Hl_ghost' Hl_ghost'2]". wp_let. wp_pures. wp_bind (! _)%E. simpl.
(* 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].
......@@ -857,7 +830,7 @@ Section cond_counter.
(* 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 | .. ];
destruct b2; wp_if; [ wp_op | .. ]; wp_pures;
iApply ((complete_succeeding_thread_pending _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ Heq)
with "InvC InvS PAU Hl_ghost'2 HQ Hn●").
+ (* Pending (wrong proph): update to accepted (wrong proph) *)
......@@ -879,7 +852,7 @@ Section cond_counter.
(* 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 | .. ];
destruct b2; wp_if; [ wp_op | .. ]; wp_pures;
iApply ((complete_succeeding_thread_pending _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ Heq)
with "InvC InvS PAU Hl_ghost'2 HQ Hn●").
+ (* Accepted: contradiction *)
......@@ -940,26 +913,24 @@ 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 [? | ?]; wp_if; [ wp_op | ..];
destruct b1; wp_if; [ wp_op | ..]; wp_pures;
iApply ((complete_failing_thread _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ Heq Hin Hnl)
with "InvC InvS PAU Hs1 HQ").
Qed.
(** ** Proof of [cinc] *)
Lemma cinc_spec e c f γs :
IntoVal e (c, f)
Lemma cinc_spec c f γs :
is_counter γs (f, c) -
<<< (b : bool) (n : Z), counter_content γs (b, n) >>>
cinc e @∖↑N
cinc c f @∖↑N
<<< counter_content γs (b, if b then n + 1 else n), RET #() >>>.
Proof.
iIntros (<-) "#InvC".
iIntros "#InvC".
iDestruct "InvC" as (γ_h γ_b γ_n f_l c_l) "[Heq InvC]".
iDestruct "Heq" as %[-> [=->->]].
iApply wp_atomic_intro. iIntros (Φ) "AU". iLöb as "IH".
repeat (wp_lam; wp_proj). wp_lam. wp_bind (!_)%E.
wp_lam. repeat wp_let. 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] InvC_rest]".
wp_load.
......@@ -969,7 +940,7 @@ Section cond_counter.
{ iModIntro. rewrite /counter_inv. iExists _, _, _, _. iFrame. iExists _, p. eauto with iFrame. }
wp_let. wp_load.
wp_match. wp_apply wp_new_proph; first done.
iIntros (p') "Hp'". iDestruct "Hp'" as (l_ghost) "Hp'".
iIntros (l_ghost p') "Hp'".
wp_let.
wp_alloc ly as "Hly". wp_let. wp_bind (CAS _ _ _ _ _)%E.
(* open outer invariant to read c_l *)
......@@ -1010,7 +981,7 @@ Section cond_counter.
}
wp_if.
wp_apply complete_spec; [iExists _, _, _, _, _; eauto | done | done | done | ..].
iIntros "Ht". iMod ("Ht" with "Token") as "Φ". wp_seq. by wp_seq.
iIntros "Ht". iMod ("Ht" with "Token") as "Φ". wp_seq. by wp_lam.
* 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.
......@@ -1024,7 +995,7 @@ Section cond_counter.
}
wp_if.
wp_apply complete_spec; [iExists _, _, _, _, _; eauto | done | done | done | ..].
iIntros "Ht". iMod ("Ht" with "Token") as "Φ". wp_seq. by wp_seq.
iIntros "Ht". iMod (