Require Import Vbase Varith.
Require Import Relations Classical ClassicalDescription.
Require Import List Permutation Vlistbase Vlist extralib.
Require Import c11 fslassn fslmodel fslassnlemmas.
Require Import fslhmap step.
Set Implicit Arguments.
Definition hbpath := list hbcase.
Definition hbpath_wf (path: hbpath) :=
∀ path1 path2 edge1 edge2 (DECOMP: path = path1 ++ edge1 :: edge2 :: path2),
hb_snd edge1 = Some (hb_fst edge2).
Definition hbpath_valid lab sb rf hmap path :=
<< WFP: hbpath_wf path >> ∧
<< EVP: ∀ edge (IN: In edge path), edge_valid lab sb rf edge >> ∧
<< PVA: ∀ edge (IN: In edge path), hmap_valid lab sb rf hmap (hb_fst edge) >>.
Definition hbpath_connects lab sb rf hmap path a b :=
(a = b ∧ path = nil) ∨
hbpath_valid lab sb rf hmap path ∧
∃ fst lst, ohead path = some fst ∧ hb_fst fst = a ∧
olast path = some lst ∧ hb_snd lst = Some b.
Lemma hbpath_wf_one:
∀ edge, hbpath_wf (edge :: nil).
Proof.
red; ins.
exfalso.
apply f_equal with (f := (@length hbcase)) in DECOMP.
rewrite app_length in DECOMP; ins.
by rewrite <- !plus_n_Sm in DECOMP.
Qed.
Lemma hbpath_wf_app:
∀ path1 path2, hbpath_wf (path1 ++ path2) → hbpath_wf path1 ∧ hbpath_wf path2.
Proof.
ins; split; red; ins; subst.
eby rewrite <- app_assoc, <- !app_comm_cons in H; eapply H.
eby rewrite app_assoc in H; eapply H.
Qed.
Lemma hbpath_wf_cons:
∀ edge path, hbpath_wf (edge :: path) → hbpath_wf path.
Proof.
ins.
rewrite <- (app_nil_l path), <- app_cons in H.
apply hbpath_wf_app in H; desf.
Qed.
Lemma hbpath_valid_nil:
∀ lab sb rf hmap, hbpath_valid lab sb rf hmap nil.
Proof.
ins; red; unnw; repeat split; ins.
red; ins.
exploit app_cons_not_nil; eauto; ins.
Qed.
Lemma connects_implies_valid:
∀ lab sb rf hmap path a b, hbpath_connects lab sb rf hmap path a b → hbpath_valid lab sb rf hmap path.
Proof.
ins; red in H; desf.
by apply hbpath_valid_nil.
Qed.
Lemma hbpath_valid_app:
∀ lab sb rf hmap path1 path2, hbpath_valid lab sb rf hmap (path1 ++ path2) →
hbpath_valid lab sb rf hmap path1 ∧ hbpath_valid lab sb rf hmap path2.
Proof.
ins; red in H; desf; split.
× red; do 3 try split; unnw.
+ apply hbpath_wf_app in WFP; desf.
+ ins; eapply EVP; eauto.
rewrite In_app; eauto.
+ ins; eapply PVA; eauto.
rewrite In_app; eauto.
× red; do 3 try split; unnw.
+ apply hbpath_wf_app in WFP; desf.
+ ins; eapply EVP; eauto.
rewrite In_app; eauto.
+ ins; eapply PVA; eauto.
rewrite In_app; eauto.
Qed.
Lemma hbpath_valid_cons:
∀ lab sb rf hmap edge path,
hbpath_valid lab sb rf hmap (edge :: path) → hbpath_valid lab sb rf hmap path.
Proof.
ins.
rewrite <- (app_nil_l path), <- app_cons in H.
apply hbpath_valid_app in H; desf.
Qed.
Lemma hbpath_valid_cons_inv:
∀ lab sb rf hmap path (PV: hbpath_valid lab sb rf hmap path)
edge (EV: edge_valid lab sb rf edge) (VALIDa: hmap_valid lab sb rf hmap (hb_fst edge))
(VALIDb: ∀ b (SND: hb_snd edge = Some b), hmap_valid lab sb rf hmap b)
(CONNECT: ∀ edge´ (FST: ohead path = Some edge´), hb_snd edge = Some (hb_fst edge´)),
hbpath_valid lab sb rf hmap (edge :: path).
Proof.
ins; red; unnw; intuition; ins; desf.
× destruct path; ins.
by apply hbpath_wf_one.
red; ins.
destruct path1; ins; desf; intuition.
rewrite H0 in PV.
eby eapply (proj1 PV).
× eby eapply (proj1 (proj2 PV)).
× eby eapply ((proj2 (proj2 PV))).
Qed.
Lemma hbpath_connects_app1:
∀ lab sb rf hmap path1 path2 edge a b
(CONNECT: hbpath_connects lab sb rf hmap (path1 ++ edge :: path2) a b),
hbpath_connects lab sb rf hmap path1 a (hb_fst edge).
Proof.
unfold hbpath_connects; ins; desf.
by exploit app_cons_not_nil; eauto.
destruct path1; ins; desf; eauto.
right; split.
by rewrite app_comm_cons in CONNECT; apply hbpath_valid_app in CONNECT; desf.
∃ fst.
des_list_tail path1 path edge´; ins.
× ∃ fst; repeat split.
eby eapply (proj1 CONNECT nil).
× rewrite !app_comm_cons, <- !app_assoc in *; ins.
∃ edge´; repeat split.
by rewrite last_app.
eby apply hbpath_valid_cons in CONNECT; eapply (proj1 CONNECT).
Qed.
Lemma hbpath_connects_app2:
∀ lab sb rf hmap path1 path2 edge a b
(CONNECT: hbpath_connects lab sb rf hmap (path1 ++ edge :: path2) a b),
hbpath_connects lab sb rf hmap (edge :: path2) (hb_fst edge) b.
Proof.
ins; red.
right; split.
by apply connects_implies_valid, hbpath_valid_app in CONNECT; desc.
red in CONNECT; ins; desf.
by exploit app_cons_not_nil; eauto; ins.
eexists,; repeat split; eauto.
destruct path1; ins; desf.
by rewrite last_app in CONNECT3.
Qed.
Lemma hbpath_connects_cons:
∀ lab sb rf hmap edge1 edge2 path a b
(CONNECT: hbpath_connects lab sb rf hmap (edge1 :: edge2 :: path) a b),
hbpath_connects lab sb rf hmap (edge2 :: path) (hb_fst edge2) b.
Proof.
eby ins; rewrite <- (app_nil_l (_ :: path)), app_comm_cons in CONNECT; eapply hbpath_connects_app2.
Qed.
Lemma hbUrf_implies_hbpath:
∀ lab sb rf hmap V (VALID: hmap_valids lab sb rf hmap V) (HC: hist_closed sb rf V)
a b (HB: happens_before_union_rf sb rf a b) (IN: In b V),
∃ path, hbpath_connects lab sb rf hmap path a b.
Proof.
ins.
apply clos_trans_t1n in HB; induction HB.
{
destruct H; [∃ (hb_sb x y :: nil) | ∃ (hb_rf x y :: nil)]; right; split;
solve [
ins; eexists,,; intuition
|
red; unnw; intuition; ins; desf; ins; desf;
[apply hbpath_wf_one | eapply VALID, HC; vauto]
].
}
{
exploit IHHB; ins; desf.
destruct H; [∃ (hb_sb x y :: path) | ∃ (hb_rf x y :: path)];
right; split; red in x1; desf;
try solve [
ins; eexists,,; intuition; destruct path; ins; desf
|
red; unnw; intuition; ins; desf; ins; desf;
[apply hbpath_wf_one | eapply VALID, HC; vauto]
|
apply clos_t1n_trans in HB; apply hbpath_valid_cons_inv; ins; desf;
[exploit hist_closedD; eauto; ins; eapply VALID, HC; vauto |
eby exploit hist_closedD; try edone; ins; eapply VALID]
].
}
Qed.
Lemma hmap_defined_on_path:
∀ lab sb rf mo (CONS_RF: ConsistentRF_basic lab sb rf mo)
hmap path (PV: hbpath_valid lab sb rf hmap path)
edge (IN: In edge path),
∃ hf, hmap edge = Hdef hf.
Proof.
ins; red in PV; desf.
rewrite <- hdef_alt.
specialize (EVP _ IN); specialize (PVA _ IN); clear IN.
ins; unfold hmap_valid, unique in PVA.
desf; desc;
try (destruct DISJ; desc); try clear TYP;
destruct edge; ins; desf;
try (by red in EVP; rewrite Heq in EVP; desc);
try (by specialize (CONS_RF e´); rewrite EVP, Heq in CONS_RF; desf);
try (eapply qU0 in EVP; desf);
try (by rewrite ?sEQ, ?rEQ);
intro U; rewrite ?U, ?hplus_udef_l, ?hplus_undef_r in *; try congruence;
try (by red in TRAN; desf).
× symmetry in qEQ; apply hplus_def_inv_l in qEQ; desf.
apply hsum_def_inv with (h := hmap (hb_sb e e´)) in qEQ; desf; try congruence.
by do 2 (rewrite In_map; eexists,; eauto); rewrite qOK.
× red in TRAN; desf.
apply hplus_def_inv_l in TRAN; desf.
apply hsum_def_inv with (h := hmap (hb_rf e e´)) in TRAN; desf; try congruence.
by do 2 (rewrite In_map; eexists,; eauto); rewrite rfsOK.
× cut (Hsim (hmap (hb_sb pre e)) Hundef).
by intro S; red in S; desf.
rewrite pEQ, qEQ.
apply hplus_sim.
+ apply Hsim_refl.
by intro CONTRA; rewrite CONTRA, !hplus_undef_l in ×.
+ eapply hplus_sim; eauto.
by intro CONTRA; rewrite CONTRA, !hplus_undef_r in ×.
+ by intro CONTRA; rewrite CONTRA in ×.
Qed.
Lemma nonatomic_loc_on_path:
∀ lab sb rf mo (CONS_RF: ConsistentRF_basic lab sb rf mo)
hmap path (PV: hbpath_valid lab sb rf hmap path)
l (ALL: ∀ edge (IN: In edge path) hf (MAP: hmap edge = Hdef hf), hf l ≠ HVnone)
(NAX: ∃ edge, << IN: In edge path >> ∧
<< NA: ∀ hf (MAP: hmap edge = Hdef hf), is_nonatomic (hf l) >>),
∀ edge (IN: In edge path) hf (MAP: hmap edge = Hdef hf), is_nonatomic (hf l).
Proof.
induction path; ins; desc.
desf; desf.
× by apply NA.
× assert (NApath: ∀ edge (IN: In edge path) hf (MAP: hmap edge = Hdef hf), is_nonatomic (hf l)).
{
apply IHpath.
+ eby eapply hbpath_valid_cons.
+ ins; eapply ALL; eauto.
+ unnw; eexists,; eauto.
}
destruct path as [ | edge´ path´]; ins.
exploit (hmap_defined_on_path CONS_RF PV edge´); try find_in_list.
ins; desc.
assert (NA´: is_nonatomic (hf0 l)) by (apply (NApath edge´); eauto).
eapply na_propagates_back with (edge1 := edge) (edge2 := edge´); eauto.
by red in PV; desc; eapply EVP.
by red in PV; desc; eapply EVP; vauto.
eby red in PV; desc; eapply (WFP nil); rewrite app_nil_l.
by red in PV; desc; eapply PVA; vauto.
× destruct path as [ | edge1 path´]; ins.
exploit (hmap_defined_on_path CONS_RF PV edge0); try find_in_list.
exploit (hmap_defined_on_path CONS_RF PV edge1); try find_in_list.
ins; desc.
assert (NA´: is_nonatomic (hf1 l)).
{
eapply na_propagates_forward with (edge1 := edge0) (edge2 := edge1); eauto.
by red in PV; desc; eapply EVP.
by red in PV; desc; eapply EVP; vauto.
eby red in PV; desc; eapply (WFP nil); rewrite app_nil_l.
by red in PV; desc; eapply PVA; vauto.
}
eapply IHpath; eauto.
eby eapply hbpath_valid_cons.
unnw; ∃ edge1,; eauto; ins; congruence.
× eapply IHpath; eauto.
eby eapply hbpath_valid_cons.
Qed.
Lemma sink_is_always_last :
∀ path (WF: hbpath_wf path) a (SIN: In (hb_sink a) path), olast path = Some (hb_sink a).
Proof.
ins.
apply In_split in SIN; desf.
destruct l2 as [ | edge path2].
× destruct l1; ins.
f_equal.
by rewrite last_app.
× exploit WF; eauto; ins.
Qed.
Lemma sink_is_always_last_alt:
∀ path edge (WF: hbpath_wf (path ++ edge :: nil)), ¬ ∃ edge´, In edge´ path ∧ is_sink edge´.
Proof.
ins; intro; desf.
apply In_split in H; desf.
destruct l2; [rewrite <- app_assoc, <- app_comm_cons, app_nil_l in WF | apply hbpath_wf_app in WF; desf];
exploit (WF l1); eauto; destruct edge´; ins; desf.
Qed.
Lemma connects_implies_no_sink:
∀ lab sb rf hmap path a b,
hbpath_connects lab sb rf hmap path a b → ∀ e, ¬ In (hb_sink e) path.
Proof.
ins; intro S.
do 2 (red in H; desf).
exploit sink_is_always_last; ins; eauto; desf.
Qed.
Lemma connect_implies_hbUrf:
∀ lab sb rf hmap path a b (CONNECT: hbpath_connects lab sb rf hmap path a b),
clos_refl_trans _ (happens_before_union_rf sb rf) a b.
Proof.
induction path as [ | edge path]; ins.
by red in CONNECT; desf; vauto.
red in CONNECT; ins; desf.
exploit (proj1 (proj2 CONNECT) fst); ins; eauto.
destruct path as [ | edge´ path]; ins.
× apply rt_step, t_step.
destruct fst; ins; desf; vauto.
× apply rt_trans with (y := (hb_fst edge´)).
+ exploit ((proj1 CONNECT) nil); ins; eauto.
apply rt_step, t_step.
destruct fst; ins; desf; vauto.
+ apply IHpath.
red; ins.
right; split.
eby eapply hbpath_valid_cons.
eexists,; repeat split; eauto.
Qed.
Lemma connect_implies_hbUrf_strong:
∀ lab sb rf hmap path a b (CONNECT: hbpath_connects lab sb rf hmap path a b),
path ≠ nil → happens_before_union_rf sb rf a b.
Proof.
ins.
destruct path as [ | edge path]; desf.
exploit (proj1 (proj2 (connects_implies_valid CONNECT)) edge); ins; try find_in_list.
assert (¬ is_sink edge).
by intro; destruct edge; ins; exploit connects_implies_no_sink; eauto; find_in_list.
destruct path as [ | edge´ path]; desf.
by red in CONNECT; ins; desf; destruct fst; ins; vauto.
exploit (proj1 (connects_implies_valid CONNECT) nil); ins; eauto.
assert (a = hb_fst edge).
by red in CONNECT; ins; desf.
eapply hbpath_connects_cons, connect_implies_hbUrf, clos_refl_transE in CONNECT; desf.
by destruct edge; ins; vauto.
apply clos_trans_hbUrfE in CONNECT.
eapply t_trans; eauto.
by destruct edge; ins; vauto.
Qed.
Lemma hb_trough_sb_path:
∀ lab sb rf mo path
(WF: hbpath_wf path) (NT: path ≠ nil) (EVP: ∀ edge (IN: In edge path), edge_valid lab sb rf edge)
(SB: ∀ edge (IN: In edge path), is_sb edge)
a (A: ∀ first (FST: ohead path = Some first), hb_fst first = a)
b (B: ∀ last (LST: olast path = Some last), hb_snd last = Some b),
happens_before lab sb rf mo a b.
Proof.
induction path as [ | edge1 path´]; ins.
destruct path´ as [ | edge2 path´´]; ins.
× clear IHpath´.
apply t_step; left.
exploit SB; ins; eauto.
exploit A; ins; eauto.
exploit B; ins; eauto.
exploit EVP; ins; eauto.
destruct edge1; ins; desf.
× apply t_trans with (y := hb_fst edge2).
+ apply t_step; left.
exploit (WF nil); ins; eauto.
exploit (SB edge1); ins; eauto.
exploit (EVP edge1); ins; eauto.
exploit A; ins; eauto.
destruct edge1; ins; desf.
+ eapply IHpath´; ins; eauto.
- eby eapply hbpath_wf_cons.
- inv FST.
Qed.
Lemma HBuRF_trough_path:
∀ lab sb rf path
(WF: hbpath_wf path) (NT: path ≠ nil) (EVP: ∀ edge (IN: In edge path), edge_valid lab sb rf edge)
a (A: ∀ first (FST: ohead path = Some first), hb_fst first = a)
b (B: ∀ last (LST: olast path = Some last), hb_snd last = Some b),
happens_before_union_rf sb rf a b.
Proof.
induction path as [ | edge1 path´]; ins.
destruct path´ as [ | edge2 path´´]; ins.
× clear IHpath´.
apply t_step.
exploit A; ins; eauto.
exploit B; ins; eauto.
exploit EVP; ins; eauto.
destruct edge1; ins; vauto.
× apply t_trans with (y := hb_fst edge2).
+ apply t_step.
exploit (WF nil); ins; eauto.
exploit (EVP edge1); ins; eauto.
exploit A; ins; eauto.
destruct edge1; ins; vauto.
+ eapply IHpath´; ins; eauto.
- eby eapply hbpath_wf_cons.
- inv FST.
Qed.
Lemma HBuRF_trough_path1 :
∀ lab sb rf path
(WF: hbpath_wf path) (NT: path ≠ nil) (EVP: ∀ edge (IN: In edge path), edge_valid lab sb rf edge)
first (FST: ohead path = Some first) last (LST: olast path = Some last),
clos_refl_trans _ (happens_before_union_rf sb rf) (hb_fst first) (hb_fst last).
Proof.
induction path as [ | edge1 path´]; ins.
inv FST.
destruct path´ as [ | edge2 path´´]; ins; vauto.
generalize (hbpath_wf_cons WF); ins.
exploit IHpath´; ins; eauto.
eapply rt_trans; eauto.
apply rt_step, t_step.
exploit (WF nil); ins; eauto.
exploit (EVP first); ins; eauto.
destruct first as [a b | a b | a]; ins; inv x1; vauto.
Qed.
Lemma NoDup_path :
∀ lab sb rf path
(ACYCLIC: IrreflexiveHBuRF sb rf)
(WF: hbpath_wf path)
(EVP: ∀ edge (IN: In edge path), edge_valid lab sb rf edge),
NoDup path.
Proof.
induction path as [ | edge1 path´]; ins.
apply NoDup_cons.
2: eby apply IHpath´; auto; eapply hbpath_wf_cons.
intro IN; clear IHpath´.
apply In_split in IN; desf.
cut (∃ b, hb_snd edge1 = Some b ∧ happens_before_union_rf sb rf b (hb_fst edge1)).
by ins; desf; eapply ACYCLIC; eapply t_trans; eauto;
apply t_step; exploit (EVP edge1); ins; eauto; destruct edge1; ins; vauto.
rewrite <- (app1l _ l2), <- appA, <- app_cons in WF.
apply hbpath_wf_app in WF; desf; clear WF0.
destruct l1 as [ | edge2 path]; ins.
× exploit (WF nil); ins; eauto.
eexists,; eauto.
apply t_step.
exploit (WF nil); ins; eauto.
exploit (EVP edge1); ins; eauto.
destruct edge1; ins; vauto.
× exploit (WF nil); ins; eauto.
eexists,; eauto.
apply hbpath_wf_cons in WF.
exploit HBuRF_trough_path1; ins; eauto; try done.
by eapply EVP; ins; rewrite In_app in *; ins; desf; eauto.
rewrite last_app in x1; ins.
apply clos_refl_transE in x1; desf.
2: by apply clos_trans_hbUrfE.
exfalso.
exploit (EVP edge1); ins; eauto.
eapply ACYCLIC, t_step; instantiate (1 := hb_fst edge1).
destruct edge1 as [a b | a b | a]; ins; vauto.
Qed.
Lemma hb_trough_sb_path1 :
∀ lab sb rf mo (ACYCLIC: IrreflexiveHBuRF sb rf) path
(WF: hbpath_wf path) (NT: path ≠ nil) (EVP: ∀ edge (IN: In edge path), edge_valid lab sb rf edge)
(SB: ∀ edge (IN: In edge path) (NL: olast path ≠ Some edge), is_sb edge)
first (FST: ohead path = Some first) last (LST: olast path = Some last),
clos_refl_trans _ (happens_before lab sb rf mo) (hb_fst first) (hb_fst last).
Proof.
induction path as [ | edge1 path´]; ins.
inv FST.
destruct path´ as [ | edge2 path´´]; ins; vauto.
generalize (hbpath_wf_cons WF); ins.
exploit IHpath´; ins; eauto.
eapply rt_trans; eauto.
apply rt_step, t_step; left.
exploit (WF nil); ins; eauto.
exploit (EVP first); ins; eauto.
exploit (SB first); ins; eauto.
× fold (olast (edge2 :: path´´)); intro L.
apply olast_inv in L; desf; rewrite L in ×.
clear - ACYCLIC WF EVP L.
exploit NoDup_path; eauto; ins.
+ eapply EVP; desf; eauto.
rewrite <- L in IN; ins; eauto.
+ rewrite <- app_cons in x0; apply NoDup_remove_2 in x0.
destruct x0; vauto.
× destruct first; ins; inv x1.
Qed.
Lemma structure_of_triangled_path:
∀ lab sb rf mo
(ACYCLIC: IrreflexiveHBuRF sb rf) (CONS_RF: ConsistentRF_basic lab sb rf mo)
hmap path (PV: hbpath_valid lab sb rf hmap path)
l (DOM: ∀ edge (IN: In edge path) hf (MAP: hmap edge = Hdef hf), << NA: is_nonatomic (hf l) >> ∧
<< LAB: ¬ HVlabeled (hf l) HLnormal >>),
∃ path1 path2, << DECOMP: path = path1 ++ path2 >> ∧
<< LAB1: ∀ edge (IN: In edge path1) hf1 (MAP: hmap edge = Hdef hf1), HVlabeled (hf1 l) HLtriangle >> ∧
<< LAB2: ∀ edge (IN: In edge path2) hf2 (MAP: hmap edge = Hdef hf2), HVlabeled (hf2 l) HLnabla >>.
Proof.
induction path as [ | edge1 path´]; ins.
by ∃ nil, nil; unnw; repeat split; ins.
exploit IHpath´; eauto; ins; clear IHpath´; desf.
eby eapply hbpath_valid_cons.
exploit (hmap_defined_on_path CONS_RF PV edge1); try find_in_list.
ins; desc.
exploit (DOM edge1); eauto; ins; desf.
assert (LABe: HVlabeled (hf l) HLtriangle ∨ HVlabeled (hf l) HLnabla).
{
clear - NA LAB; destruct (hf l); ins; desf; destruct lbl; ins; eauto.
}
desf.
{
∃ (edge1 :: path1), path2; unnw; repeat split; ins; desf.
by rewrite MAP in x0; inv x0.
eby eapply LAB1.
}
{
∃ nil, (edge1 :: path1 ++ path2); unnw; repeat split; ins; desf.
by rewrite MAP in x0; inv x0.
rewrite In_app in IN; desf.
2: eby eapply LAB2.
destruct path1 as [ | edge2 path1´]; ins.
exploit (hmap_defined_on_path CONS_RF PV edge2); try find_in_list.
ins; desc.
cut (¬ HVlabeled (hf0 l) HLtriangle).
by intro N; destruct N; apply (LAB1 edge2); eauto.
eapply no_triangle_after_nabla with (edge1 := edge1) (edge2 := edge2) (hf1 := hf) (hf2 := hf0); eauto.
× apply (proj1 (proj2 PV)); vauto.
× apply (proj1 (proj2 PV)); vauto.
× eby eapply ((proj1 PV) nil); rewrite app_nil_l.
× red in PV; desc; apply PVA; vauto.
× by exploit DOM; ins; eauto; desc.
}
Qed.
Lemma find_triangled_beginning:
∀ lab sb rf mo (CONS_RF: ConsistentRF_basic lab sb rf mo)
path hmap (PV: hbpath_valid lab sb rf hmap path)
l (DOM: ∀ edge (IN: In edge path) hf (MAP: hmap edge = Hdef hf), hf l ≠ HVnone),
∃ pathT pathR, << DECOMP: path = pathT ++ pathR >> ∧
<< NN: ∀ edge (IN: In edge pathT) hf (MAP: hmap edge = Hdef hf),
(¬ HVlabeled (hf l) HLnormal) >> ∧
<< MAX: ∀ edge (E: ohead pathR = Some edge) hf (MAP: hmap edge = Hdef hf),
(HVlabeled (hf l) HLnormal) >>.
Proof.
induction path as [ | edge1 path´]; ins.
× unnw; ∃ nil, nil; ins.
× exploit (hmap_defined_on_path CONS_RF PV edge1); try find_in_list.
ins; desc.
destruct (classic (HVlabeled (hf l) HLnormal)) as [N|N].
+ unnw; ∃ nil, (edge1 :: path´); repeat split; ins; congruence.
+ exploit IHpath´; ins; eauto; desf.
eby eapply hbpath_valid_cons.
unnw; ∃ (edge1 :: pathT), pathR; repeat split; ins; desf; try congruence.
eby eapply NN.
Qed.
Lemma sb_trough_path:
∀ lab sb rf hmap path edge1 edgeN (PV: hbpath_valid lab sb rf hmap (edge1 :: path ++ edgeN :: nil))
(pSB: ∀ edge (IN: In edge path), is_sb edge),
∀ a (SND: hb_snd edge1 = Some a), clos_refl_trans _ sb a (hb_fst edgeN).
Proof.
induction path as [ | edge path]; ins.
by exploit ((proj1 PV) nil); ins; desf; vauto.
exploit ((proj1 (proj2 PV)) edge); ins; eauto.
exploit (pSB edge); eauto; ins.
destruct edge; ins.
exploit ((proj1 PV) nil); ins; desf.
apply hbpath_valid_cons in PV.
exploit IHpath; ins; try edone; eauto.
eapply rt_trans; vauto.
Qed.
Lemma only_first_nabla_is_rf:
∀ lab sb rf mo (CONS_RF: ConsistentRF_basic lab sb rf mo)
edge path hmap (PV: hbpath_valid lab sb rf hmap (edge :: path))
l (DOM: ∀ edge´ (IN: In edge´ (edge :: path)) hf (MAP: hmap edge´ = Hdef hf),
<< NA: is_nonatomic (hf l) >> ∧ << LAB: HVlabeled (hf l) HLnabla >>),
∀ edge´ (IN: In edge´ path), is_sb edge´ ∨ is_sink edge´.
Proof.
intros until edge´; revert edge´.
apply (not_ex_not_all _ (fun edge´ ⇒ In edge´ path → is_sb edge´ ∨ is_sink edge´)).
intro; desf.
apply imply_to_and in H.
exploit (first_exists path (fun edge ⇒ ¬ (is_sb edge ∨ is_sink edge))); eauto; ins; desf.
rename a´ into edge´.
exploit (hmap_defined_on_path CONS_RF PV edge); try find_in_list.
exploit (hmap_defined_on_path CONS_RF PV edge´); try find_in_list.
ins; desc.
exploit (DOM edge); try find_in_list.
exploit (DOM edge´); try find_in_list.
ins; desc.
destruct x1.
des_list_tail l1 path edge´´.
× rewrite app_nil_l in PV.
exploit (step_from_nabla CONS_RF edge edge´); eauto.
by apply (proj1 (proj2 PV)); find_in_list.
by apply (proj1 (proj2 PV)); find_in_list.
eby eapply (proj1 PV nil).
by apply ((proj2 (proj2 PV))); find_in_list.
by intro X; rewrite X in ×.
intro C; desf; eauto.
+ destruct edge´; ins; eauto.
+ red in C0; desf.
× apply hbpath_valid_cons in PV.
rewrite <- !app_assoc, <- !app_comm_cons, app_nil_l in PV.
exploit (hmap_defined_on_path CONS_RF PV edge´´); try find_in_list.
ins; desc.
exploit (DOM edge´´); eauto; try find_in_list.
ins; desc.
exploit (step_from_nabla CONS_RF edge´´ edge´); eauto.
by apply (proj1 (proj2 PV)); find_in_list.
by apply (proj1 (proj2 PV)); find_in_list.
eby eapply (proj1 PV).
by apply ((proj2 (proj2 PV))); find_in_list.
by intro X; rewrite X in ×.
intro C; desf; eauto.
+ destruct edge´; ins; eauto.
+ red in C0; desf.
Qed.
Lemma hb_trough_path_simple:
∀ lab sb rf mo (ACYCLIC: IrreflexiveHBuRF sb rf) (CONS_RF: ConsistentRF_basic lab sb rf mo)
path edge1 edgeN hmap (PV: hbpath_valid lab sb rf hmap (edge1 :: path ++ edgeN :: nil))
l (NORMALfst: ∀ hf (MAPfst: hmap edge1 = Hdef hf), HVlabeled (hf l) HLnormal)
(NORMALlst: ∀ hf (MAPfst: hmap edgeN = Hdef hf), HVlabeled (hf l) HLnormal)
(MID: ∀ edge (IN: In edge path) hf (MAP: hmap edge = Hdef hf), ¬ HVlabeled (hf l) HLnormal)
(NA: ∀ edge (IN: In edge (edge1 :: path ++ edgeN :: nil)) hf (MAP: hmap edge = Hdef hf),
is_nonatomic (hf l)),
∀ b (SND: hb_snd edge1 = Some b), clos_refl_trans _ (happens_before lab sb rf mo) b (hb_fst edgeN).
Proof.
ins.
exploit (structure_of_triangled_path ACYCLIC CONS_RF (hmap := hmap) (path := path)).
by apply hbpath_valid_cons, hbpath_valid_app in PV; desf.
by instantiate (1 := l); ins; repeat split;
solve [exploit (NA edge); try find_in_list; ins; desf; eauto | eby eapply MID].
ins; desf.
exploit (hmap_defined_on_path CONS_RF PV edge1); try find_in_list; ins; desc.
rename hf into h1.
assert (ONE: HVlabeled (h1 l) HLnormal ∧ is_nonatomic (h1 l)).
{
split.
apply NORMALfst; congruence.
exploit (NA edge1); find_in_list.
}
exploit (hmap_defined_on_path CONS_RF PV edgeN); try find_in_list; ins; desc.
rename hf into hN.
assert (N: HVlabeled (hN l) HLnormal ∧ is_nonatomic (hN l)).
{
split.
apply NORMALlst; congruence.
exploit (NA edgeN); find_in_list.
}
des_list_tail path1 path1´ edgei; destruct path2 as [ | edgej path2´]; desf.
{
rewrite app_nil_l in PV.
exploit ((proj1 PV) nil); ins.
rewrite x2 in SND; desf; vauto.
}
{
rewrite app_nil_l, <- app_comm_cons in ×.
exploit (hmap_defined_on_path CONS_RF PV edgej); try find_in_list; ins; desc.
rename hf into hj.
assert (J: HVlabeled (hj l) HLnabla ∧ is_nonatomic (hj l)).
{
split.
by eapply LAB2; ins; eauto.
exploit (NA edgej); ins; desf; eauto; find_in_list.
}
assert (SINK: ¬ is_sink edgej).
{
destruct edgej; ins.
red in PV; desc; clear - WFP EVP ACYCLIC.
exploit sink_is_always_last; eauto; ins; eauto; desf.
rewrite last_app in H0; ins; desf.
exploit NoDup_path; ins; eauto.
repeat (rewrite nodup_cons in *; desf).
destruct x1; rewrite In_app; ins; eauto.
}
desc.
assert (P2sb: ∀ edge (InP2: In edge path2´), is_sb edge).
{
ins.
apply hbpath_valid_cons in PV.
rewrite app_comm_cons in PV.
exploit (only_first_nabla_is_rf CONS_RF (proj1 (hbpath_valid_app _ _ PV)) l); eauto.
by split; try eapply NA; try eapply LAB2; try edone; ins; desf; find_in_list.
ins; desf.
apply hbpath_valid_cons in PV; red in PV; desc.
exfalso; eapply sink_is_always_last_alt; eauto.
}
exploit (step_from_normal CONS_RF edge1 edgej); eauto.
by apply (proj1 (proj2 PV)); ins; rewrite In_app; ins; eauto.
by apply (proj1 (proj2 PV)); ins; rewrite In_app; ins; eauto.
by eapply ((proj1 PV) nil); rewrite app_comm_cons; eauto.
by apply ((proj2 (proj2 PV))); ins; rewrite In_app; ins; eauto.
by intro X; rewrite X in ×.
intro FIRST_CHANGE; desf; try (by red in J; desf; desf).
des_list_tail path2´ path edgek.
{
rewrite app_nil_l in *; ins.
exploit ((proj1 PV) (edge1 :: nil)).
eby rewrite <- app_comm_cons, app_nil_l.
intro E.
exploit ((proj1 (proj2 PV)) edgej); vauto.
intro EV.
exploit (step_from_nabla CONS_RF edgej edgeN); eauto.
by apply (proj1 (proj2 PV)); ins; eauto.
by apply ((proj2 (proj2 PV))); ins; eauto.
by intro X; rewrite X in ×.
intro SECOND_CHANGE; desf; try (by red in N; desf; desf).
× exploit ((proj1 PV) nil).
eby rewrite app_nil_l.
ins; desf.
apply rt_step, t_step. right. red. left. intuition.
destruct edgej; ins; desf.
eexists,; eauto.
vauto.
× exfalso.
clear - FIRST_CHANGE1 SECOND_CHANGE2 E EV CONS_RF.
destruct edgej; ins; desf.
specialize (CONS_RF (hb_fst edgeN)); desf; desf.
by destruct (lab (hb_fst edgeN)).
}
{
rewrite <- app_assoc in PV, NA; ins.
exploit (hmap_defined_on_path CONS_RF PV edgek); try find_in_list; ins; desc.
rename hf into hk.
assert (K: HVlabeled (hk l) HLnabla ∧ is_nonatomic (hk l)).
{
split.
by eapply (LAB2 edgek); eauto; rewrite In_app; ins; eauto.
exploit (NA edgek); ins; desf; eauto; rewrite In_app; ins; eauto.
}
desc.
exploit ((proj1 PV) (edge1 :: edgej :: path)); try edone.
intro Ek.
exploit ((proj1 (proj2 PV)) edgek).
by ins; rewrite In_app; ins; eauto.
intro EVk.
exploit (step_from_nabla CONS_RF edgek edgeN); eauto.
by apply (proj1 (proj2 PV)); ins; rewrite In_app; ins; eauto 6.
by apply ( (proj2 (proj2 PV))); ins; rewrite In_app; ins; eauto 6.
by intro X; rewrite X in ×.
intro SECOND_CHANGE; desf.
× red in N; desf; desf.
× exfalso.
exploit (P2sb edgek).
by rewrite In_app; ins; eauto.
clear - SECOND_CHANGE; destruct edgek; ins.
× exploit ((proj1 PV) nil).
eby rewrite app_nil_l.
ins; desf.
apply rt_step, t_step. right. red. right; left. intuition.
exploit ((proj1 (proj2 PV)) edgej); vauto.
destruct edgej; ins.
eexists,; repeat split; eauto.
2: by vauto.
clear - PV Ek SECOND_CHANGE P2sb; apply hbpath_valid_cons in PV.
exploit (@sb_trough_path lab sb rf hmap (path ++ edgek :: nil) (hb_rf e e´) edgeN); ins; eauto.
rewrite app_comm_cons in PV.
by rewrite <- app_assoc, <- app_comm_cons.
}
}
{
exfalso.
rewrite app_nil_r, <- app_assoc, <- app_comm_cons, app_nil_l in ×.
exploit (hmap_defined_on_path CONS_RF PV edgei); try find_in_list; ins; desc.
rename hf into hi.
exploit (step_from_triangle CONS_RF edgei edgeN); eauto.
by apply (proj1 (proj2 PV)); find_in_list.
by apply (proj1 (proj2 PV)); find_in_list.
by eapply (proj1 PV); rewrite app_comm_cons; eauto.
by apply ((proj2 (proj2 PV))); find_in_list.
by instantiate (1 := l); exploit (NA edgei); eauto; ins; desf; find_in_list.
by eapply LAB1; eauto; find_in_list.
by intro X; rewrite X in ×.
ins; desf; red in N; desf; desf.
}
{
rewrite <- !app_assoc, <- !app_comm_cons, app_nil_l in ×.
exploit (hmap_defined_on_path CONS_RF PV edgei); try find_in_list; ins; desc.
rename hf into hi.
assert (I: HVlabeled (hi l) HLtriangle ∧ is_nonatomic (hi l)).
{
split.
by eapply LAB1; eauto; rewrite In_app; ins; eauto.
exploit (NA edgei); ins; desf; eauto; rewrite In_app; ins; eauto.
}
exploit (hmap_defined_on_path CONS_RF PV edgej); try find_in_list; ins; desc.
rename hf into hj.
assert (J: HVlabeled (hj l) HLnabla ∧ is_nonatomic (hj l)).
{
split.
by eapply LAB2; ins; eauto.
exploit (NA edgej); ins; desf; eauto; rewrite In_app; ins; eauto.
}
assert (<< EVi: edge_valid lab sb rf edgei >> ∧ << EVj: edge_valid lab sb rf edgej >>).
{
unnw; split; [exploit (proj1 (proj2 PV) edgei) | exploit (proj1 (proj2 PV) edgej)];
ins; eauto; repeat progress (rewrite ?In_app; ins); eauto.
}
desc.
exploit ((proj1 PV) (edge1 :: path1´)).
eby rewrite <- app_comm_cons.
intro Ei.
exploit (step_from_triangle CONS_RF edgei edgej); eauto.
apply ((proj2 (proj2 PV))); repeat progress (rewrite ?In_app; ins); eauto.
by intro X; rewrite X in ×.
intro M; desf.
× red in J; desf.
× assert (P1sb: ∀ edge (InP1: In edge path1´), is_sb edge).
{
ins.
exploit (hmap_defined_on_path CONS_RF PV edge); try find_in_list; ins; desc.
exploit (triangles_never_on_rf edge); eauto.
by apply (proj1 (proj2 PV)); find_in_list.
by apply ((proj2 (proj2 PV))); find_in_list.
by instantiate (1 := l); exploit (NA edge); eauto; try find_in_list; ins;
intro X; instantiate; rewrite X in ×.
by eapply LAB1; eauto; find_in_list.
ins; desf.
exfalso.
rewrite !app_comm_cons, !app_assoc in PV.
red in PV; desc; eapply sink_is_always_last_alt; eauto.
eexists,; eauto; find_in_list.
}
assert (P2sb: ∀ edge (InP2: In edge path2´), is_sb edge).
{
ins.
apply hbpath_valid_cons, hbpath_valid_app in PV; desc.
apply hbpath_valid_cons in PV0.
rewrite app_comm_cons in PV0.
exploit (only_first_nabla_is_rf CONS_RF (proj1 (hbpath_valid_app _ _ PV0)) l); eauto.
by split; try eapply NA; try eapply LAB2; try edone; ins; desf; find_in_list.
ins; desf.
apply hbpath_valid_cons in PV0; red in PV0; desc.
exfalso; eapply sink_is_always_last_alt; eauto.
}
assert (FENCErel: is_release_fence (lab b)).
{
destruct path1´ as [ | edge path].
× rewrite app_nil_l in ×.
exploit (proj1 PV nil).
eby rewrite <- app_nil_l.
ins; desf.
exploit (step_from_normal CONS_RF edge1 edgei); eauto.
by apply (proj1 (proj2 PV)); find_in_list.
by apply ((proj2 (proj2 PV))); find_in_list.
by intro X; rewrite X in ×.
intro C; desf; try (by red in I; desf).
exfalso; red in PV; desf; clear - WFP C.
rewrite !app_comm_cons in WFP.
eapply sink_is_always_last_alt; eauto.
eexists,; eauto; find_in_list.
× rewrite <- app_comm_cons in ×.
exploit (proj1 PV nil).
eby rewrite <- app_nil_l.
ins; desf.
exploit (hmap_defined_on_path CONS_RF PV edge); try find_in_list; ins; desc.
assert (E: HVlabeled (hf l) HLtriangle ∧ is_nonatomic (hf l)).
{
split.
by apply (LAB1 edge); find_in_list.
exploit (NA edge); ins; desf; eauto; find_in_list.
}
desc.
exploit (step_from_normal CONS_RF edge1 edge); eauto.
by apply (proj1 (proj2 PV)); find_in_list.
by apply (proj1 (proj2 PV)); find_in_list.
by apply ((proj2 (proj2 PV))); find_in_list.
by intro X; rewrite X in ×.
intro C; desf; try (by red in E; desf).
exfalso; red in PV; desf; clear - WFP C.
rewrite !app_comm_cons, !app_assoc in WFP.
eapply sink_is_always_last_alt; eauto.
eexists,; eauto; find_in_list.
}
des_list_tail path2´ path edgek.
+ rewrite app_nil_l in ×.
exploit (proj1 (hbpath_valid_cons (proj2 (hbpath_valid_app _ _ (hbpath_valid_cons PV)))) nil).
eby rewrite <- app_nil_l.
intro E.
exploit (step_from_nabla CONS_RF edgej edgeN); eauto.
by apply (proj1 (proj2 PV)); find_in_list.
by apply ((proj2 (proj2 PV))); find_in_list.
by intro X; rewrite X in ×.
intro C. desf.
- red in C ; desf.
- apply rt_step, t_step; right. red.
right; right; left.
intuition.
destruct edgej; ins; desf.
∃ e, e; repeat split; try by vauto.
rewrite <- (app_nil_l (_ :: _ :: nil)), <- (app_nil_l (_ :: nil)), !app_comm_cons, !app_assoc in PV.
apply hbpath_valid_app in PV; desc.
rewrite <- !app_comm_cons in PV.
exploit sb_trough_path; eauto; ins.
rewrite In_app in IN; desf; ins; desf; intuition.
- destruct edgej; ins.
+ rewrite <- app_assoc, <- app_comm_cons, app_nil_l in ×.
exploit (proj1 (hbpath_valid_cons (hbpath_valid_cons
(proj2 (hbpath_valid_app _ _(hbpath_valid_cons PV)))))); eauto.
intro E.
exploit (hmap_defined_on_path CONS_RF PV edgek); try find_in_list; ins; desc.
rename hf into hk.
assert (K: HVlabeled (hk l) HLnabla ∧ is_nonatomic (hk l)).
{
split.
by apply (LAB2 edgek); find_in_list.
exploit (NA edgek); ins; desf; eauto; find_in_list.
}
desc.
exploit (P2sb edgek); try find_in_list.
intro SBk.
exploit (step_from_nabla CONS_RF edgek edgeN); eauto.
by apply (proj1 (proj2 PV)); find_in_list.
by apply (proj1 (proj2 PV)); find_in_list.
by apply ( (proj2 (proj2 PV))); find_in_list.
by intro X; rewrite X in ×.
intro C; desf.
by red in C; desf.
by destruct edgek.
apply rt_step, t_step; right. red.
repeat right.
intuition.
destruct edgej; ins.
∃ e, e, e´; repeat split; try by vauto.
- rewrite <- (app_nil_l path), !app_comm_cons, !app_assoc in PV.
do 2 (apply hbpath_valid_app in PV; desc).
rewrite <- app_comm_cons, <- (app_nil_l (_ :: nil)),
!app_comm_cons, app_assoc, <- !app_comm_cons in PV.
exploit sb_trough_path; eauto.
ins; rewrite In_app in IN; ins; desf; intuition.
- apply hbpath_valid_cons, hbpath_valid_app in PV; desc.
apply hbpath_valid_cons in PV0.
rewrite <- (app_nil_l (_ :: nil)), !app_comm_cons, app_assoc, <- !app_comm_cons in PV0.
exploit sb_trough_path; eauto; ins.
× exfalso; red in PV; desf; clear - WFP M1.
rewrite !app_comm_cons, !app_assoc in WFP.
eapply sink_is_always_last_alt; eauto.
eexists,; eauto.
repeat progress (rewrite ?In_app; ins); eauto.
}
Qed.
Require Import Wf Wf_nat.
Lemma hb_trough_path:
∀ lab sb rf mo (ACYCLIC: IrreflexiveHBuRF sb rf) (CONS_RF: ConsistentRF_basic lab sb rf mo)
path edge1 edgeN hmap (PV: hbpath_valid lab sb rf hmap (edge1 :: path ++ edgeN :: nil))
l (NORMALfst: ∀ hf (MAPfst: hmap edge1 = Hdef hf), HVlabeled (hf l) HLnormal)
(NORMALlst: ∀ hf (MAPfst: hmap edgeN = Hdef hf), HVlabeled (hf l) HLnormal)
(NA: ∀ edge (IN: In edge (edge1 :: path ++ edgeN :: nil)) hf (MAP: hmap edge = Hdef hf),
is_nonatomic (hf l)),
∀ b (SND1: hb_snd edge1 = Some b), clos_refl_trans _ (happens_before lab sb rf mo) b (hb_fst edgeN).
Proof.
induction path using (well_founded_induction (well_founded_ltof _ (@length _))).
rename H into IH.
destruct path as [ | edge2 path´]; ins.
by exploit ((proj1 PV) nil nil edge1 edgeN); ins; desf; apply rt_refl.
exploit ((proj1 PV) nil).
eby rewrite ?app_nil_l.
intro FSTN.
exploit (hmap_defined_on_path CONS_RF PV edge2); try find_in_list; ins; desc.
rename hf into hf2.
assert (C: ∃ c, hb_snd edge2 = Some c).
{
red in PV; desf; clear - WFP.
apply hbpath_wf_cons in WFP.
destruct path´; ins; exploit (WFP nil); ins; eauto.
}
desc.
destruct (classic (HVlabeled (hf2 l) HLnormal)).
{
apply rt_trans with (y := c).
× apply rt_step, t_step; left.
red in PV; desf.
exploit (EVP edge2); ins; eauto.
exploit (PVA edge2); ins; eauto.
exploit (NA edge2); ins; eauto.
destruct edge2; ins; desf.
exfalso; eapply no_normals_on_rf; eauto.
by intro X; rewrite X in ×.
× eapply (IH path´); try (eby eapply hbpath_valid_cons); eauto; try edone; ins.
congruence.
}
{
exploit (first_exists (path´ ++ edgeN :: nil)
(fun edge ⇒ ∀ hf, hmap edge = Hdef hf → HVlabeled (hf l) HLnormal)).
by ∃ edgeN; intuition.
intro EX; desf.
rename a´ into edgei; rename l1 into path1.
des_list_tail l2 path2 edgeN´.
× clear IH.
apply app_inj_tail in EX; desf.
rewrite app_comm_cons in PV.
exploit (hb_trough_path_simple ACYCLIC CONS_RF); eauto; ins; desf.
by inv MAP; congruence.
specialize (EX1 edge IN).
apply not_all_ex_not in EX1; desc.
apply imply_to_and in EX1; desc; congruence.
× rewrite EX in ×.
rewrite !app_comm_cons, !app_assoc in EX.
apply app_inj_tail in EX; desf.
exploit (proj1 (proj2 PV) edgei); try find_in_list.
intro EVi.
exploit (hmap_defined_on_path CONS_RF PV edgei); try find_in_list; ins; desc.
rename hf into hfi.
destruct edgei; ins; desf.
Focus 2. exfalso; eapply no_normals_on_rf; eauto.
by eapply ((proj2 (proj2 PV)) (hb_rf _ _)); find_in_list.
by exploit (NA (hb_rf e e´)); try find_in_list; ins; intro X; instantiate; rewrite X in ×.
Focus 2. exfalso; red in PV; desf; clear - WFP.
do 2 apply hbpath_wf_cons in WFP.
by destruct path2; ins; exploit (WFP path1); ins.
apply rt_trans with (y := e´).
apply rt_trans with (y := e).
+ eapply (hb_trough_path_simple _ _ _ (hb_sb _ _) (edge1 := edge1)); eauto.
- rewrite <- (app_nil_l path2), !app_comm_cons, !app_assoc in PV.
eby do 2 (apply hbpath_valid_app in PV; desc); rewrite <- app_comm_cons in PV.
- ins; desf; try congruence.
specialize (EX1 edge IN).
apply not_all_ex_not in EX1; desc.
apply imply_to_and in EX1; desc; congruence.
- ins; eapply NA; try edone.
rewrite In_app in IN; ins; desf; find_in_list.
+ apply rt_step, t_step; vauto.
+ do 2 apply hbpath_valid_cons in PV; apply hbpath_valid_app in PV; desc.
eapply (IH _ _ _ _ _ PV0); eauto.
ins; eapply NA; try edone.
rewrite In_app in IN; ins; desf; find_in_list.
}
Grab Existential Variables.
× red; ins; rewrite length_app; ins; omega.
× trivial.
× trivial.
Qed.
This page has been generated by coqdoc