(*********************************************************************)
(* A Formal Hierarchy of Weak Memory Models *)
(* *)
(* Jade Alglave INRIA Paris-Rocquencourt, France. *)
(* *)
(* Copyright 2010 Institut National de Recherche en Informatique et *)
(* en Automatique. All rights reserved. This file is distributed *)
(* under the terms of the Lesser GNU General Public License. *)
(*********************************************************************)
Require Import Ensembles.
Require Import Arith.
Require Import util.
Require Import wmm.
Require Import Classical_Prop.
Import OEEvt.
Set Implicit Arguments.
Module Basic (A : Archi).
Import A.
Module AWmm := Wmm A.
Import AWmm.
Section Ax.
(** evts *)
Lemma read_write_contrad :
forall x l1 l2,
~(write_to x l1 /\ read_from x l2).
Proof.
intros x l1 l2 [[v1 Hw] [v2 Hr]].
rewrite Hw in Hr; inversion Hr.
Qed.
Lemma write_to_implies_writes: (*basic*)
forall E x l,
(events E) x ->
write_to x l ->
(writes E) x.
Proof.
intros E x l He [v Hw]; unfold writes; split; auto.
exists l; exists v; auto.
Qed.
Lemma read_from_implies_reads: (*basic*)
forall E x l,
(events E) x ->
read_from x l ->
(reads E) x.
Proof.
intros E x l He [v Hw]; unfold reads; split; auto.
exists l; exists v; auto.
Qed.
Lemma read_from_implies_same_loc :
forall x l1 l2,
read_from x l1 ->
read_from x l2 ->
l1 = l2.
Proof.
intros x l1 l2 [v1 H1] [v2 H2].
rewrite H1 in H2; inversion H2; auto.
Qed.
Lemma rf_implies_same_loc :
forall E X w y l,
valid_execution E X ->
rf X w y ->
read_from y l ->
write_to w l.
Proof.
intros E X w y l Hv Hrf Hr.
destruct_valid Hv.
generalize (Hrf_cands w y Hrf); intros [? [? [l' [Hw Hr']]]].
generalize (read_from_implies_same_loc Hr Hr'); intro Heq; subst; auto.
Qed.
Lemma rf_implies_same_loc2 :
forall E X w y,
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
rf X w y ->
loc w = loc y.
Proof.
intros E X w y [Hwswf Hrfwf] Hrf.
destruct Hrfwf as [? [Hrf_cands ?]].
generalize (Hrf_cands w y Hrf); intros [? [? [l [[v1 Hw] [v2 Hr]]]]];
unfold loc; rewrite Hw; rewrite Hr; auto.
Qed.
Lemma write_to_implies_this_loc :
forall y l,
write_to y l ->
loc y = (*Some*) l.
Proof.
intros x l [v Hw]; unfold loc; rewrite Hw; auto.
Qed.
Lemma ws_implies_same_loc :
forall E X w y,
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
ws X w y ->
loc w = loc y.
Proof.
intros E X w y [Hwswf Hrfwf] Hws.
destruct Hwswf as [? Hl].
generalize (Hl w y Hws); intros [l [[? Hw] [? Hy]]].
rewrite (write_to_implies_this_loc Hw);
rewrite (write_to_implies_this_loc Hy); trivial.
Qed.
Lemma fr_implies_same_loc :
forall E X w y,
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
fr E X w y ->
loc w = loc y.
Proof.
intros E X w y Hs [Hw [Hy [wr [Hrf Hws]]]].
rewrite <- (ws_implies_same_loc X wr y Hs); auto.
eapply sym_eq.
eapply rf_implies_same_loc2; [apply Hs | apply Hrf].
Qed.
Lemma fr_implies_same_loc2 :
forall E X x y l,
valid_execution E X ->
fr E X x y ->
read_from x l ->
write_to y l.
Proof.
intros E X x y l Hv [Hew [Hey [z [Hrf Hws]]]] Hr.
destruct_valid Hv.
generalize (Hws_cands z y Hws); intros [ly [[? Hwz] [? Hwy]]].
assert (write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X)) as Hand.
split; split; auto.
generalize (rf_implies_same_loc2 X z x Hand Hrf); intro Heq.
destruct Hr as [Hvx Hax]; destruct Hwz as [Hvz Haz].
unfold loc in Heq; rewrite Hax in Heq; rewrite Haz in Heq;
inversion Heq as [Hl]; rewrite <- Hl; auto.
Qed.
Lemma read_from_implies_this_loc :
forall y l,
read_from y l ->
loc y = (*Some*) l.
Proof.
intros x l [v Hw].
unfold loc; rewrite Hw; auto.
Qed.
Lemma write_to_implies_same_loc :
forall y l1 l2 v,
action y = Access W l1 v ->
write_to y l2 ->
l1 = l2.
Proof.
intros x l1 l2 v H1 [v2 H2].
rewrite H1 in H2; inversion H2.
trivial.
Qed.
Lemma write_implies_write_to :
forall x l v,
action x = Access W l v ->
write_to x l.
Proof.
intros x l v Hx; unfold write_to; exists v; auto.
Qed.
(** po *)
Lemma pos_trans :
forall E x y z,
(po_strict E) x y ->
(po_strict E) y z ->
(po_strict E) x z.
Proof.
unfold po_strict;
intros E x y z [Hpxy [Hinf_xy [Hex Hey]]] [Hpyz [Hinf_yz [Heyb Hez]]].
split; [rewrite Hpxy; rewrite Hpyz; trivial |
split; [ | split; [apply Hex | apply Hez]]].
eapply lt_trans; [apply Hinf_xy | apply Hinf_yz].
Qed.
Lemma po_iico_trans :
forall E x y z,
well_formed_event_structure E ->
(po_strict E) x y ->
(iico E) y z ->
(po_strict E) x z.
Proof.
unfold po_strict;
intros E x y z Hwf [Hpxy [Hinf_xy [Hex Hey]]] Hyz.
unfold well_formed_event_structure in Hwf.
destruct Hwf as [? [? [? [? [? [? [Heq ?]]]]]]].
generalize (Heq y z Hyz); intro Heqi.
rewrite <- Heqi.
split; [apply Hpxy | split; [apply Hinf_xy |
split; [apply Hex | ]]].
apply H2; exists y; apply Hyz.
Qed.
Lemma iico_po_trans :
forall E x y z,
well_formed_event_structure E ->
(iico E) x y ->
(po_strict E) y z ->
(po_strict E) x z.
Proof.
unfold po_strict;
intros E x y z Hwf Hxy [Hpyz [Hinf_yz [Hey Hez]]].
unfold well_formed_event_structure in Hwf.
destruct Hwf as [? [? [? [? [? [? [Heq ?]]]]]]].
generalize (Heq x y Hxy); intro Heqi.
rewrite Heqi.
split; [apply Hpyz | split; [apply Hinf_yz |
split; [ | apply Hez]]].
apply H1; exists y; apply Hxy.
Qed.
Lemma iico_trans :
forall E x y z,
well_formed_event_structure E ->
(iico E) x y ->
(iico E) y z ->
(iico E) x z.
Proof.
intros E x y z Hwf Hxy Hyz.
destruct Hwf as [? [? [? [? [? [? [? Htrans]]]]]]].
unfold trans in Htrans; apply (Htrans x y z Hxy Hyz).
Qed.
Lemma po_trans :
forall E x y z,
well_formed_event_structure E ->
(po_iico E) x y ->
(po_iico E) y z ->
(po_iico E) x z.
Proof.
unfold po_iico;
intros E x y z Hwf Hxy Hyz.
inversion Hxy as [Hpo_xy | Hiico_xy];
inversion Hyz as [Hpo_yz | Hiico_yz].
left; eapply pos_trans; eauto.
left; eapply po_iico_trans; eauto.
left; eapply iico_po_trans; eauto.
right; eapply iico_trans; eauto.
Qed.
Lemma po_ac :
forall E x,
well_formed_event_structure E ->
~((po_iico E) x x).
Proof.
unfold not;
intros E x Hwf Hpo_iico.
unfold well_formed_event_structure in Hwf.
destruct Hwf as [? [? [? [? [Hac ?]]]]].
inversion Hpo_iico as [Hpo | Hiico].
unfold po_strict in Hpo.
destruct Hpo as [? [Hinf [? ?]]].
generalize (gt_irrefl (poi (iiid x))); intro Hc.
contradiction.
unfold acyclic in Hac; apply (Hac x);
apply trc_step; apply Hiico.
Qed.
Lemma diff_proc_implies_not_po :
forall E x y,
well_formed_event_structure E ->
proc_of x <> proc_of y ->
~(po_iico E x y).
Proof.
intros E x y Hwf Hdiff Hxy.
inversion Hxy as [Hpo | Hiico].
destruct Hpo as [Hpr ?].
unfold not in Hdiff; unfold proc_of in Hdiff.
apply (Hdiff Hpr).
destruct Hwf as [? [? [? [? [? [? [Heq ?]]]]]]].
generalize (Heq x y Hiico); intro Heqi.
unfold proc_of in Hdiff; unfold not in Hdiff; rewrite Heqi in Hdiff;
apply Hdiff; auto.
Qed.
Lemma same_proc_implies_po :
forall E x y,
well_formed_event_structure E ->
proc_of x = proc_of y ->
In _ (events E) x -> In _ (events E) y ->
po_iico E x y \/ po_iico E y x.
Proof.
intros E x y Hwf Heqp Hex Hey.
destruct (lt_eq_lt_dec x.(iiid).(poi) y.(iiid).(poi)) as [Horb | Hsup].
inversion Horb as [Hinf | Heq].
left; left; split; auto.
left; right.
destruct Hwf as [? [? [? [? [? [Hii ?]]]]]].
apply (Hii x y Heq).
right; left; split; auto.
Qed.
Lemma po_implies_same_proc :
forall E x y,
well_formed_event_structure E ->
In _ (events E) x -> In _ (events E) y ->
po_iico E x y -> proc_of x = proc_of y.
Proof.
intros E x y Hwf Hex Hey Hpo_xy.
destruct Hwf as [Ht ?].
apply Ht; auto.
Qed.
(** ws*)
Lemma ws_cands :
forall E X x e,
write_serialization_well_formed (events E) (ws X) ->
ws X x e ->
exists l : Location,
In _ (writes_to_same_loc_l (events E) l) x /\
In _ (writes_to_same_loc_l (events E) l) e.
Proof.
intros E X x e Hv Hws.
destruct Hv as [? Hws_cands]; apply (Hws_cands x e Hws).
Qed.
Lemma ws_cy :
forall E X x,
(forall l : Location,
linear_strict_order
(rrestrict (ws X) (writes_to_same_loc_l (events E) l))
(writes_to_same_loc_l (events E) l)) ->
(forall x e, ws X x e ->
(exists l : Location,
In _ (writes_to_same_loc_l (events E) l) x /\
In _ (writes_to_same_loc_l (events E) l) e)) ->
~(ws X x x).
Proof.
intros E X x Hl Hcands.
unfold not; intro Hws;
generalize (Hcands x x Hws); intros [lx [[Hex Hwx] ?]].
destruct (Hl lx) as [Hdr [Htrans [Hac Htot]]].
generalize (Hac x); intro Hn.
unfold not in Hn; apply Hn; split;
[apply Hws | unfold In; unfold writes_to_same_loc_l].
split; [split; [apply Hex | apply Hwx] |
split; [apply Hex | apply Hwx]].
Qed.
Lemma ws_evt_right :
forall E X x y,
(forall l : Location,
linear_strict_order
(rrestrict (ws X) (writes_to_same_loc_l (events E) l))
(writes_to_same_loc_l (events E) l)) ->
(forall x e, ws X x e ->
(exists l : Location,
In _ (writes_to_same_loc_l (events E) l) x /\
In _ (writes_to_same_loc_l (events E) l) e)) ->
ws X x y ->
In _ (events E) y.
Proof.
intros E X x y Hlin Hcands Hws.
generalize (Hcands x y Hws); intros [l [[Hex Hwx] [Hey Hwy]]];
apply Hey.
Qed.
Lemma ws_evt_left :
forall E X x y,
(forall l : Location,
linear_strict_order
(rrestrict (ws X) (writes_to_same_loc_l (events E) l))
(writes_to_same_loc_l (events E) l)) ->
(forall x e, ws X x e ->
(exists l : Location,
In _ (writes_to_same_loc_l (events E) l) x /\
In _ (writes_to_same_loc_l (events E) l) e)) ->
ws X x y ->
In _ (events E) x.
Proof.
intros E X x y Hlin Hcands Hws.
generalize (Hcands x y Hws); intros [l [[Hex Hwx] [Hey Hwy]]];
apply Hex.
Qed.
Lemma ws_right :
forall E X x y,
(forall l : Location,
linear_strict_order
(rrestrict (ws X) (writes_to_same_loc_l (events E) l))
(writes_to_same_loc_l (events E) l)) ->
(forall x e, ws X x e ->
(exists l : Location,
In _ (writes_to_same_loc_l (events E) l) x /\
In _ (writes_to_same_loc_l (events E) l) e)) ->
ws X x y ->
exists v, exists l, action y = Access W l v.
Proof.
intros E X x y Hlin Hcands Hws.
generalize (Hcands x y Hws); intros [l [[Hex Hwx] [Hey Hwy]]].
case_eq (action y).
intros d ly v Hy.
case_eq d.
intro Hr; unfold write_to in Hwy; rewrite Hy in Hwy; rewrite Hr in Hwy;
destruct Hwy as [vy Hwy]; inversion Hwy.
intro Hw; exists v; exists ly; trivial.
Qed.
Lemma dom_ws_is_write :
forall E X x y,
write_serialization_well_formed (events E) (ws X) ->
ws X x y ->
exists l, exists v, action x = Access W l v.
Proof.
intros E X x y [? Hws_cands] Hws.
generalize (Hws_cands x y Hws); intros [l [[Hex Hwx] [Hey Hwy]]].
case_eq (action x).
intros d lx v Hx.
case_eq d.
intro Hr; unfold write_to in Hwx; rewrite Hx in Hwx; rewrite Hr in Hwx;
destruct Hwx as [vx Hwx]; inversion Hwx.
intro Hw; exists lx; exists v; trivial.
Qed.
Lemma ran_ws_is_write :
forall E X x y,
write_serialization_well_formed (events E) (ws X) ->
ws X x y ->
exists v, exists l, action y = Access W l v.
Proof.
intros E X x y [Hws_tot Hws_cands] Hws.
apply (ws_right E X x y Hws_tot Hws_cands Hws).
Qed.
Lemma ws_trans :
forall E X x y z,
write_serialization_well_formed (events E) (ws X) ->
ws X x y -> ws X y z ->
ws X x z.
Proof.
intros E X x y z [Hws_tot Hws_cands] Hxy Hyz.
generalize (ws_right E X x y Hws_tot Hws_cands Hxy); intros [v [l Hy]].
generalize (Hws_tot l); intros [Hdr [Htrans [Hac Htot]]].
assert (rrestrict (ws X) (writes_to_same_loc_l (events E) l) x y) as Hxyb.
split; [apply Hxy |].
generalize (Hws_cands x y Hxy); intros [lx [Hlx Hlxy]].
generalize Hlxy; intro Hlxyb.
destruct Hlxy as [? Hwlxy].
generalize (write_to_implies_same_loc Hy Hwlxy); intro Heq.
rewrite Heq; split; auto.
assert (rrestrict (ws X) (writes_to_same_loc_l (events E) l) y z) as Hyzb.
split; [apply Hyz |].
destruct Hxyb as [? [? Hly]].
split; [apply Hly |].
generalize (Hws_cands y z Hyz); intros [ly [Hlyy Hlyz]].
destruct Hlyy as [? Hwlyy].
generalize (write_to_implies_same_loc Hy Hwlyy); intro Heq.
rewrite Heq; auto.
assert (rrestrict (ws X) (writes_to_same_loc_l (events E) l) x y /\
rrestrict (ws X) (writes_to_same_loc_l (events E) l) y z) as Hand.
split; auto.
generalize (Htrans x y z Hand); intros [Hxz ?].
auto.
Qed.
(** rf *)
Lemma dom_rf_is_write :
forall E X x y,
(forall e1 e2 : Event, rf X e1 e2 -> rfmaps (events E) e1 e2) ->
rf X x y ->
exists l, exists v, action x = Access W l v.
Proof.
intros E X x y Hrf_cands Hxy.
case_eq (action x).
intros dx lx vx Hx.
case_eq dx.
intro Hr.
generalize (Hrf_cands x y Hxy); intro Hc.
destruct Hc as [? [? [? [Hwx Hry]]]].
unfold write_to in Hwx; rewrite Hx in Hwx; rewrite Hr in Hwx;
destruct Hwx as [v Hwx]; inversion Hwx.
intro Hw; rewrite Hw in Hx.
exists lx; exists vx; trivial.
Qed.
Lemma ran_rf_is_read :
forall E X x y,
(forall e1 e2 : Event, rf X e1 e2 -> rfmaps (events E) e1 e2) ->
rf X x y ->
exists l, exists v, action y = Access R l v.
Proof.
intros E X x y Hrf_cands Hxy.
case_eq (action y).
intros dy ly vy Hy.
case_eq dy.
intro Hr; rewrite Hr in Hy.
exists ly; exists vy; trivial.
intro Hw.
generalize (Hrf_cands x y Hxy); intro Hc.
destruct Hc as [? [? [? [Hwx Hry]]]].
unfold read_from in Hry; rewrite Hy in Hry; rewrite Hw in Hry;
destruct Hry as [v Hry]; inversion Hry.
Qed.
Lemma rf_uni :
forall E X x w1 w2,
rfmaps_well_formed E (events E) (rf X) ->
rf X w1 x -> rf X w2 x ->
w1 = w2.
Proof.
intros E X x w1 w2 Hrfwf Hxy.
destruct Hrfwf as [? [? Hrf_uni]].
apply Hrf_uni; [apply Hxy].
Qed.
Lemma dom_rf_in_events :
forall E X x e,
well_formed_event_structure E ->
rfmaps_well_formed E (events E) (rf X) ->
(rf X) x e ->
In _ (events E) x.
Proof.
intros E X x e Hwf Hrfwf Hrf.
destruct Hrfwf as [? [Hrf_cands ?]].
generalize (Hrf_cands x e Hrf); unfold rfmaps; intro Hrfmap.
destruct Hrfmap as [Hevt_x Hrest]; exact Hevt_x.
Qed.
Lemma ran_rf_in_events :
forall E X x e,
well_formed_event_structure E ->
rfmaps_well_formed E (events E) (rf X) ->
(rf X) x e ->
In _ (events E) e.
Proof.
intros E X x e Hwf Hrfwf Hrf.
destruct Hrfwf as [? [Hrf_cands ?]].
generalize (Hrf_cands x e Hrf); unfold rfmaps; intro Hrfmap.
destruct Hrfmap as [Hevt_x [Hevt_e Hrest]]; exact Hevt_e.
Qed.
(*mrf*)
Lemma dom_mrf_is_write :
forall E X x y,
(forall e1 e2 : Event, rf X e1 e2 -> rfmaps (events E) e1 e2) ->
mrf X x y ->
exists l, exists v, action x = Access W l v.
Proof.
case_eq inter; case_eq intra; intros Hinter Hintra; unfold mrf;
unfold mrfi; unfold mrfe; rewrite Hinter; rewrite Hintra;
intros E X x y Hrf_cands Hxy; simpl in Hxy; inversion Hxy as [Hrfi | Hrfe].
case_eq (action x).
intros dx lx vx Hx.
case_eq dx.
intro Hr.
destruct Hrfi as [Hrf ?].
generalize (Hrf_cands x y Hrf); intro Hc.
destruct Hc as [? [? [? [Hwx Hry]]]].
unfold write_to in Hwx; rewrite Hx in Hwx; rewrite Hr in Hwx;
destruct Hwx as [v Hwx]; inversion Hwx.
intro Hw; rewrite Hw in Hx.
exists lx; exists vx; trivial.
case_eq (action x).
intros dx lx vx Hx.
case_eq dx.
intro Hr.
destruct Hrfe as [Hrf ?].
generalize (Hrf_cands x y Hrf); intro Hc.
destruct Hc as [? [? [? [Hwx Hry]]]].
unfold write_to in Hwx; rewrite Hx in Hwx; rewrite Hr in Hwx;
destruct Hwx as [v Hwx]; inversion Hwx.
intro Hw; rewrite Hw in Hx.
exists lx; exists vx; trivial.
inversion Hrfi.
case_eq (action x).
intros dx lx vx Hx.
case_eq dx.
intro Hr.
destruct Hrfe as [Hrf ?].
generalize (Hrf_cands x y Hrf); intro Hc.
destruct Hc as [? [? [? [Hwx Hry]]]].
unfold write_to in Hwx; rewrite Hx in Hwx; rewrite Hr in Hwx;
destruct Hwx as [v Hwx]; inversion Hwx.
intro Hw; rewrite Hw in Hx.
exists lx; exists vx; trivial.
case_eq (action x).
intros dx lx vx Hx.
case_eq dx.
intro Hr.
destruct Hrfi as [Hrf ?].
generalize (Hrf_cands x y Hrf); intro Hc.
destruct Hc as [? [? [? [Hwx Hry]]]].
unfold write_to in Hwx; rewrite Hx in Hwx; rewrite Hr in Hwx;
destruct Hwx as [v Hwx]; inversion Hwx.
intro Hw; rewrite Hw in Hx.
exists lx; exists vx; trivial.
inversion Hrfe.
inversion Hrfi.
inversion Hrfe.
Qed.
Lemma ran_mrf_is_read :
forall E X x y,
(forall e1 e2 : Event, rf X e1 e2 -> rfmaps (events E) e1 e2) ->
mrf X x y ->
exists l, exists v, action y = Access R l v.
Proof.
case_eq inter; case_eq intra; intros Hinter Hintra; unfold mrf;
unfold mrfi; unfold mrfe; rewrite Hinter; rewrite Hintra;
intros E X x y Hrf_cands Hxy; simpl in Hxy; inversion Hxy as [Hrfi | Hrfe].
case_eq (action y).
intros dy ly vy Hy.
case_eq dy.
intro Hr; rewrite Hr in Hy.
exists ly; exists vy; trivial.
intro Hw.
destruct Hrfi as [Hrf ?].
generalize (Hrf_cands x y Hrf); intro Hc.
destruct Hc as [? [? [? [Hwx Hry]]]].
unfold read_from in Hry; rewrite Hy in Hry; rewrite Hw in Hry;
destruct Hry as [v Hry]; inversion Hry.
case_eq (action y).
intros dy ly vy Hy.
case_eq dy.
intro Hr; rewrite Hr in Hy.
exists ly; exists vy; trivial.
intro Hw.
destruct Hrfe as [Hrf ?].
generalize (Hrf_cands x y Hrf); intro Hc.
destruct Hc as [? [? [? [Hwx Hry]]]].
unfold read_from in Hry; rewrite Hy in Hry; rewrite Hw in Hry;
destruct Hry as [v Hry]; inversion Hry.
inversion Hrfi.
case_eq (action y).
intros dy ly vy Hy.
case_eq dy.
intro Hr; rewrite Hr in Hy.
exists ly; exists vy; trivial.
intro Hw.
destruct Hrfe as [Hrf ?].
generalize (Hrf_cands x y Hrf); intro Hc.
destruct Hc as [? [? [? [Hwx Hry]]]].
unfold read_from in Hry; rewrite Hy in Hry; rewrite Hw in Hry;
destruct Hry as [v Hry]; inversion Hry.
case_eq (action y).
intros dy ly vy Hy.
case_eq dy.
intro Hr; rewrite Hr in Hy.
exists ly; exists vy; trivial.
intro Hw.
destruct Hrfi as [Hrf ?].
generalize (Hrf_cands x y Hrf); intro Hc.
destruct Hc as [? [? [? [Hwx Hry]]]].
unfold read_from in Hry; rewrite Hy in Hry; rewrite Hw in Hry;
destruct Hry as [v Hry]; inversion Hry.
inversion Hrfe.
inversion Hrfi.
inversion Hrfe.
Qed.
Lemma mrf_uni :
forall E X x w1 w2,
rfmaps_well_formed E (events E) (rf X) ->
mrf X w1 x -> mrf X w2 x ->
w1 = w2.
Proof.
case_eq inter; case_eq intra; intros Hinter Hintra; unfold mrf;
unfold mrfi; unfold mrfe; rewrite Hinter; rewrite Hintra; simpl;
intros E X x w1 w2 Hrfwf H1 H2; destruct Hrfwf as [? [? Hrf_uni]];
inversion H1 as [Hrfi1 | Hrfe1]; inversion H2 as [Hrfi2 | Hrfe2].
destruct Hrfi1 as [Hrf1 ?]; destruct Hrfi2 as [Hrf2 ?];
apply (Hrf_uni x w1 w2 Hrf1 Hrf2).
destruct Hrfi1 as [Hrf1 ?]; destruct Hrfe2 as [Hrf2 ?];
apply (Hrf_uni x w1 w2 Hrf1 Hrf2).
destruct Hrfe1 as [Hrf1 ?]; destruct Hrfi2 as [Hrf2 ?];
apply (Hrf_uni x w1 w2 Hrf1 Hrf2).
destruct Hrfe1 as [Hrf1 ?]; destruct Hrfe2 as [Hrf2 ?];
apply (Hrf_uni x w1 w2 Hrf1 Hrf2).
inversion Hrfi1.
inversion Hrfi1.
inversion Hrfi2.
destruct Hrfe1 as [Hrf1 ?]; destruct Hrfe2 as [Hrf2 ?];
apply (Hrf_uni x w1 w2 Hrf1 Hrf2).
destruct Hrfi1 as [Hrf1 ?]; destruct Hrfi2 as [Hrf2 ?];
apply (Hrf_uni x w1 w2 Hrf1 Hrf2).
inversion Hrfe2.
inversion Hrfe1.
inversion Hrfe2.
inversion Hrfi2.
inversion Hrfe2.
inversion Hrfi2.
inversion Hrfe2.
Qed.
Lemma mrf_rf_uni :
forall E X x w1 w2,
rfmaps_well_formed E (events E) (rf X) ->
mrf X w1 x -> rf X w2 x ->
w1 = w2.
Proof.
case_eq inter; case_eq intra; intros Hinter Hintra; unfold mrf;
unfold mrfi; unfold mrfe; rewrite Hinter; rewrite Hintra; simpl;
intros E X x w1 w2 Hrfwf H1 Hrf2; destruct Hrfwf as [? [? Hrf_uni]];
inversion H1 as [Hrfi1 | Hrfe1].
destruct Hrfi1 as [Hrf1 ?]; apply (Hrf_uni x w1 w2 Hrf1 Hrf2).
destruct Hrfe1 as [Hrf1 ?]; apply (Hrf_uni x w1 w2 Hrf1 Hrf2).
inversion Hrfi1.
destruct Hrfe1 as [Hrf1 ?]; apply (Hrf_uni x w1 w2 Hrf1 Hrf2).
destruct Hrfi1 as [Hrf1 ?]; apply (Hrf_uni x w1 w2 Hrf1 Hrf2).
inversion Hrfe1.
inversion Hrfi1.
inversion Hrfe1.
Qed.
(** fr *)
Lemma fr_ax1 :
forall E X x y,
fr E X x y ->
exists wr, rf X wr x /\ ws X wr y.
Proof.
intros E X x y Hxy.
destruct Hxy as [? [? Hxy]]; auto.
Qed.
Lemma fr_ax2 :
forall E X x y,
well_formed_event_structure E ->
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
(exists wr, rf X wr x /\ ws X wr y) ->
fr E X x y.
Proof.
intros E X x y Hwf Hvalid Hxy.
generalize Hvalid; intro Hv.
destruct Hvalid as [Hwswf Hrfwf].
destruct Hxy as [? [Hrf Hws]]; split; [| split].
eapply ran_rf_in_events; [apply Hwf | apply Hrfwf | apply Hrf].
destruct Hwswf as [Hws_tot Hws_cands].
eapply ws_evt_right; [apply Hws_tot | apply Hws_cands | apply Hws].
exists x0; auto.
Qed.
Lemma dom_fr_is_read :
forall E X x y,
rfmaps_well_formed E (events E) (rf X) ->
fr E X x y ->
exists l, exists v, action x = Access R l v.
Proof.
intros E X x y Hvalid Hxy.
generalize (fr_ax1 Hxy); intros [? [Hrf Hws]].
destruct Hvalid as [? [Hrf_cands ?]].
eapply ran_rf_is_read; [apply Hrf_cands | apply Hrf].
Qed.
Lemma ran_fr_is_write :
forall E X x y,
write_serialization_well_formed (events E) (ws X) ->
fr E X x y ->
exists v, exists l, action y = Access W l v.
Proof.
intros E X x y Hvalid Hxy.
generalize (fr_ax1 Hxy); intros [? [Hrf Hws]].
eapply ran_ws_is_write; [apply Hvalid | apply Hws].
Qed.
End Ax.
Section DomRan.
(** po *)
Lemma po_strict_domain_in_events (E:Event_struct) (e e0:Event) :
(po_strict E) e e0 ->
In _ (events E) e.
Proof.
unfold po_strict; unfold In; intros E e e0 Hin.
destruct Hin as [Hproc [Hpoi [He He0]]].
exact He.
Qed.
Lemma po_strict_range_in_events (E:Event_struct) (e e0:Event) :
(po_strict E) e e0 ->
In _ (events E) e0.
Proof.
unfold po_strict; unfold In; intros E e e0 Hin.
destruct Hin as [Hproc [Hpoi [He He0]]].
exact He0.
Qed.
(** iico *)
Lemma iico_domain_incl_in_events (E:Event_struct) (e e0: Event) :
(well_formed_event_structure E) ->
iico E e e0 -> In _ (events E) e.
Proof.
unfold well_formed_event_structure.
intros E e e0 Hwf.
destruct Hwf as [? Hwf].
destruct Hwf as [Hsame_eiid_iiid Hwf].
destruct Hwf as [Hdomain_intra Hwf].
destruct Hwf as [Hrange_intra Hwf].
intros He_in_range_intra.
assert (In _ (dom (iico E)) e).
unfold ran; unfold In; exists e0; exact He_in_range_intra.
unfold Included in Hdomain_intra; apply Hdomain_intra; exact H0.
Qed.
Lemma iico_range_incl_in_events (E:Event_struct) (e e0: Event) : (* basic *)
(well_formed_event_structure E) ->
iico E e e0 -> In _ (events E) e0.
Proof.
unfold well_formed_event_structure.
intros E e e0 Hwf.
destruct Hwf as [? Hwf].
destruct Hwf as [Hsame_eiid_iiid Hwf].
destruct Hwf as [Hdomain_intra Hwf].
destruct Hwf as [Hrange_intra Hwf].
intros He0_in_domain_intra.
assert (In _ (ran (iico E)) e0).
unfold range; unfold In; exists e; exact He0_in_domain_intra.
unfold Included in Hrange_intra; apply Hrange_intra; exact H0.
Qed.
(** po_iico *)
Lemma po_iico_domain_in_events (E:Event_struct) (e e0:Event) :
(well_formed_event_structure E) ->
(po_iico E) e e0 -> In _ (events E) e.
Proof.
intros E e e0 Hwf Hpo_iico.
unfold In in Hpo_iico; unfold po_iico in Hpo_iico.
inversion Hpo_iico as [Hpo | Hiico].
eapply po_strict_domain_in_events; apply Hpo.
eapply iico_domain_incl_in_events; [exact Hwf | apply Hiico].
Qed.
Lemma po_iico_range_in_events (E:Event_struct) (e e0:Event) : (* basic *)
(well_formed_event_structure E) ->
(po_iico E) e e0 -> In Event (events E) e0.
Proof.
intros E e e0 Hwf Hpo_iico.
unfold In in Hpo_iico; unfold po_iico in Hpo_iico.
inversion Hpo_iico as [Hpo | Hiico].
eapply po_strict_range_in_events; apply Hpo.
eapply iico_range_incl_in_events; [exact Hwf | apply Hiico].
Qed.
Lemma hb_ran_in_evts :
forall E X x y,
well_formed_event_structure E ->
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
(hb E X) y x ->
In _ (events E) x.
Proof.
intros E X x y Hwf [Hwswf Hrfwf] Hhb.
destruct Hwswf as [Hws_tot Hws_cands];
destruct Hrfwf as [? [Hrf_cands ?]].
inversion Hhb as [Hrf_fr | Hws].
inversion Hrf_fr as [Hrf | Hfr].
generalize (Hrf_cands y x Hrf); intro Hrfm.
destruct Hrfm as [Hy [Hx Hrfm]]; apply Hx.
destruct Hfr as [Hy [Hx Hrest]]; apply Hx.
eapply ws_evt_right.
apply Hws_tot. (*ws ax*)
apply Hws_cands.
apply Hws.
Qed.
Lemma hb_dom_in_evts :
forall E X x y,
well_formed_event_structure E ->
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
(hb E X) x y ->
In _ (events E) x.
Proof.
intros E X x y Hwf [Hwswf Hrfwf] Hhb.
destruct Hwswf as [Hws_tot Hws_cands];
destruct Hrfwf as [? [Hrf_cands ?]].
inversion Hhb as [Hrf_fr | Hws].
inversion Hrf_fr as [Hrf | Hfr].
generalize (Hrf_cands x y Hrf); intro Hrfm.
destruct Hrfm as [Hx [Hy Hrfm]]; apply Hx.
destruct Hfr as [Hx [Hy Hrest]]; apply Hx.
eapply ws_evt_left.
apply Hws_tot. (*ws ax*)
apply Hws_cands.
apply Hws.
Qed.
Lemma dom_ws_in_events :
forall E X x e,
well_formed_event_structure E ->
write_serialization_well_formed (events E) (ws X) ->
(ws X) x e ->
In _ (events E) x.
Proof.
intros E X x e Hwf Hwswf Hws.
generalize (ws_cands E X x e Hwswf Hws); intro Hmem.
destruct Hmem as [l [Hmx Hme]].
destruct Hmx as [Hdr Hrest].
unfold udr in Hdr.
auto.
Qed.
Lemma ran_ws_in_events :
forall E X x e,
well_formed_event_structure E ->
write_serialization_well_formed (events E) (ws X) ->
(ws X) x e ->
In _ (events E) e.
Proof.
intros E X x e Hwf Hwswf Hws.
generalize (ws_cands E X x e Hwswf Hws); intro Hmem.
destruct Hmem as [l [Hmx Hme]].
destruct Hme as [Hdr Hrest].
auto.
Qed.
Lemma dom_fr_in_events :
forall E X x e,
well_formed_event_structure E ->
(fr E X) x e ->
In _ (events E) x.
Proof.
intros E X x e Hwf Hfr.
unfold In in Hfr; unfold fr in Hfr; unfold frmaps in Hfr.
destruct Hfr as [Hevt_x Hrest].
exact Hevt_x.
Qed.
Lemma ran_fr_in_events :
forall E X x e,
well_formed_event_structure E ->
(fr E X) x e ->
In _ (events E) e.
Proof.
intros E X x e Hwf Hfr.
unfold In in Hfr; unfold fr in Hfr; unfold frmaps in Hfr.
destruct Hfr as [Hevt_x [Hevt_e Hrest]].
exact Hevt_e.
Qed.
Lemma hb_domain_in_events (E:Event_struct) (X:Execution_witness) (e e0:Event) :
well_formed_event_structure E ->
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
(hb E X) e e0 -> In _ (events E) e.
Proof.
intros E X e e0 Hwf Hvalid Hhb.
inversion Hhb as [Hrf_fr | Hws].
inversion Hrf_fr as [Hrf | Hfr].
(*rf*)
destruct Hvalid as [Hwswf Hrfwf];
eapply dom_rf_in_events; [apply Hwf | apply Hrfwf | apply Hrf].
(*fr*)
eapply dom_fr_in_events; [apply Hwf | apply Hfr].
(*ws*)
destruct Hvalid as [Hwswf Hrfwf];
eapply dom_ws_in_events; [apply Hwf | apply Hwswf | apply Hws].
Qed.
Lemma hb_range_in_events (E:Event_struct) (X:Execution_witness) (e e0:Event) :
well_formed_event_structure E ->
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
(hb E X) e e0 -> In _ (events E) e0.
Proof.
intros E X e e0 Hwf Hs Hhb.
inversion Hhb as [Hrf_fr | Hws].
inversion Hrf_fr as [Hrf | Hfr].
(*rf*)
destruct Hs as [Hwswf Hrfwf];
eapply ran_rf_in_events; [apply Hwf | apply Hrfwf | apply Hrf].
(*fr*)
eapply ran_fr_in_events; [apply Hwf | apply Hfr].
(*ws*)
destruct Hs as [Hwswf Hrfwf];
eapply ran_ws_in_events; [apply Hwf | apply Hwswf | apply Hws].
Qed.
Lemma ghb_domain_in_events (E:Event_struct) (X:Execution_witness) (e e0:Event) :
well_formed_event_structure E ->
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
(ghb E X) e e0 -> In _ (events E) e.
Proof.
intros E X e e0 Hwf Hvalid Hghb; unfold ghb in Hghb.
case_eq inter; case_eq intra; intros Hintra Hinter;
rewrite Hinter in Hghb; rewrite Hintra in Hghb.
(*true true*)
inversion Hghb as [Hrf_inter | Hrest].
destruct Hrf_inter as [Hrf ?].
destruct Hvalid as [Hwswf Hrfwf];
eapply dom_rf_in_events; [apply Hwf | apply Hrfwf | apply Hrf].
inversion Hrest as [Hrf_intra | Hres].
destruct Hrf_intra as [Hrf ?].
destruct Hvalid as [Hwswf Hrfwf];
eapply dom_rf_in_events; [apply Hwf | apply Hrfwf | apply Hrf].
inversion Hres as [Hin_ab | Hre].
generalize (ab_evts Hin_ab); intros [He He0]; auto.
inversion Hre as [Hws_fr | Hppo].
inversion Hws_fr as [Hws | Hfr].
destruct Hvalid as [Hwswf Hrfwf];
eapply dom_ws_in_events; [apply Hwf | apply Hwswf | apply Hws].
eapply dom_fr_in_events; [apply Hwf | apply Hfr].
eapply po_iico_domain_in_events; [apply Hwf |].
apply ppo_valid; apply Hppo.
(*true false*)
inversion Hghb as [Hrf_inter | Hrest].
destruct Hrf_inter as [Hrf ?].
destruct Hvalid as [Hwswf Hrfwf];
eapply dom_rf_in_events; [apply Hwf | apply Hrfwf | apply Hrf].
inversion Hrest as [Hin_ab | Hre].
generalize (ab_evts Hin_ab); intros [He He0]; auto.
inversion Hre as [Hws_fr | Hppo].
inversion Hws_fr as [Hws | Hfr].
destruct Hvalid as [Hwswf Hrfwf];
eapply dom_ws_in_events; [apply Hwf | apply Hwswf | apply Hws].
eapply dom_fr_in_events; [apply Hwf | apply Hfr].
eapply po_iico_domain_in_events; [apply Hwf |].
apply ppo_valid; apply Hppo.
(*false true*)
inversion Hghb as [Hrf_intra | Hres].
destruct Hrf_intra as [Hrf ?].
destruct Hvalid as [Hwswf Hrfwf];
eapply dom_rf_in_events; [apply Hwf | apply Hrfwf | apply Hrf].
inversion Hres as [Hin_ab | Hre].
generalize (ab_evts Hin_ab); intros [He He0]; auto.
inversion Hre as [Hws_fr | Hppo].
inversion Hws_fr as [Hws | Hfr].
destruct Hvalid as [Hwswf Hrfwf];
eapply dom_ws_in_events; [apply Hwf | apply Hwswf | apply Hws].
eapply dom_fr_in_events; [apply Hwf | apply Hfr].
eapply po_iico_domain_in_events; [apply Hwf |].
apply ppo_valid; apply Hppo.
(*false false*)
inversion Hghb as [Hin_ab | Hre].
generalize (ab_evts Hin_ab); intros [He He0]; auto.
inversion Hre as [Hws_fr | Hppo].
inversion Hws_fr as [Hws | Hfr].
destruct Hvalid as [Hwswf Hrfwf];
eapply dom_ws_in_events; [apply Hwf | apply Hwswf | apply Hws].
eapply dom_fr_in_events; [apply Hwf | apply Hfr].
eapply po_iico_domain_in_events; [apply Hwf |].
apply ppo_valid; apply Hppo.
Qed.
Lemma ghb_range_in_events (E:Event_struct) (X:Execution_witness) (e e0:Event) :
well_formed_event_structure E ->
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
(ghb E X) e e0 -> In _ (events E) e0.
Proof.
intros E X e e0 Hwf Hvalid Hghb; unfold ghb in Hghb.
case_eq inter; case_eq intra; intros Hintra Hinter;
rewrite Hinter in Hghb; rewrite Hintra in Hghb.
(*true true*)
inversion Hghb as [Hrf_inter | Hrest].
destruct Hrf_inter as [Hrf ?].
destruct Hvalid as [Hwswf Hrfwf];
eapply ran_rf_in_events; [apply Hwf | apply Hrfwf | apply Hrf].
inversion Hrest as [Hrf_intra | Hres].
destruct Hrf_intra as [Hrf ?].
destruct Hvalid as [Hwswf Hrfwf];
eapply ran_rf_in_events; [apply Hwf | apply Hrfwf | apply Hrf].
inversion Hres as [Hin_ab | Hre].
generalize (ab_evts Hin_ab); intros [He He0]; auto.
inversion Hre as [Hws_fr | Hppo].
inversion Hws_fr as [Hws | Hfr].
destruct Hvalid as [Hwswf Hrfwf];
eapply ran_ws_in_events; [apply Hwf | apply Hwswf | apply Hws].
eapply ran_fr_in_events; [apply Hwf | apply Hfr].
eapply po_iico_range_in_events; [apply Hwf |].
apply ppo_valid; apply Hppo.
(*true false*)
inversion Hghb as [Hrf_inter | Hrest].
destruct Hrf_inter as [Hrf ?].
destruct Hvalid as [Hwswf Hrfwf];
eapply ran_rf_in_events; [apply Hwf | apply Hrfwf | apply Hrf].
inversion Hrest as [Hin_ab | Hre].
generalize (ab_evts Hin_ab); intros [He He0]; auto.
inversion Hre as [Hws_fr | Hppo].
inversion Hws_fr as [Hws | Hfr].
destruct Hvalid as [Hwswf Hrfwf];
eapply ran_ws_in_events; [apply Hwf | apply Hwswf | apply Hws].
eapply ran_fr_in_events; [apply Hwf | apply Hfr].
eapply po_iico_range_in_events; [apply Hwf |].
apply ppo_valid; apply Hppo.
(*false true*)
inversion Hghb as [Hrf_intra | Hres].
destruct Hrf_intra as [Hrf ?].
destruct Hvalid as [Hwswf Hrfwf];
eapply ran_rf_in_events; [apply Hwf | apply Hrfwf | apply Hrf].
inversion Hres as [Hin_ab | Hre].
generalize (ab_evts Hin_ab); intros [He He0]; auto.
inversion Hre as [Hws_fr | Hppo].
inversion Hws_fr as [Hws | Hfr].
destruct Hvalid as [Hwswf Hrfwf];
eapply ran_ws_in_events; [apply Hwf | apply Hwswf | apply Hws].
eapply ran_fr_in_events; [apply Hwf | apply Hfr].
eapply po_iico_range_in_events; [apply Hwf |].
apply ppo_valid; apply Hppo.
(*false false*)
inversion Hghb as [Hin_ab | Hre].
generalize (ab_evts Hin_ab); intros [He He0]; auto.
inversion Hre as [Hws_fr | Hppo].
inversion Hws_fr as [Hws | Hfr].
destruct Hvalid as [Hwswf Hrfwf];
eapply ran_ws_in_events; [apply Hwf | apply Hwswf | apply Hws].
eapply ran_fr_in_events; [apply Hwf | apply Hfr].
eapply po_iico_range_in_events; [apply Hwf |].
apply ppo_valid; apply Hppo.
Qed.
Lemma ghb_in_evts :
forall E X,
(well_formed_event_structure E) ->
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
Included _
(Union _ (dom (ghb E X)) (ran (ghb E X))) (events E).
Proof.
unfold Included; unfold domain; unfold range; unfold In;
intros E X Hwf Hvalid x Hx.
inversion Hx as [e Hdom | e Hran];
[unfold In in Hdom; destruct Hdom as [x0 Hdom] |
unfold In in Hran; destruct Hran as [x0 Hran]].
(*dom*)
change (events E x) with (In _ (events E) x);
eapply ghb_domain_in_events; [apply Hwf | apply Hvalid | apply Hdom].
(*ran*)
change (events E x) with (In _ (events E) x);
eapply ghb_range_in_events; [apply Hwf | apply Hvalid | apply Hran].
Qed.
Lemma ws_in_ghb :
forall E X x y,
ws X x y ->
ghb E X x y.
Proof.
intros E X x y Hws.
case_eq inter; case_eq intra; intros Hinter Hintra;
unfold ghb; rewrite Hinter; rewrite Hintra.
right; right; right; left; left; auto.
right; right; left; left; auto.
right; right; left; left; auto.
right; left; left; auto.
Qed.
Lemma fr_in_ghb :
forall E X x y,
fr E X x y ->
ghb E X x y.
Proof.
intros E X x y Hfr.
case_eq inter; case_eq intra; intros Hinter Hintra;
unfold ghb; rewrite Hinter; rewrite Hintra.
right; right; right; left; right; auto.
right; right; left; right; auto.
right; right; left; right; auto.
right; left; right; auto.
Qed.
Lemma ppo_in_ghb :
forall E X x y,
ppo E x y ->
ghb E X x y.
Proof.
intros E X x y Hppo.
case_eq inter; case_eq intra; intros Hinter Hintra;
unfold ghb; rewrite Hinter; rewrite Hintra.
right; right; right; right; auto.
right; right; right; auto.
right; right; right; auto.
right; right; auto.
Qed.
Lemma ws_ax2 :
forall E X x y,
well_formed_event_structure E ->
valid_execution E X ->
tc (ghb E X) x y ->
(exists l : Location,
In _
(writes_to_same_loc_l
(udr (tc (ghb E X))) l) y /\
In _
(writes_to_same_loc_l
(udr (tc (ghb E X))) l) x) ->
ws X x y.
Proof.
intros E X x y Hwf Hvalid Htc Hl.
generalize Hvalid; intro Hv.
destruct_valid Hvalid; assert (write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X)) as Hs.
split; split; auto.
destruct Hl as [l [Hy Hx]].
assert (In _ (writes_to_same_loc_l (events E) l) y) as Hmy.
split; destruct Hy as [Hy Hw]; [|apply Hw].
generalize (ghb_in_evts X Hwf Hs); intro Hi; unfold Included in Hi;
apply Hi.
generalize (dom_ran_tc (ghb E X)); intro Heq; rewrite Heq; auto.
assert (In _ (writes_to_same_loc_l (events E) l) x) as Hmx.
split; destruct Hx as [Hx Hw]; [|apply Hw].
generalize (ghb_in_evts X Hwf Hs); intro Hi; unfold Included in Hi;
apply Hi.
generalize (dom_ran_tc (ghb E X)); intro Heq; rewrite Heq; auto.
generalize (Hws_tot l); intros [Hdr [Htrans [Hac Htot]]].
destruct (eqEv_dec x y) as [Hxyeq | Hdiff].
rewrite <- Hxyeq in Htc; unfold acyclic in Hvalid; generalize (Hvalid x); intro Hc.
contradiction.
generalize (Htot x y Hdiff Hmx Hmy); intro Horxy.
inversion Horxy as [Hxy | Hyx].
destruct Hxy as [Hxy ?]; apply Hxy.
destruct Hyx as [Hyx ?].
assert (tc (ghb E X) x x) as Hxx.
apply trc_ind with y; [apply Htc | apply trc_step; apply ws_in_ghb; apply Hyx].
unfold acyclic in Hvalid; generalize (Hvalid x); intro Hc.
contradiction.
Qed.
Lemma po_union_hb_in_evts :
forall E X,
(well_formed_event_structure E) ->
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
Included _
(Union _ (dom (rel_union (po_iico E) (hb E X)))
(ran (rel_union (po_iico E) (hb E X)))) (events E).
Proof.
unfold Included; unfold domain; unfold range; unfold In;
intros E X Hwf Hvalid x Hx.
inversion Hx as [e Hdom | e Hran];
[unfold In in Hdom; destruct Hdom as [x0 Hdom] |
unfold In in Hran; destruct Hran as [x0 Hran]].
(*dom*)
inversion Hdom as [Hpo | Hhb].
(*po_iico*)
change (events E x) with (In _ (events E) x);
eapply po_iico_domain_in_events; [apply Hwf | apply Hpo].
(*hb*)
change (events E x) with (In _ (events E) x);
eapply hb_domain_in_events; [apply Hwf | apply Hvalid | apply Hhb].
(*ran*)
inversion Hran as [Hpo | Hhb].
(*po_iico*)
change (events E x) with (In _ (events E) x);
eapply po_iico_range_in_events; [apply Hwf | apply Hpo].
(*hb*)
change (events E x) with (In _ (events E) x);
eapply hb_range_in_events; [apply Hwf | apply Hvalid | apply Hhb].
Qed.
Lemma dom_ran_so_incl_po_hb :
forall E X,
(well_formed_event_structure E) ->
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
Included _ (Union _ (dom (rel_union (po_iico E) (hb E X)))
(ran (rel_union (po_iico E) (hb E X)))) (events E).
Proof.
intros E X Hwf Hvalid;
apply po_union_hb_in_evts; auto.
Qed.
End DomRan.
Section Hexa.
Definition hb' (E:Event_struct) (X:Execution_witness) : Rln Event :=
fun e1 => fun e2 => (rel_union (rel_union (hb E X) (rel_seq (ws X) (rf X))) (rel_seq (fr E X) (rf X))) e1 e2.
Definition maybe_po (E:Event_struct) : Rln Event :=
fun e1 => fun e2 => (po_iico E) e1 e2 \/ e1 = e2.
Definition maybe_hb' (E:Event_struct) (X:Execution_witness) : Rln Event :=
fun e1 => fun e2 => (hb' E X) e1 e2 \/ e1 = e2.
Definition pre_hexa (E:Event_struct) (X:Execution_witness) : Rln Event :=
fun e1 => fun e2 => (tc (rel_seq (hb' E X) (po_iico E))) e1 e2 \/ e1 = e2.
Definition hexa (E:Event_struct) (X:Execution_witness) : Rln Event :=
fun e1 => fun e2 =>
rel_seq (maybe_po E) (rel_seq (pre_hexa E X) (maybe_hb' E X)) e1 e2.
Definition pb (E:Event_struct) : Rln Event := po_iico E.
Lemma pb_in_hb_po :
forall E X,
rel_incl (pb E) (tc (rel_union (hb E X) (po_iico E))).
Proof.
unfold Included; unfold In; unfold pb;
intros E X x e Hpb.
apply trc_step; right; auto.
Qed.
Lemma ab_in_ghb :
forall E X,
rel_incl (abc E X) (ghb E X).
Proof.
unfold rel_incl;
intros E X x y Hab.
case_eq inter; case_eq intra; unfold ghb;
intros Hintra Hinter; rewrite Hintra; rewrite Hinter.
(*true,true*)
right; right; left; apply Hab.
(*true,false*)
right; left; apply Hab.
(*false,true*)
right; left; apply Hab.
(*false,false*)
left; apply Hab.
Qed.
Lemma ws_u_fr_in_ghb :
forall E X,
valid_execution E X ->
rel_incl (rel_union (ws X) (fr E X)) (ghb E X).
Proof.
unfold rel_incl;
intros E X Hvalid x y Hab.
case_eq inter; case_eq intra; unfold ghb;
intros Hintra Hinter; rewrite Hintra; rewrite Hinter.
(*true,true*)
right; right; right; left; apply Hab.
(*true,false*)
right; right; left; apply Hab.
(*false,true*)
right; right; left; apply Hab.
(*false,false*)
right; left; apply Hab.
Qed.
Lemma hb_ac :
forall E X x,
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
~(hb E X x x).
Proof.
unfold not;
intros E X x [Hwswf Hrfwf] Hhb.
destruct Hrfwf as [? [Hrf_cands ?]].
inversion Hhb as [Hrf_fr | Hws].
inversion Hrf_fr as [Hrf | Hfr].
(*rf*)
generalize (Hrf_cands x x Hrf); intro Hrfc.
destruct Hrfc as [Hex [Heex [l [Hwx Hrx]]]].
case_eq (action x).
intros dx lx vx Hx; case_eq dx; intro Hdx; rewrite Hdx in Hx;
unfold write_to in Hwx; unfold read_from in Hrx;
rewrite Hx in Hwx; rewrite Hx in Hrx.
destruct Hwx as [v1 Hwx];
inversion Hwx.
destruct Hrx as [v1 Hrx];
inversion Hrx.
(*fr*)
destruct Hfr as [Hex [Heex [wr [Hrf Hws]]]].
generalize (Hrf_cands wr x Hrf); intro Hrfc.
destruct Hrfc as [Hewr [Heeex [l [Hwwr Hrx]]]].
case_eq (action x).
intros dx lx vx Hx; case_eq dx; intro Hdx; rewrite Hdx in Hx;
unfold read_from in Hrx; rewrite Hx in Hrx.
generalize (ws_cands E X wr x Hwswf Hws); intro Hw.
destruct Hw as [lwr [Hw_wr Hw_x]].
destruct Hw_x as [Hudr Hwt_x].
unfold write_to in Hwt_x; rewrite Hx in Hwt_x.
destruct Hwt_x as [v1 Hwt_x];
inversion Hwt_x.
destruct Hrx as [v1 Hrx];
inversion Hrx.
(*ws*)
destruct Hwswf as [Hws_tot Hws_cands].
generalize (ws_cy E X x Hws_tot Hws_cands); intro Hc; contradiction.
Qed.
Lemma hb_seq_hb_implies_hb' :
forall E X x y z,
well_formed_event_structure E ->
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
hb E X x y ->
hb E X y z ->
hb' E X x z.
Proof.
intros E X x y z Hwf [Hwswf Hrfwf] Hxy Hyz.
inversion Hxy as [Hrf_fr_xy | Hws_xy];
inversion Hyz as [Hrf_fr_yz | Hws_yz].
inversion Hrf_fr_xy as [Hrf_xy | Hfr_xy];
inversion Hrf_fr_yz as [Hrf_yz | Hfr_yz].
destruct_rf Hrfwf.
generalize (ran_rf_is_read E X x y Hrf_cands Hrf_xy); intros [l [v Hry]].
generalize (dom_rf_is_write E X y z Hrf_cands Hrf_yz); intros [ly [vy Hwy]].
rewrite Hwy in Hry; inversion Hry.
generalize (fr_ax1 Hfr_yz); intros [wr [Hrf Hws]].
generalize (rf_uni X y x wr Hrfwf Hrf_xy Hrf); intro Heq.
rewrite <- Heq in Hws; left; left; right; apply Hws.
right; exists y; split; auto.
generalize (ran_fr_is_write Hwswf Hfr_xy); intros [l [v Hwy]].
generalize (dom_fr_is_read Hrfwf Hfr_yz); intros [ly [vy Hry]].
rewrite Hwy in Hry; inversion Hry.
inversion Hrf_fr_xy as [Hrf_xy | Hfr_xy].
destruct_rf Hrfwf.
generalize (ran_rf_is_read E X x y Hrf_cands Hrf_xy); intros [l [v Hry]].
generalize (dom_ws_is_write E X y z Hwswf Hws_yz); intros [ly [vy Hwy]].
rewrite Hwy in Hry; inversion Hry.
destruct Hfr_xy as [? [? [wr [Hrf Hws]]]].
generalize (ws_trans E X wr y z Hwswf Hws Hws_yz); intro Hws_wrz.
left; left; left; right.
eapply fr_ax2; [apply Hwf | | exists wr; split; auto]; split; auto.
inversion Hrf_fr_yz as [Hrf_yz | Hfr_yz].
left; right; exists y; split; auto.
generalize (ran_ws_is_write E X x y Hwswf Hws_xy); intros [l [v Hwy]].
generalize (dom_fr_is_read Hrfwf Hfr_yz); intros [ly [vy Hry]].
rewrite Hwy in Hry; inversion Hry.
left; left; right;
apply (ws_trans E X x y z Hwswf Hws_xy Hws_yz).
Qed.
Lemma hb_seq_ws_rf_implies_hb' :
forall E X x y z,
well_formed_event_structure E ->
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
hb E X x y ->
rel_seq (ws X) (rf X) y z ->
hb' E X x z.
Proof.
intros E X x y z Hwf [Hwswf Hrfwf] Hxy Hyz.
inversion Hxy as [Hrf_fr_xy | Hws_xy].
inversion Hrf_fr_xy as [Hrf_xy | Hfr_xy].
destruct Hyz as [? [Hws Hrf]].
destruct Hrfwf as [? [Hrf_cands ?]].
generalize (ran_rf_is_read E X x y Hrf_cands Hrf_xy); intros [l [v Hry]].
generalize (dom_ws_is_write E X y x0 Hwswf Hws); intros [ly [vy Hwy]].
rewrite Hwy in Hry; inversion Hry.
destruct Hyz as [wz [Hws_ywz Hrfwz]].
destruct Hfr_xy as [? [? [wx [Hrf_wx Hws_wxy]]]].
generalize (ws_trans E X wx y wz Hwswf Hws_wxy Hws_ywz); intro Hws_wxwz.
right; exists wz; split; [|apply Hrfwz].
eapply fr_ax2;
[apply Hwf | | exists wx; split; [apply Hrf_wx | apply Hws_wxwz]]; split; auto.
destruct Hyz as [wz [Hws_ywz Hrfwz]].
generalize (ws_trans E X x y wz Hwswf Hws_xy Hws_ywz); intro Hws_xwz.
left; right; exists wz; split; auto.
Qed.
Lemma hb_seq_fr_rf_implies_hb' :
forall E X x y z,
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
hb E X x y ->
rel_seq (fr E X) (rf X) y z ->
hb' E X x z.
Proof.
intros E X x y z Hs Hxy Hyz.
generalize Hs; intros [Hwswf Hrfwf].
inversion Hxy as [Hrf_fr_xy | Hws_xy].
inversion Hrf_fr_xy as [Hrf_xy | Hfr_xy].
destruct Hyz as [wz [Hfr Hrf]].
destruct Hfr as [? [? [wy [Hrf_y Hws_z]]]].
generalize (rf_uni X y x wy Hrfwf Hrf_xy Hrf_y); intro Heq.
rewrite <- Heq in Hws_z.
left; right; exists wz; split; auto.
destruct Hyz as [? [Hfr Hrf]].
generalize (ran_fr_is_write Hwswf Hfr_xy); intros [l [v Hwy]].
generalize (dom_fr_is_read Hrfwf Hfr); intros [ly [vy Hry]].
rewrite Hwy in Hry; inversion Hry.
destruct Hyz as [? [Hfr Hrf]].
generalize (ran_ws_is_write E X x y Hwswf Hws_xy); intros [l [v Hwy]].
generalize (dom_fr_is_read Hrfwf Hfr); intros [ly [vy Hry]].
rewrite Hwy in Hry; inversion Hry.
Qed.
Lemma hb_seq_hb'_implies_hb' :
forall E X x y z,
well_formed_event_structure E ->
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
hb E X x y ->
hb' E X y z ->
hb' E X x z.
Proof.
intros E X x y z Hwf Hvalid Hxy Hyz.
inversion Hyz as [Hhb_wsrf | Hfrrf].
inversion Hhb_wsrf as [Hhb | Hwsrf].
eapply hb_seq_hb_implies_hb'; [apply Hwf | apply Hvalid | apply Hxy | apply Hhb].
eapply hb_seq_ws_rf_implies_hb'; [apply Hwf | apply Hvalid | apply Hxy | apply Hwsrf].
eapply hb_seq_fr_rf_implies_hb'; [apply Hvalid | apply Hxy | apply Hfrrf].
Qed.
Lemma ws_rf_seq_hb_implies_hb' :
forall E X x y z,
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
rel_seq (ws X) (rf X) x y ->
hb E X y z ->
hb' E X x z.
Proof.
intros E X x y z [Hwswf Hrfwf] Hxy Hyz.
inversion Hyz as [Hrf_fr_yz | Hws_yz].
inversion Hrf_fr_yz as [Hrf_yz | Hfr_yz].
destruct Hxy as [? [Hws Hrf]].
destruct Hrfwf as [? [Hrf_cands ?]].
generalize (ran_rf_is_read E X x0 y Hrf_cands Hrf); intros [l [v Hry]].
generalize (dom_rf_is_write E X y z Hrf_cands Hrf_yz); intros [ly [vy Hwy]].
rewrite Hwy in Hry; inversion Hry.
destruct Hxy as [wy1 [Hws_xwy1 Hrf_wy1]].
generalize (fr_ax1 Hfr_yz); intros [wy2 [Hrf_y2 Hws_z]].
generalize (rf_uni X y wy1 wy2 Hrfwf Hrf_wy1 Hrf_y2); intro Heq.
rewrite <- Heq in Hws_z.
left; left; right; eapply ws_trans; [apply Hwswf | apply Hws_xwy1 | apply Hws_z].
destruct Hxy as [? [Hws Hrf]].
destruct Hrfwf as [? [Hrf_cands ?]].
generalize (ran_rf_is_read E X x0 y Hrf_cands Hrf); intros [l [v Hry]].
generalize (dom_ws_is_write E X y z Hwswf Hws_yz); intros [ly [vy Hwy]].
rewrite Hwy in Hry; inversion Hry.
Qed.
Lemma ws_rf_seq_hb'_implies_hb' :
forall E X x y z,
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
rel_seq (ws X) (rf X) x y ->
hb' E X y z ->
hb' E X x z.
Proof.
intros E X x y z Hvalid Hxy Hyz.
generalize Hvalid; intros [Hwswf Hrfwf].
inversion Hyz as [Hhb_wsrf_yz | Hfrrf_yz].
inversion Hhb_wsrf_yz as [Hhb_yz | Hwsrf_yz].
eapply ws_rf_seq_hb_implies_hb'; [apply Hvalid | apply Hxy | apply Hhb_yz].
destruct Hxy as [? [Hws_x Hrf_y]].
destruct Hwsrf_yz as [? [Hws_y Hrf_z]].
destruct Hrfwf as [? [Hrf_cands ?]].
generalize (ran_rf_is_read E X x0 y Hrf_cands Hrf_y); intros [? [? Hry]].
generalize (dom_ws_is_write E X y x1 Hwswf Hws_y); intros [? [? Hwy]].
rewrite Hwy in Hry; inversion Hry.
destruct Hxy as [? [Hws_x Hrf_y]].
destruct Hfrrf_yz as [? [Hfr_y Hrf_z]].
destruct Hfr_y as [? [? [wy [Hrf_y2 Hws_z]]]].
generalize (rf_uni X y x0 wy Hrfwf Hrf_y Hrf_y2); intro Heq.
rewrite <- Heq in Hws_z.
generalize (ws_trans E X x x0 x1 Hwswf Hws_x Hws_z); intro Hws_xx1.
left; right; exists x1; split; auto.
Qed.
Lemma fr_rf_seq_hb_implies_hb' :
forall E X x y z,
well_formed_event_structure E ->
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
rel_seq (fr E X) (rf X) x y ->
hb E X y z ->
hb' E X x z.
Proof.
intros E X x y z Hwf [Hwswf Hrfwf] Hxy Hyz.
inversion Hyz as [Hrf_fr_yz | Hws_yz].
inversion Hrf_fr_yz as [Hrf_yz | Hfr_yz].
destruct Hxy as [? [Hfr Hrf]].
destruct Hrfwf as [? [Hrf_cands ?]].
generalize (ran_rf_is_read E X x0 y Hrf_cands Hrf); intros [l [v Hry]].
generalize (dom_rf_is_write E X y z Hrf_cands Hrf_yz); intros [ly [vy Hwy]].
rewrite Hwy in Hry; inversion Hry.
destruct Hxy as [? [Hfr Hrf]].
destruct Hfr as [? [? [wx [Hrf_x Hws_wx]]]].
destruct Hfr_yz as [? [? [wy [Hrf_y Hws_wyz]]]].
generalize (rf_uni X y x0 wy Hrfwf Hrf Hrf_y); intro Heq.
rewrite <- Heq in Hws_wyz.
generalize (ws_trans E X wx x0 z Hwswf Hws_wx Hws_wyz); intro Hws_wxz.
left; left; left; right; eapply fr_ax2; [apply Hwf | | exists wx; split; [apply Hrf_x | apply Hws_wxz]].
split; auto.
destruct Hxy as [? [Hfr Hrf]].
destruct Hrfwf as [? [Hrf_cands ?]].
generalize (ran_rf_is_read E X x0 y Hrf_cands Hrf); intros [l [v Hry]].
generalize (dom_ws_is_write E X y z Hwswf Hws_yz); intros [ly [vy Hwy]].
rewrite Hwy in Hry; inversion Hry.
Qed.
Lemma hb'_trans :
forall E X x y z,
well_formed_event_structure E ->
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
hb' E X x y ->
hb' E X y z ->
hb' E X x z.
Proof.
intros E X x y z Hwf Ha Hxy Hyz.
inversion Hxy as [Hpxy | Hfrrf_xy];
inversion Hyz as [Hpyz | Hfrrf_yz].
inversion Hpxy as [Hhb_xy | Hwsfr_xy];
inversion Hpyz as [Hhb_yz | Hwsfr_yz].
eapply hb_seq_hb_implies_hb'; [apply Hwf | apply Ha | apply Hhb_xy | apply Hhb_yz].
eapply hb_seq_ws_rf_implies_hb'; [apply Hwf | apply Ha | apply Hhb_xy | apply Hwsfr_yz].
eapply ws_rf_seq_hb_implies_hb'; [apply Ha | apply Hwsfr_xy | apply Hhb_yz].
destruct Hwsfr_xy as [? [Hws_x Hrf_y]];
destruct Hwsfr_yz as [? [Hws_y Hrf_z]].
destruct Ha as [Hwswf Hrfwf].
destruct Hrfwf as [? [Hrf_cands ?]].
generalize (ran_rf_is_read E X x0 y Hrf_cands Hrf_y); intros [l [v Hry]].
generalize (dom_ws_is_write E X y x1 Hwswf Hws_y); intros [? [? Hwy]].
rewrite Hwy in Hry; inversion Hry.
inversion Hpxy as [Hhb_xy | Hwsfr_xy].
eapply hb_seq_fr_rf_implies_hb'; [apply Ha | apply Hhb_xy | apply Hfrrf_yz].
destruct Hfrrf_yz as [wz [Hfr_y Hrf_z]];
destruct Hwsfr_xy as [wy1 [Hws_x Hrf_y1]].
destruct Hfr_y as [? [? [wy2 [Hrf_y2 Hws_wz]]]].
destruct Ha as [Hwswf Hrfwf].
generalize (rf_uni X y wy1 wy2 Hrfwf Hrf_y1 Hrf_y2); intro Heq.
rewrite <- Heq in Hws_wz.
generalize (ws_trans E X x wy1 wz Hwswf Hws_x Hws_wz); intro Hws_xwz.
left; right; exists wz; split; auto.
inversion Hpyz as [Hhb_yz | Hwsfr_yz].
eapply fr_rf_seq_hb_implies_hb'; [apply Hwf | apply Ha | apply Hfrrf_xy | apply Hhb_yz].
destruct Hfrrf_xy as [? [Hfr_x Hrf_y]].
destruct Hwsfr_yz as [? [Hws_y Hrf_z]].
destruct Ha as [Hwswf Hrfwf].
destruct Hrfwf as [? [Hrf_cands ?]].
generalize (ran_rf_is_read E X x0 y Hrf_cands Hrf_y); intros [l [v Hry]].
generalize (dom_ws_is_write E X y x1 Hwswf Hws_y); intros [? [? Hwy]].
rewrite Hwy in Hry; inversion Hry.
destruct Hfrrf_xy as [wy1 [Hfr_x Hrf_y]];
destruct Hfrrf_yz as [wz [Hfr_y Hrf_z]].
destruct Hfr_y as [? [? [wy2 [Hrf_y2 Hws_wz]]]].
destruct Hfr_x as [? [? [wx [Hrf_x Hws_x]]]].
generalize Ha; intros [Hwswf Hrfwf].
generalize (rf_uni X y wy1 wy2 Hrfwf Hrf_y Hrf_y2); intro Heq.
rewrite <- Heq in Hws_wz.
generalize (ws_trans E X wx wy1 wz Hwswf Hws_x Hws_wz); intro Hws_wxwz.
assert (exists wr : Event, rf X wr x /\ ws X wr wz) as Hfrax_xwz.
exists wx; split; auto.
generalize (fr_ax2 X x wz Hwf Ha Hfrax_xwz); intro Hfr_xwz.
right; exists wz; split; auto.
Qed.
Lemma pre_hexa_rel_seq_left :
forall E X x y z,
pre_hexa E X x y ->
rel_seq (hb' E X) (po_iico E) y z ->
pre_hexa E X x z.
Proof.
intros E X x y z Hhx_xy Hseq_yz.
inversion Hhx_xy as [Htc_xy | Heq_xy].
left; apply trc_ind with y; [apply Htc_xy | apply trc_step; apply Hseq_yz].
subst; left; apply trc_step; apply Hseq_yz.
Qed.
Lemma pre_hexa_trans :
forall E X x y z,
pre_hexa E X x y ->
pre_hexa E X y z ->
pre_hexa E X x z.
Proof.
intros E X x y z Hxy Hyz.
inversion Hxy as [Htc_xy | Heq_xy];
inversion Hyz as [Htc_yz | Heq_yz].
left; apply trc_ind with y; auto.
left; subst; auto.
left; subst; auto.
right; subst; auto.
Qed.
Lemma hexa_trans :
forall E X x y z,
well_formed_event_structure E ->
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
hexa E X x z -> hexa E X z y ->
hexa E X x y.
Proof.
intros E X x y z Hwf Hvalid Hxz Hzy.
assert (trans (hb' E X)) as Htr_hb'.
unfold trans; intros e1 e2 e3 H12 H23.
eapply hb'_trans; [apply Hwf | apply Hvalid | apply H12 | apply H23].
assert (trans (po_iico E)) as Htr_po.
unfold trans; intros e1 e2 e3 H12 H23.
eapply po_trans; [apply Hwf | apply H12 | apply H23].
generalize (hx_trans Htr_hb' Htr_po); intro Htr_hx.
unfold util.trans in Htr_hx; unfold hx in Htr_hx; unfold phx in Htr_hx.
unfold hexa in * |- *.
apply (Htr_hx x z y Hxz Hzy).
Qed.
Lemma hx_hexa :
forall E X,
hexa E X = hx (hb' E X) (po_iico E).
Proof.
intros E X.
unfold hexa; unfold hx; unfold maybe_po; unfold phx;
unfold pre_hexa; unfold maybe_hb'; unfold maybe; auto.
Qed.
Lemma hb_po_implies_hexa_path : (*1*)
forall E X x y,
well_formed_event_structure E ->
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
(tc (rel_union (hb E X) (po_iico E)) x y)->
(hexa E X) x y.
Proof.
intros E X x y Hwf Hvalid Hin.
rewrite (hx_hexa E X).
eapply union_implies_hexa_path.
unfold trans; intros x1 x2 x3 H12 H23; apply hb'_trans with x2; auto.
unfold trans; intros x1 x2 x3 H12 H23; apply po_trans with x2; auto.
intros e1 e2 H12; left; left; apply H12.
exact Hin.
Qed.
Lemma ac_u :
forall E X,
well_formed_event_structure E ->
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
~(exists x, rel_union (hb E X) (po_iico E) x x).
unfold not;
intros E X Hwf Hs [x Hx].
inversion Hx as [Hhb | Hpo].
generalize (hb_ac Hs Hhb); trivial.
generalize (po_ac Hwf Hpo); trivial.
Qed.
Lemma hb'_ac :
forall E X x,
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
~(hb' E X x x).
Proof.
unfold not;
intros E X x Hs Hx.
inversion Hx as [Hpx | Hfrrf].
inversion Hpx as [Hhb | Hwsrf].
generalize Hhb; fold (~(hb E X x x)); eapply hb_ac.
auto.
destruct Hwsrf as [? [Hws Hrf]].
destruct Hs as [Hwswf [? [Hrf_cands ?]]].
generalize (ran_rf_is_read E X x0 x Hrf_cands Hrf); intros [? [? Hrx]].
generalize (dom_ws_is_write E X x x0 Hwswf Hws); intros [? [? Hwx]].
rewrite Hwx in Hrx; inversion Hrx.
destruct Hfrrf as [wx1 [Hfr Hrf1]].
destruct Hfr as [? [? [wx2 [Hrf2 Hws]]]].
destruct Hs as [Hwswf Hrfwf].
generalize (rf_uni X x wx1 wx2 Hrfwf Hrf1 Hrf2); intro Heq; subst.
destruct Hwswf as [Hws_tot Hws_cands].
generalize (ws_cy E X wx2 Hws_tot Hws_cands); intro Hc.
contradiction.
Qed.
Lemma hb_hexa :
forall E X x z,
well_formed_event_structure E ->
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
hb E X x z ->
hexa E X z x ->
exists y : Event, tc (rel_seq (hb' E X) (po_iico E)) y y.
Proof.
intros E X x z Hwf Hvalid Hhb_xz Hhx_zx.
eapply r1_hexa.
unfold not; intros [e Hhb].
generalize (hb'_ac); intro thm; unfold not in thm; apply (thm E X e Hvalid Hhb).
intros e1 e2 H12; left; left; apply H12.
unfold trans; intros; eapply hb'_trans; auto.
apply H. apply H0.
unfold trans; intros; eapply po_trans; auto.
apply H. apply H0.
apply Hhb_xz.
rewrite <- hx_hexa; auto.
Qed.
Lemma hexa_po :
forall E X x z,
well_formed_event_structure E ->
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
hexa E X x z ->
(po_iico E) z x ->
exists y : Event, tc (rel_seq (hb' E X) (po_iico E)) y y.
Proof.
intros E X x z Hwf Hvalid Hhx_xz Hpo_zx.
eapply hexa_r.
unfold not; intros [e Hpo].
generalize (po_ac); intro thm; unfold not in thm; apply (thm E e Hwf Hpo).
unfold trans; intros; eapply po_trans; auto.
apply H. apply H0.
rewrite <- hx_hexa; auto.
apply Hhx_xz.
apply Hpo_zx.
Qed.
Lemma hb_union_po_cycle_implies_hb'_seq_po_cycle : (*2*)
forall E X x,
well_formed_event_structure E ->
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
(tc (rel_union (hb E X) (po_iico E))) x x ->
(exists y, (tc (rel_seq (hb' E X) (po_iico E))) y y).
Proof.
intros E X x Hwf Hvalid Hc.
eapply union_cycle_implies_seq_cycle.
apply (ac_u Hwf Hvalid).
unfold not; intros [e Hpo].
generalize (po_ac); intro thm; unfold not in thm; apply (thm E e Hwf Hpo).
unfold not; intros [e Hhb].
generalize (hb'_ac); intro thm; unfold not in thm; apply (thm E X e Hvalid Hhb).
unfold trans; intros; eapply hb'_trans; auto.
apply H. apply H0.
unfold trans; intros; eapply po_trans; auto.
apply H. apply H0.
left; left; auto.
apply Hc.
Qed.
Lemma ppo_ac :
forall E x,
well_formed_event_structure E ->
~((ppo E) x x).
Proof.
unfold not;
intros E x Hwf Hppo.
unfold well_formed_event_structure in Hwf.
generalize (ppo_valid Hppo); intro Hpo_iico.
apply (po_ac Hwf Hpo_iico).
Qed.
Lemma ac_u_ppo :
forall E X,
well_formed_event_structure E ->
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
~(exists x, rel_union (hb E X) (ppo E) x x).
unfold not;
intros E X Hwf Hvalid [x Hx].
inversion Hx as [Hhb | Hpo].
generalize (hb_ac Hvalid Hhb); trivial.
generalize (ppo_ac Hwf Hpo); trivial.
Qed.
Lemma mhb_in_hb :
forall E X,
rel_incl (mhb E X) (hb E X).
Proof.
case_eq inter; case_eq intra; intros Hinter Hintra;
unfold mhb; rewrite Hinter; rewrite Hintra; intros E X x y Hxy.
inversion Hxy as [Hrfe | Hr].
left; left; destruct Hrfe; auto.
inversion Hr as [Hrfi | Hu].
left; left; destruct Hrfi; auto.
inversion Hu as [Hws | Hfr].
right; auto. left; right; auto.
inversion Hxy as [Hrfe | Hu].
left; left; destruct Hrfe; auto.
inversion Hu as [Hws | Hfr].
right; auto. left; right; auto.
inversion Hxy as [Hrfi | Hu].
left; left; destruct Hrfi; auto.
inversion Hu as [Hws | Hfr].
right; auto. left; right; auto.
inversion Hxy as [Hws | Hfr].
right; auto. left; right; auto.
Qed.
Lemma mhb_ac :
forall E X x,
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
~(mhb E X x x).
Proof.
unfold not;
intros E X x Hs Hx.
generalize (mhb_in_hb E X x x Hx); intro Hhb.
apply (hb_ac Hs Hhb).
Qed.
Lemma ac_mhb_u_ppo :
forall E X,
well_formed_event_structure E ->
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
~(exists x, rel_union (mhb E X) (ppo E) x x).
unfold not;
intros E X Hwf Hs [x Hx].
inversion Hx as [Hhb | Hpo].
generalize (mhb_ac X x Hs Hhb); trivial.
generalize (ppo_ac Hwf Hpo); trivial.
Qed.
Lemma mhb_seq_mhb_implies_mhb' :
forall E X x y z,
well_formed_event_structure E ->
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
mhb E X x y ->
mhb E X y z ->
mhb' E X x z.
Proof.
case_eq inter; case_eq intra; intros Hintra Hinter;
unfold mhb'; unfold mhb; unfold mrf; unfold mrfi; unfold mrfe;
rewrite Hinter; rewrite Hintra;
intros E X x y z Hwf [Hwswf Hrfwf] Hxy Hyz.
inversion Hxy as [Hrfe_xy | Hr_xy];
inversion Hyz as [Hrfe_yz | Hr_yz].
destruct_rf Hrfwf.
destruct Hrfe_xy as [Hrf_xy ?]; destruct Hrfe_yz as [Hrf_yz ?].
generalize (ran_rf_is_read E X x y Hrf_cands Hrf_xy); intros [l [v Hry]].
generalize (dom_rf_is_write E X y z Hrf_cands Hrf_yz); intros [ly [vy Hwy]].
rewrite Hwy in Hry; inversion Hry.
inversion Hr_yz as [Hrfi_yz | Hws_fr_yz].
destruct_rf Hrfwf.
destruct Hrfe_xy as [Hrf_xy ?]; destruct Hrfi_yz as [Hrf_yz ?].
generalize (ran_rf_is_read E X x y Hrf_cands Hrf_xy); intros [l [v Hry]].
generalize (dom_rf_is_write E X y z Hrf_cands Hrf_yz); intros [ly [vy Hwy]].
rewrite Hwy in Hry; inversion Hry.
inversion Hws_fr_yz as [Hws_yz | Hfr_yz].
destruct_rf Hrfwf.
destruct Hrfe_xy as [Hrf_xy ?].
generalize (ran_rf_is_read E X x y Hrf_cands Hrf_xy); intros [l [v Hry]].
generalize (dom_ws_is_write E X y z Hwswf Hws_yz); intros [ly [vy Hwy]].
rewrite Hwy in Hry; inversion Hry.
generalize (fr_ax1 Hfr_yz); intros [wr [Hrf Hws]].
destruct Hrfe_xy as [Hrf_xy ?].
generalize (rf_uni X y x wr Hrfwf Hrf_xy Hrf); intro Heq.
rewrite <- Heq in Hws; left; left; right; right; left; apply Hws.
inversion Hr_xy as [Hrfi_xy | Hws_fr_xy].
destruct_rf Hrfwf.
destruct Hrfi_xy as [Hrf_xy ?]; destruct Hrfe_yz as [Hrf_yz ?].
generalize (ran_rf_is_read E X x y Hrf_cands Hrf_xy); intros [l [v Hry]].
generalize (dom_rf_is_write E X y z Hrf_cands Hrf_yz); intros [ly [vy Hwy]].
rewrite Hwy in Hry; inversion Hry.
inversion Hws_fr_xy as [Hws_xy | Hfr_xy].
left; right; exists y; split; auto; right; auto.
right; exists y; split; auto; right; auto.
inversion Hr_xy as [Hrfi_xy | Hws_fr_xy]; inversion Hr_yz as [Hrfi_yz | Hws_fr_yz].
destruct_rf Hrfwf.
destruct Hrfi_xy as [Hrf_xy ?]; destruct Hrfi_yz as [Hrf_yz ?].
generalize (ran_rf_is_read E X x y Hrf_cands Hrf_xy); intros [l [v Hry]].
generalize (dom_rf_is_write E X y z Hrf_cands Hrf_yz); intros [ly [vy Hwy]].
rewrite Hwy in Hry; inversion Hry.
inversion Hws_fr_yz as [Hws_yz | Hfr_yz].
destruct_rf Hrfwf.
destruct Hrfi_xy as [Hrf_xy ?].
generalize (ran_rf_is_read E X x y Hrf_cands Hrf_xy); intros [l [v Hry]].
generalize (dom_ws_is_write E X y z Hwswf Hws_yz); intros [ly [vy Hwy]].
rewrite Hwy in Hry; inversion Hry.
generalize (fr_ax1 Hfr_yz); intros [wr [Hrf Hws]].
destruct Hrfi_xy as [Hrf_xy ?].
generalize (rf_uni X y x wr Hrfwf Hrf_xy Hrf); intro Heq.
rewrite <- Heq in Hws; left; left; right; right; left; apply Hws.
inversion Hws_fr_xy as [Hws_xy | Hfr_xy].
left; right; exists y; split; auto; left; auto.
right; exists y; split; auto; left; auto.
inversion Hws_fr_yz as [Hws_yz | Hfr_yz]; inversion Hws_fr_xy as [Hws_xy | Hfr_xy].
left; left; right; right; left.
apply (ws_trans E X x y z Hwswf Hws_xy Hws_yz).
destruct Hfr_xy as [? [? [wr [Hrf Hws]]]].
generalize (ws_trans E X wr y z Hwswf Hws Hws_yz); intro Hws_wrz.
left; left; right; right; right.
eapply fr_ax2; [apply Hwf | | exists wr; split; auto]; split; auto.
generalize (ran_ws_is_write E X x y Hwswf Hws_xy); intros [l [v Hwy]].
generalize (dom_fr_is_read Hrfwf Hfr_yz); intros [ly [vy Hry]].
rewrite Hwy in Hry; inversion Hry.
generalize (ran_fr_is_write Hwswf Hfr_xy); intros [l [v Hwy]].
generalize (dom_fr_is_read Hrfwf Hfr_yz); intros [ly [vy Hry]].
rewrite Hwy in Hry; inversion Hry.
inversion Hxy as [Hrfe_xy | Hr_xy];
inversion Hyz as [Hrfe_yz | Hr_yz].
destruct_rf Hrfwf.
destruct Hrfe_xy as [Hrf_xy ?]; destruct Hrfe_yz as [Hrf_yz ?].
generalize (ran_rf_is_read E X x y Hrf_cands Hrf_xy); intros [l [v Hry]].
generalize (dom_rf_is_write E X y z Hrf_cands Hrf_yz); intros [ly [vy Hwy]].
rewrite Hwy in Hry; inversion Hry.
inversion Hr_yz as [Hws_yz | Hfr_yz].
destruct_rf Hrfwf.
destruct Hrfe_xy as [Hrf_xy ?].
generalize (ran_rf_is_read E X x y Hrf_cands Hrf_xy); intros [l [v Hry]].
generalize (dom_ws_is_write E X y z Hwswf Hws_yz); intros [ly [vy Hwy]].
rewrite Hwy in Hry; inversion Hry.
generalize (fr_ax1 Hfr_yz); intros [wr [Hrf Hws]].
destruct Hrfe_xy as [Hrf_xy ?].
generalize (rf_uni X y x wr Hrfwf Hrf_xy Hrf); intro Heq.
rewrite <- Heq in Hws; left; left; right; left ; apply Hws.
inversion Hr_xy as [Hws_xy | Hfr_xy].
left; right; exists y; split; auto; right; auto.
right; exists y; split; auto; right; auto.
inversion Hr_xy as [Hws_xy | Hfr_xy]; inversion Hr_yz as [Hws_yz | Hfr_yz].
left; left; right; left.
apply (ws_trans E X x y z Hwswf Hws_xy Hws_yz).
generalize (ran_ws_is_write E X x y Hwswf Hws_xy); intros [l [v Hwy]].
generalize (dom_fr_is_read Hrfwf Hfr_yz); intros [ly [vy Hry]].
rewrite Hwy in Hry; inversion Hry.
destruct Hfr_xy as [? [? [wr [Hrf Hws]]]].
generalize (ws_trans E X wr y z Hwswf Hws Hws_yz); intro Hws_wrz.
left; left; right; right.
eapply fr_ax2; [apply Hwf | | exists wr; split; auto]; split; auto.
generalize (ran_fr_is_write Hwswf Hfr_xy); intros [l [v Hwy]].
generalize (dom_fr_is_read Hrfwf Hfr_yz); intros [ly [vy Hry]].
rewrite Hwy in Hry; inversion Hry.
inversion Hxy as [Hrfi_xy | Hr_xy];
inversion Hyz as [Hrfi_yz | Hr_yz].
destruct_rf Hrfwf.
destruct Hrfi_xy as [Hrf_xy ?]; destruct Hrfi_yz as [Hrf_yz ?].
generalize (ran_rf_is_read E X x y Hrf_cands Hrf_xy); intros [l [v Hry]].
generalize (dom_rf_is_write E X y z Hrf_cands Hrf_yz); intros [ly [vy Hwy]].
rewrite Hwy in Hry; inversion Hry.
inversion Hr_yz as [Hws_yz | Hfr_yz].
destruct_rf Hrfwf.
destruct Hrfi_xy as [Hrf_xy ?].
generalize (ran_rf_is_read E X x y Hrf_cands Hrf_xy); intros [l [v Hry]].
generalize (dom_ws_is_write E X y z Hwswf Hws_yz); intros [ly [vy Hwy]].
rewrite Hwy in Hry; inversion Hry.
generalize (fr_ax1 Hfr_yz); intros [wr [Hrf Hws]].
destruct Hrfi_xy as [Hrf_xy ?].
generalize (rf_uni X y x wr Hrfwf Hrf_xy Hrf); intro Heq.
rewrite <- Heq in Hws; left; left; right; left ; apply Hws.
inversion Hr_xy as [Hws_xy | Hfr_xy].
left; right; exists y; split; auto; left; auto.
right; exists y; split; auto; left; auto.
inversion Hr_xy as [Hws_xy | Hfr_xy]; inversion Hr_yz as [Hws_yz | Hfr_yz].
left; left; right; left.
apply (ws_trans E X x y z Hwswf Hws_xy Hws_yz).
generalize (ran_ws_is_write E X x y Hwswf Hws_xy); intros [l [v Hwy]].
generalize (dom_fr_is_read Hrfwf Hfr_yz); intros [ly [vy Hry]].
rewrite Hwy in Hry; inversion Hry.
destruct Hfr_xy as [? [? [wr [Hrf Hws]]]].
generalize (ws_trans E X wr y z Hwswf Hws Hws_yz); intro Hws_wrz.
left; left; right; right.
eapply fr_ax2; [apply Hwf | | exists wr; split; auto]; split; auto.
generalize (ran_fr_is_write Hwswf Hfr_xy); intros [l [v Hwy]].
generalize (dom_fr_is_read Hrfwf Hfr_yz); intros [ly [vy Hry]].
rewrite Hwy in Hry; inversion Hry.
inversion Hxy as [Hws_xy | Hfr_xy];
inversion Hyz as [Hws_yz | Hfr_yz].
left; left; left;
apply (ws_trans E X x y z Hwswf Hws_xy Hws_yz).
generalize (ran_ws_is_write E X x y Hwswf Hws_xy); intros [l [v Hwy]].
generalize (dom_fr_is_read Hrfwf Hfr_yz); intros [ly [vy Hry]].
rewrite Hwy in Hry; inversion Hry.
destruct Hfr_xy as [? [? [wr [Hrf Hws]]]].
generalize (ws_trans E X wr y z Hwswf Hws Hws_yz); intro Hws_wrz.
left; left; right.
eapply fr_ax2; [apply Hwf | | exists wr; split; auto]; split; auto.
generalize (ran_fr_is_write Hwswf Hfr_xy); intros [l [v Hwy]].
generalize (dom_fr_is_read Hrfwf Hfr_yz); intros [ly [vy Hry]].
rewrite Hwy in Hry; inversion Hry.
Qed.
Lemma mhb_seq_ws_rf_implies_mhb' :
forall E X x y z,
well_formed_event_structure E ->
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
mhb E X x y ->
rel_seq (ws X) (mrf X) y z ->
mhb' E X x z.
Proof.
case_eq inter; case_eq intra; intros Hintra Hinter;
unfold mhb'; unfold mhb; unfold mrf; unfold mrfi; unfold mrfe;
rewrite Hinter; rewrite Hintra;
intros E X x y z Hwf [Hwswf Hrfwf] Hxy Hyz.
inversion Hxy as [Hrfe_xy | Hr_xy]; destruct Hyz as [? [Hws Hrf]].
destruct Hrfwf as [? [Hrf_cands ?]].
destruct Hrfe_xy as [Hrf_xy ?].
generalize (ran_rf_is_read E X x y Hrf_cands Hrf_xy); intros [l [v Hry]].
generalize (dom_ws_is_write E X y x0 Hwswf Hws); intros [ly [vy Hwy]].
rewrite Hwy in Hry; inversion Hry.
inversion Hr_xy as [Hrfi_xy | Hws_fr_xy].
destruct Hrfwf as [? [Hrf_cands ?]].
destruct Hrfi_xy as [Hrf_xy ?].
generalize (ran_rf_is_read E X x y Hrf_cands Hrf_xy); intros [l [v Hry]].
generalize (dom_ws_is_write E X y x0 Hwswf Hws); intros [ly [vy Hwy]].
rewrite Hwy in Hry; inversion Hry.
inversion Hws_fr_xy as [Hws_xy | Hfr_xy].
left; right; exists x0; split; auto.
apply (ws_trans E X x y x0 Hwswf Hws_xy Hws).
right; exists x0; split; auto.
destruct Hfr_xy as [? [? [wx [Hrf_wx Hws_wxy]]]].
eapply fr_ax2;
[apply Hwf | | exists wx; split; [apply Hrf_wx | ]]. auto.
apply (ws_trans E X wx y x0 Hwswf Hws_wxy Hws).
inversion Hxy as [Hrfi_xy | Hr_xy]; destruct Hyz as [? [Hws Hrf]].
destruct Hrfwf as [? [Hrf_cands ?]].
destruct Hrfi_xy as [Hrf_xy ?].
generalize (ran_rf_is_read E X x y Hrf_cands Hrf_xy); intros [l [v Hry]].
generalize (dom_ws_is_write E X y x0 Hwswf Hws); intros [ly [vy Hwy]].
rewrite Hwy in Hry; inversion Hry.
inversion Hr_xy as [Hws_xy | Hfr_xy].
left; right; exists x0; split; auto.
apply (ws_trans E X x y x0 Hwswf Hws_xy Hws).
right; exists x0; split; auto.
destruct Hfr_xy as [? [? [wx [Hrf_wx Hws_wxy]]]].
eapply fr_ax2;
[apply Hwf | | exists wx; split; [apply Hrf_wx | ]]. auto.
apply (ws_trans E X wx y x0 Hwswf Hws_wxy Hws).
inversion Hxy as [Hrfi_xy | Hr_xy]; destruct Hyz as [? [Hws Hrf]].
destruct Hrfwf as [? [Hrf_cands ?]].
destruct Hrfi_xy as [Hrf_xy ?].
generalize (ran_rf_is_read E X x y Hrf_cands Hrf_xy); intros [l [v Hry]].
generalize (dom_ws_is_write E X y x0 Hwswf Hws); intros [ly [vy Hwy]].
rewrite Hwy in Hry; inversion Hry.
inversion Hr_xy as [Hws_xy | Hfr_xy].
left; right; exists x0; split; auto.
apply (ws_trans E X x y x0 Hwswf Hws_xy Hws).
right; exists x0; split; auto.
destruct Hfr_xy as [? [? [wx [Hrf_wx Hws_wxy]]]].
eapply fr_ax2;
[apply Hwf | | exists wx; split; [apply Hrf_wx | ]]. auto.
apply (ws_trans E X wx y x0 Hwswf Hws_wxy Hws).
inversion Hxy as [Hws_xy | Hfr_xy]; destruct Hyz as [? [Hws Hrf]].
left; right; exists x0; split; auto.
apply (ws_trans E X x y x0 Hwswf Hws_xy Hws).
right; exists x0; split; auto.
destruct Hfr_xy as [? [? [wx [Hrf_wx Hws_wxy]]]].
eapply fr_ax2;
[apply Hwf | | exists wx; split; [apply Hrf_wx | ]]. auto.
apply (ws_trans E X wx y x0 Hwswf Hws_wxy Hws).
Qed.
Lemma mhb_seq_fr_mrf_implies_mhb' :
forall E X x y z,
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
mhb E X x y ->
rel_seq (fr E X) (mrf X) y z ->
mhb' E X x z.
Proof.
case_eq inter; case_eq intra; intros Hintra Hinter;
unfold mhb'; unfold mhb; unfold mrf; unfold mrfi; unfold mrfe;
rewrite Hinter; rewrite Hintra;
intros E X x y z Hs Hxy Hyz;
generalize Hs; intros [Hwswf Hrfwf].
inversion Hxy as [Hrfe_xy | Hr_xy]; destruct Hyz as [? [Hfr Hrf]].
destruct Hfr as [? [? [wy [Hrf_y Hws_z]]]].
destruct Hrfe_xy as [Hrf_xy ?].
generalize (rf_uni X y x wy Hrfwf Hrf_xy Hrf_y); intro Heq.
rewrite <- Heq in Hws_z.
left; right; exists x0; split; auto.
inversion Hr_xy as [Hrfi_xy | Hws_fr_xy].
destruct Hfr as [? [? [wy [Hrf_y Hws_z]]]].
destruct Hrfi_xy as [Hrf_xy ?].
generalize (rf_uni X y x wy Hrfwf Hrf_xy Hrf_y); intro Heq.
rewrite <- Heq in Hws_z.
left; right; exists x0; split; auto.
inversion Hws_fr_xy as [Hws_xy | Hfr_xy].
generalize (ran_ws_is_write E X x y Hwswf Hws_xy); intros [l [v Hwy]].
generalize (dom_fr_is_read Hrfwf Hfr); intros [ly [vy Hry]].
rewrite Hwy in Hry; inversion Hry.
generalize (ran_fr_is_write Hwswf Hfr_xy); intros [l [v Hwy]].
generalize (dom_fr_is_read Hrfwf Hfr); intros [ly [vy Hry]].
rewrite Hwy in Hry; inversion Hry.
inversion Hxy as [Hrfe_xy | Hr_xy]; destruct Hyz as [? [Hfr Hrf]].
destruct Hfr as [? [? [wy [Hrf_y Hws_z]]]].
destruct Hrfe_xy as [Hrf_xy ?].
generalize (rf_uni X y x wy Hrfwf Hrf_xy Hrf_y); intro Heq.
rewrite <- Heq in Hws_z.
left; right; exists x0; split; auto.
inversion Hr_xy as [Hws_xy | Hfr_xy].
generalize (ran_ws_is_write E X x y Hwswf Hws_xy); intros [l [v Hwy]].
generalize (dom_fr_is_read Hrfwf Hfr); intros [ly [vy Hry]].
rewrite Hwy in Hry; inversion Hry.
generalize (ran_fr_is_write Hwswf Hfr_xy); intros [l [v Hwy]].
generalize (dom_fr_is_read Hrfwf Hfr); intros [ly [vy Hry]].
rewrite Hwy in Hry; inversion Hry.
inversion Hxy as [Hrfi_xy | Hr_xy]; destruct Hyz as [? [Hfr Hrf]].
destruct Hfr as [? [? [wy [Hrf_y Hws_z]]]].
destruct Hrfi_xy as [Hrf_xy ?].
generalize (rf_uni X y x wy Hrfwf Hrf_xy Hrf_y); intro Heq.
rewrite <- Heq in Hws_z.
left; right; exists x0; split; auto.
inversion Hr_xy as [Hws_xy | Hfr_xy].
generalize (ran_ws_is_write E X x y Hwswf Hws_xy); intros [l [v Hwy]].
generalize (dom_fr_is_read Hrfwf Hfr); intros [ly [vy Hry]].
rewrite Hwy in Hry; inversion Hry.
generalize (ran_fr_is_write Hwswf Hfr_xy); intros [l [v Hwy]].
generalize (dom_fr_is_read Hrfwf Hfr); intros [ly [vy Hry]].
rewrite Hwy in Hry; inversion Hry.
inversion Hxy as [Hws_xy | Hfr_xy]; destruct Hyz as [? [Hfr Hrf]].
generalize (ran_ws_is_write E X x y Hwswf Hws_xy); intros [l [v Hwy]].
generalize (dom_fr_is_read Hrfwf Hfr); intros [ly [vy Hry]].
rewrite Hwy in Hry; inversion Hry.
generalize (ran_fr_is_write Hwswf Hfr_xy); intros [l [v Hwy]].
generalize (dom_fr_is_read Hrfwf Hfr); intros [ly [vy Hry]].
rewrite Hwy in Hry; inversion Hry.
Qed.
Lemma mhb_seq_mhb'_implies_mhb' :
forall E X x y z,
well_formed_event_structure E ->
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
mhb E X x y ->
mhb' E X y z ->
mhb' E X x z.
Proof.
intros E X x y z Hwf Hvalid Hxy Hyz;
inversion Hyz as [Hmhb_wsrf | Hfrrf].
inversion Hmhb_wsrf as [Hmhb | Hwsrf].
eapply mhb_seq_mhb_implies_mhb'; [apply Hwf | apply Hvalid | apply Hxy | apply Hmhb].
eapply mhb_seq_ws_rf_implies_mhb'; [apply Hwf | apply Hvalid | apply Hxy | apply Hwsrf].
eapply mhb_seq_fr_mrf_implies_mhb'; [apply Hvalid | apply Hxy | apply Hfrrf].
Qed.
Lemma ws_mrf_seq_mhb_implies_mhb' :
forall E X x y z,
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
rel_seq (ws X) (mrf X) x y ->
mhb E X y z ->
mhb' E X x z.
Proof.
case_eq inter; case_eq intra; intros Hintra Hinter;
unfold mhb'; unfold mhb; unfold mrf; unfold mrfi; unfold mrfe;
rewrite Hinter; rewrite Hintra;
intros E X x y z Hs Hxy Hyz;
generalize Hs; intros [Hwswf Hrfwf].
inversion Hyz as [Hrfe_yz | Hu_yz]; destruct Hxy as [? [Hws Hrf]].
simpl in Hrf; inversion Hrf as [Hrfi_y | Hrfe_y].
destruct Hrfi_y as [Hrf_y ?]; destruct Hrfe_yz as [Hrf_yz ?].
destruct Hrfwf as [? [Hrf_cands ?]].
generalize (ran_rf_is_read E X x0 y Hrf_cands Hrf_y); intros [l [v Hry]].
generalize (dom_rf_is_write E X y z Hrf_cands Hrf_yz); intros [ly [vy Hwy]].
rewrite Hwy in Hry; inversion Hry.
destruct Hrfe_y as [Hrf_y ?]; destruct Hrfe_yz as [Hrf_yz ?].
destruct Hrfwf as [? [Hrf_cands ?]].
generalize (ran_rf_is_read E X x0 y Hrf_cands Hrf_y); intros [l [v Hry]].
generalize (dom_rf_is_write E X y z Hrf_cands Hrf_yz); intros [ly [vy Hwy]].
rewrite Hwy in Hry; inversion Hry.
inversion Hu_yz as [Hrfi_yz | Hws_fr_yz].
simpl in Hrf; inversion Hrf as [Hrfi_y | Hrfe_y].
destruct Hrfi_y as [Hrf_y ?]; destruct Hrfi_yz as [Hrf_yz ?].
destruct Hrfwf as [? [Hrf_cands ?]].
generalize (ran_rf_is_read E X x0 y Hrf_cands Hrf_y); intros [l [v Hry]].
generalize (dom_rf_is_write E X y z Hrf_cands Hrf_yz); intros [ly [vy Hwy]].
rewrite Hwy in Hry; inversion Hry.
destruct Hrfe_y as [Hrf_y ?]; destruct Hrfi_yz as [Hrf_yz ?].
destruct Hrfwf as [? [Hrf_cands ?]].
generalize (ran_rf_is_read E X x0 y Hrf_cands Hrf_y); intros [l [v Hry]].
generalize (dom_rf_is_write E X y z Hrf_cands Hrf_yz); intros [ly [vy Hwy]].
rewrite Hwy in Hry; inversion Hry.
inversion Hws_fr_yz as [Hws_yz | Hfr_yz].
simpl in Hrf; inversion Hrf as [Hrfi_y | Hrfe_y].
destruct Hrfi_y as [Hrf_y ?].
destruct Hrfwf as [? [Hrf_cands ?]].
generalize (ran_rf_is_read E X x0 y Hrf_cands Hrf_y); intros [l [v Hry]].
generalize (dom_ws_is_write E X y z Hwswf Hws_yz); intros [ly [vy Hwy]].
rewrite Hwy in Hry; inversion Hry.
destruct Hrfe_y as [Hrf_y ?].
destruct Hrfwf as [? [Hrf_cands ?]].
generalize (ran_rf_is_read E X x0 y Hrf_cands Hrf_y); intros [l [v Hry]].
generalize (dom_ws_is_write E X y z Hwswf Hws_yz); intros [ly [vy Hwy]].
rewrite Hwy in Hry; inversion Hry.
simpl in Hrf; inversion Hrf as [Hrfi_y | Hrfe_y];
generalize (fr_ax1 Hfr_yz); intros [wy2 [Hrf_y2 Hws_z]].
destruct Hrfi_y as [Hrf_y ?].
generalize (rf_uni X y x0 wy2 Hrfwf Hrf_y Hrf_y2); intro Heq.
rewrite <- Heq in Hws_z.
left; left; right; right; left; eapply ws_trans; [apply Hwswf | apply Hws | apply Hws_z].
destruct Hrfe_y as [Hrf_y ?].
generalize (rf_uni X y x0 wy2 Hrfwf Hrf_y Hrf_y2); intro Heq.
rewrite <- Heq in Hws_z.
left; left; right; right; left; eapply ws_trans; [apply Hwswf | apply Hws | apply Hws_z].
inversion Hyz as [Hrfe_yz | Hu_yz]; destruct Hxy as [? [Hws Hrf]].
simpl in Hrf; inversion Hrf as [Hrfi_y | Hrfe_y].
inversion Hrfi_y.
destruct Hrfe_y as [Hrf_y ?]; destruct Hrfe_yz as [Hrf_yz ?].
destruct Hrfwf as [? [Hrf_cands ?]].
generalize (ran_rf_is_read E X x0 y Hrf_cands Hrf_y); intros [l [v Hry]].
generalize (dom_rf_is_write E X y z Hrf_cands Hrf_yz); intros [ly [vy Hwy]].
rewrite Hwy in Hry; inversion Hry.
inversion Hu_yz as [Hws_yz | Hfr_yz].
simpl in Hrf; inversion Hrf as [Hrfi_y | Hrfe_y].
inversion Hrfi_y.
destruct Hrfe_y as [Hrf_y ?].
destruct Hrfwf as [? [Hrf_cands ?]].
generalize (ran_rf_is_read E X x0 y Hrf_cands Hrf_y); intros [l [v Hry]].
generalize (dom_ws_is_write E X y z Hwswf Hws_yz); intros [ly [vy Hwy]].
rewrite Hwy in Hry; inversion Hry.
simpl in Hrf; inversion Hrf as [Hrfi_y | Hrfe_y];
generalize (fr_ax1 Hfr_yz); intros [wy2 [Hrf_y2 Hws_z]].
inversion Hrfi_y.
destruct Hrfe_y as [Hrf_y ?].
generalize (rf_uni X y x0 wy2 Hrfwf Hrf_y Hrf_y2); intro Heq.
rewrite <- Heq in Hws_z.
left; left; right; left; eapply ws_trans; [apply Hwswf | apply Hws | apply Hws_z].
inversion Hyz as [Hrfi_yz | Hu_yz]; destruct Hxy as [? [Hws Hrf]].
simpl in Hrf; inversion Hrf as [Hrfi_y | Hrfe_y].
destruct Hrfi_y as [Hrf_y ?]; destruct Hrfi_yz as [Hrf_yz ?].
destruct Hrfwf as [? [Hrf_cands ?]].
generalize (ran_rf_is_read E X x0 y Hrf_cands Hrf_y); intros [l [v Hry]].
generalize (dom_rf_is_write E X y z Hrf_cands Hrf_yz); intros [ly [vy Hwy]].
rewrite Hwy in Hry; inversion Hry.
inversion Hrfe_y.
inversion Hu_yz as [Hws_yz | Hfr_yz].
simpl in Hrf; inversion Hrf as [Hrfi_y | Hrfe_y].
destruct Hrfi_y as [Hrf_y ?].
destruct Hrfwf as [? [Hrf_cands ?]].
generalize (ran_rf_is_read E X x0 y Hrf_cands Hrf_y); intros [l [v Hry]].
generalize (dom_ws_is_write E X y z Hwswf Hws_yz); intros [ly [vy Hwy]].
rewrite Hwy in Hry; inversion Hry.
inversion Hrfe_y.
simpl in Hrf; inversion Hrf as [Hrfi_y | Hrfe_y];
generalize (fr_ax1 Hfr_yz); intros [wy2 [Hrf_y2 Hws_z]].
destruct Hrfi_y as [Hrf_y ?].
generalize (rf_uni X y x0 wy2 Hrfwf Hrf_y Hrf_y2); intro Heq.
rewrite <- Heq in Hws_z.
left; left; right; left; eapply ws_trans; [apply Hwswf | apply Hws | apply Hws_z].
inversion Hrfe_y.
inversion Hyz as [Hws_yz | Hfr_yz]; destruct Hxy as [? [Hws Hrf]].
simpl in Hrf; inversion Hrf as [Hrfi_y | Hrfe_y].
inversion Hrfi_y.
inversion Hrfe_y.
simpl in Hrf; inversion Hrf as [Hrfi_y | Hrfe_y].
inversion Hrfi_y.
inversion Hrfe_y.
Qed.
Lemma ws_rf_seq_mhb'_implies_mhb' :
forall E X x y z,
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
rel_seq (ws X) (mrf X) x y ->
mhb' E X y z ->
mhb' E X x z.
Proof.
intros E X x y z Hvalid Hxy Hyz.
generalize Hvalid; intros [Hwswf Hrfwf].
inversion Hyz as [Hhb_wsrf_yz | Hfrrf_yz].
inversion Hhb_wsrf_yz as [Hhb_yz | Hwsrf_yz].
eapply ws_mrf_seq_mhb_implies_mhb'; [apply Hvalid | apply Hxy | apply Hhb_yz].
destruct Hxy as [? [Hws_x Hrf_y]].
destruct Hwsrf_yz as [? [Hws_y Hrf_z]].
destruct Hrfwf as [? [Hrf_cands ?]].
generalize (ran_mrf_is_read E Hrf_cands Hrf_y); intros [? [? Hry]].
generalize (dom_ws_is_write E X y x1 Hwswf Hws_y); intros [? [? Hwy]].
rewrite Hwy in Hry; inversion Hry.
destruct Hxy as [? [Hws_x Hrf_y]].
destruct Hfrrf_yz as [? [Hfr_y Hrf_z]].
destruct Hfr_y as [? [? [wy [Hrf_y2 Hws_z]]]].
generalize (mrf_rf_uni wy Hrfwf Hrf_y Hrf_y2); intro Heq.
rewrite <- Heq in Hws_z.
generalize (ws_trans E X x x0 x1 Hwswf Hws_x Hws_z); intro Hws_xx1.
left; right; exists x1; split; auto.
Qed.
Lemma fr_mrf_seq_mhb_implies_mhb' :
forall E X x y z,
well_formed_event_structure E ->
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
rel_seq (fr E X) (mrf X) x y ->
mhb E X y z ->
mhb' E X x z.
Proof.
case_eq inter; case_eq intra; intros Hintra Hinter;
unfold mhb'; unfold mhb; unfold mrf; unfold mrfi; unfold mrfe;
rewrite Hinter; rewrite Hintra;
intros E X x y z Hwf Hs Hxy Hyz;
generalize Hs; intros [Hwswf Hrfwf].
inversion Hyz as [Hrfe_yz | Hu_yz]; destruct Hxy as [? [Hfr Hrf]].
simpl in Hrf; inversion Hrf as [Hrfi_y | Hrfe_y]; destruct Hrfe_yz as [Hrf_yz ?].
destruct Hrfi_y as [Hrf_y ?].
destruct Hrfwf as [? [Hrf_cands ?]].
generalize (ran_rf_is_read E X x0 y Hrf_cands Hrf_y); intros [l [v Hry]].
generalize (dom_rf_is_write E X y z Hrf_cands Hrf_yz); intros [ly [vy Hwy]].
rewrite Hwy in Hry; inversion Hry.
destruct Hrfe_y as [Hrf_y ?].
destruct Hrfwf as [? [Hrf_cands ?]].
generalize (ran_rf_is_read E X x0 y Hrf_cands Hrf_y); intros [l [v Hry]].
generalize (dom_rf_is_write E X y z Hrf_cands Hrf_yz); intros [ly [vy Hwy]].
rewrite Hwy in Hry; inversion Hry.
inversion Hu_yz as [Hrfi_yz | Hws_fr_yz].
simpl in Hrf; inversion Hrf as [Hrfi_y | Hrfe_y]; destruct Hrfi_yz as [Hrf_yz ?].
destruct Hrfi_y as [Hrf_y ?].
destruct Hrfwf as [? [Hrf_cands ?]].
generalize (ran_rf_is_read E X x0 y Hrf_cands Hrf_y); intros [l [v Hry]].
generalize (dom_rf_is_write E X y z Hrf_cands Hrf_yz); intros [ly [vy Hwy]].
rewrite Hwy in Hry; inversion Hry.
destruct Hrfe_y as [Hrf_y ?].
destruct Hrfwf as [? [Hrf_cands ?]].
generalize (ran_rf_is_read E X x0 y Hrf_cands Hrf_y); intros [l [v Hry]].
generalize (dom_rf_is_write E X y z Hrf_cands Hrf_yz); intros [ly [vy Hwy]].
rewrite Hwy in Hry; inversion Hry.
inversion Hws_fr_yz as [Hws_yz | Hfr_yz].
simpl in Hrf; inversion Hrf as [Hrfi_y | Hrfe_y].
destruct Hrfi_y as [Hrf_y ?].
destruct Hrfwf as [? [Hrf_cands ?]].
generalize (ran_rf_is_read E X x0 y Hrf_cands Hrf_y); intros [l [v Hry]].
generalize (dom_ws_is_write E X y z Hwswf Hws_yz); intros [ly [vy Hwy]].
rewrite Hwy in Hry; inversion Hry.
destruct Hrfe_y as [Hrf_y ?].
destruct Hrfwf as [? [Hrf_cands ?]].
generalize (ran_rf_is_read E X x0 y Hrf_cands Hrf_y); intros [l [v Hry]].
generalize (dom_ws_is_write E X y z Hwswf Hws_yz); intros [ly [vy Hwy]].
rewrite Hwy in Hry; inversion Hry.
simpl in Hrf; inversion Hrf as [Hrfi_y | Hrfe_y].
destruct Hrfi_y as [Hrf_y ?].
destruct Hfr_yz as [? [? [wy [Hrf_yw Hws_wyz]]]].
destruct Hfr as [? [? [wx [Hrf_x Hws_wx]]]].
generalize (rf_uni X y x0 wy Hrfwf Hrf_y Hrf_yw); intro Heq.
rewrite <- Heq in Hws_wyz.
generalize (ws_trans E X wx x0 z Hwswf Hws_wx Hws_wyz); intro Hws_wxz.
left; left; right; right; right; eapply fr_ax2; [apply Hwf | | exists wx; split; [apply Hrf_x | apply Hws_wxz]].
split; auto.
destruct Hrfe_y as [Hrf_y ?].
destruct Hfr_yz as [? [? [wy [Hrf_yw Hws_wyz]]]].
destruct Hfr as [? [? [wx [Hrf_x Hws_wx]]]].
generalize (rf_uni X y x0 wy Hrfwf Hrf_y Hrf_yw); intro Heq.
rewrite <- Heq in Hws_wyz.
generalize (ws_trans E X wx x0 z Hwswf Hws_wx Hws_wyz); intro Hws_wxz.
left; left; right; right; right; eapply fr_ax2; [apply Hwf | | exists wx; split; [apply Hrf_x | apply Hws_wxz]].
split; auto.
inversion Hyz as [Hrfe_yz | Hu_yz]; destruct Hxy as [? [Hfr Hrf]].
simpl in Hrf; inversion Hrf as [Hrfi_y | Hrfe_y]; destruct Hrfe_yz as [Hrf_yz ?].
inversion Hrfi_y.
destruct Hrfe_y as [Hrf_y ?].
destruct Hrfwf as [? [Hrf_cands ?]].
generalize (ran_rf_is_read E X x0 y Hrf_cands Hrf_y); intros [l [v Hry]].
generalize (dom_rf_is_write E X y z Hrf_cands Hrf_yz); intros [ly [vy Hwy]].
rewrite Hwy in Hry; inversion Hry.
inversion Hu_yz as [Hws_yz | Hfr_yz].
simpl in Hrf; inversion Hrf as [Hrfi_y | Hrfe_y].
inversion Hrfi_y.
destruct Hrfe_y as [Hrf_y ?].
destruct Hrfwf as [? [Hrf_cands ?]].
generalize (ran_rf_is_read E X x0 y Hrf_cands Hrf_y); intros [l [v Hry]].
generalize (dom_ws_is_write E X y z Hwswf Hws_yz); intros [ly [vy Hwy]].
rewrite Hwy in Hry; inversion Hry.
simpl in Hrf; inversion Hrf as [Hrfi_y | Hrfe_y].
inversion Hrfi_y.
destruct Hrfe_y as [Hrf_y ?].
destruct Hfr_yz as [? [? [wy [Hrf_yw Hws_wyz]]]].
destruct Hfr as [? [? [wx [Hrf_x Hws_wx]]]].
generalize (rf_uni X y x0 wy Hrfwf Hrf_y Hrf_yw); intro Heq.
rewrite <- Heq in Hws_wyz.
generalize (ws_trans E X wx x0 z Hwswf Hws_wx Hws_wyz); intro Hws_wxz.
left; left; right; right; eapply fr_ax2; [apply Hwf | | exists wx; split; [apply Hrf_x | apply Hws_wxz]].
split; auto.
inversion Hyz as [Hrfi_yz | Hu_yz]; destruct Hxy as [? [Hfr Hrf]].
simpl in Hrf; inversion Hrf as [Hrfi_y | Hrfe_y]; destruct Hrfi_yz as [Hrf_yz ?].
destruct Hrfi_y as [Hrf_y ?].
destruct Hrfwf as [? [Hrf_cands ?]].
generalize (ran_rf_is_read E X x0 y Hrf_cands Hrf_y); intros [l [v Hry]].
generalize (dom_rf_is_write E X y z Hrf_cands Hrf_yz); intros [ly [vy Hwy]].
rewrite Hwy in Hry; inversion Hry.
inversion Hrfe_y.
inversion Hu_yz as [Hws_yz | Hfr_yz].
simpl in Hrf; inversion Hrf as [Hrfi_y | Hrfe_y].
destruct Hrfi_y as [Hrf_y ?].
destruct Hrfwf as [? [Hrf_cands ?]].
generalize (ran_rf_is_read E X x0 y Hrf_cands Hrf_y); intros [l [v Hry]].
generalize (dom_ws_is_write E X y z Hwswf Hws_yz); intros [ly [vy Hwy]].
rewrite Hwy in Hry; inversion Hry.
inversion Hrfe_y.
simpl in Hrf; inversion Hrf as [Hrfi_y | Hrfe_y].
destruct Hrfi_y as [Hrf_y ?].
destruct Hfr_yz as [? [? [wy [Hrf_yw Hws_wyz]]]].
destruct Hfr as [? [? [wx [Hrf_x Hws_wx]]]].
generalize (rf_uni X y x0 wy Hrfwf Hrf_y Hrf_yw); intro Heq.
rewrite <- Heq in Hws_wyz.
generalize (ws_trans E X wx x0 z Hwswf Hws_wx Hws_wyz); intro Hws_wxz.
left; left; right; right; eapply fr_ax2; [apply Hwf | | exists wx; split; [apply Hrf_x | apply Hws_wxz]].
split; auto.
inversion Hrfe_y.
inversion Hyz as [Hws_yz | Hfr_yz]; destruct Hxy as [? [Hfr Hrf]].
simpl in Hrf; inversion Hrf as [Hrfi_y | Hrfe_y].
inversion Hrfi_y.
inversion Hrfe_y.
simpl in Hrf; inversion Hrf as [Hrfi_y | Hrfe_y].
inversion Hrfi_y.
inversion Hrfe_y.
Qed.
Lemma mhb'_dec :
forall E X x y,
well_formed_event_structure E ->
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
mhb' E X x y ->
mhb E X x y \/ rel_seq (ws X) (mrf X) x y \/ rel_seq (fr E X) (mrf X) x y.
Proof.
case_eq inter; case_eq intra; intros Hintra Hinter;
unfold mhb'; unfold mrf; unfold mrfi; unfold mrfe;
rewrite Hinter; rewrite Hintra; intros E X x y Hwf Hs Hxy.
inversion Hxy as [Hu | Hfrs];
[inversion Hu as [Hmhb | Hwss];
[left; auto | right; left; auto] |
right; auto].
inversion Hxy as [Hu | Hfrs];
[inversion Hu as [Hmhb | Hwss];
[left; auto | right; left; auto] |
right; auto].
inversion Hxy as [Hu | Hfrs];
[inversion Hu as [Hmhb | Hwss];
[left; auto | right; left; auto] |
right; auto].
inversion Hxy as [Hu | Hfrs];
[inversion Hu as [Hmhb | Hwss];
[left; auto | right; left; auto] |
right; auto].
Qed.
Lemma ws_mrf_fr_mrf_implies_mhb' :
forall E X x y z,
well_formed_event_structure E ->
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
rel_seq (ws X) (mrf X) x y ->
rel_seq (fr E X) (mrf X) y z ->
mhb' E X x z.
Proof.
case_eq inter; case_eq intra; intros Hintra Hinter;
unfold mhb'; unfold mrf; unfold mrfi; unfold mrfe;
rewrite Hinter; rewrite Hintra; simpl; intros E X x y z Hwf Hs Hxy Hyz;
generalize Hs; intros [Hwswf Hrfwf];
destruct Hxy as [w1 [Hws1 Hmrf1]]; destruct Hyz as [w2 [[Hey [Hez [wy [Hrf Hws2]]]] Hmrf2]].
inversion Hmrf1 as [Hmrfi1 | Hmrfe1].
destruct Hmrfi1 as [Hrf1 ?].
generalize (rf_uni X y wy w1 Hrfwf Hrf Hrf1); intro Heq.
rewrite Heq in Hws2; generalize (ws_trans E X x w1 w2 Hwswf Hws1 Hws2); intro Hws.
left; right; exists w2; split; auto.
destruct Hmrfe1 as [Hrf1 ?].
generalize (rf_uni X y wy w1 Hrfwf Hrf Hrf1); intro Heq.
rewrite Heq in Hws2; generalize (ws_trans E X x w1 w2 Hwswf Hws1 Hws2); intro Hws.
left; right; exists w2; split; auto.
inversion Hmrf1 as [Hmrfi1 | Hmrfe1].
inversion Hmrfi1.
destruct Hmrfe1 as [Hrf1 ?].
generalize (rf_uni X y wy w1 Hrfwf Hrf Hrf1); intro Heq.
rewrite Heq in Hws2; generalize (ws_trans E X x w1 w2 Hwswf Hws1 Hws2); intro Hws.
left; right; exists w2; split; auto.
inversion Hmrf1 as [Hmrfi1 | Hmrfe1].
destruct Hmrfi1 as [Hrf1 ?].
generalize (rf_uni X y wy w1 Hrfwf Hrf Hrf1); intro Heq.
rewrite Heq in Hws2; generalize (ws_trans E X x w1 w2 Hwswf Hws1 Hws2); intro Hws.
left; right; exists w2; split; auto.
inversion Hmrfe1.
inversion Hmrf1 as [Hmrfi1 | Hmrfe1].
inversion Hmrfi1.
inversion Hmrfe1.
Qed.
Lemma fr_mrf_fr_mrf_implies_mhb' :
forall E X x y z,
well_formed_event_structure E ->
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
rel_seq (fr E X) (mrf X) x y ->
rel_seq (fr E X) (mrf X) y z ->
mhb' E X x z.
Proof.
case_eq inter; case_eq intra; intros Hintra Hinter;
unfold mhb'; unfold mrf; unfold mrfi; unfold mrfe;
rewrite Hinter; rewrite Hintra; simpl; intros E X x y z Hwf Hs Hxy Hyz;
generalize Hs; intros [Hwswf Hrfwf];
destruct Hxy as [w1 [[Hex [Hey1 [wx [Hrf1 Hws1]]]] Hmrf1]]; destruct Hyz as [w2 [[Hey2 [Hez [wy2 [Hrf2 Hws2]]]] Hmrf2]].
inversion Hmrf1 as [Hmrfi1 | Hmrfe1].
destruct Hmrfi1 as [Hrfi1 ?].
generalize (rf_uni X y wy2 w1 Hrfwf Hrf2 Hrfi1); intro Heq.
assert (fr E X x w2) as Hfr.
split; auto; split; auto.
exists wx; split; auto.
rewrite Heq in Hws2; apply (ws_trans E X wx w1 w2); auto.
right; exists w2; split; auto.
destruct Hmrfe1 as [Hrfe1 ?].
generalize (rf_uni X y wy2 w1 Hrfwf Hrf2 Hrfe1); intro Heq.
assert (fr E X x w2) as Hfr.
split; auto; split; auto.
exists wx; split; auto.
rewrite Heq in Hws2; apply (ws_trans E X wx w1 w2); auto.
right; exists w2; split; auto.
inversion Hmrf1 as [Hmrfi1 | Hmrfe1].
inversion Hmrfi1.
destruct Hmrfe1 as [Hrfe1 ?].
generalize (rf_uni X y wy2 w1 Hrfwf Hrf2 Hrfe1); intro Heq.
assert (fr E X x w2) as Hfr.
split; auto; split; auto.
exists wx; split; auto.
rewrite Heq in Hws2; apply (ws_trans E X wx w1 w2); auto.
right; exists w2; split; auto.
inversion Hmrf1 as [Hmrfi1 | Hmrfe1].
destruct Hmrfi1 as [Hrfi1 ?].
generalize (rf_uni X y wy2 w1 Hrfwf Hrf2 Hrfi1); intro Heq.
assert (fr E X x w2) as Hfr.
split; auto; split; auto.
exists wx; split; auto.
rewrite Heq in Hws2; apply (ws_trans E X wx w1 w2); auto.
right; exists w2; split; auto.
inversion Hmrfe1.
inversion Hmrf1 as [Hmrfi1 | Hmrfe1].
inversion Hmrfi1.
inversion Hmrfe1.
Qed.
Lemma mhb'_trans :
forall E X x y z,
well_formed_event_structure E ->
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
mhb' E X x y ->
mhb' E X y z ->
mhb' E X x z.
Proof.
intros E X x y z Hwf Hs Hxy Hyz;
generalize Hs; intros [Hwswf Hrfwf].
generalize (mhb'_dec Hwf Hs Hxy); intro Horxy.
generalize (mhb'_dec Hwf Hs Hyz); intro Horyz.
inversion Horxy as [Hmhbxy | Huxy]; inversion Horyz as [Hmhbyz | Huyz].
eapply mhb_seq_mhb_implies_mhb'; [apply Hwf | apply Hs | apply Hmhbxy | apply Hmhbyz].
inversion Huyz as [Hwssyz | Hfrsyz].
eapply mhb_seq_ws_rf_implies_mhb'; [apply Hwf | apply Hs | apply Hmhbxy | apply Hwssyz].
eapply mhb_seq_fr_mrf_implies_mhb'; [apply Hs | apply Hmhbxy | apply Hfrsyz].
inversion Huxy as [Hwssxy | Hfrsxy].
eapply ws_mrf_seq_mhb_implies_mhb'; [apply Hs | apply Hwssxy | apply Hmhbyz].
eapply fr_mrf_seq_mhb_implies_mhb'; [apply Hwf | apply Hs | apply Hfrsxy | apply Hmhbyz].
inversion Huxy as [Hwssxy | Hfrsxy]; inversion Huyz as [Hwssyz | Hfrsyz].
destruct Hwssxy as [? [Hws_x Hrf_y]];
destruct Hwssyz as [? [Hws_y Hrf_z]].
destruct Hrfwf as [? [Hrf_cands ?]].
generalize (ran_mrf_is_read E Hrf_cands Hrf_y); intros [l [v Hry]].
generalize (dom_ws_is_write E X y x1 Hwswf Hws_y); intros [? [? Hwy]].
rewrite Hwy in Hry; inversion Hry.
eapply ws_mrf_fr_mrf_implies_mhb'; auto.
apply Hwssxy. apply Hfrsyz.
destruct Hrfwf as [? [Hrf_cands ?]].
destruct Hfrsxy as [? [? Hmrf]]; destruct Hwssyz as [? [Hws ?]];
generalize (ran_mrf_is_read E Hrf_cands Hmrf); intros [l [v Hry]].
generalize (dom_ws_is_write E X y x1 Hwswf Hws); intros [? [? Hwy]].
rewrite Hwy in Hry; inversion Hry.
eapply fr_mrf_fr_mrf_implies_mhb'; auto.
apply Hfrsxy. apply Hfrsyz.
Qed.
Lemma mhb'_in_hb' :
forall E X,
rel_incl (mhb' E X) (hb' E X).
Proof.
case_eq inter; case_eq intra; intros Hinter Hintra; unfold mhb';
unfold mrf; unfold mhb; unfold mrfi; unfold mrfe;
rewrite Hinter; rewrite Hintra; intros E X x y Hxy.
inversion Hxy as [Hr | Hs].
inversion Hr as [Hre | Hu].
inversion Hre as [Hrfe | Hres].
left; left; left; left; destruct Hrfe; auto.
inversion Hres as [Hrfi | Hu].
left; left; left; left; destruct Hrfi; auto.
inversion Hu as [Hws | Hfr].
left; left; right; auto. left; left; left; right; auto.
simpl in Hu; destruct Hu as [z [Hxz Hzy]]; inversion Hzy as [Hrfi | Hrfe];
left; right; exists z; split; auto. destruct Hrfi; auto. destruct Hrfe; auto.
simpl in Hs; destruct Hs as [z [Hxz Hzy]]; inversion Hzy as [Hrfi | Hrfe];
right; exists z; split; auto. destruct Hrfi; auto. destruct Hrfe; auto.
inversion Hxy as [Hr | Hs].
inversion Hr as [Hre | Hu].
inversion Hre as [Hrfe | Hres].
left; left; left; left; destruct Hrfe; auto.
inversion Hres as [Hws | Hfr].
left; left; right; auto. left; left; left; right; auto.
simpl in Hu; destruct Hu as [z [Hxz Hzy]]; inversion Hzy as [Hrfi | Hrfe];
left; right; exists z; split; auto. inversion Hrfi. destruct Hrfe; auto.
simpl in Hs; destruct Hs as [z [Hxz Hzy]]; inversion Hzy as [Hrfi | Hrfe];
right; exists z; split; auto. inversion Hrfi; auto. destruct Hrfe; auto.
inversion Hxy as [Hr | Hs].
inversion Hr as [Hre | Hu].
inversion Hre as [Hrfe | Hres].
left; left; left; left; destruct Hrfe; auto.
inversion Hres as [Hws | Hfr].
left; left; right; auto. left; left; left; right; auto.
simpl in Hu; destruct Hu as [z [Hxz Hzy]]; inversion Hzy as [Hrfi | Hrfe];
left; right; exists z; split; auto. destruct Hrfi; auto. inversion Hrfe.
simpl in Hs; destruct Hs as [z [Hxz Hzy]]; inversion Hzy as [Hrfi | Hrfe];
right; exists z; split; auto. destruct Hrfi; auto. inversion Hrfe.
inversion Hxy as [Hr | Hs].
inversion Hr as [Hre | Hu].
inversion Hre as [Hws | Hfr].
left; left; right; auto. left; left; left; right; auto.
simpl in Hu; destruct Hu as [z [Hxz Hzy]]; inversion Hzy as [Hrfi | Hrfe];
left; right; exists z; split; auto. inversion Hrfi. inversion Hrfe.
simpl in Hs; destruct Hs as [z [Hxz Hzy]]; inversion Hzy as [Hrfi | Hrfe];
right; exists z; split; auto. inversion Hrfi. inversion Hrfe.
Qed.
Lemma mhb'_ac :
forall E X x,
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
~(mhb' E X x x).
Proof.
unfold not;
intros E X x Hvalid Hx.
generalize (mhb'_in_hb' Hx); intro Hhb.
apply (hb'_ac Hvalid Hhb).
Qed.
Lemma ac_mhb'_u_ppo :
forall E X,
well_formed_event_structure E ->
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
~(exists x, rel_union (mhb' E X) (ppo E) x x).
unfold not;
intros E X Hwf Hs [x Hx].
inversion Hx as [Hhb | Hpo].
generalize (mhb'_ac Hs Hhb); trivial.
generalize (ppo_ac Hwf Hpo); trivial.
Qed.
Lemma mhb_union_ppo_cycle_implies_mhb'_seq_ppo_cycle2 : (*2*)
forall E X x,
well_formed_event_structure E ->
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
(tc (rel_union (mhb E X) (ppo E))) x x ->
(exists y, (tc (rel_seq (maybe (mhb' E X)) (tc (ppo E)))) y y).
Proof.
intros E X x Hwf Hvalid Hc.
eapply union_cycle_implies_seq_cycle'.
apply (ac_mhb_u_ppo X Hwf Hvalid).
unfold not; intros [e Hppo].
generalize (ppo_ac); intro thm; unfold not in thm; apply (thm E e Hwf Hppo).
unfold not; intros [e Hmhb].
generalize (mhb'_ac); intro thm; unfold not in thm; apply (thm E X e Hvalid Hmhb).
unfold trans; intros; eapply mhb'_trans; auto.
apply H. apply H0.
left; left; auto.
apply Hc.
Qed.
Lemma mhb_union_ppo_sub_cycle_implies_mhb'_seq_ppo_sub_cycle : (*2*)
forall E X x, forall r,
trans r ->
~(exists x, rel_union (mhb E X) r x x) ->
~(exists x, r x x) ->
well_formed_event_structure E ->
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
(tc (rel_union (mhb E X) r)) x x ->
(exists y, (tc (rel_seq (mhb' E X) r)) y y).
Proof.
intros E X x r Htr Hacu Hacr Hwf Hvalid Hc.
eapply union_cycle_implies_seq_cycle.
apply Hacu.
unfold not; intros [e Hppo].
apply Hacr; exists e; auto.
unfold not; intros [e Hmhb].
generalize (mhb'_ac); intro thm; unfold not in thm; apply (thm E X e Hvalid Hmhb).
unfold trans; intros; eapply mhb'_trans; auto.
apply H. apply H0.
apply Htr; auto.
left; left; auto.
apply Hc.
Qed.
Definition po_tso (E:Event_struct) : Rln Event :=
fun e1 => fun e2 => (po_iico E) e1 e2 /\
(reads E e1 \/ (writes E e1 /\ writes E e2)).
Definition hb_tso (E:Event_struct) (X:Execution_witness) : Rln Event :=
rel_union (rel_union (ws X) (fr E X)) (rf_inter X).
Definition hb'_tso (E:Event_struct) (X:Execution_witness) : Rln Event :=
rel_union (rel_union (hb_tso E X) (rel_seq (ws X) (rf_inter X)))
(rel_seq (fr E X) (rf_inter X)).
Lemma hb_tso_in_hb :
forall E X x y,
well_formed_event_structure E ->
hb_tso E X x y ->
hb E X x y.
Proof.
intros E X x y Hwf Hxy.
inversion Hxy as [Hws_fr | Hrf].
inversion Hws_fr as [Hws | Hfr].
right; auto.
left; right; auto.
destruct Hrf; left; left; auto.
Qed.
Lemma po_hb_tso_in_po_hb :
forall E X,
well_formed_event_structure E ->
Included _ (udr (rel_union (po_tso E) (hb_tso E X)))
(udr (rel_union (po_iico E) (hb E X))).
Proof.
intros E X Hwf x Hx.
inversion Hx as [e Hd | e Hr].
destruct Hd as [y Hord]; unfold udr; apply incl_union_left_in; exists y.
inversion Hord as [Hpo | Hhb].
left; destruct Hpo; auto.
right; apply (hb_tso_in_hb Hwf Hhb).
destruct Hr as [y Horr]; unfold udr; apply incl_union_right_in; exists y.
inversion Horr as [Hpo | Hhb].
left; destruct Hpo; auto.
right; apply (hb_tso_in_hb Hwf Hhb).
Qed.
Lemma hb'_tso_in_hb' :
forall E X x y,
well_formed_event_structure E ->
hb'_tso E X x y ->
hb' E X x y.
Proof.
intros E X x y Hwf Hxy.
inversion Hxy as [Hhb_wsrf | Hrf_fr].
inversion Hhb_wsrf as [Hhb | Hws_rf].
left; left; apply hb_tso_in_hb; auto.
left; right; destruct Hws_rf as [z [Hws Hrf]]; exists z; split;
destruct Hrf; auto.
right; destruct Hrf_fr as [z [Hfr Hrf]]; exists z; split;
destruct Hrf; auto.
Qed.
Lemma hb_tso_in_hb'_tso :
forall E X x y,
well_formed_event_structure E ->
hb_tso E X x y ->
hb'_tso E X x y.
Proof.
intros E X x y Hwf Hxy.
inversion Hxy as [Hws_fr | Hrf].
inversion Hws_fr as [Hws | Hfr].
left; left; auto.
left; left; auto.
destruct Hrf; left; left; auto.
Qed.
Lemma po_tso_trans :
forall E x y z,
well_formed_event_structure E ->
(po_tso E) x y ->
(po_tso E) y z ->
(po_tso E) x z.
Proof.
unfold po_tso;
intros E x y z Hwf [Hxy Horx] [Hyz Hory].
inversion Hxy as [Hpo_xy | Hiico_xy];
inversion Hyz as [Hpo_yz | Hiico_yz].
split; auto. left; eapply pos_trans; eauto.
inversion Horx; auto.
inversion Hory; destruct H as [Hwx Hwy].
destruct Hwy as [? [ly [vy Hwy]]];
destruct H0 as [? [l [v Hry]]]; rewrite Hry in Hwy; inversion Hwy.
right; destruct H0; auto.
split. left; eapply po_iico_trans; eauto.
inversion Horx; auto.
inversion Hory; destruct H as [Hwx Hwy].
destruct Hwy as [? [ly [vy Hwy]]];
destruct H0 as [? [l [v Hry]]]; rewrite Hry in Hwy; inversion Hwy.
right; destruct H0; auto.
split. left; eapply iico_po_trans; eauto.
inversion Horx; auto.
inversion Hory; destruct H as [Hwx Hwy].
destruct Hwy as [? [ly [vy Hwy]]];
destruct H0 as [? [l [v Hry]]]; rewrite Hry in Hwy; inversion Hwy.
right; destruct H0; auto.
split. right; eapply iico_trans; eauto.
inversion Horx; auto.
inversion Hory; destruct H as [Hwx Hwy].
destruct Hwy as [? [ly [vy Hwy]]];
destruct H0 as [? [l [v Hry]]]; rewrite Hry in Hwy; inversion Hwy.
right; destruct H0; auto.
Qed.
Lemma ac_u_tso :
forall E X,
well_formed_event_structure E ->
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
~(exists x, rel_union (hb_tso E X) (po_tso E) x x).
unfold not;
intros E X Hwf Hvalid [x Hx].
inversion Hx as [Hhb | Hpo].
assert (hb E X x x) as Hin.
apply hb_tso_in_hb; auto.
generalize (hb_ac Hvalid Hin); trivial.
destruct Hpo as [Hpo ?].
generalize (po_ac Hwf Hpo); trivial.
Qed.
Lemma hb_tso_seq_hb_tso_implies_hb'_tso :
forall E X x y z,
well_formed_event_structure E ->
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
hb_tso E X x y ->
hb_tso E X y z ->
hb'_tso E X x z.
Proof.
intros E X x y z Hwf [Hwswf Hrfwf] Hxy Hyz.
inversion Hxy as [Hws_fr_xy | Hrf_xy];
inversion Hyz as [Hws_fr_yz | Hrf_yz].
inversion Hws_fr_xy as [Hws_xy | Hfr_xy];
inversion Hws_fr_yz as [Hws_yz | Hfr_yz].
left; left; left; left;
apply (ws_trans E X x y z Hwswf Hws_xy Hws_yz).
left; right; exists y; split; auto.
generalize (ran_ws_is_write E X x y Hwswf Hws_xy); intros [l [v Hwy]].
generalize (dom_fr_is_read Hrfwf Hfr_yz); intros [ly [vy Hry]].
rewrite Hwy in Hry; inversion Hry.
destruct Hfr_xy as [? [? [wr [Hrf Hws]]]].
generalize (ws_trans E X wr y z Hwswf Hws Hws_yz); intro Hws_wrz.
left; left; left; right.
eapply fr_ax2; [apply Hwf | | exists wr; split; auto]; split; auto.
generalize (ran_fr_is_write Hwswf Hfr_xy); intros [l [v Hwy]].
generalize (dom_fr_is_read Hrfwf Hfr_yz); intros [ly [vy Hry]].
rewrite Hwy in Hry; inversion Hry.
inversion Hws_fr_xy as [Hws_xy | Hfr_xy].
left; right; exists y; split; auto.
right; exists y; auto.
inversion Hws_fr_yz as [Hws_yz | Hfr_yz].
destruct Hrf_xy as [Hrf_xy ?].
destruct Hrfwf as [? [Hrf_cands ?]].
generalize (ran_rf_is_read E X x y Hrf_cands Hrf_xy); intros [l [v Hry]].
generalize (dom_ws_is_write E X y z Hwswf Hws_yz); intros [ly [vy Hwy]].
rewrite Hwy in Hry; inversion Hry.
generalize (fr_ax1 Hfr_yz); intros [wr [Hrf Hws]].
destruct Hrf_xy as [Hrf_xy ?].
generalize (rf_uni X y x wr Hrfwf Hrf_xy Hrf); intro Heq.
rewrite <- Heq in Hws; left; left; left; left; apply Hws.
destruct Hrf_xy as [Hrf_xy ?].
destruct Hrf_yz as [Hrf_yz ?].
destruct Hrfwf as [? [Hrf_cands ?]].
generalize (ran_rf_is_read E X x y Hrf_cands Hrf_xy); intros [l [v Hry]].
generalize (dom_rf_is_write E X y z Hrf_cands Hrf_yz); intros [ly [vy Hwy]].
rewrite Hwy in Hry; inversion Hry.
Qed.
Lemma hb_tso_seq_ws_rf_implies_hb'_tso :
forall E X x y z,
well_formed_event_structure E ->
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
hb_tso E X x y ->
rel_seq (ws X) (rf_inter X) y z ->
hb'_tso E X x z.
Proof.
intros E X x y z Hwf [Hwswf Hrfwf] Hxy Hyz.
inversion Hxy as [Hws_fr_xy | Hrf_xy].
inversion Hws_fr_xy as [Hws_xy | Hfr_xy].
destruct Hyz as [wz [Hws_ywz Hrfwz]].
generalize (ws_trans E X x y wz Hwswf Hws_xy Hws_ywz); intro Hws_xwz.
left; right; exists wz; split; auto.
destruct Hyz as [wz [Hws_ywz Hrfwz]].
destruct Hfr_xy as [? [? [wx [Hrf_wx Hws_wxy]]]].
generalize (ws_trans E X wx y wz Hwswf Hws_wxy Hws_ywz); intro Hws_wxwz.
right; exists wz; split; [|apply Hrfwz].
eapply fr_ax2;
[apply Hwf | | exists wx; split; [apply Hrf_wx | apply Hws_wxwz]]; split; auto.
destruct Hyz as [wz [Hws_ywz Hrfwz]].
destruct Hrf_xy as [Hrf_xy ?].
destruct Hrfwf as [? [Hrf_cands ?]].
generalize (ran_rf_is_read E X x y Hrf_cands Hrf_xy); intros [l [v Hry]].
generalize (dom_ws_is_write E X y wz Hwswf Hws_ywz); intros [ly [vy Hwy]].
rewrite Hwy in Hry; inversion Hry.
Qed.
Lemma ws_rf_seq_hb_tso_implies_hb'_tso :
forall E X x y z,
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
rel_seq (ws X) (rf_inter X) x y ->
hb_tso E X y z ->
hb'_tso E X x z.
Proof.
intros E X x y z [Hwswf Hrfwf] Hxy Hyz.
inversion Hyz as [Hws_fr_yz | Hrf_yz].
inversion Hws_fr_yz as [Hws_yz | Hfr_yz].
destruct Hxy as [? [Hws Hrf]].
destruct Hrf as [Hrf ?].
destruct Hrfwf as [? [Hrf_cands ?]].
generalize (ran_rf_is_read E X x0 y Hrf_cands Hrf); intros [l [v Hry]].
generalize (dom_ws_is_write E X y z Hwswf Hws_yz); intros [ly [vy Hwy]].
rewrite Hwy in Hry; inversion Hry.
destruct Hxy as [wy1 [Hws_xwy1 Hrf_wy1]].
generalize (fr_ax1 Hfr_yz); intros [wy2 [Hrf_y2 Hws_z]].
destruct Hrf_wy1 as [Hrf_wy1 ?].
generalize (rf_uni X y wy1 wy2 Hrfwf Hrf_wy1 Hrf_y2); intro Heq.
rewrite <- Heq in Hws_z.
left; left; left; left; eapply ws_trans; [ apply Hwswf | apply Hws_xwy1 | apply Hws_z].
destruct Hxy as [? [Hws Hrf]].
destruct Hrf as [Hrf ?].
destruct Hrfwf as [? [Hrf_cands ?]].
generalize (ran_rf_is_read E X x0 y Hrf_cands Hrf); intros [l [v Hry]].
destruct Hrf_yz as [Hfr_yz ?].
generalize (dom_rf_is_write E X y z Hrf_cands Hfr_yz); intros [ly [vy Hwy]].
rewrite Hwy in Hry; inversion Hry.
Qed.
Lemma hb_tso_seq_fr_rf_implies_hb'_tso :
forall E X x y z,
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
hb_tso E X x y ->
rel_seq (fr E X) (rf_inter X) y z ->
hb'_tso E X x z.
Proof.
intros E X x y z [Hwswf Hrfwf] Hxy Hyz.
inversion Hxy as [Hws_fr_xy | Hrf_xy].
inversion Hws_fr_xy as [Hws_xy | Hfr_xy].
destruct Hyz as [? [Hfr Hrf]].
generalize (ran_ws_is_write E X x y Hwswf Hws_xy); intros [l [v Hwy]].
generalize (dom_fr_is_read Hrfwf Hfr); intros [ly [vy Hry]].
rewrite Hwy in Hry; inversion Hry.
destruct Hyz as [? [Hfr Hrf]].
generalize (ran_fr_is_write Hwswf Hfr_xy); intros [l [v Hwy]].
generalize (dom_fr_is_read Hrfwf Hfr); intros [ly [vy Hry]].
rewrite Hwy in Hry; inversion Hry.
destruct Hyz as [wz [Hfr Hrf]].
destruct Hfr as [? [? [wy [Hrf_y Hws_z]]]].
destruct Hrf_xy as [Hrf_xy ?].
generalize (rf_uni X y x wy Hrfwf Hrf_xy Hrf_y); intro Heq.
rewrite <- Heq in Hws_z.
left; right; exists wz; split; auto.
Qed.
Lemma fr_rf_seq_hb_tso_implies_hb'_tso :
forall E X x y z,
well_formed_event_structure E ->
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
rel_seq (fr E X) (rf X) x y ->
hb_tso E X y z ->
hb'_tso E X x z.
Proof.
intros E X x y z Hwf [Hwswf Hrfwf] Hxy Hyz.
inversion Hyz as [Hws_fr_yz | Hrf_yz].
inversion Hws_fr_yz as [Hws_yz | Hfr_yz].
destruct Hxy as [? [Hfr Hrf]].
destruct Hrfwf as [? [Hrf_cands ?]].
generalize (ran_rf_is_read E X x0 y Hrf_cands Hrf); intros [l [v Hry]].
generalize (dom_ws_is_write E X y z Hwswf Hws_yz); intros [ly [vy Hwy]].
rewrite Hwy in Hry; inversion Hry.
destruct Hxy as [? [Hfr Hrf]].
destruct Hfr as [? [? [wx [Hrf_x Hws_wx]]]].
destruct Hfr_yz as [? [? [wy [Hrf_y Hws_wyz]]]].
generalize (rf_uni X y x0 wy Hrfwf Hrf Hrf_y); intro Heq.
rewrite <- Heq in Hws_wyz.
generalize (ws_trans E X wx x0 z Hwswf Hws_wx Hws_wyz); intro Hws_wxz.
left; left; left; right; eapply fr_ax2; [apply Hwf | | exists wx; split; [apply Hrf_x | apply Hws_wxz]]; split; auto.
destruct Hxy as [? [Hfr Hrf]].
destruct Hrfwf as [? [Hrf_cands ?]].
generalize (ran_rf_is_read E X x0 y Hrf_cands Hrf); intros [l [v Hry]].
destruct Hrf_yz as [Hrf_yz ?].
generalize (dom_rf_is_write E X y z Hrf_cands Hrf_yz); intros [ly [vy Hwy]].
rewrite Hwy in Hry; inversion Hry.
Qed.
Lemma hb'_tso_trans :
forall E X x y z,
well_formed_event_structure E ->
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
hb'_tso E X x y ->
hb'_tso E X y z ->
hb'_tso E X x z.
Proof.
intros E X x y z Hwf Hvalid Hxy Hyz.
inversion Hxy as [Hpxy | Hfrrf_xy];
inversion Hyz as [Hpyz | Hfrrf_yz].
inversion Hpxy as [Hhb_xy | Hwsfr_xy];
inversion Hpyz as [Hhb_yz | Hwsfr_yz].
eapply hb_tso_seq_hb_tso_implies_hb'_tso; [apply Hwf | apply Hvalid | apply Hhb_xy | apply Hhb_yz].
eapply hb_tso_seq_ws_rf_implies_hb'_tso; [apply Hwf | apply Hvalid | apply Hhb_xy | apply Hwsfr_yz ].
eapply ws_rf_seq_hb_tso_implies_hb'_tso; [apply Hvalid | apply Hwsfr_xy | apply Hhb_yz].
destruct Hwsfr_xy as [? [Hws_x Hrf_y]];
destruct Hwsfr_yz as [? [Hws_y Hrf_z]].
destruct Hrf_y as [Hrf_y ?].
destruct Hvalid as [Hwswf [? [Hrf_cands ?]]].
generalize (ran_rf_is_read E X x0 y Hrf_cands Hrf_y); intros [l [v Hry]].
generalize (dom_ws_is_write E X y x1 Hwswf Hws_y); intros [? [? Hwy]].
rewrite Hwy in Hry; inversion Hry.
inversion Hpxy as [Hhb_xy | Hwsfr_xy].
eapply hb_tso_seq_fr_rf_implies_hb'_tso; [apply Hvalid | apply Hhb_xy | apply Hfrrf_yz].
destruct Hfrrf_yz as [wz [Hfr_y Hrf_z]];
destruct Hwsfr_xy as [wy1 [Hws_x Hrf_y1]].
destruct Hfr_y as [? [? [wy2 [Hrf_y2 Hws_wz]]]].
destruct Hrf_y1 as [Hrf_y1 ?].
destruct Hvalid as [Hwswf Hrfwf].
generalize (rf_uni X y wy1 wy2 Hrfwf Hrf_y1 Hrf_y2); intro Heq.
rewrite <- Heq in Hws_wz.
generalize (ws_trans E X x wy1 wz Hwswf Hws_x Hws_wz); intro Hws_xwz.
left; right; exists wz; split; auto.
inversion Hpyz as [Hhb_yz | Hwsfr_yz].
eapply fr_rf_seq_hb_tso_implies_hb'_tso; [apply Hwf | apply Hvalid | (*apply Hfrrf_xy*) | apply Hhb_yz].
destruct Hfrrf_xy as [e [Hfr [Hrf ?]]]; exists e; split; auto.
destruct Hfrrf_xy as [? [Hfr_x Hrf_y]].
destruct Hwsfr_yz as [? [Hws_y Hrf_z]].
destruct Hrf_y as [Hrf_y ?].
destruct Hvalid as [Hwswf [? [Hrf_cands ?]]].
generalize (ran_rf_is_read E X x0 y Hrf_cands Hrf_y); intros [l [v Hry]].
generalize (dom_ws_is_write E X y x1 Hwswf Hws_y); intros [? [? Hwy]].
rewrite Hwy in Hry; inversion Hry.
destruct Hfrrf_xy as [wy1 [Hfr_x Hrf_y]];
destruct Hfrrf_yz as [wz [Hfr_y Hrf_z]].
destruct Hfr_y as [? [? [wy2 [Hrf_y2 Hws_wz]]]].
destruct Hfr_x as [? [? [wx [Hrf_x Hws_x]]]].
destruct Hrf_y as [Hrf_y ?].
generalize Hvalid; intros [Hwswf Hrfwf].
generalize (rf_uni X y wy1 wy2 Hrfwf Hrf_y Hrf_y2); intro Heq.
rewrite <- Heq in Hws_wz.
generalize (ws_trans E X wx wy1 wz Hwswf Hws_x Hws_wz); intro Hws_wxwz.
assert (exists wr : Event, rf X wr x /\ ws X wr wz) as Hfrax_xwz.
exists wx; split; auto.
generalize (fr_ax2 X x wz Hwf Hvalid Hfrax_xwz); intro Hfr_xwz.
right; exists wz; split; auto.
Qed.
Lemma hb_tso_union_po_tso_cycle_implies_hb'_tso_seq_po_tso_cycle :
forall E X x,
well_formed_event_structure E ->
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
(tc (rel_union (hb_tso E X) (po_tso E))) x x ->
(exists y, (tc (rel_seq (hb'_tso E X) (po_tso E))) y y).
Proof.
intros E X x Hwf Hvalid Hc.
eapply union_cycle_implies_seq_cycle.
apply (ac_u_tso Hwf Hvalid).
unfold not; intros [e Hpo].
generalize (po_ac); intro thm; unfold not in thm; apply (thm E e Hwf).
destruct Hpo; auto.
unfold not; intros [e Hhb].
generalize (hb'_ac); intro thm; unfold not in thm; apply (thm E X e Hvalid).
apply hb'_tso_in_hb'; auto.
unfold trans; intros; eapply hb'_tso_trans; auto.
apply H. apply H0.
unfold trans; intros; eapply po_tso_trans; auto.
apply H. apply H0.
left; left. apply H.
apply Hc.
Qed.
Lemma hb'_dom_in_evts :
forall E X x y,
well_formed_event_structure E ->
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
(hb' E X) x y ->
In _ (events E) x.
Proof.
intros E X x y Hwf Hvalid Hhb'.
inversion Hhb' as [Hhb_wsrf | Hfrrf].
inversion Hhb_wsrf as [Hhb | Hwsrf].
eapply hb_dom_in_evts; [apply Hwf | apply Hvalid | apply Hhb].
destruct Hwsrf as [? [Hws ?]].
destruct Hvalid as [Hwswf Hrfwf];
eapply dom_ws_in_events; [apply Hwf | apply Hwswf | apply Hws].
destruct Hfrrf as [? [Hfr ?]].
eapply dom_fr_in_events; [apply Hwf | apply Hfr].
Qed.
Lemma hb'_ran_in_evts :
forall E X x y,
well_formed_event_structure E ->
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
(hb' E X) x y ->
In _ (events E) y.
Proof.
intros E X x y Hwf Hvalid Hhb'.
inversion Hhb' as [Hhb_wsrf | Hfrrf].
inversion Hhb_wsrf as [Hhb | Hwsrf].
eapply hb_ran_in_evts; [apply Hwf | apply Hvalid | apply Hhb].
destruct Hwsrf as [? [Hws Hrf]].
destruct Hvalid as [Hwswf Hrfwf];
eapply ran_rf_in_events; [apply Hwf | apply Hrfwf | apply Hrf].
destruct Hfrrf as [? [Hfr Hrf]].
destruct Hvalid as [Hwswf Hrfwf];
eapply ran_rf_in_events; [apply Hwf | apply Hrfwf | apply Hrf].
Qed.
Lemma ws_u_fr_seq_ab_path_implies_ghb_path :
forall E X x y,
well_formed_event_structure E ->
valid_execution E X ->
tc (rel_union (rel_seq (rel_union (ws X) (fr E X)) (abc E X)) (abc E X)) x y ->
tc (ghb E X) x y.
Proof.
intros E X x y Hwf Hvalid Hxy.
induction Hxy.
inversion H as [Hwsfr_ab | Hab_xy].
destruct Hwsfr_ab as [z [Hws_u_fr_xz Hab_zy]].
apply trc_ind with z; apply trc_step.
apply (ws_u_fr_in_ghb Hvalid Hws_u_fr_xz).
apply (ab_in_ghb Hab_zy).
apply trc_step; apply (ab_in_ghb Hab_xy).
apply trc_ind with z; auto.
Qed.
End Hexa.
Section Obs.
Lemma in_rr_or :
forall E X l x e,
(rrestrict (ws X) (writes_to_same_loc_l (events E) l)) x e \/
(rrestrict (ws X) (writes_to_same_loc_l (events E) l)) e x ->
x <> e ->
ws X x e \/ ws X e x.
Proof.
intros E X l x e Hor Hdiff.
inversion Hor as [Hxe | Hex].
left; destruct Hxe as [Hws Hrest]; apply Hws.
right; destruct Hex as [Hws Hrest]; apply Hws.
Qed.
Lemma ws_tot :
forall E X l x e,
linear_strict_order
(rrestrict (ws X) (writes_to_same_loc_l (events E) l))
(writes_to_same_loc_l (events E) l) ->
In _ (writes_to_same_loc_l (events E) l) x /\
In _ (writes_to_same_loc_l (events E) l) e ->
x <> e ->
ws X x e \/ ws X e x.
Proof.
intros E X l x e Hlin Hin Hdiff; destruct Hlin as [Hdr [Htrans [Hac Htot]]];
destruct Hin as [Hx He].
apply (in_rr_or E X (Htot x e Hdiff Hx He) Hdiff).
Qed.
End Obs.
Lemma topo_ordering_correct :
forall r S,
Included _ (Union Event (dom r) (ran r)) S ->
acyclic r ->
(exists so,
linear_strict_order so S /\
rel_incl r so).
Proof.
intros r S Hincl Hac; unfold acyclic in Hac.
exists (LE (tc r)).
assert (partial_order (tc r) (Union _ (dom r) (ran r))) as Hpart.
split.
rewrite (dom_ran_tc r); intro x; trivial.
split; auto.
intros x1 x2 x3 [H12 H23]; apply trc_ind with x2; auto.
generalize (OE Hincl Hpart); intros [? ?]; split; auto.
apply (rel_incl_trans) with (tc r).
intros x y Hxy; apply trc_step; apply Hxy.
apply H.
Qed.
Lemma udr_r_in_udr_le :
forall r x,
rel_incl r (LE r) ->
In _ (Union _ (dom r) (ran r)) x ->
In _ (Union _ (dom (LE r)) (ran (LE r))) x.
Proof.
intros r x Hincl Hin; inversion Hin as [e Hd | e Hr]; [left | right].
destruct Hd as [y Hd]; exists y; apply Hincl; auto.
destruct Hr as [y Hr]; exists y; apply Hincl; auto.
Qed.
Lemma hb_implies_same_loc :
forall E X e1 e2,
well_formed_event_structure E ->
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
hb E X e1 e2 -> loc e1 = loc e2.
Proof.
intros E X e1 e2 Hwf [Hwfws Hwfrf] Hhb;
inversion Hhb as [Hrffr | Hws].
inversion Hrffr as [Hrf | Hfr].
eapply rf_implies_same_loc2; [split; [apply Hwfws | apply Hwfrf] | apply Hrf].
eapply fr_implies_same_loc; [split; [apply Hwfws | apply Hwfrf] | apply Hfr].
eapply ws_implies_same_loc; [split; [apply Hwfws | apply Hwfrf] | apply Hws].
Qed.
Lemma hb'_implies_same_loc :
forall E X e1 e2,
well_formed_event_structure E ->
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
hb' E X e1 e2 -> loc e1 = loc e2.
Proof.
intros E X e1 e2 Hwf Hs Hhb';
inversion Hhb' as [Hu | Hfrrf].
inversion Hu as [Hhb | Hwsrf].
apply hb_implies_same_loc with E X; auto.
destruct Hwsrf as [e [Hws Hrf]].
rewrite (ws_implies_same_loc X e1 e Hs Hws).
apply rf_implies_same_loc2 with E X; auto.
destruct Hfrrf as [e [Hfr Hrf]].
rewrite (fr_implies_same_loc Hs Hfr).
apply rf_implies_same_loc2 with E X; auto.
Qed.
Lemma hb_implies_writes :
forall E X e1 e2,
well_formed_event_structure E ->
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
hb E X e1 e2 -> writes E e1 \/ writes E e2.
Proof.
intros E X e1 e2 Hwf [Hwswf Hrfwf] Hhb.
inversion Hhb as [Hrffr | Hws].
inversion Hrffr as [Hrf | Hfr].
generalize Hrfwf; intro Hbis.
destruct Hrfwf as [? [Hrf_cands ?]].
left; unfold writes; split; [
eapply dom_rf_in_events; auto; [apply Hbis| apply Hrf] |
eapply dom_rf_is_write; [apply Hrf_cands | apply Hrf]].
destruct Hfr as [He1 [He2 [w [Hrf Hws]]]].
destruct Hrfwf as [? [Hrf_cands ?]].
right; unfold writes; split; [
eapply ran_ws_in_events; auto; [apply Hwswf | apply Hws] | ].
generalize (ran_ws_is_write E X w e2 Hwswf Hws); intros [v [l H2]];
exists l; exists v; apply H2.
right; unfold writes; split; [
eapply ran_ws_in_events; auto; [apply Hwswf | apply Hws] | ].
generalize (ran_ws_is_write E X e1 e2 Hwswf Hws); intros [v [l H2]];
exists l; exists v; apply H2.
Qed.
Lemma hb_implies_compete :
forall E X e1 e2,
well_formed_event_structure E ->
write_serialization_well_formed (events E) (ws X) /\
rfmaps_well_formed E (events E) (rf X) ->
hb E X e1 e2 /\ proc_of e1 <> proc_of e2 -> compete E e1 e2.
Proof.
unfold compete; intros E X e1 e2 Hwf [Hws Hrf] [Hhb Hp]; split; [|split; [|split; [|split]]].
change (events E e1) with (In _ (events E) e1); eapply hb_domain_in_events; auto.
split; [apply Hws | apply Hrf].
apply Hhb.
change (events E e2) with (In _ (events E) e2); eapply hb_range_in_events; auto.
split; [apply Hws | apply Hrf].
apply Hhb.
eapply hb_implies_same_loc; auto;
[apply Hwf | split; [apply Hws | apply Hrf] | apply Hhb].
auto.
eapply hb_implies_writes;
[apply Hwf | split; [apply Hws | apply Hrf] | apply Hhb].
Qed.
Definition bot_ghb (E:Event_struct) (X:Execution_witness) :=
rel_union (abc E X)
(rel_union (rel_union (ws X) (fr E X)) (ppo E)).
Lemma bot_ghb_in_ghb :
forall E X,
rel_incl (bot_ghb E X) (ghb E X).
Proof.
case_eq inter; case_eq intra;
intros Hintra Hinter E X; unfold ghb;
rewrite Hintra; rewrite Hinter; simpl.
right; right; trivial.
right; trivial.
right; trivial.
unfold bot_ghb; intros x y Hxy; trivial.
Qed.
Lemma not_diff_proc_class :
forall e z, ~ proc_of e <> proc_of z -> proc_of e = proc_of z.
Proof.
intros e z Hn.
apply NNPP; auto.
Qed.
End Basic.