Require Import List Permutation Vbase Relations ExtraRelations.
Require Import actions c11 opsemsets.
Require Import Classical extralib.
Set Implicit Arguments.
Expressions consist of values, memory allocation, loads, stores, compare
and swaps (CAS), fences, let (sequential composition), forking of threads,
non-deterministic choice, and loops.
Inductive cexp :=
| Evalue (n: nat)
| Ealloc (n: nat)
| Eload (typ: read_access_type) (l : nat)
| Estore (typ: write_access_type) (l v : nat)
| Ecas (typ_succ : rmw_access_type) (typ_fail: read_access_type) (l v v' : nat)
| Efence (typ: fence_access_type)
| Elet (e1: cexp) (e2: nat -> cexp)
| Efork (e: cexp)
| Echoice (e1: cexp) (e2: cexp)
| Erepeat (e : cexp).
We now give the semantics of these expressions as opsemsets. To do so, we
first define some combinators for defining opsemsets.
Definition oss_one_div act o :=
exists a,
<< O_Res : Res o = None >>
/\ << O_Tid : Tid o = thread act >>
/\ << O_Acts : Acts o = a :: nil >>
/\ << O_LabA : Lab o a = act >>
/\ << O_LabB : forall b (NEQ: b <> a), Lab o b = Askip 0 >>
/\ << O_Sb : forall a b (SB: Sb o a b), False >>
/\ << O_Dsb : forall a b (SB: Dsb o a b), False >>
/\ << O_Asw : forall a b (SB: Asw o a b), False >>.
Definition oss_one res act o :=
exists a,
<< O_Res : Res o = None \/ Res o = Some res >>
/\ << O_Tid : Tid o = thread act >>
/\ << O_Acts : Acts o = a :: nil >>
/\ << O_LabA : Lab o a = act >>
/\ << O_LabB : forall b (NEQ: b <> a), Lab o b = Askip 0 >>
/\ << O_Sb : forall a b (SB: Sb o a b), False >>
/\ << O_Dsb : forall a b (SB: Dsb o a b), False >>
/\ << O_Asw : forall a b (SB: Asw o a b), False >>.
Definition oss_seqcomp o1 o2 o :=
<< O_Res : Res o = Res o2 >>
/\ << O_TidA : Tid o = Tid o1 >>
/\ << O_TidB : Tid o = Tid o2 >>
/\ << O_Acts : Permutation (Acts o) (Acts o1 ++ Acts o2) >>
/\ << O_ND : NoDup (Acts o) >>
/\ << O_LabA : forall x (IN: In x (Acts o1)), Lab o x = Lab o1 x >>
/\ << O_LabB : forall x (NIN: ~ In x (Acts o1)), Lab o x = Lab o2 x >>
/\ << O_Sb : same_relation _ (Sb o)
(union _ (fun x y => In x (Acts o1) /\ In y (Acts o2) /\
thread (Lab o1 x) = thread (Lab o2 y))
(union _ (Sb o1) (Sb o2))) >>
/\ << O_DSb : same_relation _ (Dsb o) (union _ (Dsb o1) (Dsb o2)) >>
/\ << O_Asw : same_relation _ (Asw o) (union _ (Asw o1) (Asw o2)) >>.
Definition oss_fork tid tid' o1 o :=
exists a,
<< O_Res : Res o = None \/ Res o = Some tid' >>
/\ << O_Tid : Tid o = tid >>
/\ << O_Acts : Permutation (Acts o) (a :: Acts o1) >>
/\ << O_LabA : Lab o a = Askip tid >>
/\ << O_NIN : ~ In a (Acts o1) >>
/\ << O_LabB : forall x (NEQ: x <> a), Lab o x = Lab o1 x >>
/\ << O_Sb : same_relation _ (Sb o) (Sb o1) >>
/\ << O_DSb : same_relation _ (Dsb o) (Dsb o1) >>
/\ << O_Asw : same_relation _ (Asw o)
(union _ (fun x y => x = a /\ In y (Acts o1)) (Asw o1)) >>.
Fixpoint oss_repeat n f o :=
match n with
| 0 =>
Res o <> Some 0 /\ f o
| S m =>
Res o = None /\ f o \/
exists o1 o2,
Res o1 = Some 0 /\
f o1 /\
oss_repeat m f o2 /\
oss_seqcomp o1 o2 o
end.
Fixpoint exp_sem (e: cexp) (tid : nat) (o : opsem) :=
match e with
| Evalue n =>
oss_one n (Askip tid) o
| Ealloc n =>
exists l, oss_one l (Aalloc tid l n) o
| Eload typ l =>
exists v, oss_one v (Aload tid typ l v) o
| Estore typ l v =>
oss_one v (Astore tid typ l v) o
| Ecas typ1 typ2 l v v' =>
oss_one v (Armw tid typ1 l v v') o \/
(exists v'', v'' <> v /\ oss_one v'' (Aload tid typ2 l v'') o) \/
(exists v'', oss_one_div (Aload tid RATrlx l v'') o) \/
oss_one_div (Aload tid typ2 l v) o
| Efence typ =>
oss_one 0 (Afence tid typ) o
| Elet e1 e2 =>
Res o = None /\ exp_sem e1 tid o \/
exists vmid o1 o2,
Res o1 = Some vmid /\
exp_sem e1 tid o1 /\
exp_sem (e2 vmid) tid o2 /\
oss_seqcomp o1 o2 o
| Efork e =>
(exists tid', oss_one tid' (Askip tid) o) \/
exists tid' o',
exp_sem e tid' o' /\
oss_fork tid tid' o' o
| Echoice e1 e2 =>
exp_sem e1 tid o \/ exp_sem e2 tid o
| Erepeat e =>
exists n, oss_repeat n (exp_sem e tid) o
end.
We now prove that opsemsets returned by exp_sem are valid. We start with
a helper lemma, and then prove each property of valid opsemsets in turn.
Lemma oss_one_div_one :
forall act o (D: oss_one_div act o) n, oss_one n act o.
Proof. unfold oss_one_div, oss_one; ins; desf; unnw; eauto 10. Qed.
- The set of actions contains no duplicates.
Theorem NoDup_exp_sem : forall e tid o, exp_sem e tid o -> NoDup (Acts o).
Proof.
induction e; ins; desf; eauto;
unfold oss_one, oss_one_div, oss_seqcomp, oss_fork in *; desc; eauto;
try rewrite O_Acts; eauto.
by eapply Permutation_NoDup, NoDup_cons, (IHe _ _ H); eauto using Permutation_sym.
by induction n; ins; unfold oss_seqcomp in *; desf; eauto.
Qed.
- Every execution is finite.
Lemma ExecutionFinite_one :
forall n act o,
oss_one n act o ->
ExecutionFinite (Acts o) (Lab o) (Sb o) (Asw o).
Proof.
unfold oss_one; ins; destruct o; desf; ins; red; unnw;
repeat split; ins; desf; ins; try (by exfalso; eauto);
destruct (eqP a a0); vauto; exfalso; eauto.
Qed.
Lemma ExecutionFinite_one_div :
forall act o,
oss_one_div act o ->
ExecutionFinite (Acts o) (Lab o) (Sb o) (Asw o).
Proof.
unfold oss_one_div; ins; destruct o; desf; ins; red; unnw;
repeat split; ins; desf; ins; try (by exfalso; eauto);
destruct (eqP a a0); vauto; exfalso; eauto.
Qed.
Lemma ExecutionFinite_seqcomp :
forall o1 o2 o (SEQ : oss_seqcomp o1 o2 o)
(IH1 : ExecutionFinite (Acts o1) (Lab o1) (Sb o1) (Asw o1))
(IH2 : ExecutionFinite (Acts o2) (Lab o2) (Sb o2) (Asw o2)),
ExecutionFinite (Acts o) (Lab o) (Sb o) (Asw o).
Proof.
ins; unfold oss_seqcomp, ExecutionFinite in *; desc.
destruct o; ins; unnw; split; ins; subst.
eapply Permutation_in, in_app_iff; eauto using Permutation_sym.
destruct (classic (In a (opsemsets.Acts o1))); eauto.
by right; rewrite O_LabB in H; eauto.
specialize (CLOsb a b); specialize (CLOsb0 a b); split;
eapply Permutation_in, in_app_iff; eauto using Permutation_sym;
(desf; [eapply O_Sb in H|eapply O_Asw in H]); unfold union in H; desf; tauto.
Qed.
Lemma ExecutionFinite_fork :
forall tid tid' o' o (SEQ : oss_fork tid tid' o' o)
(IH : ExecutionFinite (Acts o') (Lab o') (Sb o') (Asw o')),
ExecutionFinite (Acts o) (Lab o) (Sb o) (Asw o).
Proof.
ins; unfold oss_fork, ExecutionFinite in *; desc; clear O_Res.
destruct o; ins; unnw; split; ins; subst; ins.
eapply Permutation_in; try eapply Permutation_sym; eauto.
by destruct (eqP a a0); desf; vauto; right; rewrite O_LabB in H; eauto.
specialize (CLOsb a0 b).
split; eapply Permutation_in; try apply Permutation_sym; eauto;
(desf; [eapply O_Sb in H|eapply O_Asw in H]); unfold union in H; desf; ins; tauto.
Qed.
Lemma ExecutionFinite_exp_sem :
forall e tid o,
exp_sem e tid o ->
ExecutionFinite (Acts o) (Lab o) (Sb o) (Asw o).
Proof.
induction e; ins; desf;
eauto using ExecutionFinite_one, ExecutionFinite_one_div,
ExecutionFinite_seqcomp, ExecutionFinite_fork.
revert o H; induction n; ins; desf; eauto using ExecutionFinite_seqcomp.
Qed.
Theorem oss_ef_exp_sem e tid : oss_ef (exp_sem e tid).
Proof. red; ins; eauto using ExecutionFinite_exp_sem. Qed.
Lemma acyclic_sbw_one n act o : oss_one n act o -> acyclic (Sbw o).
Proof.
unfold oss_one, Sbw; destruct o; repeat red; ins; desf;
induction H0; desf; eauto.
Qed.
Lemma acyclic_sbw_one_div act o : oss_one_div act o -> acyclic (Sbw o).
Proof.
unfold oss_one_div, Sbw; destruct o; repeat red; ins; desf;
induction H0; desf; eauto.
Qed.
Lemma acyclic_sbw_seqcomp :
forall o1 o2 o (SEQ : oss_seqcomp o1 o2 o)
e1 tid (X: exp_sem e1 tid o1)
e2 (Y: exp_sem e2 tid o2)
(A1 : acyclic (Sbw o1))
(A2 : acyclic (Sbw o2)),
acyclic (Sbw o).
Proof.
ins; unfold oss_seqcomp in *; desc.
apply ExecutionFinite_exp_sem in X.
apply ExecutionFinite_exp_sem in Y.
intros x M; eapply clos_trans_mon with
(r' := union _ (Sbw o2)
(union _ (fun x y : actid => In x (Acts o1) /\ In y (Acts o2))
(Sbw o1))) in M.
eapply (Permutation_NoDup O_Acts), nodup_app in O_ND; desf.
apply cycle_decomp_u_1 in M; desf; eauto.
2: by unfold union; desf; ins; desf; eapply Y in R; try eapply X in R'; desf; eauto.
apply cycle_decomp_u_1 in M; desf; eauto.
2: by ins; desf; eapply X in R'; desf; eauto.
by apply cycle_disj in M; ins; desf; eauto.
by unfold Sbw, union in *; ins; desf; [eapply O_Sb in H|eapply O_Asw in H]; desf; eauto.
Qed.
Lemma acyclic_sbw_exp_sem : forall e tid o, exp_sem e tid o -> acyclic (Sbw o).
Proof.
induction e; ins; desf;
eauto using acyclic_sbw_one, acyclic_sbw_one_div, acyclic_sbw_seqcomp.
exploit (oss_ef_exp_sem e); eauto; intro X.
eapply IHe in H; red in H0; desc; clear O_Res.
intros x M; eapply clos_trans_mon with
(r' := union _ (Sbw o') (fun x y : actid => x = a /\ In y (Acts o'))) in M.
apply cycle_decomp_u_1 in M; desf; eauto.
by apply cycle_disj in M; ins; desf.
by ins; desf; eapply X in R; desf; eauto.
by unfold Sbw, union in *; ins; desf; [eapply O_Sb in H0|eapply O_Asw in H0]; desf; eauto.
revert o H; induction n; ins; desf; eauto.
eapply acyclic_sbw_seqcomp with (e2 := Erepeat e); ins; eauto.
Qed.
Theorem oss_sbw_acyc_exp_sem e tid : oss_sbw_acyc (exp_sem e tid).
Proof. red; ins; eauto using acyclic_sbw_exp_sem. Qed.
- Sequence before relations only events from the same thread.
Lemma ConsistentSB_seqcomp :
forall o1 o2 o (SEQ : oss_seqcomp o1 o2 o)
e1 tid (X: exp_sem e1 tid o1)
e2 (Y: exp_sem e2 tid o2)
(IH1 : ConsistentSB (Lab o1) (Sb o1))
(IH2 : ConsistentSB (Lab o2) (Sb o2)),
ConsistentSB (Lab o) (Sb o).
Proof.
unfold oss_seqcomp, ConsistentSB; ins; desf.
eapply (Permutation_NoDup O_Acts), nodup_app in O_ND; desf.
apply O_Sb in SB; unfold union in SB; desf; eauto.
by rewrite O_LabA, O_LabB; eauto.
by rewrite !O_LabA; eauto;
eapply or_introl, oss_ef_exp_sem in SB; desf; eauto.
by rewrite !O_LabB; eauto;
eapply or_introl, oss_ef_exp_sem in SB; desf; eauto.
Qed.
Theorem ConsistentSB_exp_sem :
forall e tid o (OSS: exp_sem e tid o), ConsistentSB (Lab o) (Sb o).
Proof.
induction e; ins; desf; eauto using ConsistentSB_seqcomp;
try (by unfold ConsistentSB, oss_one, oss_one_div in *; ins ; exfalso; desf; eauto).
unfold ConsistentSB, oss_fork in *; ins; desc; clear O_Res.
apply O_Sb in SB; unfold union in SB; desf; eauto.
by rewrite !O_LabB; eauto; intro; desf;
eapply or_introl, oss_ef_exp_sem in SB; desf; eauto.
revert o OSS; induction n; ins; desf; eauto.
eapply ConsistentSB_seqcomp with (e2 := Erepeat e); ins; eauto.
Qed.
- Dependent sequence before is a subset of sequenced before and
Lemma ConsistentDSB_seqcomp :
forall o1 o2 o (SEQ : oss_seqcomp o1 o2 o)
e1 tid (E1: exp_sem e1 tid o1)
e2 (E2: exp_sem e2 tid o2)
(IH1 : ConsistentDSB (Lab o1) (Sb o1) (Dsb o1))
(IH2 : ConsistentDSB (Lab o2) (Sb o2) (Dsb o2)),
ConsistentDSB (Lab o) (Sb o) (Dsb o).
Proof.
unfold oss_seqcomp; ins; desf.
eapply (Permutation_NoDup O_Acts), nodup_app in O_ND; desf.
unfold ConsistentDSB in *; desf.
repeat split; intros x y X; try apply O_Sb; apply O_DSb in X;
unfold union in *; desf; try eapply clos_trans_mon; eauto; ins; try apply O_Sb; eauto;
try (by rewrite !O_LabA; eauto; eapply IH1 in X; induction X; eauto;
eapply or_introl, oss_ef_exp_sem in H; desf; eauto);
try (by rewrite !O_LabB; eauto; eapply IH2 in X; induction X; eauto;
eapply or_introl, oss_ef_exp_sem in H; desf; eauto).
Qed.
Theorem ConsistentDSB_exp_sem :
forall e tid o (OSS: exp_sem e tid o), ConsistentDSB (Lab o) (Sb o) (Dsb o).
Proof.
induction e; ins; desf; eauto using ConsistentDSB_seqcomp;
try (by repeat split; repeat red; ins; exfalso;
unfold oss_one, oss_one_div in *; desf; eauto).
unfold oss_fork in *; desc; clear O_Res.
specialize (IHe _ _ OSS); unfold ConsistentDSB in *; desf.
repeat split; intros x y X; try eapply clos_trans_mon, O_Sb; apply O_DSb in X;
unfold union in *; desf; eauto.
by rewrite !O_LabB; eauto; intro; desf; eapply IHe in X;
apply t_step_rt in X; desf; eauto;
eapply or_introl, oss_ef_exp_sem in X; desf; eauto.
by rewrite !O_LabB; eauto; intro; desf; eapply IHe in X;
apply t_rt_step in X; desf; eauto;
eapply or_introl, oss_ef_exp_sem in X0; desf; eauto.
revert o OSS; induction n; ins; desf; eauto.
eapply ConsistentDSB_seqcomp with (e2 := Erepeat e); ins; eauto.
Qed.
- Executions start with an action with thread identifier tid.
Lemma StartTID_seqcomp :
forall o1 o2 o (SEQ : oss_seqcomp o1 o2 o)
e1 tid (E1: exp_sem e1 tid o1)
e2 (E2: exp_sem e2 tid o2)
a1 (IN1: In a1 (Acts o1)) (T1: thread (Lab o1 a1) = tid)
(T'1: Tid o1 = tid)
(N: ~ (exists b, Sb o1 b a1))
(N': ~ (exists b, Asw o1 b a1))
(R1: forall b (IN: In b (Acts o1)), clos_refl_trans _ (Sbw o1) a1 b)
a2 (IN1: In a2 (Acts o2)) (T1: thread (Lab o2 a2) = tid)
(R2: forall b (IN: In b (Acts o2)), clos_refl_trans _ (Sbw o2) a2 b),
exists a, In a (Acts o) /\ thread (Lab o a) = tid /\ Tid o = tid /\
~ (exists b, Sb o b a) /\ ~ (exists b, Asw o b a) /\
(forall b (IN: In b (Acts o)), clos_refl_trans _ (Sbw o) a b).
Proof.
unfold oss_seqcomp; ins; desc.
eapply (Permutation_NoDup O_Acts), nodup_app in O_ND; desc.
exists a1,; [|rewrite O_LabA; ins; repeat split; try congruence].
by apply (Permutation_in _ (Permutation_sym O_Acts)), in_app_iff; eauto.
unfold union in *; intro M; desf; eapply O_Sb in M; desf; eauto.
by eapply or_introl, ExecutionFinite_exp_sem in M; desf; eauto.
unfold union in *; intro M; desf; eapply O_Asw in M; desf; eauto.
by eapply or_intror, ExecutionFinite_exp_sem in M; desf; eauto.
ins; apply (Permutation_in _ O_Acts), in_app_iff in IN; desf; eauto.
eapply R1 in IN; rewrite clos_refl_transE in *; desf; eauto;
right; eapply clos_trans_mon; eauto; unfold Sbw; ins; desf;
[left; eapply O_Sb | right; eapply O_Asw]; unfold union; eauto.
eapply rt_trans with a2.
by eapply rt_step, or_introl, O_Sb; unfold union; eauto.
eapply R2 in IN; rewrite clos_refl_transE in *; desf; eauto;
right; eapply clos_trans_mon; eauto; unfold Sbw; ins; desf;
[left; eapply O_Sb | right; eapply O_Asw]; unfold union; eauto.
Qed.
Theorem StartTID_exp_sem :
forall e tid o (OSS: exp_sem e tid o),
exists a, In a (Acts o) /\ thread (Lab o a) = tid /\ Tid o = tid /\
~ (exists b, Sb o b a) /\ ~ (exists b, Asw o b a) /\
(forall b (IN: In b (Acts o)), clos_refl_trans _ (Sbw o) a b).
Proof.
induction e; ins; desf; eauto;
try (by unfold oss_one, oss_one_div in *; desc;
exists a; rewrite O_Acts, O_LabA; ins; repeat split; eauto;
intro; ins; desf; eauto using rt_refl).
edestruct H; desc; eauto.
edestruct IHe; desc; eauto.
by eapply StartTID_seqcomp; eauto.
unfold oss_fork in *; desc; clear O_Res.
exists a; rewrite O_LabA; repeat split; ins.
by apply (Permutation_in _ (Permutation_sym O_Acts)); vauto.
unfold union in *; intro M; desf; eapply O_Sb in M; desf; eauto.
by eapply or_introl, ExecutionFinite_exp_sem in M; desf; eauto.
unfold union in *; intro M; desf; eapply O_Asw in M; desf; eauto.
by eapply or_intror, ExecutionFinite_exp_sem in M; desf; eauto.
ins; apply (Permutation_in _ O_Acts) in IN; ins; desf; eauto using rt_refl.
exploit IHe; eauto; intro N; desf.
eapply rt_trans with a0.
by eapply rt_step, or_intror, O_Asw; unfold union; eauto.
eapply N4 in IN; rewrite clos_refl_transE in *; desf; eauto;
right; eapply clos_trans_mon; eauto; unfold Sbw; ins; desf;
[left; eapply O_Sb | right; eapply O_Asw]; unfold union; eauto.
revert o OSS; induction n; ins; desf; eauto.
edestruct IHn; desc; eauto.
edestruct IHe; desc; eauto.
by eapply StartTID_seqcomp with (e2 := Erepeat e); ins; eauto.
Qed.
- Executions are prefix-closed.
Lemma pref_opsem_one :
forall act n x y,
oss_one n act y ->
pref_opsem x y ->
oss_one n act x.
Proof.
unfold pref_opsem, oss_one; ins; desc.
destruct x, y; ins; desc; unnw.
destruct Acts; ins.
generalize (Pref_Acts _ (in_eq _ _)); ins; desc; clarify; ins; destruct H; clarify.
destruct Acts; ins.
repeat eexists; ins; eauto.
by desf; eauto.
by rewrite Pref_LabOut; intuition.
by apply Pref_Sb in SB; red in SB; desf; eauto.
by apply Pref_Dsb in SB; red in SB; desf; eauto.
by apply Pref_Asw in SB; red in SB; desf; eauto.
exfalso.
destruct (Pref_Acts a); ins; vauto.
inv Pref_ND; ins; eauto.
Qed.
Lemma pref_opsem_one_div :
forall act x y,
oss_one_div act y ->
pref_opsem x y ->
oss_one_div act x.
Proof.
unfold pref_opsem, oss_one_div; ins; desc.
destruct x, y; ins; desc; unnw.
destruct Acts; ins.
generalize (Pref_Acts _ (in_eq _ _)); ins; desc; clarify; ins; destruct H; clarify.
destruct Acts; ins.
repeat eexists; ins; eauto.
by desf; eauto.
by rewrite Pref_LabOut; intuition.
by apply Pref_Sb in SB; red in SB; desf; eauto.
by apply Pref_Dsb in SB; red in SB; desf; eauto.
by apply Pref_Asw in SB; red in SB; desf; eauto.
exfalso.
destruct (Pref_Acts a); ins; vauto.
inv Pref_ND; ins; eauto.
Qed.
Lemma Pref_closed_fork :
forall e tid' o'
(E : exp_sem e tid' o')
(IH : forall x, pref_opsem x o' -> exp_sem e tid' x)
x y (S : pref_opsem x y) tid
(E0 : oss_fork tid tid' o' y),
(exists tid', oss_one tid' (Askip tid) x) \/
(exists (tid'0 : nat) (o'0 : opsem),
exp_sem e tid'0 o'0 /\ oss_fork tid tid'0 o'0 x).
Proof.
ins; exploit ConsistentDSB_exp_sem; [exact E|]; intro Cdsb; apply proj1 in Cdsb.
assert (ACYC: exp_sem (Efork e) tid y) by (right; eauto).
exploit ConsistentDSB_exp_sem; [exact ACYC|]; intro Cdsb'; apply proj1 in Cdsb'.
apply acyclic_sbw_exp_sem in ACYC.
unfold oss_fork in *; desc; unnw.
assert (In a (Acts x)).
red in S; desc; clear Pref_Res.
destruct (Acts x); ins.
destruct (eqP a0 a); clarify; eauto.
eapply (Pref_UCAsw _ a0); vauto.
apply O_Asw; left; split; ins.
specialize (Pref_Acts _ (In_eq _ _)).
by eapply Permutation_in in Pref_Acts; try eapply O_Acts; eauto; ins; desf.
destruct (filter_Prop Peano_dec.eq_nat_dec (NoDup_exp_sem _ _ _ E) (fun a => In a (Acts x)))
as (acts & acts_ND & acts_In).
destruct (classic (acts = nil)).
subst; ins.
red in S; desc.
left; eexists tid', a; unnw.
split; [desf; constructor (congruence) | clear O_Res Pref_Res].
assert (EQ: Acts x = a :: nil).
eapply NoDup_eq_one; eauto.
intros m INm; apply NNPP; intro NEQ; apply (acts_In m); split; eauto.
by exploit (Permutation_in m O_Acts); eauto; ins; desf.
repeat (split; ins); desf; eauto.
by rewrite Pref_LabIn.
by apply Pref_LabOut; rewrite EQ; ins; intro; desf.
by eapply Pref_Sb in SB; unfold restr_rel in *; rewrite EQ in *; ins; desf; desf;
eapply ACYC; vauto.
by eapply Pref_Dsb in SB; unfold restr_rel in *; rewrite EQ in *; ins; desf; desf;
eapply Cdsb' in SB; eapply ACYC, clos_trans_mon; vauto.
by eapply Pref_Asw in SB; unfold restr_rel in *; rewrite EQ in *; ins; desf; desf;
eapply ACYC; vauto.
right.
eexists tid', {|
Res := None ;
Acts := acts ;
Lab := fun x => if (In_dec Peano_dec.eq_nat_dec x acts) then (Lab o' x) else Askip 0 ;
Sb := restr_rel (fun x => In x acts) (Sb o') ;
Dsb := restr_rel (fun x => In x acts) (Dsb o') ;
Asw := restr_rel (fun x => In x acts) (Asw o') |},; [eapply IH|]; clear IH; ins.
red; ins; unnw; repeat (split; try done); ins; try (by desf; vauto).
by rewrite acts_In in *; desf; eauto.
clear O_Res; red; ins.
rewrite acts_In in *; desf; split.
eapply oss_ef_exp_sem in E.
eapply or_introl, E in REL; desf.
apply O_Sb in REL; red in S; desf; eauto.
clear O_Res; red; ins.
rewrite acts_In in *; desf; split.
eapply oss_ef_exp_sem in E.
eapply or_intror, E in REL; desf.
eapply or_intror, O_Asw in REL; red in S; desf; eauto.
red in S; desc.
exists a,; [|clear O_Res Pref_Res].
by desf; vauto; constructor (congruence).
split; [congruence|]; split.
apply NoDup_Permutation; vauto.
by constructor; eauto; rewrite acts_In in *; intro; desf.
ins.
rewrite acts_In; desf; split; ins; desf; eauto.
specialize (Pref_Acts _ H1).
eapply Permutation_in in Pref_Acts; try eassumption; ins; desf; eauto.
eapply oss_ef_exp_sem in E.
rewrite Pref_LabIn; ins; intuition; desf; eauto.
rewrite acts_In in *; desf; eauto.
rewrite Pref_LabIn; eauto; rewrite acts_In in *; desf; eauto.
eapply Pref_LabOut; intro; destruct n; rewrite acts_In; desf; split; ins.
eapply Pref_Acts, (Permutation_in _ O_Acts) in H1; ins; desf; exfalso; eauto.
by rewrite Pref_Sb, O_Sb; unfold restr_rel; split; intros m n M; desf; rewrite !acts_In in *; desf;
split; ins; eapply or_introl, E in M; desf.
by rewrite Pref_Dsb, O_DSb; unfold restr_rel; split; intros m n M; desf; rewrite !acts_In in *; desf;
intuition; eapply Cdsb in M; clear - M E; induction M; eauto; eapply or_introl, E in H; desf.
by rewrite Pref_Asw, O_Asw; unfold restr_rel, union; split; intros m n M; desf; rewrite !acts_In in *; desf;
eauto; right; split; ins; eapply or_intror, E in M; desf.
Qed.
Lemma NonEmpty2_exp_sem e tid o : exp_sem e tid o -> Acts o <> nil.
Proof.
red; ins; edestruct StartTID_exp_sem as (? & ? & _); eauto.
by rewrite H0 in *.
Qed.
Lemma upward_closed_sbw :
forall y P
(U_Sb : upward_closed (Sb y) P)
(U_Asw : upward_closed (Asw y) P) a
(H: P a) b
(C: clos_trans _ (Sbw y) b a),
P b.
Proof.
unfold Sbw; ins; induction C; desf; eauto.
Qed.
Lemma upward_closed_rt_sbw :
forall y P
(U_Sb : upward_closed (Sb y) P)
(U_Asw : upward_closed (Asw y) P) a
(H: P a) b
(C: clos_refl_trans _ (Sbw y) b a),
P b.
Proof.
unfold Sbw; ins; induction C; desf; eauto.
Qed.
Lemma Pref_closed_seqcomp :
forall o1 o2 y (SEQ : oss_seqcomp o1 o2 y)
e1 tid (E1 : exp_sem e1 tid o1)
(IH1 : forall x, pref_opsem x o1 -> exp_sem e1 tid x)
e2 (E2 : exp_sem e2 tid o2)
(IH2 : forall x, pref_opsem x o2 -> exp_sem e2 tid x)
vmid (RES : Res o1 = Some vmid)
x (S : pref_opsem x y),
Res x = None /\ exp_sem e1 tid x \/
(exists (o0 o3 : opsem),
Res o0 = Some vmid /\
exp_sem e1 tid o0 /\ exp_sem e2 tid o3 /\ oss_seqcomp o0 o3 x).
Proof.
ins.
exploit ConsistentDSB_exp_sem; [exact E1|]; intro Cdsb1; apply proj1 in Cdsb1.
exploit ConsistentDSB_exp_sem; [exact E2|]; intro Cdsb2; apply proj1 in Cdsb2.
destruct (classic (forall a, In a (Acts x) -> In a (Acts o1))) as [Y|N].
assert (RR: Res x = None).
exploit (StartTID_exp_sem e2); eauto; intro NE; desf.
unfold oss_seqcomp, pref_opsem in *; desf.
eapply (Permutation_NoDup O_Acts), nodup_app in O_ND; desc.
exfalso; assert (NE' := NE).
eapply In_appI2, (Permutation_in _ (Permutation_sym O_Acts)), Pref_Res1, Y in NE; eauto.
by rewrite O_LabB; try congruence; intro; eauto.
cut (pref_opsem x o1); eauto.
eapply oss_ef_exp_sem in E2.
clear IH1 IH2 RES E1; red in SEQ; desc.
eapply (Permutation_NoDup O_Acts), nodup_app in O_ND; desf.
unfold pref_opsem in *; desc; unnw.
split; [congruence|].
split; [vauto|clear Pref_Res O_Res; intuition].
by rewrite Pref_LabIn, O_LabA; ins; eauto.
by rewrite Pref_Sb, O_Sb; apply same_relation_restr; ins;
unfold union; split; ins; desf; eauto;
exfalso; eauto; eapply or_introl, E2 in H; desf; eauto.
by rewrite Pref_Dsb, O_DSb; apply same_relation_restr; ins;
unfold union; split; ins; desf; eauto;
exfalso; eauto; eapply Cdsb2, t_step_rt in H; desf;
eapply or_introl, E2 in H; desf; eauto.
by rewrite Pref_Asw, O_Asw; apply same_relation_restr; ins;
unfold union; split; ins; desf; eauto;
exfalso; eauto; eapply or_intror, E2 in H; desf; eauto.
by red; ins; eapply Pref_UCSb; eauto; apply O_Sb; vauto.
by red; ins; eapply Pref_UCAsw; eauto; apply O_Asw; vauto.
apply not_all_ex_not in N; desf; apply imply_to_and in N; desf.
right.
destruct (filter_Prop Peano_dec.eq_nat_dec (NoDup_exp_sem _ _ _ E1) (fun a => In a (Acts x)))
as (acts & acts_ND & acts_In).
destruct (filter_Prop Peano_dec.eq_nat_dec (NoDup_exp_sem _ _ _ E2) (fun a => In a (Acts x)))
as (acts2 & acts2_ND & acts2_In).
assert (G: forall a, In a (Acts o1) -> thread (Lab o1 a) = Tid o1 -> In a (Acts x)).
red in SEQ; red in S; desc; clear O_Res Pref_Res.
ins; exploit (StartTID_exp_sem e2); eauto.
intros [k K]; desc; subst.
exploit (K4 n).
by eapply Pref_Acts, (Permutation_in _ O_Acts), in_app_iff in N; desf.
intro RT.
assert (Sb y a k) by (apply O_Sb, or_introl; repeat split; ins; congruence).
assert (clos_trans _ (Sbw y) a n).
by apply t_step_rt; eexists,; [left|]; eauto;
rewrite clos_refl_transE in *; desf; eauto;
right; eapply clos_trans_mon; eauto; unfold Sbw; ins; desf;
[left; eapply O_Sb | right; eapply O_Asw]; unfold union; eauto.
by eapply (upward_closed_sbw Pref_UCSb Pref_UCAsw); eauto.
exists {|
Tid := Tid o1 ;
Res := Res o1 ;
Acts := acts ;
Lab := fun z => if in_dec Peano_dec.eq_nat_dec z acts then Lab o1 z else Askip 0 ;
Sb := restr_rel (fun x => In x acts) (Sb o1) ;
Dsb := restr_rel (fun x => In x acts) (Dsb o1) ;
Asw := restr_rel (fun x => In x acts) (Asw o1) |},
{|
Tid := Tid o2 ;
Res := Res x ;
Acts := acts2 ;
Lab := fun z => if in_dec Peano_dec.eq_nat_dec z acts2 then Lab o2 z else Askip 0 ;
Sb := restr_rel (fun x => In x acts2) (Sb o2) ;
Dsb := restr_rel (fun x => In x acts2) (Dsb o2) ;
Asw := restr_rel (fun x => In x acts2) (Asw o2) |}; ins.
split; ins.
split.
eapply IH1; clear IH1 IH2; eauto.
split; ins; unnw.
split.
right; repeat split; ins; eauto using NonEmpty2_exp_sem.
by rewrite acts_In; split; ins; eauto.
red in SEQ; red in S; desc; clear O_Res Pref_Res.
intuition; desf; ins.
ins; exploit (StartTID_exp_sem e1); eauto.
by intros [k K]; desc; eapply (acts_In k); clarify; eauto.
by rewrite acts_In in *; desc; eauto.
red; ins; rewrite acts_In in *; desc; split; eauto.
eby eapply or_introl, ExecutionFinite_exp_sem in REL; desc.
by eapply Pref_UCSb; eauto; apply O_Sb; unfold union; eauto.
red; ins; rewrite acts_In in *; desc; split; eauto.
eby eapply or_intror, ExecutionFinite_exp_sem in REL; desc.
by eapply Pref_UCAsw; eauto; apply O_Asw; unfold union; eauto.
split.
eapply IH2; clear IH1 IH2; eauto.
split; ins; unnw.
split.
red in SEQ; red in S; desf; eauto.
right; repeat split; ins; try congruence; eauto using NonEmpty2_exp_sem.
rewrite acts2_In; split; ins.
eapply (Permutation_NoDup O_Acts), nodup_app in O_ND; desc.
eapply Pref_Res1; ins.
by eapply (Permutation_in _ (Permutation_sym O_Acts)), In_appI2.
by rewrite O_LabB; try congruence; intro; eauto.
red in SEQ; red in S; desc; clear O_Res Pref_Res.
intuition; desf; ins.
ins; exploit (StartTID_exp_sem e2); eauto.
intros [k K]; desc.
exploit (K4 n); clear K4.
by eapply Pref_Acts, (Permutation_in _ O_Acts), in_app_iff in N; desf.
intro; apply (acts2_In k); rewrite clos_refl_transE in *; desf.
split; ins; eapply (upward_closed_rt_sbw Pref_UCSb Pref_UCAsw); eauto.
eapply clos_refl_transE; right; eapply clos_trans_mon; eauto.
by unfold Sbw; ins; desf; [left; eapply O_Sb|right; eapply O_Asw]; unfold union; eauto.
by rewrite acts2_In in *; desc; eauto.
red; ins; rewrite acts2_In in *; desc; split; eauto.
eby eapply or_introl, ExecutionFinite_exp_sem in REL; desc.
by eapply Pref_UCSb; eauto; apply O_Sb; unfold union; eauto.
red; ins; rewrite acts2_In in *; desc; split; eauto.
eby eapply or_intror, ExecutionFinite_exp_sem in REL; desc.
by eapply Pref_UCAsw; eauto; apply O_Asw; unfold union; eauto.
assert (P : Permutation (Acts x) (acts ++ acts2)).
red in SEQ; red in S; desc; clear O_Res Pref_Res.
eapply (Permutation_NoDup O_Acts), nodup_app in O_ND; desc.
apply NoDup_Permutation; eauto.
apply nodup_app; repeat split; try red; ins;
rewrite acts_In, acts2_In in *; desf; eauto.
ins; rewrite in_app_iff, acts_In, acts2_In; split; ins; desf; eauto.
exploit Pref_Acts; eauto; intro M.
eapply (Permutation_in _ O_Acts), in_app_iff in M; tauto.
red in SEQ; red in S; desc; clear O_Res Pref_Res.
red; ins; unnw.
rewrite Pref_Sb, Pref_Dsb, Pref_Asw, O_Sb, O_DSb, O_Asw;
clear Pref_Sb Pref_Dsb Pref_Asw O_Sb O_DSb O_Asw; intuition; desf; desf;
rewrite ?acts_In, ?acts2_In in *; desf.
by rewrite Pref_LabIn; eauto.
by rewrite Pref_LabIn; eauto.
by destruct (classic (In x0 (Acts x))); eauto;
exfalso; apply (Permutation_in _ P), in_app_iff in H;
rewrite acts_In, acts2_In in *; desf; eauto.
unfold restr_rel, union; split; red; ins; des;
rewrite ?acts_In, ?acts2_In in *; desc; eauto 8.
left; repeat split; ins; rewrite ?acts_In, ?acts2_In; ins.
by desf; exfalso; rewrite ?acts_In, ?acts2_In in *; desc; eauto.
right; left; rewrite ?acts_In, ?acts2_In in *; desc; repeat split; ins;
try (by eapply or_introl, ExecutionFinite_exp_sem in H; desc; eauto).
right; right; rewrite ?acts_In, ?acts2_In in *; desc; repeat split; ins;
try (by eapply or_introl, ExecutionFinite_exp_sem in H; desc; eauto).
repeat split; ins; left; repeat split; ins.
by desf; exfalso; rewrite ?acts_In, ?acts2_In in *; desc; eauto.
unfold restr_rel, union; split; red; ins; desf;
rewrite ?acts_In, ?acts2_In in *; desc; eauto;
[left|right]; repeat split; ins;
try (by first [apply Cdsb1 in H|apply Cdsb2 in H]; apply t_step_rt in H; desf;
eapply or_introl, ExecutionFinite_exp_sem in H; desc; eauto);
try (by first [apply Cdsb1 in H|apply Cdsb2 in H]; apply t_rt_step in H; desf;
eapply or_introl, ExecutionFinite_exp_sem in H2; desc; eauto).
unfold restr_rel, union; split; red; ins; desf;
rewrite ?acts_In, ?acts2_In in *; desc; eauto;
[left|right]; repeat split; ins;
try (by eapply or_intror, ExecutionFinite_exp_sem in H; desc; eauto).
Qed.
Theorem Pref_closed_exp_sem : forall e tid, Pref_closed (exp_sem e tid).
Proof.
intros e tid x y SS E; revert e tid x y E SS.
induction e; ins; desf; eauto;
try (by exploit pref_opsem_one; eauto; ins; desf; eauto 8);
try (by exploit pref_opsem_one_div; eauto; ins; desf; eauto 8).
by left; split; eauto; unfold pref_opsem in *; desf; congruence.
by edestruct Pref_closed_seqcomp; eauto.
by eapply Pref_closed_fork; eauto.
revert x y E SS.
induction n; ins; desf; eauto.
exists 0; split; eauto.
by red in SS; desf; congruence.
exists 1; left; split; eauto.
by red in SS; desf; congruence.
edestruct Pref_closed_seqcomp with (e2 := Erepeat e); ins; desc; eauto.
by exists 1; ins; eauto.
by exists (S n0); right; desc; eauto 10.
Qed.
- Executions are receptive: they are closed under changing the value
Lemma alt_read_final_load :
forall n tid typ l v x y,
oss_one n (Aload tid typ l v) y ->
alt_read_final_one x y ->
exists v', oss_one_div (Aload tid typ l v') x.
Proof.
unfold oss_one, oss_one_div, alt_read_final_one; ins; desc; unnw; clear O_Res.
unfold alt_read in *; desc.
destruct (eqP a0 a); [|by desf; rewrite O_LabB in AFRO_Rd0; eauto]; subst.
des; try congruence.
rewrite O_Acts in *; ins.
unfold same_relation in *; desc.
exists v1, a; unnw; repeat (split; ins); eauto; try congruence.
desf; ins; rewrite AFRO_Rd, AFRO_Rd0 in *; ins; clarify; congruence.
by eapply NoDup_eq_one; ins; rewrite AFRO_Acts in *; desf; eauto.
by rewrite AFRO_Lab; eauto.
Qed.
Lemma alt_read_final_rmw :
forall n tid typ l v v' x y,
oss_one n (Armw tid typ l v v') y ->
alt_read_final_one x y ->
exists v', oss_one_div (Aload tid RATrlx l v') x.
Proof.
unfold oss_one, oss_one_div, alt_read_final_one; ins; desc; unnw; clear O_Res.
unfold alt_read in *; desc.
destruct (eqP a0 a); [|by desf; rewrite O_LabB in AFRO_Rd0; eauto]; subst.
des; try congruence.
rewrite O_Acts in *; ins.
unfold same_relation in *; desc.
exists v1, a; unnw; repeat (split; ins); eauto; try congruence.
desf; ins; rewrite AFRO_Rd, AFRO_Rd0 in *; ins; clarify; congruence.
by eapply NoDup_eq_one; ins; rewrite AFRO_Acts in *; desf; eauto.
by rewrite AFRO_Lab; eauto.
Qed.
Lemma alt_read_final_fork :
forall e tid' o'
(H : exp_sem e tid' o')
(IH: forall x, alt_read_final_one x o' -> exp_sem e tid' x)
tid x y
(F : oss_fork tid tid' o' y)
(R : alt_read_final_one x y),
exists o, exp_sem e tid' o /\ oss_fork tid tid' o x.
Proof.
ins; exploit ConsistentDSB_exp_sem; [exact H|]; intro Cdsb; apply proj1 in Cdsb.
assert (FIN := oss_ef_exp_sem _ _ _ H).
unfold oss_fork, alt_read_final_one in *; desc; unnw.
eexists {|
Tid := Tid o' ;
Res := if thread (Lab o' a) == Tid o' then None else Res o' ;
Acts := Acts o' ;
Lab := fun z => if z == a0 then Askip 0 else if z == a then Lab x a else Lab o' z ;
Sb := restr_rel (fun x => In x (Acts o')) (Sb x) ;
Dsb := restr_rel (fun x => In x (Acts o')) (Dsb x) ;
Asw := restr_rel (fun x => In x (Acts o')) (Asw x) |},; [eapply IH|]; clear IH; ins; eauto.
exists a; rewrite eqxx.
clear AFRO_Res O_Res.
unfold Sbw in *; ins; rewrite AFRO_Sb, AFRO_Dsb, AFRO_Asw, O_Sb, O_DSb, O_Asw.
destruct (eqP a a0); clarify.
exfalso; unfold alt_read in *; desf; congruence.
unfold same_relation, alt_read, union, inclusion, restr_rel in *; des;
rewrite AFRO_Rd, <- O_LabB, AFRO_Rd0; ins.
repeat (split; ins); desf; desf; eauto 9 using NoDup_exp_sem.
by red; ins; desf; eauto.
by apply NNPP; intro; eapply O_NIN, (proj1 (oss_ef_exp_sem _ _ _ H)); congruence.
by eapply or_introl, FIN in H0; desf.
by eapply or_introl, FIN in H0; desf.
by eapply Cdsb, t_step_rt in H0; destruct H0 as (? & H0 & _); eapply or_introl, FIN in H0; desf.
by eapply Cdsb, t_rt_step in H0; destruct H0 as (? & _ & H0); eapply or_introl, FIN in H0; desf.
by eapply or_intror, FIN in H0; desf.
by eapply or_intror, FIN in H0; desf.
repeat (split; ins); desf; desf; eauto 9 using NoDup_exp_sem.
by red; ins; desf; eauto.
by apply NNPP; intro; eapply O_NIN, (proj1 (oss_ef_exp_sem _ _ _ H)); congruence.
by eapply or_introl, FIN in H0; desf.
by eapply or_introl, FIN in H0; desf.
by eapply Cdsb, t_step_rt in H0; destruct H0 as (? & H0 & _); eapply or_introl, FIN in H0; desf.
by eapply Cdsb, t_rt_step in H0; destruct H0 as (? & _ & H0); eapply or_introl, FIN in H0; desf.
by eapply or_intror, FIN in H0; desf.
by eapply or_intror, FIN in H0; desf.
exists a0; rewrite AFRO_Sb, AFRO_Dsb, AFRO_Asw, O_Sb, O_DSb, O_Asw.
split.
by desf; eauto; constructor (congruence).
clear O_Res AFRO_Res.
unfold same_relation, inclusion, union, restr_rel.
repeat split; ins; desf; desf; eauto.
transitivity (Acts y); eauto.
apply NoDup_Permutation; eauto.
eapply Permutation_NoDup, NoDup_cons, (NoDup_exp_sem _ _ _ H); eauto using Permutation_sym.
by rewrite AFRO_Lab; ins; intro; desf; unfold alt_read in *; desf; congruence.
by rewrite AFRO_Lab; ins; eauto.
by eapply or_introl, FIN in H0; desf.
by eapply or_introl, FIN in H0; desf.
by eapply Cdsb, t_step_rt in H0; destruct H0 as (? & H0 & _); eapply or_introl, FIN in H0; desf.
by eapply Cdsb, t_rt_step in H0; destruct H0 as (? & _ & H0); eapply or_introl, FIN in H0; desf.
by right; split; eauto; eapply or_intror, FIN in H0; desf.
Qed.
Lemma alt_read_final_seqcomp :
forall o1 o2 y (SEQ : oss_seqcomp o1 o2 y)
e1 tid (E1 : exp_sem e1 tid o1)
(IH1 : forall x, alt_read_final_one x o1 -> exp_sem e1 tid x)
vmid (RES : Res o1 = Some vmid)
e2 (E2 : exp_sem e2 tid o2)
(IH2 : forall x, alt_read_final_one x o2 -> exp_sem e2 tid x)
x (S : alt_read_final_one x y),
exists (o0 o3 : opsem),
Res o0 = Some vmid /\
exp_sem e1 tid o0 /\ exp_sem e2 tid o3 /\ oss_seqcomp o0 o3 x.
Proof.
ins;
exploit (ExecutionFinite_exp_sem (Elet e1 (fun _ => e2))).
by right; eauto 8.
intro FIN.
unfold oss_seqcomp in *; desf; unnw.
assert (ND := Permutation_NoDup O_Acts O_ND); apply nodup_app in ND; desf.
red in S; desc.
assert (IN: In a (Acts y)).
apply (proj1 FIN); unfold alt_read in *; desf; congruence.
eapply (Permutation_in _ O_Acts), in_app_iff in IN; destruct IN as [IN|IN].
eexists {|
Tid := Tid o1 ;
Res := Res o1 ;
Acts := Acts o1 ;
Lab := fun z => if z == a then Lab x a else Lab o1 z ;
Sb := Sb o1 ;
Dsb := Dsb o1 ;
Asw := Asw o1 |}, o2; ins.
rewrite AFRO_Sb, AFRO_Dsb, AFRO_Asw, O_Sb.
split; try done.
split.
eapply IH1; clear IH1; eauto.
exists a; unnw; ins; rewrite eqxx; split; ins.
split.
desf; desf; eauto; try congruence.
exploit (StartTID_exp_sem e2); eauto; intro; desf.
exfalso; eapply (AFRO_Max a0), or_introl, AFRO_Sb, O_Sb, or_introl; repeat split; ins.
rewrite <- O_LabA; ins; eauto.
unfold alt_read in *; desf; rewrite AFRO_Rd, AFRO_Rd0 in *; ins; desf; congruence.
clear AFRO_Res.
repeat (split; ins); desf; desf; unfold Sbw; ins; try red; ins; desf.
by eapply AFRO_Max, or_introl, AFRO_Sb, O_Sb; unfold union; eauto.
by eapply AFRO_Max, or_intror, AFRO_Asw, O_Asw; unfold union; eauto.
by rewrite <- O_LabA; eauto.
split; try done.
split; [|clear AFRO_Res]; intuition.
desf; try congruence.
exploit (StartTID_exp_sem e2); eauto; intro; desf.
exfalso; eapply (AFRO_Max a0), or_introl, AFRO_Sb, O_Sb, or_introl; repeat split; ins.
rewrite <- O_LabA; ins; eauto.
unfold alt_read in *; desf; rewrite AFRO_Rd, AFRO_Rd0 in *; ins; desf; congruence.
rewrite Permutation_trans; eauto.
by apply NoDup_Permutation; eauto.
desf; desf.
by rewrite AFRO_Lab, O_LabA; ins; desf.
by rewrite AFRO_Lab, O_LabB; ins; desf.
eapply union_mor; try reflexivity.
split; red; ins; desf; desf; intuition;
rewrite <- O_LabA in *; ins;
unfold alt_read in *; desf; rewrite AFRO_Rd, AFRO_Rd0 in *; ins.
eexists o1,{|
Tid := Tid o2 ;
Res := Res x ;
Acts := Acts o2 ;
Lab := fun z => if z == a then Lab x a else Lab o2 z ;
Sb := Sb o2 ;
Dsb := Dsb o2 ;
Asw := Asw o2 |}; ins.
rewrite AFRO_Sb, AFRO_Dsb, AFRO_Asw, O_Sb.
intuition.
eapply IH2; eauto.
exists a; unnw; ins; rewrite eqxx; split; ins.
split; [|clear AFRO_Res].
desf; congruence.
repeat (split; ins); desf; desf; unfold Sbw; ins; try red; ins; desf.
by eapply AFRO_Max, or_introl, AFRO_Sb, O_Sb; unfold union; eauto.
by eapply AFRO_Max, or_intror, AFRO_Asw, O_Asw; unfold union; eauto.
by rewrite <- O_LabB; eauto.
rewrite Permutation_trans; eauto.
by apply NoDup_Permutation; eauto.
by rewrite AFRO_Lab, O_LabA; ins; desf; eauto.
by desf; desf; rewrite AFRO_Lab, O_LabB; ins; desf; eauto.
eapply union_mor; try reflexivity.
split; red; ins; desf; desf; intuition;
rewrite <- O_LabB in *; ins; eauto;
unfold alt_read in *; desf; rewrite AFRO_Rd, AFRO_Rd0 in *; ins.
Qed.
Theorem AFR_closed_exp_sem : forall e tid, AFR_closed (exp_sem e tid).
Proof.
red; red; induction e; ins; desf; eauto;
try (by exfalso; eauto using alt_read_final_empty);
try (by exfalso; red in REL; red in POST; desc; clear O_Res AFRO_Res;
unfold alt_read in *; desf; (destruct (eqP a0 a); [congruence|]);
rewrite O_LabB in AFRO_Rd0; eauto 6).
exploit alt_read_final_load; eauto; intros [vn X]; desf.
by eauto using oss_one_div_one.
by exploit alt_read_final_rmw; eauto; intros [vn X]; desf.
exploit alt_read_final_load; eauto; intros [vn X]; desf.
by destruct (eqP vn v); desf; eauto 8 using oss_one_div_one.
apply oss_one_div_one with (n := v'') in POST.
by exploit alt_read_final_load; eauto.
apply oss_one_div_one with (n := v) in POST.
exploit alt_read_final_load; eauto; intros [vn X]; desf.
by destruct (eqP vn v); desf; eauto 8 using oss_one_div_one.
by left; split; eauto; red in REL; desf; congruence.
by edestruct alt_read_final_seqcomp; eauto.
by exploit alt_read_final_fork; eauto.
revert x y REL POST.
induction n; ins; desf; eauto.
exists 0; split; eauto.
by red in REL; desf; congruence.
exists 1; left; split; eauto.
by red in REL; desf; congruence.
edestruct alt_read_final_seqcomp with (e2 := Erepeat e); ins; desc; eauto.
by exists (S n0); right; desc; eauto 10.
Qed.
This page has been generated by coqdoc