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 path ihc.
Set Implicit Arguments.
Lemma hist_closed_connect:
∀ lab sb rf hmap path a b V
(CONNECT: hbpath_connects lab sb rf hmap path a b)
(HC: hist_closed sb rf V) (IN: In b V),
In a V.
Proof.
ins.
apply connect_implies_hbUrf, clos_refl_trans_hbUrfE in CONNECT; desf.
eby eapply hist_closedD.
Qed.
Lemma nonatomics_strongly_connected_helper:
∀ acts lab sb rf mo hmap V
(FIN: ExecutionFinite acts lab sb)
(ACYCLIC: IrreflexiveHBuRF sb rf)
(CONS_RF: ConsistentRF_basic lab sb rf mo)
(CONS_A: ConsistentAlloc lab)
(HC: hist_closed sb rf V) (VALID: hmap_valids lab sb rf hmap V)
a1 a2 b1 b2 (DIF: b1 ≠ b2) (EV1: sb a1 b1) (EV2: sb a2 b2) (IN1: In a1 V) (IN2: In a2 V)
hf1 hf2 (MAP1: hmap (hb_sb a1 b1) = Hdef hf1) (MAP2: hmap (hb_sb a2 b2) = Hdef hf2)
l (ALL1: hf1 l ≠ HVnone) (ALL2: hf2 l ≠ HVnone) (NA: is_nonatomic (hf1 l) ∨ is_nonatomic (hf2 l)),
∀ n, ∃ path1 path2,
<< CONNECT: hbpath_connects lab sb rf hmap (path1 ++ path2) b1 a2 ∨
hbpath_connects lab sb rf hmap (path1 ++ path2) b2 a1 >> ∧
<< ALL: ∀ edge (IN: In edge path1) hf (MAP: hmap edge = Hdef hf), hf l ≠ HVnone >> ∧
<< LEN: path2 = nil ∨ length path1 = n >>.
Proof.
induction n.
{
assert (DEP: ¬ independent sb rf (hb_sb a1 b1 :: hb_sb a2 b2 :: nil)).
by eapply not_independent_two; eauto; try congruence.
clear NA.
eapply destruct_not_independent_two in DEP; ins; eauto; desf.
× apply clos_refl_transE in DEP0; desf.
by ∃ nil, nil; ins; split; vauto.
eapply clos_trans_hbUrfE, hbUrf_implies_hbpath in DEP0; eauto; desf.
∃ nil, path; ins; split; vauto.
× apply clos_refl_transE in DEP0; desf.
by ∃ nil, nil; ins; split; vauto.
eapply clos_trans_hbUrfE, hbUrf_implies_hbpath in DEP0; eauto; desf.
∃ nil, path; ins; split; vauto.
}
{
revert NA; desf; try (by ∃ path1, nil; ins; split; vauto); ins.
{
des_list_tail path1 path1´ edge1; ins.
× eapply location_does_not_vanish with (b := b1) in ALL1; eauto; ins; desc.
2: eby eapply VALID, hist_closed_connect.
destruct (classic (edge´ = hb_sb a2 b2)) as [| NEQ]; clarify; ins.
by ∃ nil, nil; repeat split; ins; vauto.
∃ (edge´ :: nil); ins.
assert (DEP: ¬ independent sb rf (edge´ :: hb_sb a2 b2 :: nil)).
{
eapply not_independent_two; eauto; ins; try congruence.
eby eapply hist_closed_connect.
desf; eauto.
left; eapply (na_propagates_forward _ (hb_sb a1 _)); eauto.
eby eapply VALID, hist_closed_connect.
}
clear NA.
eapply destruct_not_independent_two in DEP; ins; eauto; desf.
{
apply clos_refl_transE in DEP0; desf.
× ∃ nil; unnw; repeat split; ins; desf; eauto; try congruence.
left; red; ins.
right; split.
2: by eexists,,; repeat split; eauto.
red; unnw; repeat split; ins; desf.
+ by apply hbpath_wf_one.
+ eby eapply VALID, hist_closed_connect.
× eapply clos_trans_hbUrfE, hbUrf_implies_hbpath in DEP0; eauto; desf.
∃ path; unnw; repeat split; ins; eauto; desf; try congruence.
left; red; ins.
right; split.
+ apply hbpath_valid_cons_inv; ins; desf.
eby eapply connects_implies_valid.
eby eapply VALID, hist_closed_connect.
eby eapply VALID, hist_closed_connect.
by red in DEP0; desf.
+ eexists,; repeat split; eauto.
red in DEP0; desf.
apply olast_inv in DEP3; desf.
rewrite last_app; ins.
}
{
exfalso; clear - ACYCLIC CONNECT DEP0 EV1 EV2.
apply connect_implies_hbUrf in CONNECT.
apply clos_refl_transE in CONNECT; apply clos_refl_transE in DEP0; desf.
× eapply ACYCLIC, t_step; vauto.
× apply clos_trans_hbUrfE in CONNECT.
eapply ACYCLIC, t_trans; eauto.
apply t_step; vauto.
× apply clos_trans_hbUrfE in DEP0.
eapply ACYCLIC, t_trans; eauto.
apply t_step; vauto.
× apply clos_trans_hbUrfE in DEP0; apply clos_trans_hbUrfE in CONNECT.
eapply ACYCLIC, t_trans; eauto.
eapply t_trans; eauto.
apply t_step; vauto.
}
× rewrite <- app_assoc in *; ins.
destruct path2 as [ | edge2 path2´]; ins.
by ∃ (path1´ ++ edge1 :: nil), nil; unnw; rewrite app_nil_r; split; eauto.
exploit (hmap_defined_on_path CONS_RF (connects_implies_valid CONNECT) edge1); try find_in_list; ins; desc.
exploit (location_does_not_vanish CONS_RF edge1); try edone.
by apply (proj1 (proj2 (connects_implies_valid CONNECT))); find_in_list.
eby eapply (proj1 (connects_implies_valid CONNECT)).
by apply (proj2 (proj2 (connects_implies_valid CONNECT))); find_in_list.
by apply (ALL edge1); find_in_list.
ins; desc.
destruct (classic (edge´ = hb_sb a2 b2)) as [| NEQ]; clarify; ins.
{
∃ (path1´ ++ edge1 :: nil), nil; unnw; rewrite app_nil_r; split; ins; vauto.
left; red. right; ins; split.
× rewrite <- (app_nil_l path2´), app_comm_cons, <- (app_nil_l (_ :: nil)), app_comm_cons,
!app_assoc in CONNECT.
apply connects_implies_valid, hbpath_valid_app in CONNECT; desc.
rewrite app_comm_cons, app_assoc in CONNECT.
by apply hbpath_valid_app in CONNECT; desc.
× clear NA; red in CONNECT; desf.
by exploit app_cons_not_nil; eauto; ins.
∃ fst, edge1; repeat split.
by destruct path1´; ins.
by destruct path1´; ins; rewrite last_app.
eby eapply (proj1 CONNECT).
}
∃ (path1´ ++ edge1 :: edge´ :: nil); ins.
rewrite !length_app, plus_n_Sm; ins.
assert (DEP: ¬ independent sb rf (edge´ :: hb_sb a2 b2 :: nil)).
{
eapply not_independent_two; eauto; ins.
× rewrite <- CON.
apply hbpath_connects_app2, hbpath_connects_cons in CONNECT.
eby eapply hist_closed_connect.
× desf; eauto.
left; eapply (na_propagates_forward _ edge1); eauto.
by apply (proj1 (proj2 (connects_implies_valid CONNECT))); find_in_list.
eby rewrite <- CON; eapply (proj1 (connects_implies_valid CONNECT)).
by rewrite <- CON; apply (proj2 (proj2 (connects_implies_valid CONNECT))); find_in_list.
assert (PV: hbpath_valid lab sb rf hmap (hb_sb a1 b1 :: path1´ ++ edge1 :: nil)).
{
apply hbpath_valid_cons_inv; ins; eauto; desf.
× rewrite <- (app_nil_l path2´), app_comm_cons, <- (app_nil_l (_ :: nil)), app_comm_cons,
!app_assoc in CONNECT.
apply connects_implies_valid, hbpath_valid_app in CONNECT; desc.
rewrite app_comm_cons, app_assoc in CONNECT.
by apply hbpath_valid_app in CONNECT; desc.
× eby eapply VALID, hist_closed_connect.
× red in CONNECT; desf.
by exploit app_cons_not_nil; eauto; ins.
destruct path1´; ins; desf.
}
eapply nonatomic_loc_on_path; eauto.
+ ins; rewrite In_app in IN; ins; desf; solve [eby rewrite MAP in *; desf |
eapply ALL; try edone; find_in_list].
+ ∃ (hb_sb a1 b1); unnw; split; ins; try find_in_list.
eby rewrite MAP in *; desf.
+ find_in_list.
}
clear NA.
eapply destruct_not_independent_two in DEP; ins; eauto; desf.
{
apply clos_refl_transE in DEP0; desf.
× ∃ nil; unnw; repeat split; ins; desf; eauto; try congruence.
2: by repeat progress (rewrite ?In_app in *; ins); desf;
solve [eapply ALL; eauto; find_in_list| rewrite MAP in *; desf].
rewrite app_nil_r.
left; red; ins.
right; split.
Focus 2.
red in CONNECT; desf.
by exploit app_cons_not_nil; eauto; ins.
eexists,; repeat split; eauto; destruct path1´; ins; desf.
by rewrite last_app; ins.
red; unnw; repeat split; ins; desf.
+ red; ins.
destruct path2.
- rewrite <- (app_nil_l (edge´ :: _)), <- (app_nil_l (edge3 :: _)),
!app_comm_cons, !app_assoc in DECOMP.
do 2 (apply app_inj_tail in DECOMP; desf).
rewrite <- CON.
eby eapply (proj1 (connects_implies_valid CONNECT)).
- assert (DECOMP´: ∃ path, path1´ ++ edge1 :: nil = path1 ++ edge0 :: edge3 :: path).
{
clear - DECOMP.
des_list_tail path2 path edge.
× rewrite <- (app_nil_l (edge´ :: _)), <- (app_nil_l (h :: _)),
!app_comm_cons, !app_assoc in DECOMP.
apply app_inj_tail in DECOMP; desf.
eby eexists.
× rewrite <- (app_nil_l (edge´ :: _)), !app_comm_cons, !app_assoc in DECOMP.
apply app_inj_tail in DECOMP; desf.
eby eexists.
}
desf.
rewrite <- (app_nil_l (edge2 :: _)), !app_comm_cons, !app_assoc, DECOMP´ in CONNECT.
apply connects_implies_valid, hbpath_valid_app in CONNECT; desf.
eby eapply (proj1 CONNECT).
+ repeat progress (rewrite ?In_app in *; ins); desf; eauto;
eapply (proj1 (proj2 (connects_implies_valid CONNECT))); find_in_list.
+ repeat progress (rewrite ?In_app in *; ins); desf; eauto;
rewrite <- ?CON; eapply (proj2 (proj2 (connects_implies_valid CONNECT))); find_in_list.
× eapply clos_trans_hbUrfE, hbUrf_implies_hbpath in DEP0; eauto; desf.
∃ path; unnw; repeat split; ins; eauto; desf.
2: by repeat progress (rewrite ?In_app in *; ins); desf;
solve [eapply ALL; eauto; find_in_list| rewrite MAP in *; desf].
left; rewrite <- app_assoc; red; ins.
right; split.
+ red; unnw; repeat split; ins.
- red; ins.
destruct path as [ | edge´´ path´´].
{
destruct path2.
× rewrite <- (app_nil_l (edge´ :: _)), <- (app_nil_l (edge3 :: _)),
!app_comm_cons, !app_assoc in DECOMP.
do 2 (apply app_inj_tail in DECOMP; desf).
rewrite <- CON.
eby eapply (proj1 (connects_implies_valid CONNECT)).
× assert (DECOMP´: ∃ path, path1´ ++ edge1 :: nil = path1 ++ edge0 :: edge3 :: path).
{
clear - DECOMP.
des_list_tail path2 path edge.
× rewrite <- (app_nil_l (edge´ :: _)), <- (app_nil_l (h :: _)),
!app_comm_cons, !app_assoc in DECOMP.
apply app_inj_tail in DECOMP; desf.
eby eexists.
× rewrite <- (app_nil_l (edge´ :: _)), !app_comm_cons, !app_assoc in DECOMP.
apply app_inj_tail in DECOMP; desf.
eby eexists.
}
desf.
rewrite <- (app_nil_l (edge2 :: _)), !app_comm_cons, !app_assoc, DECOMP´ in CONNECT.
apply connects_implies_valid, hbpath_valid_app in CONNECT; desf.
eby eapply (proj1 CONNECT).
}
assert( (edge0 = edge1 ∧ edge3 = edge´) ∨ (edge0 = edge´ ∧ edge3 = edge´´) ∨
(∃ path, edge´´ :: path´´ = path ++ edge0 :: edge3 :: path2) ∨
(∃ path, path1´ ++ edge1 :: nil = path1 ++ edge0 :: edge3 :: path) ).
{
clear - DECOMP.
revert DECOMP.
revert path1´ path1 path´´ path2 edge1 edge´ edge´´ edge0 edge3.
induction path1´ as [ | edgeA pathA]; ins.
× destruct path1 as [ | edgeB pathB]; ins; desf; eauto.
destruct pathB as [ | edgeC pathC]; ins; desf; eauto.
× destruct path1 as [ | edgeB pathB]; ins; desf.
+ destruct pathA as [ | edgeC pathC]; ins; desf; eauto.
+ exploit IHpathA; eauto; ins; desf; eauto.
by repeat right; ∃ path; rewrite x0.
}
desf.
eby rewrite <- CON; eapply (proj1 (connects_implies_valid CONNECT)).
by red in DEP0; ins; desf.
eby rewrite H in DEP0; eapply (proj1 (connects_implies_valid DEP0)).
rewrite <- (app_nil_l (edge2 :: _)), !app_comm_cons, !app_assoc, H in CONNECT.
apply connects_implies_valid, hbpath_valid_app in CONNECT; desf.
eby eapply (proj1 CONNECT).
- by repeat progress (rewrite ?In_app in *; ins); desf; eauto;
try (eapply (proj1 (proj2 (connects_implies_valid CONNECT))); find_in_list);
eapply (proj1 (proj2 (connects_implies_valid DEP0))).
- by repeat progress (rewrite ?In_app in *; ins); desf; eauto; rewrite <- ?CON;
try (eapply (proj2 (proj2 (connects_implies_valid CONNECT))); find_in_list);
eapply (proj2 (proj2 (connects_implies_valid DEP0))).
+ red in CONNECT; desf.
by exploit app_cons_not_nil; eauto.
∃ fst.
red in DEP0; desf.
by ∃ edge´; repeat split; eauto; destruct path1´; ins; rewrite last_app; ins.
by ∃ lst0; repeat split; eauto; destruct path1´; ins; apply olast_inv in DEP3; desf;
repeat progress (rewrite ?last_app; ins).
}
{ exfalso; rewrite <- CON in *; clear - ACYCLIC CONNECT DEP0 EV2.
apply hbpath_connects_app2, hbpath_connects_cons, connect_implies_hbUrf in CONNECT.
apply clos_refl_transE in CONNECT; apply clos_refl_transE in DEP0; desf.
× eapply ACYCLIC, t_step; vauto.
× apply clos_trans_hbUrfE in CONNECT.
eapply ACYCLIC, t_trans; eauto.
apply t_step; vauto.
× apply clos_trans_hbUrfE in DEP0.
eapply ACYCLIC, t_trans; eauto.
apply t_step; vauto.
× apply clos_trans_hbUrfE in DEP0; apply clos_trans_hbUrfE in CONNECT.
eapply ACYCLIC, t_trans; eauto.
eapply t_trans; eauto.
apply t_step; vauto.
}
}
{
des_list_tail path1 path1´ edge1; ins.
× eapply location_does_not_vanish with (b := b2) in ALL2; eauto; ins; desc.
2: eby eapply VALID, hist_closed_connect.
destruct (classic (edge´ = hb_sb a1 b1)) as [| NEQ]; clarify; ins.
by ∃ nil, nil; repeat split; ins; vauto.
∃ (edge´ :: nil); ins.
assert (DEP: ¬ independent sb rf (edge´ :: hb_sb a1 b1 :: nil)).
{
eapply not_independent_two; eauto; ins; try congruence.
eby eapply hist_closed_connect.
desf; eauto.
left; eapply (na_propagates_forward _ (hb_sb a2 _)); eauto.
eby eapply VALID, hist_closed_connect.
}
clear NA.
eapply destruct_not_independent_two in DEP; ins; eauto; desf.
{
apply clos_refl_transE in DEP0; desf.
× ∃ nil; unnw; repeat split; ins; desf; eauto; try congruence.
right; red; ins.
right; split.
2: by eexists,,; repeat split; eauto.
red; unnw; repeat split; ins; desf.
+ by apply hbpath_wf_one.
+ eby eapply VALID, hist_closed_connect.
× eapply clos_trans_hbUrfE, hbUrf_implies_hbpath in DEP0; eauto; desf.
∃ path; unnw; repeat split; ins; eauto; desf; try congruence.
right; red; ins.
right; split.
+ apply hbpath_valid_cons_inv; ins; desf.
- eby eapply connects_implies_valid.
- eby eapply VALID, hist_closed_connect.
- eby eapply VALID, hist_closed_connect.
- red in DEP0; desf.
+ eexists,; repeat split; eauto.
red in DEP0; desf.
apply olast_inv in DEP3; desf.
rewrite last_app; ins.
}
{ exfalso; clear - ACYCLIC CONNECT DEP0 EV1.
apply connect_implies_hbUrf in CONNECT.
apply clos_refl_transE in CONNECT; apply clos_refl_transE in DEP0; desf.
× eapply ACYCLIC, t_step; vauto.
× apply clos_trans_hbUrfE in CONNECT.
eapply ACYCLIC, t_trans; eauto.
apply t_step; vauto.
× apply clos_trans_hbUrfE in DEP0.
eapply ACYCLIC, t_trans; eauto.
apply t_step; vauto.
× apply clos_trans_hbUrfE in DEP0; apply clos_trans_hbUrfE in CONNECT.
eapply ACYCLIC, t_trans; eauto.
eapply t_trans; eauto.
apply t_step; vauto.
}
× rewrite <- app_assoc in *; ins.
destruct path2 as [ | edge2 path2´]; ins.
by ∃ (path1´ ++ edge1 :: nil), nil; unnw; rewrite app_nil_r; split; eauto.
exploit (hmap_defined_on_path CONS_RF (connects_implies_valid CONNECT) edge1); try find_in_list; ins; desc.
exploit (location_does_not_vanish CONS_RF edge1); try edone.
by apply (proj1 (proj2 (connects_implies_valid CONNECT))); find_in_list.
eby eapply (proj1 (connects_implies_valid CONNECT)).
by apply (proj2 (proj2 (connects_implies_valid CONNECT))); find_in_list.
by apply (ALL edge1); find_in_list.
ins; desc.
destruct (classic (edge´ = hb_sb a1 b1)) as [| NEQ]; clarify; ins.
{
∃ (path1´ ++ edge1 :: nil), nil; unnw; rewrite app_nil_r; split; ins; vauto.
right; red. right; ins; split.
× rewrite <- (app_nil_l path2´), app_comm_cons, <- (app_nil_l (_ :: nil)), app_comm_cons,
!app_assoc in CONNECT.
apply connects_implies_valid, hbpath_valid_app in CONNECT; desc.
rewrite app_comm_cons, app_assoc in CONNECT.
by apply hbpath_valid_app in CONNECT; desc.
× clear NA; red in CONNECT; desf.
by exploit app_cons_not_nil; eauto; ins.
∃ fst, edge1; repeat split.
by destruct path1´; ins.
by destruct path1´; ins; rewrite last_app.
eby eapply (proj1 CONNECT).
}
∃ (path1´ ++ edge1 :: edge´ :: nil); ins.
rewrite !length_app, plus_n_Sm; ins.
assert (DEP: ¬ independent sb rf (edge´ :: hb_sb a1 b1 :: nil)).
{
eapply not_independent_two; eauto; ins.
× rewrite <- CON.
apply hbpath_connects_app2, hbpath_connects_cons in CONNECT.
eby eapply hist_closed_connect.
× desf; eauto.
left; eapply (na_propagates_forward _ edge1); eauto.
by apply (proj1 (proj2 (connects_implies_valid CONNECT))); find_in_list.
eby rewrite <- CON; eapply (proj1 (connects_implies_valid CONNECT)).
by rewrite <- CON; apply (proj2 (proj2 (connects_implies_valid CONNECT))); find_in_list.
assert (PV: hbpath_valid lab sb rf hmap (hb_sb a2 b2 :: path1´ ++ edge1 :: nil)).
{
apply hbpath_valid_cons_inv; ins; eauto; desf.
× rewrite <- (app_nil_l path2´), app_comm_cons, <- (app_nil_l (_ :: nil)), app_comm_cons,
!app_assoc in CONNECT.
apply connects_implies_valid, hbpath_valid_app in CONNECT; desc.
rewrite app_comm_cons, app_assoc in CONNECT.
by apply hbpath_valid_app in CONNECT; desc.
× eby eapply VALID, hist_closed_connect.
× red in CONNECT; desf.
by exploit app_cons_not_nil; eauto; ins.
destruct path1´; ins; desf.
}
eapply nonatomic_loc_on_path; eauto.
+ ins; rewrite In_app in IN; ins; desf; solve [eby rewrite MAP in *; desf |
eapply ALL; try edone; find_in_list].
+ ∃ (hb_sb a2 b2); unnw; split; ins; try find_in_list.
eby rewrite MAP in *; desf.
+ find_in_list.
}
clear NA.
eapply destruct_not_independent_two in DEP; ins; eauto; desf.
{
apply clos_refl_transE in DEP0; desf.
× ∃ nil; unnw; repeat split; ins; desf; eauto; try congruence.
2: by repeat progress (rewrite ?In_app in *; ins); desf;
solve [eapply ALL; eauto; find_in_list| rewrite MAP in *; desf].
rewrite app_nil_r.
right; red; ins.
right; split.
Focus 2.
red in CONNECT; desf.
by exploit app_cons_not_nil; eauto; ins.
eexists,; repeat split; eauto; destruct path1´; ins; desf.
by rewrite last_app; ins.
red; unnw; repeat split; ins; desf.
+ red; ins.
destruct path2.
- rewrite <- (app_nil_l (edge´ :: _)), <- (app_nil_l (edge3 :: _)),
!app_comm_cons, !app_assoc in DECOMP.
do 2 (apply app_inj_tail in DECOMP; desf).
rewrite <- CON.
eby eapply (proj1 (connects_implies_valid CONNECT)).
- assert (DECOMP´: ∃ path, path1´ ++ edge1 :: nil = path1 ++ edge0 :: edge3 :: path).
{
clear - DECOMP.
des_list_tail path2 path edge.
× rewrite <- (app_nil_l (edge´ :: _)), <- (app_nil_l (h :: _)),
!app_comm_cons, !app_assoc in DECOMP.
apply app_inj_tail in DECOMP; desf.
eby eexists.
× rewrite <- (app_nil_l (edge´ :: _)), !app_comm_cons, !app_assoc in DECOMP.
apply app_inj_tail in DECOMP; desf.
eby eexists.
}
desf.
rewrite <- (app_nil_l (edge2 :: _)), !app_comm_cons, !app_assoc, DECOMP´ in CONNECT.
apply connects_implies_valid, hbpath_valid_app in CONNECT; desf.
eby eapply (proj1 CONNECT).
+ repeat progress (rewrite ?In_app in *; ins); desf; eauto;
eapply (proj1 (proj2 (connects_implies_valid CONNECT))); find_in_list.
+ repeat progress (rewrite ?In_app in *; ins); desf; eauto;
rewrite <- ?CON; eapply (proj2 (proj2 (connects_implies_valid CONNECT))); find_in_list.
× eapply clos_trans_hbUrfE, hbUrf_implies_hbpath in DEP0; eauto; desf.
∃ path; unnw; repeat split; ins; eauto; desf.
2: by repeat progress (rewrite ?In_app in *; ins); desf;
solve [eapply ALL; eauto; find_in_list| rewrite MAP in *; desf].
right; rewrite <- app_assoc; red; ins.
right; split.
+ red; unnw; repeat split; ins.
- red; ins.
destruct path as [ | edge´´ path´´].
{
destruct path2.
× rewrite <- (app_nil_l (edge´ :: _)), <- (app_nil_l (edge3 :: _)),
!app_comm_cons, !app_assoc in DECOMP.
do 2 (apply app_inj_tail in DECOMP; desf).
rewrite <- CON.
eby eapply (proj1 (connects_implies_valid CONNECT)).
× assert (DECOMP´: ∃ path, path1´ ++ edge1 :: nil = path1 ++ edge0 :: edge3 :: path).
{
clear - DECOMP.
des_list_tail path2 path edge.
× rewrite <- (app_nil_l (edge´ :: _)), <- (app_nil_l (h :: _)),
!app_comm_cons, !app_assoc in DECOMP.
apply app_inj_tail in DECOMP; desf.
eby eexists.
× rewrite <- (app_nil_l (edge´ :: _)), !app_comm_cons, !app_assoc in DECOMP.
apply app_inj_tail in DECOMP; desf.
eby eexists.
}
desf.
rewrite <- (app_nil_l (edge2 :: _)), !app_comm_cons, !app_assoc, DECOMP´ in CONNECT.
apply connects_implies_valid, hbpath_valid_app in CONNECT; desf.
eby eapply (proj1 CONNECT).
}
assert( (edge0 = edge1 ∧ edge3 = edge´) ∨ (edge0 = edge´ ∧ edge3 = edge´´) ∨
(∃ path, edge´´ :: path´´ = path ++ edge0 :: edge3 :: path2) ∨
(∃ path, path1´ ++ edge1 :: nil = path1 ++ edge0 :: edge3 :: path) ).
{
clear - DECOMP.
revert DECOMP.
revert path1´ path1 path´´ path2 edge1 edge´ edge´´ edge0 edge3.
induction path1´ as [ | edgeA pathA]; ins.
× destruct path1 as [ | edgeB pathB]; ins; desf; eauto.
destruct pathB as [ | edgeC pathC]; ins; desf; eauto.
× destruct path1 as [ | edgeB pathB]; ins; desf.
+ destruct pathA as [ | edgeC pathC]; ins; desf; eauto.
+ exploit IHpathA; eauto; ins; desf; eauto.
by repeat right; ∃ path; rewrite x0.
}
desf.
eby rewrite <- CON; eapply (proj1 (connects_implies_valid CONNECT)).
by red in DEP0; ins; desf.
eby rewrite H in DEP0; eapply (proj1 (connects_implies_valid DEP0)).
rewrite <- (app_nil_l (edge2 :: _)), !app_comm_cons, !app_assoc, H in CONNECT.
apply connects_implies_valid, hbpath_valid_app in CONNECT; desf.
eby eapply (proj1 CONNECT).
- by repeat progress (rewrite ?In_app in *; ins); desf; eauto;
try (eapply (proj1 (proj2 (connects_implies_valid CONNECT))); find_in_list);
eapply (proj1 (proj2 (connects_implies_valid DEP0))).
- by repeat progress (rewrite ?In_app in *; ins); desf; eauto; rewrite <- ?CON;
try (eapply (proj2 (proj2 (connects_implies_valid CONNECT))); find_in_list);
eapply (proj2 (proj2 (connects_implies_valid DEP0))).
+ red in CONNECT; desf.
by exploit app_cons_not_nil; eauto.
∃ fst.
red in DEP0; desf.
by ∃ edge´; repeat split; eauto; destruct path1´; ins; rewrite last_app; ins.
by ∃ lst0; repeat split; eauto; destruct path1´; ins; apply olast_inv in DEP3; desf;
repeat progress (rewrite ?last_app; ins).
}
{ exfalso; rewrite <- CON in *; clear - ACYCLIC CONNECT DEP0 EV1.
apply hbpath_connects_app2, hbpath_connects_cons, connect_implies_hbUrf in CONNECT.
apply clos_refl_transE in CONNECT; apply clos_refl_transE in DEP0; desf.
× eapply ACYCLIC, t_step; vauto.
× apply clos_trans_hbUrfE in CONNECT.
eapply ACYCLIC, t_trans; eauto.
apply t_step; vauto.
× apply clos_trans_hbUrfE in DEP0.
eapply ACYCLIC, t_trans; eauto.
apply t_step; vauto.
× apply clos_trans_hbUrfE in DEP0; apply clos_trans_hbUrfE in CONNECT.
eapply ACYCLIC, t_trans; eauto.
eapply t_trans; eauto.
apply t_step; vauto.
}
}
}
Grab Existential Variables. edone. edone. edone. edone. edone.
Qed.
Lemma exists_path_with_location_throughout:
∀ acts lab sb rf mo hmap V
(FIN: ExecutionFinite acts lab sb)
(ACYCLIC: IrreflexiveHBuRF sb rf)
(CONS_RF: ConsistentRF_basic lab sb rf mo)
(CONS_A: ConsistentAlloc lab)
(HC: hist_closed sb rf V) (VALID: hmap_valids lab sb rf hmap V)
a1 a2 b1 b2 (DIF: b1 ≠ b2) (EV1: sb a1 b1) (EV2: sb a2 b2) (IN1: In a1 V) (IN2: In a2 V)
hf1 hf2 (MAP1: hmap (hb_sb a1 b1) = Hdef hf1) (MAP2: hmap (hb_sb a2 b2) = Hdef hf2)
l (ALL1: hf1 l ≠ HVnone) (ALL2: hf2 l ≠ HVnone) (NA: is_nonatomic (hf1 l) ∨ is_nonatomic (hf2 l))
(NORMAL1: HVlabeled (hf1 l) HLnormal) (NORMAL2: HVlabeled (hf2 l) HLnormal),
∃ path,
<< CONNECT: hbpath_connects lab sb rf hmap path b1 a2 ∨
hbpath_connects lab sb rf hmap path b2 a1 >> ∧
<< ALL: ∀ edge (IN: In edge path) hf (MAP: hmap edge = Hdef hf), hf l ≠ HVnone >>.
Proof.
ins.
exploit nonatomics_strongly_connected_helper; eauto.
instantiate (1 := length acts + 1).
ins; desc.
destruct LEN as [ | LEN].
{
clarify; rewrite !app_nil_r in ×.
repeat eexists; try edone.
}
{
exfalso; clear NA.
assert (PV: hbpath_valid lab sb rf hmap path1).
by desf; apply connects_implies_valid, hbpath_valid_app in CONNECT; desf.
assert (SINK: ∀ e, ¬ In (hb_sink e) path1).
by ins; intro; desf; exploit connects_implies_no_sink; eauto; find_in_list.
assert (SUBSET: ∀ e (IN: In e (map hb_fst path1)), In e acts).
{
clear CONNECT.
ins; rewrite In_map in IN; desf.
exploit (proj1 (proj2 PV) x); eauto; ins.
destruct x; ins.
by exploit (proj2 FIN); eauto; ins; desf.
by specialize (CONS_RF e´); desf; desf; apply (proj1 FIN); intro S; rewrite S in ×.
by exploit SINK; eauto; ins.
}
exploit perm_from_subset; try eassumption.
× apply nodup_map.
by eapply NoDup_path; eauto; red in PV; desf; intuition.
ins; intro EQ.
revert CONNECT.
apply In_split in H; desf.
eby rewrite In_app in H0; simpls; desf; apply In_split in H0; desf;
rewrite ?app_comm_cons, <- !app_assoc in *; ins; desf;
apply hbpath_connects_app2 in CONNECT;
rewrite app_comm_cons in CONNECT;
apply hbpath_connects_app1 in CONNECT;
apply connect_implies_hbUrf_strong in CONNECT; desf;
rewrite EQ in *; eapply ACYCLIC.
× clear - LEN; intro L; desf.
apply Permutation_length in L.
rewrite length_app, length_map in L; omega.
}
Qed.
Lemma nonatomics_strongly_connected:
∀ acts lab sb rf mo hmap V
(FIN: ExecutionFinite acts lab sb)
(ACYCLIC: IrreflexiveHBuRF sb rf)
(CONS_RF: ConsistentRF_basic lab sb rf mo)
(CONS_A: ConsistentAlloc lab)
(HC: hist_closed sb rf V) (VALID: hmap_valids lab sb rf hmap V)
a1 a2 b1 b2 (DIF: b1 ≠ b2) (EV1: sb a1 b1) (EV2: sb a2 b2) (IN1: In a1 V) (IN2: In a2 V)
hf1 hf2 (MAP1: hmap (hb_sb a1 b1) = Hdef hf1) (MAP2: hmap (hb_sb a2 b2) = Hdef hf2)
l (ALL1: hf1 l ≠ HVnone) (ALL2: hf2 l ≠ HVnone) (NA: is_nonatomic (hf1 l) ∨ is_nonatomic (hf2 l))
(NORMAL1: HVlabeled (hf1 l) HLnormal) (NORMAL2: HVlabeled (hf2 l) HLnormal),
clos_refl_trans _ (happens_before lab sb rf mo) b1 a2 ∨
clos_refl_trans _ (happens_before lab sb rf mo) b2 a1.
Proof.
ins.
exploit exists_path_with_location_throughout; eauto; ins; desc.
revert NA; desf.
× red in CONNECT; desf; ins; try by vauto.
assert (PV: hbpath_valid lab sb rf hmap (hb_sb a1 (hb_fst fst) :: path ++ hb_sb a2 b2 :: nil)).
{
clear NA.
red; unnw; repeat split; ins.
× red; ins.
apply olast_inv in CONNECT2; desf.
destruct prefix as [ | edge path]; ins.
by repeat (destruct path1; ins; desf).
rewrite <- app_assoc in DECOMP; ins.
destruct path1 as [ | edgeA pathA]; ins; desf.
des_list_tail path2 pathZ edgeZ.
+ rewrite <- (app_nil_l (hb_sb _ _ :: _)), <- (app_nil_l (edge2 :: _)),
!app_comm_cons, !app_assoc in H0.
do 2 (apply app_inj_tail in H0; desf).
+ rewrite <- (app_nil_l (hb_sb _ _ :: _)), !app_comm_cons, !app_assoc in H0.
apply app_inj_tail in H0; desf.
rewrite !app_comm_cons, H0 in CONNECT.
eby eapply (proj1 CONNECT).
× rewrite In_app in IN; ins; desf; try (eby eapply VALID).
by apply (proj1 (proj2 CONNECT)).
× rewrite In_app in IN; ins; desf; ins.
by apply VALID.
by apply (proj2 (proj2 CONNECT)).
by apply VALID.
}
exploit hb_trough_path; try (by ins; eauto).
+ eby ins; rewrite MAP1 in *; desf.
+ eby ins; rewrite MAP2 in *; desf.
+ eapply nonatomic_loc_on_path; ins; eauto.
by rewrite In_app in IN; ins; desf; ins; solve [congruence | eby eapply ALL].
by unnw; desf; [eexists (hb_sb a1 _) | eexists (hb_sb a2 _)];
split; (try find_in_list); unnw; ins; rewrite MAP in *; desf.
× red in CONNECT; desf; ins; try by vauto.
assert (PV: hbpath_valid lab sb rf hmap (hb_sb a2 (hb_fst fst) :: path ++ hb_sb a1 b1 :: nil)).
{
clear NA.
red; unnw; repeat split; ins.
× red; ins.
apply olast_inv in CONNECT2; desf.
destruct prefix as [ | edge path]; ins.
by repeat (destruct path1; ins; desf).
rewrite <- app_assoc in DECOMP; ins.
destruct path1 as [ | edgeA pathA]; ins; desf.
des_list_tail path2 pathZ edgeZ.
+ rewrite <- (app_nil_l (hb_sb _ _ :: _)), <- (app_nil_l (edge2 :: _)),
!app_comm_cons, !app_assoc in H0.
do 2 (apply app_inj_tail in H0; desf).
+ rewrite <- (app_nil_l (hb_sb _ _ :: _)), !app_comm_cons, !app_assoc in H0.
apply app_inj_tail in H0; desf.
rewrite !app_comm_cons, H0 in CONNECT.
eby eapply (proj1 CONNECT).
× rewrite In_app in IN; ins; desf; try (eby eapply VALID).
by apply (proj1 (proj2 CONNECT)).
× rewrite In_app in IN; ins; desf; ins.
by eapply VALID.
by apply (proj2 (proj2 CONNECT)).
by eapply VALID.
}
exploit hb_trough_path; try (by ins; eauto).
+ eby ins; rewrite MAP2 in *; desf.
+ eby ins; rewrite MAP1 in *; desf.
+ eapply nonatomic_loc_on_path; ins; eauto.
by rewrite In_app in IN; ins; desf; ins; solve [congruence | eby eapply ALL].
by unnw; desf; [eexists (hb_sb a1 _) | eexists (hb_sb a2 _)];
split; (try find_in_list); unnw; ins; rewrite MAP in *; desf.
Qed.
Theorem valid_implies_race_free :
∀ acts lab sb rf mo hmap V
(FIN: ExecutionFinite acts lab sb)
(ACYCLIC: IrreflexiveHBuRF sb rf)
(CONS_A: ConsistentAlloc lab)
(CONS_RF: ConsistentRF_basic lab sb rf mo)
(HC: hist_closed sb rf V)
(VALID: hmap_valids lab sb rf hmap V),
race_free V lab sb rf mo.
Proof.
red; ins.
clear WRI.
eapply valid_accessD in Aa; ins; eauto; desc.
eapply valid_accessD in Ab; ins; eauto; desc.
exploit nonatomics_strongly_connected; eauto; ins; instantiate; try congruence.
by apply (HC a); vauto.
by apply (HC b); vauto.
by desf; exploit valid_na_accessD; try exact NA; eauto; rewrite LOC; ins; eauto.
by clear NA; desf; apply clos_refl_transE in x0; desf; try (by left; vauto); try (by right; vauto);
apply clos_trans_hbE in x0; [left | right]; eapply t_trans; vauto.
Qed.
This page has been generated by coqdoc