Require Import Vbase Varith.
Require Import Relations Classical ClassicalDescription.
Require Import Wf Wf_nat.
Require Import List Permutation Vlistbase Vlist extralib.
Require Import c11 fslassn fslassnsem fslmodel fslassnlemmas.
Require Import permission fslhmap.
Require Import Omega.
Set Implicit Arguments.
THE IDEA: If we can construct paths on which neighboring edges respect
the sync_step property, then we can infer a synchronizes_with
relation from that path.
Definition hbpath := list (hbcase × HeapLabel).
Definition sync_step lab (edge1 edge2 : hbcase × HeapLabel) :=
<< CONN: hb_snd (fst edge1) = Some (hb_fst (fst edge2)) >> ∧
<< STEP: (snd edge1 = HLnormal ∧ is_sb (fst edge1) ∧
((snd edge2 = HLnormal ∧ ¬ is_rf (fst edge2)) ∨
(snd edge2 = HLtriangle ∧ is_sb (fst edge2) ∧ is_release_fence (lab (hb_fst (fst edge2)))) ∨
(snd edge2 = HLnabla ∧ ¬ is_sb (fst edge2) ∧ is_release_write (lab (hb_fst (fst edge2))))))
∨
(snd edge1 = HLtriangle ∧ is_sb (fst edge1) ∧
((snd edge2 = HLtriangle ∧ ¬ is_rf (fst edge2)) ∨
(snd edge2 = HLnabla ∧ ¬ is_sb (fst edge2) ∧ is_write (lab (hb_fst (fst edge2)))) ∨
(snd edge2 = HLnabla ∧ is_sink (fst edge2))))
∨
(snd edge1 = HLnabla ∧
((snd edge2 = HLnabla ∧ ¬ is_rf (fst edge2)) ∨
(is_rf (fst edge1) ∧ snd edge2 = HLnormal ∧ ¬ is_rf (fst edge2)
∧ is_acquire_read (lab (hb_fst (fst edge2)))) ∨
(is_sb (fst edge1) ∧ snd edge2 = HLnormal ∧ is_sb (fst edge2)
∧ is_acquire_fence (lab (hb_fst (fst edge2)))) ∨
(is_rf (fst edge1) ∧ snd edge2 = HLnabla ∧ ¬ is_sb (fst edge2)
∧ is_rmw (lab (hb_fst (fst edge2)))))) >>.
Definition hbpath_wf lab sb rf (path: hbpath) :=
<< SYNC: ∀ path1 path2 edge1 edge2 (DECOMP: path = path1 ++ edge1 :: edge2 :: path2),
sync_step lab edge1 edge2 >> ∧
<< EVP : ∀ edge (IN: In edge path), edge_valid lab sb rf (fst edge) >>.
Some basic lemmas about hbpath_wf predicate.
Lemma hbpath_wf_nil lab sb rf : hbpath_wf lab sb rf nil.
Lemma hbpath_wf_one lab sb rf :
∀ edge, edge_valid lab sb rf (fst edge) → hbpath_wf lab sb rf (edge :: nil).
Lemma hbpath_wf_app lab sb rf:
∀ path1 path2,
hbpath_wf lab sb rf (path1 ++ path2) → hbpath_wf lab sb rf path1 ∧ hbpath_wf lab sb rf path2.
Lemma hbpath_wf_app_l lab sb rf :
∀ path1 path2, hbpath_wf lab sb rf (path1 ++ path2) → hbpath_wf lab sb rf path1.
Lemma hbpath_wf_app_r lab sb rf :
∀ path1 path2, hbpath_wf lab sb rf (path1 ++ path2) → hbpath_wf lab sb rf path2.
Lemma hbpath_wf_cons lab sb rf:
∀ edge path, hbpath_wf lab sb rf (edge :: path) → hbpath_wf lab sb rf path.
Lemma extend_path_right :
∀ lab sb rf path (WFP: hbpath_wf lab sb rf path)
edge (LAST: olast path = Some edge) edge' (VALID: edge_valid lab sb rf (fst edge'))
(SYNC: sync_step lab edge edge'),
hbpath_wf lab sb rf (path ++ edge' :: nil).
Lemma extend_path_left :
∀ lab sb rf path (WFP: hbpath_wf lab sb rf path)
edge (FIRST: ohead path = Some edge) edge' (VALID: edge_valid lab sb rf (fst edge'))
(SYNC: sync_step lab edge' edge),
hbpath_wf lab sb rf (edge' :: path).
Lemmas about the structure of well-formed paths.
Lemma sink_is_always_last lab sb rf:
∀ path edge (WF: hbpath_wf lab sb rf (path ++ edge :: nil)),
¬ ∃ edge', In edge' path ∧ is_sink (fst edge').
Lemma inside_path_normals_are_on_sb_edges :
∀ lab sb rf path edgeN (WFP: hbpath_wf lab sb rf (path ++ edgeN :: nil))
edge (IN: In edge path) (LAB: snd edge = HLnormal),
is_sb (fst edge).
Lemma inside_path_triangles_are_on_sb_edges :
∀ lab sb rf path edgeN (WFP: hbpath_wf lab sb rf (path ++ edgeN :: nil))
edge (IN: In edge path) (LAB: snd edge = HLtriangle),
is_sb (fst edge).
Lemma structure_of_nonnormal_path:
∀ lab sb rf mo (ACYCLIC: IrreflexiveHBuRF sb rf) (CONS_RF: ConsistentRF_basic lab sb rf mo)
path (PV: hbpath_wf lab sb rf path)
(LAB: ∀ edge (IN: In edge path), snd edge ≠ HLnormal),
∃ path1 path2, << DECOMP: path = path1 ++ path2 >> ∧
<< LAB1: ∀ edge (IN: In edge path1), snd edge = HLtriangle >> ∧
<< LAB2: ∀ edge (IN: In edge path2), snd edge = HLnabla >>.
Lemma structure_of_nabla_path:
∀ lab sb rf mo (ACYCLIC: IrreflexiveHBuRF sb rf) (CONS_RF: ConsistentRF_basic lab sb rf mo)
path (PV: hbpath_wf lab sb rf path) (SINK: ∀ edge (IN: In edge path), ¬ is_sink (fst edge))
(LAB: ∀ edge (IN: In edge path), snd edge = HLnabla),
∃ pathRF pathSB,
<< DECOMP: path = pathRF ++ pathSB >> ∧
<< SB: ∀ edge (IN: In edge pathSB), is_sb (fst edge) >> ∧
<< RF: ∀ edge (IN: In edge pathRF), is_rf (fst edge) >>.
Lemma structure_of_normal_to_normal_transition:
∀ lab sb rf mo (ACYCLIC: IrreflexiveHBuRF sb rf) (CONS_RF: ConsistentRF_basic lab sb rf mo)
path edge1 edgeN (WFP: hbpath_wf lab sb rf (edge1 :: path ++ edgeN :: nil))
(NORMALfst: snd edge1 = HLnormal) (NORMALlst: snd edgeN = HLnormal)
(MID: ∀ edge (IN: In edge path), snd edge ≠ HLnormal),
path = nil ∨
∃ pathTRIANGLE edgeRF pathRMW pathNABLA,
<< DECOMP: path = pathTRIANGLE ++ edgeRF :: pathRMW ++ pathNABLA >> ∧
<< TRIANGLE: ∀ edge (IN: In edge pathTRIANGLE), snd edge = HLtriangle >> ∧
<< NABLA: ∀ edge (IN: In edge (edgeRF :: pathRMW ++ pathNABLA)), snd edge = HLnabla >> ∧
<< SB: ∀ edge (IN: In edge (pathTRIANGLE ++ pathNABLA)), is_sb (fst edge) >> ∧
<< RF: ∀ edge (IN: In edge (edgeRF :: pathRMW)), is_rf (fst edge) >> ∧
<< RMW: ∀ edge (IN: In edge pathRMW), is_rmw (lab (hb_fst (fst edge))) >>.
Lemmas about inferring important relations from well-formed paths.
Lemma sb_from_path:
∀ lab sb rf path edge1 edgeN (WFP: hbpath_wf lab sb rf (edge1 :: path ++ edgeN :: nil))
(pSB: ∀ edge (IN: In edge path), is_sb (fst edge)),
∀ a (SND: hb_snd (fst edge1) = Some a), clos_refl_trans _ sb a (hb_fst (fst edgeN)).
Lemma release_seq_from_path:
∀ lab sb rf mo w r path edgeN lbl
(PV: hbpath_wf lab sb rf ((hb_rf w r, lbl) :: path ++ edgeN :: nil))
(RMWr: is_rmw (lab r))
(RMWn: is_rmw (lab (hb_fst (fst edgeN))))
(PATH: ∀ edge (IN: In edge path), << RMW: is_rmw (lab (hb_fst (fst edge))) >> ∧
<< RF: is_rf (fst edge) >>),
release_seq lab sb rf mo w (hb_fst (fst edgeN)).
Lemma hb_from_path_simple:
∀ lab sb rf mo (ACYCLIC: IrreflexiveHBuRF sb rf) (CONS_RF: ConsistentRF_basic lab sb rf mo)
path edge1 edgeN (WFP: hbpath_wf lab sb rf (edge1 :: path ++ edgeN :: nil))
(NORMALfst: snd edge1 = HLnormal) (NORMALlst: snd edgeN = HLnormal)
(MID: ∀ edge (IN: In edge path), snd edge ≠ HLnormal),
∀ b (SND: hb_snd (fst edge1) = Some b),
clos_refl_trans _ (happens_before lab sb rf mo) b (hb_fst (fst edgeN)).
The main lemma: well-formed path starting and ending in a normal edge
induces the happens-before relation.
Lemma hb_from_path:
∀ lab sb rf mo (ACYCLIC: IrreflexiveHBuRF sb rf) (CONS_RF: ConsistentRF_basic lab sb rf mo)
path edge1 edgeN (WFP: hbpath_wf lab sb rf (edge1 :: path ++ edgeN :: nil))
(NORMALfst: snd edge1 = HLnormal) (NORMALlst: snd edgeN = HLnormal),
∀ b (SND1: hb_snd (fst edge1) = Some b),
clos_refl_trans _ (happens_before lab sb rf mo) b (hb_fst (fst edgeN)).
∀ lab sb rf mo (ACYCLIC: IrreflexiveHBuRF sb rf) (CONS_RF: ConsistentRF_basic lab sb rf mo)
path edge1 edgeN (WFP: hbpath_wf lab sb rf (edge1 :: path ++ edgeN :: nil))
(NORMALfst: snd edge1 = HLnormal) (NORMALlst: snd edgeN = HLnormal),
∀ b (SND1: hb_snd (fst edge1) = Some b),
clos_refl_trans _ (happens_before lab sb rf mo) b (hb_fst (fst edgeN)).
In order to apply the hb_from_path lemma, we have to be able to talk about
nodes being connected trough paths.
Definition hbpath_connects lab sb rf path a b :=
<< EMPTY: path = nil ∧ a = b >> ∨
<< WFP: hbpath_wf lab sb rf path >> ∧
∃ alpha omega, << HEAD: ohead path = some alpha >> ∧ << ALPHA: hb_fst (fst alpha) = a >> ∧
<< TAIL: olast path = some omega >> ∧ << OMEGA: hb_snd (fst omega) = Some b >>.
Basic properties of hbpath_connects predicate.
Lemma connects_implies_wf:
∀ lab sb rf path a b, hbpath_connects lab sb rf path a b → hbpath_wf lab sb rf path.
Lemma hbpath_connects_app1:
∀ lab sb rf path1 path2 edge a b
(CONNECT: hbpath_connects lab sb rf (path1 ++ edge :: path2) a b),
hbpath_connects lab sb rf path1 a (hb_fst (fst edge)).
Lemma hbpath_connects_app2:
∀ lab sb rf path1 path2 edge a b
(CONNECT: hbpath_connects lab sb rf (path1 ++ edge :: path2) a b),
hbpath_connects lab sb rf (edge :: path2) (hb_fst (fst edge)) b.
Lemma hbpath_connects_cons:
∀ lab sb rf edge1 edge2 path a b
(CONNECT: hbpath_connects lab sb rf (edge1 :: edge2 :: path) a b),
hbpath_connects lab sb rf (edge2 :: path) (hb_fst (fst edge2)) b.
Lemma connects_implies_no_sink:
∀ lab sb rf path a b,
hbpath_connects lab sb rf path a b → ∀ edge (IN: In edge path), ¬ is_sink (fst edge).
∀ lab sb rf path a b, hbpath_connects lab sb rf path a b → hbpath_wf lab sb rf path.
Lemma hbpath_connects_app1:
∀ lab sb rf path1 path2 edge a b
(CONNECT: hbpath_connects lab sb rf (path1 ++ edge :: path2) a b),
hbpath_connects lab sb rf path1 a (hb_fst (fst edge)).
Lemma hbpath_connects_app2:
∀ lab sb rf path1 path2 edge a b
(CONNECT: hbpath_connects lab sb rf (path1 ++ edge :: path2) a b),
hbpath_connects lab sb rf (edge :: path2) (hb_fst (fst edge)) b.
Lemma hbpath_connects_cons:
∀ lab sb rf edge1 edge2 path a b
(CONNECT: hbpath_connects lab sb rf (edge1 :: edge2 :: path) a b),
hbpath_connects lab sb rf (edge2 :: path) (hb_fst (fst edge2)) b.
Lemma connects_implies_no_sink:
∀ lab sb rf path a b,
hbpath_connects lab sb rf path a b → ∀ edge (IN: In edge path), ¬ is_sink (fst edge).
Connected by a path means being hbUrf related.
Lemma connect_implies_hbUrf:
∀ lab sb rf path a b (CONNECT: hbpath_connects lab sb rf path a b),
clos_refl_trans _ (happens_before_union_rf sb rf) a b.
Lemma connect_implies_hbUrf_strong:
∀ lab sb rf path a b (CONNECT: hbpath_connects lab sb rf path a b),
path ≠ nil → happens_before_union_rf sb rf a b.
Lemma hist_closed_connect:
∀ lab sb rf path a b V
(CONNECT: hbpath_connects lab sb rf path a b)
(HC: hist_closed sb rf V) (IN: In b V),
In a V.
∀ lab sb rf path a b (CONNECT: hbpath_connects lab sb rf path a b),
clos_refl_trans _ (happens_before_union_rf sb rf) a b.
Lemma connect_implies_hbUrf_strong:
∀ lab sb rf path a b (CONNECT: hbpath_connects lab sb rf path a b),
path ≠ nil → happens_before_union_rf sb rf a b.
Lemma hist_closed_connect:
∀ lab sb rf path a b V
(CONNECT: hbpath_connects lab sb rf path a b)
(HC: hist_closed sb rf V) (IN: In b V),
In a V.
Connecting paths cannot be longer than number of nodes in the graph.
Lemma path_is_too_long :
∀ acts lab sb rf mo path a b
(FIN: ExecutionFinite acts lab sb)
(ACYCLIC: IrreflexiveHBuRF sb rf)
(CONS_RF: ConsistentRF_basic lab sb rf mo)
(CONNECT: hbpath_connects lab sb rf path a b)
(LEN: length path = length acts + 1),
False.
∀ acts lab sb rf mo path a b
(FIN: ExecutionFinite acts lab sb)
(ACYCLIC: IrreflexiveHBuRF sb rf)
(CONS_RF: ConsistentRF_basic lab sb rf mo)
(CONNECT: hbpath_connects lab sb rf path a b)
(LEN: length path = length acts + 1),
False.
Path "tracks" location l
Definition tracking_path PS PSg hmap (path : hbpath) l :=
∀ edge (IN: In edge path) hf g (MAP: hmap (fst edge) = Hdef hf g),
<< ALL: hf l ≠ @HVnone PS PSg >> ∧ << LAB: HVlabeled (hf l) (snd edge) >>.
∀ edge (IN: In edge path) hf g (MAP: hmap (fst edge) = Hdef hf g),
<< ALL: hf l ≠ @HVnone PS PSg >> ∧ << LAB: HVlabeled (hf l) (snd edge) >>.
This page has been generated by coqdoc