Library mcertikos.conlib.conmtlib.EAsmPropLib
Require Import Coqlib.
Require Import Maps.
Require Import ASTExtra.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import MemoryX.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Asm.
Require Import Conventions.
Require Import Machregs.
Require Import AuxLemma.
Require Import liblayers.logic.PTreeModules.
Require Import liblayers.compcertx.MemWithData.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compat.CompatData.
Require Import liblayers.compat.CompatPrimSem.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatExternalCalls.
Require Import Decision.
Require Import GlobIdent.
Require Import CommonTactic.
Require Import Constant.
Require Import PrimSemantics.
Require Import LRegSet.
Require Import AuxStateDataType.
Require Import AsmImplLemma.
Require Import AsmImplTactic.
Require Import GlobalOracle.
Require Import SingleConfiguration.
Require Import LAsm.
Require Import EAsm.
Require Import liblayers.compat.CompatGenSem.
Require Import LAsmAbsDataProperty.
Require Import RegsetLessdef.
Section RegsetLessdef_ThreadState.
We extend the regset_lessdef relation to our ThreadStates.
Inductive ts_lessdef : relation ThreadState :=
| ts_lessdef_environment:
ts_lessdef Environment Environment
| ts_lessdef_available:
ts_lessdef Available Available
| ts_lessdef_running rs rs´:
regset_lessdef rs rs´ →
ts_lessdef (Running rs) (Running rs´).
Lemma ts_lessdef_refl:
∀ rs,
ts_lessdef rs rs.
Proof.
intros. destruct rs; constructor.
eapply regset_lessdef_refl; eauto.
Qed.
Lemma regset_map_None_Some_neq:
∀ tid curid rsm (rs: regset),
ZMap.get tid rsm = Environment →
ZMap.get curid rsm = Running rs →
tid ≠ curid.
Proof.
red; intros; subst. congruence.
Qed.
Lemma regset_map_neq:
∀ rsm rsm´ (rs rs´ rs´´: regset) tid curid,
(∀ i,
ts_lessdef (ZMap.get i (ZMap.set tid (Running rs) rsm´))
(ZMap.get i rsm)) →
tid ≠ curid →
regset_lessdef rs´ rs´´ →
(∀ i,
ts_lessdef
(ZMap.get i (ZMap.set tid (Running rs) (ZMap.set curid (Running rs´) rsm´)))
(ZMap.get i (ZMap.set curid (Running rs´´) rsm))).
Proof.
intros. specialize (H i).
destruct (zeq i curid); subst.
- rewrite ZMap.gss. rewrite ZMap.gso; auto.
rewrite ZMap.gss.
constructor. trivial.
- destruct (zeq i tid); subst.
+ rewrite ZMap.gss in ×.
rewrite ZMap.gso; auto.
+ repeat rewrite ZMap.gso; auto.
rewrite ZMap.gso in H; auto.
Qed.
Lemma regset_map_neq´´:
∀ rsm rsm´ (ts ts´ ts´´: ThreadState) tid curid,
(∀ i,
ts_lessdef (ZMap.get i (ZMap.set tid ts rsm´))
(ZMap.get i rsm)) →
tid ≠ curid →
ts_lessdef ts´ ts´´ →
(∀ i,
ts_lessdef
(ZMap.get i (ZMap.set tid ts (ZMap.set curid ts´ rsm´)))
(ZMap.get i (ZMap.set curid ts´´ rsm))).
Proof.
intros. specialize (H i).
destruct (zeq i curid); subst.
- rewrite ZMap.gss. rewrite ZMap.gso; auto.
rewrite ZMap.gss.
assumption.
- destruct (zeq i tid); subst.
+ rewrite ZMap.gss in ×.
rewrite ZMap.gso; auto.
+ repeat rewrite ZMap.gso; auto.
rewrite ZMap.gso in H; auto.
Qed.
Lemma regset_lessdef_exists_neq:
∀ a rsm rsm´ rs ts0 a´,
ZMap.get a rsm = Running rs →
(∀ i, ts_lessdef (ZMap.get i (ZMap.set a´ ts0 rsm))
(ZMap.get i rsm´)) →
a ≠ a´ →
∃ rs´,
ZMap.get a rsm´ = Running rs´
∧ regset_lessdef rs rs´.
Proof.
intros. specialize (H0 a).
rewrite ZMap.gso in H0; auto.
rewrite H in H0. inv H0.
refine_split´; trivial.
Qed.
Lemma regset_lessdef_exists_neq´:
∀ a rsm rsm´ rs ts0 a´,
ZMap.get a rsm = Running rs →
ZMap.get a´ rsm = Environment →
(∀ i, ts_lessdef (ZMap.get i (ZMap.set a´ ts0 rsm))
(ZMap.get i rsm´)) →
∃ rs´,
ZMap.get a rsm´ = Running rs´
∧ regset_lessdef rs rs´.
Proof.
intros. eapply regset_lessdef_exists_neq; eauto.
congruence.
Qed.
Lemma regset_lessdef_exists_neq_available:
∀ a rsm rsm´ ts0 a´,
ZMap.get a rsm = Available →
(∀ i, ts_lessdef (ZMap.get i (ZMap.set a´ ts0 rsm))
(ZMap.get i rsm´)) →
a ≠ a´ →
ZMap.get a rsm´ = Available.
Proof.
intros. specialize (H0 a).
rewrite ZMap.gso in H0; auto.
rewrite H in H0. inv H0.
refine_split´; trivial.
Qed.
Lemma ts_lessdef_exists_neq:
∀ a rsm rsm´ ts ts0 a´,
ZMap.get a rsm = ts →
(∀ i, ts_lessdef (ZMap.get i (ZMap.set a´ ts0 rsm))
(ZMap.get i rsm´)) →
a ≠ a´ →
∃ ts´,
ZMap.get a rsm´ = ts´
∧ ts_lessdef ts ts´.
Proof.
intros. specialize (H0 a).
rewrite ZMap.gso in H0; auto.
rewrite H in H0.
destruct H0; eexists; split; constructor; eauto.
Qed.
Lemma ts_lessdef_exists_neq´:
∀ a rsm rsm´ rs ts0 a´,
ZMap.get a rsm = Running rs →
(∀ i, ts_lessdef (ZMap.get i (ZMap.set a´ ts0 rsm))
(ZMap.get i rsm´)) →
a ≠ a´ →
∃ rs´,
ZMap.get a rsm´ = Running rs´
∧ regset_lessdef rs rs´.
Proof.
intros.
edestruct ts_lessdef_exists_neq as (ts & Hts & Hless); eauto.
inversion Hless; clear Hless; subst.
eauto.
Qed.
Lemma regset_lessdef_exists_neq´´:
∀ a rsm rsm´ rs ts0 a´ x,
ZMap.get a rsm = Available ∧ x = Some rs ∨
ZMap.get a rsm = Running rs →
(∀ i, ts_lessdef (ZMap.get i (ZMap.set a´ ts0 rsm))
(ZMap.get i rsm´)) →
a ≠ a´ →
∃ rs´,
(ZMap.get a rsm´ = Available ∧ x = Some rs´ ∨
ZMap.get a rsm´ = Running rs´)
∧ regset_lessdef rs rs´.
Proof.
intros. specialize (H0 a).
rewrite ZMap.gso in H0; auto.
destruct H as [[H H´]|H];
rewrite H in H0; inv H0;
refine_split´; eauto using regset_lessdef_refl.
Qed.
Lemma regset_lessdef_exists_eq:
∀ a rsm rsm´ rs,
(∀ i, ts_lessdef (ZMap.get i (ZMap.set a (Running rs) rsm))
(ZMap.get i rsm´)) →
∃ rs´,
ZMap.get a rsm´ = Running rs´
∧ regset_lessdef rs rs´.
Proof.
intros. specialize (H a).
rewrite ZMap.gss in H. inv H. eauto.
Qed.
Lemma regset_lessdef_exists_eq´:
∀ a rsm rsm´ rs,
(∀ i, ts_lessdef (ZMap.get i rsm)
(ZMap.get i rsm´)) →
ZMap.get a rsm = Running rs →
∃ rs´,
ZMap.get a rsm´ = Running rs´
∧ regset_lessdef rs rs´.
Proof.
intros. specialize (H a).
rewrite H0 in H. inv H. eauto.
Qed.
Lemma regset_lessdef_exists_eq´´:
∀ a rsm rsm´ ts rs,
(∀ i, ts_lessdef (ZMap.get i (ZMap.set a ts rsm)) (ZMap.get i rsm´)) →
ZMap.set a ts (ZMap.init Environment) =
ZMap.set a (Running rs) (ZMap.init Environment) →
∃ rs´,
ZMap.get a rsm´ = Running rs´
∧ regset_lessdef rs rs´.
Proof.
intros.
assert (ts = Running rs).
{
erewrite <- (ZMap.gss a ts).
erewrite <- (ZMap.gss a (Running rs)).
f_equal.
eassumption.
}
subst.
specialize (H a).
rewrite ZMap.gss in H. inv H. eauto.
Qed.
Lemma regset_lessdef_exists_eq´´´:
∀ a rsm rsm´ ts rs x,
(∀ i, ts_lessdef (ZMap.get i (ZMap.set a ts rsm)) (ZMap.get i rsm´)) →
((ts = Available ∧ x = Some rs) ∨ Running rs = ts) →
∃ rs´,
((ZMap.get a rsm´ = Available ∧ x = Some rs´) ∨
(ZMap.get a rsm´ = Running rs´))
∧ regset_lessdef rs rs´.
Proof.
intros. specialize (H a).
rewrite ZMap.gss in H.
destruct H0 as [[Ha Hrs] | Ha];
[rewrite Ha in H | rewrite <-?Ha in H];
inv H; eauto using regset_lessdef_refl.
Qed.
Lemma ts_lessdef_gss:
∀ rsm rsm´ rs rs´ a,
(∀ i, ts_lessdef (ZMap.get i rsm) (ZMap.get i rsm´)) →
ts_lessdef rs rs´ →
(∀ i, ts_lessdef (ZMap.get i (ZMap.set a rs rsm))
(ZMap.get i (ZMap.set a rs´ rsm´))).
Proof.
intros. destruct (zeq i a); subst.
- repeat rewrite ZMap.gss; auto.
- repeat rewrite ZMap.gso; auto.
Qed.
End RegsetLessdef_ThreadState.
Section RefinementLibrary.
Context `{single_link_config: SingleLinkConfiguration}.
Context `{Hmwd: UseMemWithData mem}.
Context `{data_prf : CompatData PData}.
Context `{Hstencil: Stencil}.
Context `{L: compatlayer (cdata PData)}.
Context `{ass_def: !AccessorsDefined L}.
Context `{lasmops: !LAsmAbsDataProp}.
Local Instance : ExternalCallsOps (mwd (cdata PData)) := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance : LayerConfigurationOps := compatlayer_configuration_ops L.
Opaque Z.to_nat.
Lemma ef_case:
∀ ef,
(match ef with
| EF_external id _ ⇒
if peq id thread_yield then False
else if peq id thread_sleep then False
else True
| _ ⇒ True
end)
∨ (match ef with
| EF_external id _ ⇒
if peq id thread_yield then True
else False
| _ ⇒ False
end)
∨ (match ef with
| EF_external id _ ⇒
if peq id thread_sleep then True
else False
| _ ⇒ False
end).
Proof.
intros. destruct ef; auto.
destruct (peq name thread_yield); auto.
destruct (peq name thread_sleep); auto.
Qed.
Lemma ef_id_imply:
∀ ef a b,
match ef with
| EF_external id _ ⇒
if peq id thread_yield
then False
else
if peq id thread_sleep
then False
else (a id)
| _ ⇒ b
end →
match ef with
| EF_external id _ ⇒
if peq id thread_yield
then False
else if peq id thread_sleep then False else True
| _ ⇒ True
end.
Proof.
intros. destruct ef; trivial.
destruct (peq name thread_yield). assumption.
destruct (peq name thread_sleep); trivial.
Qed.
Lemma ef_id_imply_or:
∀ ef a b,
match ef with
| EF_external id _ ⇒
if peq id thread_yield
then False
else
if peq id thread_sleep
then False
else (a id)
| _ ⇒ b
end →
b \/(∃ id sg, ef = EF_external id sg ∧ (a id)).
Proof.
intros. destruct ef; auto.
right. refine_split´; trivial.
destruct (peq name thread_yield). inv H.
destruct (peq name thread_sleep); trivial. inv H.
Qed.
Section STAR_PROP.
Variable step_prop: genv → (estate (mem:= mem)) → trace → (estate (mem:=mem)) → Prop.
Hypothesis one_step_prop:
∀ ge s1 t s2,
estep ge s1 t s2 →
step_prop ge s1 t s2.
Hypothesis prop_refl:
∀ ge s,
step_prop ge s E0 s.
Hypothesis prop_trans:
∀ ge s0 t0 s1 t1 s2 t2,
step_prop ge s0 t0 s1 →
step_prop ge s1 t1 s2 →
t2 = (t0 ** t1) →
step_prop ge s0 t2 s2.
Lemma star_step_prop:
∀ ge s1 t s2,
star estep ge s1 t s2 →
step_prop ge s1 t s2.
Proof.
induction 1; eauto.
Qed.
End STAR_PROP.
Section STAR_RSM.
Definition P_RSM (ge: genv) (s: estate (mem:= mem)) (t: trace) (s´: estate (mem:= mem)):=
∀ rsm rsm´ curid curid´ m m´ dp dp´ l l´,
s = EState curid rsm m dp l →
s´ = EState curid´ rsm´ m´ dp´ l´ →
(∀ i, ZMap.get i rsm = Environment → ZMap.get i rsm´ = Environment)
∧ (∀ i, ZMap.get i rsm = Available ∨ (∃ rs, ZMap.get i rsm = Running rs) → ZMap.get i rsm´ = Available ∨ ∃ rs, ZMap.get i rsm´ = Running rs)
∧ (∀ i, (∃ rs, ZMap.get i rsm = Running rs) → (∃ rs, ZMap.get i rsm´ = Running rs)).
Lemma one_step_rsm:
∀ ge rsm rsm´ curid curid´ m m´ dp dp´ l l´ t,
estep ge (EState curid rsm m dp l) t (EState curid´ rsm´ m´ dp´ l´) →
(∀ i, ZMap.get i rsm = Environment → ZMap.get i rsm´ = Environment)
∧ (∀ i, ZMap.get i rsm = Available ∨ (∃ rs, ZMap.get i rsm = Running rs) → ZMap.get i rsm´ = Available ∨ ∃ rs, ZMap.get i rsm´ = Running rs)
∧ (∀ i, (∃ rs, ZMap.get i rsm = Running rs) → (∃ rs, ZMap.get i rsm´ = Running rs)).
Proof.
intros. inv H; repeat apply conj; intros; eauto;
repeat
lazymatch goal with
| H : _ ∨ _ |- _ ⇒
destruct H
| H : _ ∧ _ |- _ ⇒
destruct H
| |- context [ZMap.get ?i (ZMap.set ?i´ _ _) = _] ⇒
destruct (zeq i i´); subst;
rewrite ?ZMap.gss, ?ZMap.gso by eauto
end;
try eauto;
try congruence.
Qed.
Lemma star_step_rsm´:
∀ ge s s´ t,
star estep ge s t s´ →
P_RSM ge s t s´.
Proof.
intros.
eapply star_step_prop; eauto; unfold P_RSM; intros; subst.
-
eapply one_step_rsm; eauto.
-
inv H1. eauto.
-
destruct s1.
exploit H0; eauto; clear H0.
exploit H1; eauto; clear H1.
intros.
repeat apply conj; intros.
+ destruct H1 as (HT1 & _).
destruct H0 as (HT2 & _).
eauto.
+ destruct H1 as (_ & HT1 & _).
destruct H0 as (_ & HT21 & HT22).
edestruct HT1; eauto.
+ destruct H1 as (_ & _ & HT1).
destruct H0 as (_ & _ & HT21).
eauto.
Qed.
Lemma star_step_rsm:
∀ ge rsm rsm´ curid curid´ m m´ dp dp´ l l´ t,
star estep ge (EState curid rsm m dp l) t (EState curid´ rsm´ m´ dp´ l´) →
(∀ i, ZMap.get i rsm = Environment → ZMap.get i rsm´ = Environment)
∧ (∀ i, ZMap.get i rsm = Available ∨ (∃ rs, ZMap.get i rsm = Running rs) → ZMap.get i rsm´ = Available ∨ ∃ rs, ZMap.get i rsm´ = Running rs)
∧ (∀ i, (∃ rs, ZMap.get i rsm = Running rs) → (∃ rs, ZMap.get i rsm´ = Running rs)).
Proof.
intros.
eapply star_step_rsm´; eauto.
Qed.
End STAR_RSM.
Require Import ListLemma2.
Lemma list_eq_bidirection:
∀ {A:Type} (l l´ l0 l1: list A),
l = l0 ++ l´ →
l´ = l1 ++ l →
l = l´.
Proof.
induction l; intros.
- destruct l´.
trivial. symmetry in H.
eapply list_not_e_nil in H. inv H.
- destruct l´.
+ symmetry in H0.
eapply list_not_e_nil in H0. inv H0.
+ destruct l0.
× inv H. trivial.
× inv H. destruct l1.
{
inversion H0.
eapply list_append_neq in H2. inv H2.
}
{
inversion H0.
replace (l1 ++ a1 :: l0 ++ a :: l´) with ((l1 ++ a1 :: l0) ++ a :: l´) in H2.
eapply list_append_neq in H2. inv H2.
rewrite <- app_assoc. rewrite app_comm_cons. trivial.
}
Qed.
Lemma one_step_event:
∀ ge curid curid´ rsm rsm´ m m´ dp dp´ l l´ t,
estep ge (EState curid rsm m dp l) t (EState curid´ rsm´ m´ dp´ l´) →
l´ = l ∨ (∃ e, l´ = e :: l).
Proof.
intros. inv H; try apply list_append_nil; eauto.
- eapply ef_id_imply_or in NON_YIELD.
destruct NON_YIELD as [HT | HT]; subst.
+ left; trivial.
+ destruct HT as (id & sg & _ & Hl); subst.
destruct (has_event id).
× right.
destruct Hl as (largs & choice & Hla & Hlb & Hlc).
subst; eauto.
× subst; left; trivial.
- eapply ef_id_imply_or in NON_YIELD.
destruct NON_YIELD as [HT | HT]; subst.
+ left; trivial.
+ destruct HT as (id & sg & _ & Hl); subst.
destruct (has_event id).
× right. eauto.
× subst. left; trivial.
Qed.
Section STAR_INCR.
Definition P_INCR (ge: genv) (s: estate (mem:= mem)) (t: trace) (s´: estate (mem:= mem)):=
∀ rsm rsm´ curid curid´ m m´ dp dp´ l l´,
s = EState curid rsm m dp l →
s´ = EState curid´ rsm´ m´ dp´ l´ →
∃ l0, l´ = l0 ++ l.
Lemma one_step_log_incr:
∀ ge cid cid´ rsm rsm´ m m´ dp dp´ l l´ t,
estep ge (EState cid rsm m dp l) t (EState cid´ rsm´ m´ dp´ l´) →
∃ l0, l´ = l0 ++ l.
Proof.
intros. eapply one_step_event in H.
destruct H as [HT | HT].
- subst. ∃ nil. rewrite app_nil_l; trivial.
- destruct HT as (e & HT); subst. ∃ (e:: nil). eauto.
Qed.
Lemma star_step_log_incr´:
∀ ge s t s´,
star estep ge s t s´ →
P_INCR ge s t s´.
Proof.
intros.
eapply star_step_prop; eauto; unfold P_INCR; intros; subst.
-
eapply one_step_log_incr; eauto.
-
inv H1. ∃ nil; trivial.
-
destruct s1.
exploit H0; eauto; clear H0.
intros (l1 & Hl1).
exploit H1; eauto; clear H1.
intros (l2 & Hl2). subst.
∃ (l2 ++ l1).
rewrite app_assoc. trivial.
Qed.
Lemma star_step_log_incr:
∀ ge cid cid´ rsm rsm´ m m´ dp dp´ l l´ t,
star estep ge (EState cid rsm m dp l) t (EState cid´ rsm´ m´ dp´ l´) →
∃ l0, l´ = l0 ++ l.
Proof.
intros.
eapply star_step_log_incr´; eauto.
Qed.
End STAR_INCR.
Lemma star_log_incr_nil:
∀ ge cid cid´ rsm rsm´ m m´ dp dp´ l l´ l0 t,
star estep ge (EState cid rsm m dp l) t (EState cid´ rsm´ m´ dp´ l´) →
l = l0 ++ l´ →
l0 = nil.
Proof.
intros. eapply star_step_log_incr in H.
destruct H as (l1 & Hl).
eapply list_eq_bidirection in Hl; eauto.
subst. eapply list_append_neq´ in H0. assumption.
Qed.
Lemma list_head_neq:
∀ {A: Type} l l´ (a: A),
l = a :: l´ ++ l → False.
Proof.
intros.
rewrite app_comm_cons in H.
eapply list_append_neq´ in H. inv H.
Qed.
Ltac list_append_neq_tac:=
match goal with
| H: ?l = _ ++ ?e :: ?l |- _ ⇒
eapply list_append_neq in H; inversion H
| H: ?l = ?e :: ?l |- _ ⇒
eapply list_append_neq0 in H; inversion H
| H: ?e :: ?l = ?l |- _ ⇒
symmetry in H; eapply list_append_neq0 in H; inversion H
| H: ?l = ?e :: _ ++ ?l |- _ ⇒
eapply list_head_neq in H; inversion H
| _ ⇒ idtac
end.
Section STAR_SKIP.
Definition P_SKIP (ge: genv) (s: estate (mem:= mem)) (t: trace) (s´: estate (mem:= mem)):=
∀ rsm rsm´ curid curid´ m m´ dp dp´ l,
s = EState curid rsm m dp l →
s´ = EState curid´ rsm´ m´ dp´ l →
ZMap.get curid rsm = Environment ∨ ZMap.get curid rsm = Available →
curid´ = curid ∧ rsm´ = rsm ∧ m´ = m ∧ dp´ = dp.
Lemma skip_one_step_same_log:
∀ ge curid curid´ rsm rsm´ m m´ dp dp´ l t,
estep ge (EState curid rsm m dp l) t
(EState curid´ rsm´ m´ dp´ l) →
ZMap.get curid rsm = Environment ∨ ZMap.get curid rsm = Available →
curid´ = curid ∧ rsm´ = rsm ∧ m´ = m ∧ dp´ = dp.
Proof.
intros; destruct H0; inversion H; try congruence; list_append_neq_tac.
Qed.
Lemma skip_one_step_same_log´:
∀ ge s t s´,
estep ge s t s´ →
P_SKIP ge s t s´.
Proof.
unfold P_SKIP; intros; subst.
eapply skip_one_step_same_log; eauto.
Qed.
Lemma skip_step_same_log´:
∀ ge s t s´,
star estep ge s t s´ →
P_SKIP ge s t s´.
Proof.
induction 1.
- unfold P_SKIP. intros; subst. inv H0. eauto.
- pose proof H as Hone.
eapply skip_one_step_same_log´ in Hone; eauto.
unfold P_SKIP in ×.
intros; subst.
destruct s2.
eapply star_step_log_incr in H0.
eapply one_step_log_incr in H.
destruct H0 as (? & Hl1).
destruct H as (? & Hl2).
exploit (list_eq_bidirection (A:= LogEvent)); eauto.
clear Hl1 Hl2.
intros; subst.
exploit Hone; eauto.
intros (? & ? & ? & ?); subst.
exploit IHstar; eauto.
Qed.
Lemma skip_step_same_log:
∀ ge curid curid´ rsm rsm´ m m´ dp dp´ l t,
star estep ge (EState curid rsm m dp l) t
(EState curid´ rsm´ m´ dp´ l) →
ZMap.get curid rsm = Environment ∨ ZMap.get curid rsm = Available →
curid´ = curid ∧ rsm´ = rsm ∧ m´ = m ∧ dp´ = dp.
Proof.
intros.
eapply skip_step_same_log´; eauto.
Qed.
End STAR_SKIP.
Lemma list_append_e_or:
∀ {A : Type} l l1 l2 (e: A),
e :: l = l1 ++ l2 ++ l →
(l1 = nil ∧ l2 = e::nil) ∨ (l1 = e::nil ∧ l2 = nil).
Proof.
intros. destruct l1.
- left. destruct l2.
+ simpl in H. symmetry in H.
eapply list_append_neq0 in H. inv H.
+ inversion H. eapply list_append_neq´ in H2. subst. eauto.
- inversion H. right.
rewrite app_assoc in H2.
eapply list_append_neq´ in H2.
eapply app_eq_nil in H2. destruct H2 as (? & ?); subst. eauto.
Qed.
Section STAR_LOG.
Definition P_LOG (ge: genv) (s: estate (mem:= mem)) (t: trace) (s´: estate (mem:= mem)):=
∀ rsm rsm´ curid curid´ m m´ dp dp´ l,
s = EState curid rsm m dp l →
s´ = EState curid´ rsm´ m´ dp´ l →
curid´ = curid.
Lemma one_step_log_same:
∀ ge curid curid´ rsm rsm´ m m´ dp dp´ l t,
estep ge (EState curid rsm m dp l) t
(EState curid´ rsm´ m´ dp´ l) →
curid´ = curid.
Proof.
intros. inversion H; try reflexivity; list_append_neq_tac.
Qed.
Lemma one_step_log_same´:
∀ ge s t s´,
estep ge s t s´ →
P_LOG ge s t s´.
Proof.
unfold P_LOG; intros. subst.
eapply one_step_log_same; eauto.
Qed.
Lemma star_step_log_same´:
∀ ge s t s´,
star estep ge s t s´ →
P_LOG ge s t s´.
Proof.
induction 1.
- unfold P_LOG. intros; subst. inv H0. eauto.
- pose proof H as Hone.
eapply one_step_log_same´ in Hone; eauto.
unfold P_LOG in ×.
intros; subst.
destruct s2.
eapply star_step_log_incr in H0.
eapply one_step_log_incr in H.
destruct H0 as (? & Hl1).
destruct H as (? & Hl2).
exploit (list_eq_bidirection (A:= LogEvent)); eauto.
clear Hl1 Hl2.
intros; subst.
exploit Hone; eauto.
intros; subst.
exploit IHstar; eauto.
Qed.
Lemma star_step_log_same:
∀ ge curid curid´ rsm rsm´ m m´ dp dp´ l t,
star estep ge (EState curid rsm m dp l) t
(EState curid´ rsm´ m´ dp´ l) →
curid´ = curid.
Proof.
intros. eapply star_step_log_same´; eauto.
Qed.
End STAR_LOG.
Section STAR_SPLIT.
Definition P_SPLIT (ge: genv) (s: estate (mem:= mem)) (t: trace) (s´: estate (mem:= mem)):=
∀ rsm rsm´ curid curid´ m m´ dp dp´ l e,
s = EState curid rsm m dp l →
s´ = EState curid´ rsm´ m´ dp´ (e :: l) →
∃ t0 t1 t2 rsm0 m0 dp0 rsm1 m1 dp1,
star estep ge (EState curid rsm m dp l) t0 (EState curid rsm0 m0 dp0 l)
∧ estep ge (EState curid rsm0 m0 dp0 l) t1 (EState curid´ rsm1 m1 dp1 (e :: l))
∧ star estep ge (EState curid´ rsm1 m1 dp1 (e :: l)) t2 (EState curid´ rsm´ m´ dp´ (e :: l))
∧ t0 ** t1 ** t2 = t.
Lemma one_log_append_split´´:
∀ ge curid curid´ rsm rsm´ m m´ dp dp´ l e t,
estep ge (EState curid rsm m dp l) t
(EState curid´ rsm´ m´ dp´ (e :: l)) →
∃ t0 t1 t2 rsm0 m0 dp0 rsm1 m1 dp1,
star estep ge (EState curid rsm m dp l) t0 (EState curid rsm0 m0 dp0 l)
∧ estep ge (EState curid rsm0 m0 dp0 l) t1 (EState curid´ rsm1 m1 dp1 (e :: l))
∧ star estep ge (EState curid´ rsm1 m1 dp1 (e :: l)) t2 (EState curid´ rsm´ m´ dp´ (e :: l))
∧ t0 ** t1 ** t2 = t.
Proof.
intros.
refine_split´; eauto.
- eapply star_refl.
- eapply star_refl.
- rewrite E0_left. rewrite E0_right. reflexivity.
Qed.
Lemma one_log_append_split:
∀ ge curid curid´ rsm rsm´ m m´ dp dp´ l e,
estep ge (EState curid rsm m dp l) E0
(EState curid´ rsm´ m´ dp´ (e :: l)) →
∃ rsm0 m0 dp0 rsm1 m1 dp1,
star estep ge (EState curid rsm m dp l) E0 (EState curid rsm0 m0 dp0 l)
∧ estep ge (EState curid rsm0 m0 dp0 l) E0 (EState curid´ rsm1 m1 dp1 (e :: l))
∧ star estep ge (EState curid´ rsm1 m1 dp1 (e :: l)) E0 (EState curid´ rsm´ m´ dp´ (e :: l)).
Proof.
intros.
eapply one_log_append_split´´ in H.
destruct H as (t0 & t3 & t4 & rsm1 & m2 & dp1 & rsm2 & m3 & dp2 & Hstar1 & Hone1 & Hstar2 & Htrace).
apply Eapp_E0_inv in Htrace.
destruct Htrace as (? & Htrace); subst.
apply Eapp_E0_inv in Htrace.
destruct Htrace as (? & ?); subst.
refine_split´; eauto.
Qed.
Lemma one_log_append_split´:
∀ ge s t s´,
estep ge s t s´ →
P_SPLIT ge s t s´.
Proof.
unfold P_SPLIT; intros; subst.
eapply one_log_append_split´´; eauto.
Qed.
Lemma star_log_append_split´:
∀ ge s t s´,
star estep ge s t s´ →
P_SPLIT ge s t s´.
Proof.
induction 1.
- unfold P_SPLIT. intros; subst. inversion H0.
list_append_neq_tac.
- pose proof H as Hone.
pose proof H as Hone´.
pose proof H0 as Hstar.
eapply one_log_append_split´ in Hone´; eauto.
unfold P_SPLIT in ×.
intros; subst.
destruct s2.
eapply star_step_log_incr in H0.
eapply one_step_log_incr in H.
destruct H0 as (l1 & Hl).
destruct H as (l2 & Hl2). subst.
eapply list_append_e_or in Hl.
destruct Hl as [(Hl2 & Hl1)| (Hl2 & Hl1)]; subst.
+ clear IHstar.
simpl in ×.
edestruct Hone´ as (t0 & t3 & t4 & rsm1 & m2 & dp1 & rsm2 & m3 & dp2 & Hstar1 & Hone1 & Hstar2 & Htrace); eauto.
clear Hone´ Hone. subst.
exploit (star_step_log_same ge z curid´); eauto.
intros; subst.
refine_split´; eauto.
× eapply star_trans; eauto.
× repeat rewrite Eapp_assoc. trivial.
+ clear Hone´.
simpl in ×.
edestruct IHstar as (t0 & t3 & t4 & rsm1 & m2 & dp1 & rsm2 & m3 & dp2 & Hstar1 & Hone1 & Hstar2 & Htrace); eauto.
exploit one_step_log_same; eauto.
intros; subst.
refine_split´; eauto.
× eapply star_left; eauto.
× rewrite Eapp_assoc. trivial.
Qed.
Lemma star_log_append_split:
∀ ge curid curid´ rsm rsm´ m m´ dp dp´ l e,
star estep ge (EState curid rsm m dp l) E0
(EState curid´ rsm´ m´ dp´ (e :: l)) →
∃ rsm0 m0 dp0 rsm1 m1 dp1,
star estep ge (EState curid rsm m dp l) E0 (EState curid rsm0 m0 dp0 l)
∧ estep ge (EState curid rsm0 m0 dp0 l) E0 (EState curid´ rsm1 m1 dp1 (e :: l))
∧ star estep ge (EState curid´ rsm1 m1 dp1 (e :: l)) E0 (EState curid´ rsm´ m´ dp´ (e :: l)).
Proof.
intros. exploit star_log_append_split´; eauto.
intros (t0 & t3 & t4 & rsm1 & m2 & dp1 & rsm2 & m3 & dp2 & Hstar1 & Hone1 & Hstar2 & Htrace).
apply Eapp_E0_inv in Htrace.
destruct Htrace as (? & Htrace); subst.
apply Eapp_E0_inv in Htrace.
destruct Htrace as (? & ?); subst.
refine_split´; eauto.
Qed.
End STAR_SPLIT.
Lemma regmap_None_Some:
∀ i i´ ts (rs´: regset),
ZMap.get i´ (ZMap.set i ts (ZMap.init Environment)) = Running rs´
→ i´ = i ∧ Running rs´ = ts.
Proof.
intros. destruct (zeq i i´); subst.
- rewrite ZMap.gss in H. inv H. eauto.
- rewrite ZMap.gso in H; eauto.
rewrite ZMap.gi in H. inv H.
Qed.
Lemma regmap_None_Some´:
∀ i i´ ts (rs´: regset) x,
(ZMap.get i´ (ZMap.set i ts (ZMap.init Environment)) = Available ∧
x = Some rs´) ∨
(ZMap.get i´ (ZMap.set i ts (ZMap.init Environment)) = Running rs´) →
i´ = i ∧
((ts = Available ∧ x = Some rs´) ∨
Running rs´ = ts).
Proof.
intros. destruct (zeq i i´); subst.
- rewrite ZMap.gss in H.
decompose [and or] H; eauto.
- rewrite ZMap.gso in H; eauto.
rewrite ZMap.gi in H.
decompose [and or] H; congruence.
Qed.
Lemma regmap_None_None:
∀ i i´ ts,
ZMap.get i´ (ZMap.set i ts (ZMap.init Environment)) = Environment →
ts ≠ Environment →
i´ ≠ i.
Proof.
intros. destruct (zeq i i´); subst.
- rewrite ZMap.gss in H.
congruence.
- auto.
Qed.
Lemma set_init_eq:
∀ {A: Type} (a a´: A) i rsm,
ZMap.set i a rsm = ZMap.set i a´ rsm
→ a = a´.
Proof.
intros.
assert (Heq: ZMap.get i (ZMap.set i a rsm) = ZMap.get i (ZMap.set i a´ rsm)).
{
rewrite H. reflexivity.
}
repeat rewrite ZMap.gss in Heq.
assumption.
Qed.
Lemma lastEvType_tail:
∀ l e,
lastEvType (e :: l) = Some (getLogEventType e).
Proof.
simpl; intros.
unfold lastEvType in ×. simpl in ×. trivial.
Qed.
Lemma list_append_rewrite´:
∀ {A: Type} l (a: A),
a :: l = (a:: nil) ++ l.
Proof.
intros.
rewrite <- app_comm_cons. trivial.
Qed.
Lemma star_log_incr_nil´:
∀ ge cid cid´ rsm rsm´ m m´ dp dp´ l l´ t,
star estep ge (EState cid rsm m dp (l :: l´)) t (EState cid´ rsm´ m´ dp´ l´) →
False.
Proof.
intros. rewrite list_append_rewrite´ in H.
eapply star_log_incr_nil in H; trivial. inv H.
Qed.
Lemma regsetmap_dec:
∀ curid rsm,
ZMap.get curid rsm = Environment ∨
ZMap.get curid rsm = Available ∨
(∃ rs, ZMap.get curid rsm = Running rs).
Proof.
intros. destruct (ZMap.get curid rsm); eauto.
Qed.
Lemma zmap_set_commutative:
∀ {A: Type} i i0 i1 (a b: A) r,
i0 ≠ i1 →
ZMap.get i (ZMap.set i0 a (ZMap.set i1 b r)) =
ZMap.get i (ZMap.set i1 b (ZMap.set i0 a r)).
Proof.
intros.
destruct (zeq i i0); subst.
- rewrite ZMap.gss. rewrite ZMap.gso; auto.
rewrite ZMap.gss. trivial.
- rewrite ZMap.gso; auto.
destruct (zeq i i1); subst.
+ repeat rewrite ZMap.gss. trivial.
+ repeat rewrite ZMap.gso; auto.
Qed.
Lemma ZMap_gss_forall:
∀ {A:Type} (a a´: ZMap.t A),
(∀ i,
ZMap.get i a = ZMap.get i a´) →
∀ (b: A) i0,
(∀ i,
ZMap.get i (ZMap.set i0 b a) =
ZMap.get i (ZMap.set i0 b a´)).
Proof.
intros. destruct (zeq i i0); subst.
repeat rewrite ZMap.gss. trivial.
repeat rewrite ZMap.gso; auto.
Qed.
Lemma ZMap_gss_forall´:
∀ {A:Type} (a a´: ZMap.t A) b0 i1,
(∀ i,
ZMap.get i (ZMap.set i1 b0 a) = ZMap.get i a´) →
∀ (b: A) i0,
i0 ≠ i1 →
(∀ i,
ZMap.get i (ZMap.set i1 b0 (ZMap.set i0 b a)) =
ZMap.get i (ZMap.set i0 b a´)).
Proof.
intros. destruct (zeq i i1); subst.
{
repeat rewrite ZMap.gss.
rewrite ZMap.gso; auto.
specialize (H i1).
rewrite ZMap.gss in H. trivial.
}
{
rewrite ZMap.gso; auto.
destruct (zeq i i0); subst.
{
repeat rewrite ZMap.gss. trivial.
}
{
repeat rewrite ZMap.gso; auto.
specialize (H i).
rewrite ZMap.gso in H; auto.
}
}
Qed.
Lemma ZMap_gss_eq:
∀ {A:Type} i (d d´: A) a a´,
ZMap.set i d a = ZMap.set i d´ a´ →
d´ = d.
Proof.
intros.
assert (Heq: ZMap.get i (ZMap.set i d a) = ZMap.get i (ZMap.set i d´ a´)).
{
rewrite H. trivial.
}
repeat rewrite ZMap.gss in Heq; subst.
trivial.
Qed.
Lemma ZMap_gss_domain:
∀ {A B:Type} (rsm: ZMap.t (option A)) (dp: ZMap.t (option B)),
(∀ i,
(ZMap.get i rsm = None → ZMap.get i dp = None)
∧ (ZMap.get i dp = None → ZMap.get i rsm = None)) →
∀ i0 a b,
(∀ i,
(ZMap.get i (ZMap.set i0 (Some a) rsm) = None → ZMap.get i (ZMap.set i0 (Some b) dp) = None)
∧ (ZMap.get i (ZMap.set i0 (Some b) dp) = None → ZMap.get i (ZMap.set i0 (Some a) rsm) = None)).
Proof.
intros. destruct (zeq i i0); subst.
- repeat rewrite ZMap.gss.
split; intros HF; inv HF.
- repeat rewrite ZMap.gso; auto.
Qed.
Lemma one_step_disjoint_union_log:
∀ ge m m´ m0 gm l rsm rsm0 rsm´ tid tid´ dp dp´ dp0 d curid ts e,
estep ge (EState tid rsm m dp l) E0 (EState tid´ rsm´ m´ dp´ (e :: l)) →
mem_disjoint_union m0 m gm →
(Mem.nextblock m0 ≤ Mem.nextblock m)%positive →
(∀ i, ts_lessdef (ZMap.get i (ZMap.set curid ts rsm))
(ZMap.get i rsm0)) →
(∀ i,
ZMap.get i (ZMap.set curid (Some d) dp) = ZMap.get i dp0) →
ZMap.get curid rsm = Environment →
(ZMap.get tid rsm = Available ∨
∃ rs´, ZMap.get tid rsm = Running rs´) →
∃ gm´ rsm0´ dp0´,
estep ge (EState tid rsm0 gm dp0 l) E0 (EState tid´ rsm0´ gm´ dp0´ (e :: l))
∧ mem_disjoint_union m0 m´ gm´
∧ (∀ i, ts_lessdef (ZMap.get i (ZMap.set curid ts rsm´))
(ZMap.get i rsm0´))
∧ (∀ i,
ZMap.get i (ZMap.set curid (Some d) dp´) = ZMap.get i dp0´)
∧ (Mem.nextblock m0 ≤ Mem.nextblock m´)%positive.
Proof.
intros.
assert (Htid_curid: tid ≠ curid).
{
destruct (decide (tid = curid)); auto.
destruct H5 as [? | [? ?]]; congruence.
}
eapply mem_disjoint_union_commutativity in H0.
inversion H; list_append_neq_tac; subst.
-
exploit regset_lessdef_exists_neq´; eauto.
intros (rs´1 & Hrs´1 & Hregset_lessdef).
exploit extcall_arguments_disjoint_union; eauto.
intros (args´ & Hargs & Hless).
exploit exec_external_disjoint_union´; eauto.
{ eapply ef_id_imply; eapply NON_YIELD. }
intros (gm´ & vl´ & Hexe & Hunion & Hnb & Hless´).
pose proof H4 as Hneq.
eapply regset_map_None_Some_neq in Hneq; eauto.
refine_split´.
+ edestruct (regset_lessdef_exists_eq´ (proc_id (uRData l)) (ZMap.set curid ts rsm) rsm0) as (rs´ & Hrs´ & Hrs_rs´); eauto.
{
rewrite ZMap.gso; eauto.
}
assert (rs´1 = rs´) by congruence; subst.
eapply eexec_step_external; eauto.
{ eapply regset_lessdef_eq; eauto. congruence. }
{ destruct ef; eauto.
case_eq (peq name thread_yield); intros; [subst; rewrite peq_true in NON_YIELD; contradiction |].
case_eq (peq name thread_sleep); intros; [subst; rewrite peq_true in NON_YIELD; contradiction |].
case_eq (has_event name); intros Hhas_event; rewrite peq_false in NON_YIELD; auto;
rewrite peq_false in NON_YIELD; auto; rewrite Hhas_event in NON_YIELD; auto.
destruct NON_YIELD as (largs & choice & Hlargs & Hch & Hl );
∃ largs; ∃ choice; eauto; split.
eapply val2Lval_list_lessdef; eauto.
split; eauto. }
{ intros.
exploit STACK; eauto.
eapply regset_lessdef_eq´; eauto.
intros (Hst1 & Hst2).
split; trivial.
erewrite mem_disjoint_union_nextblock_eq; eauto. }
{ eapply regset_lessdef_neq; eauto. }
{ eapply regset_lessdef_neq; eauto. }
{ erewrite <- H3.
rewrite ZMap.gso; auto. }
+ eapply mem_disjoint_union_commutativity; eauto.
+ intros.
rewrite zmap_set_commutative; auto.
eapply ts_lessdef_gss; eauto.
constructor.
regset_lessdef_solve_tac.
+ eapply ZMap_gss_forall´; eauto.
+ eauto.
-
exploit regset_lessdef_exists_neq´; eauto.
intros (rs´1 & Hrs´1 & Hregset_lessdef).
exploit exec_primitive_disjoint_union; eauto.
{ eapply ef_id_imply; eapply NON_YIELD. }
intros (gm´ & rs0´0 & Hexe & Hunion & Hnb & Hregset_less).
pose proof H4 as Hneq.
eapply regset_map_None_Some_neq in Hneq; eauto.
refine_split´.
+ eapply eexec_step_prim_call; eauto.
eapply regset_lessdef_eq; eauto. congruence.
{
erewrite <- H3.
rewrite ZMap.gso; auto.
}
+ eapply mem_disjoint_union_commutativity; eauto.
+ intros.
rewrite zmap_set_commutative; auto.
eapply ts_lessdef_gss; eauto.
constructor. assumption.
+ eapply ZMap_gss_forall´; eauto.
+ eauto.
-
exploit regset_lessdef_exists_neq´; eauto.
intros (rs´1 & Hrs´1 & Hregset_lessdef). inv H21.
refine_split´; eauto.
+ eapply mem_disjoint_union_nextblock_eq in H0; eauto.
rewrite <- H0 in ×.
eapply eexec_step_external_yield; eauto.
× generalize (H3 (proc_id (uRData l))); intros.
rewrite ZMap.gso in H6; eauto.
rewrite <- H6; eassumption.
× eapply regset_lessdef_eq; eauto. congruence.
× constructor; eauto.
× unfold state_checks.
unfold state_checks in H24.
generalize (H3 (proc_id (uRData l))); intros.
rewrite ZMap.gso in H6; eauto.
rewrite <- H6.
eauto.
+ eapply mem_disjoint_union_commutativity; eauto.
-
exploit regset_lessdef_exists_neq´; eauto.
intros (rs´1 & Hrs´1 & Hregset_lessdef).
exploit extcall_arguments_disjoint_union; eauto.
intros (args´ & Hargs´ & Hless). inv H21.
refine_split´; eauto.
+ eapply mem_disjoint_union_nextblock_eq in H0; eauto.
rewrite <- H0 in ×.
eapply eexec_step_external_sleep; eauto.
× generalize (H3 (proc_id (uRData l))); intros.
rewrite ZMap.gso in H6; eauto.
rewrite <- H6; eassumption.
× eapply regset_lessdef_eq; eauto. congruence.
× constructor; eauto.
× unfold state_checks.
unfold state_checks in H24.
generalize (H3 (proc_id (uRData l))); intros.
rewrite ZMap.gso in H6; eauto.
rewrite <- H6.
eauto.
× inv Hless. inv H8. inv H10. trivial.
+ eapply mem_disjoint_union_commutativity; eauto.
-
destruct H5 as [? | (? & Hr)]; congruence.
-
exploit regset_lessdef_exists_neq´´; eauto.
intros (rs´1 & Hrs´1 & Hregset_lessdef). inv H19.
exploit mem_disjoint_union_nextblock_eq; eauto.
intros Hnb.
refine_split´; eauto.
+ eapply mem_disjoint_union_nextblock_eq in H0; eauto.
rewrite <- Hnb in ×.
eapply eexec_step_external_yield_back; eauto.
generalize (H3 (proc_id (uRData l))); intros.
rewrite ZMap.gso in H6; eauto.
rewrite <- H6; eassumption.
+ rewrite <- Hnb.
eapply mem_disjoint_union_commutativity.
eapply mem_disjoint_union_lift_nextblock_left; eauto.
+ intros.
rewrite zmap_set_commutative; auto.
eapply ts_lessdef_gss; eauto.
constructor.
regset_lessdef_solve_tac.
+ eapply transitivity; eauto.
eapply mem_lift_nextblock_source_target_le; eauto.
Qed.
Lemma regset_map_None_Some_neq´:
∀ tid curid rsm (rs: regset),
ZMap.get tid rsm = Running rs →
ZMap.get curid rsm = Environment →
tid ≠ curid.
Proof.
red; intros; subst. congruence.
Qed.
Section STAR_DIS.
Definition P_DIS (ge: genv) (s: estate (mem:= mem)) (t: trace) (s´: estate (mem:= mem)):=
∀ rsm rsm´ tid tid´ m m´ m0 l rsm0 gm ts d dp dp´ dp0,
s = EState tid rsm m dp l →
s´ = EState tid rsm´ m´ dp´ l →
mem_disjoint_union m0 m gm →
(Mem.nextblock m0 ≤ Mem.nextblock m)%positive →
(∀ i, ts_lessdef (ZMap.get i (ZMap.set tid´ ts rsm))
(ZMap.get i rsm0)) →
(∀ i,
ZMap.get i (ZMap.set tid´ (Some d) dp) = ZMap.get i dp0) →
ZMap.get tid´ rsm = Environment →
∃ gm´ rsm0´ dp0´,
star estep ge
(EState tid rsm0 gm dp0 l) t (EState tid rsm0´ gm´ dp0´ l)
∧ mem_disjoint_union m0 m´ gm´
∧ (∀ i, ts_lessdef (ZMap.get i (ZMap.set tid´ ts rsm´))
(ZMap.get i rsm0´))
∧ (∀ i,
ZMap.get i (ZMap.set tid´ (Some d) dp´) = ZMap.get i dp0´)
∧ (Mem.nextblock m0 ≤ Mem.nextblock m´)%positive
∧ ZMap.get tid´ rsm´ = Environment.
Lemma one_step_disjoint_union:
∀ ge s1 t s2,
estep ge s1 t s2 →
P_DIS ge s1 t s2.
Proof.
unfold P_DIS; intros; subst.
eapply mem_disjoint_union_commutativity in H2.
intros. inversion H; clear H; list_append_neq_tac; subst.
-
assert (Hneq: proc_id (uRData l) ≠ tid´).
{
eapply regset_map_None_Some_neq´; eauto. }
exploit ts_lessdef_exists_neq´; try eassumption.
intros (rs´0 & Hrs´0 & Hless).
exploit exec_instr_disjoint_union; eauto.
intros (gm´ & rs0´ & Hexe & Hdis´ & Hnb & Hreg).
refine_split´.
+ eapply star_one. econstructor; eauto.
eapply regset_lessdef_eq; eauto. congruence.
{
erewrite <- H5.
rewrite ZMap.gso; auto.
}
+ eapply mem_disjoint_union_commutativity; eauto.
+ intros.
rewrite zmap_set_commutative; eauto.
eapply ts_lessdef_gss; eauto.
constructor; eauto.
+ eapply ZMap_gss_forall´; eauto.
+ eauto.
+ rewrite ZMap.gso; eauto.
-
assert (Hneq: proc_id (uRData l) ≠ tid´).
{ eapply regset_map_None_Some_neq´; eauto. }
exploit ts_lessdef_exists_neq´; try eassumption.
intros (rs´0 & Hrs´0 & Hless).
exploit (exec_external_disjoint_union (L:=L)); eauto.
{
instantiate (1:= (map rs´0 args)).
eapply regset_lessdef_imply_list_lessdef; eauto.
}
intros (gm´ & vl´ & Hexe & Hdis & Hnb & Hless´).
refine_split´.
+ eapply star_one.
eapply eexec_step_builtin; eauto.
eapply regset_lessdef_eq; eauto. congruence.
{
erewrite <- H5.
rewrite ZMap.gso; auto.
}
+ eapply mem_disjoint_union_commutativity; eauto.
+ intros.
rewrite zmap_set_commutative; eauto.
eapply ts_lessdef_gss; eauto.
constructor; eauto.
regset_lessdef_solve_tac.
+ eapply ZMap_gss_forall´; eauto.
+ eauto.
+ rewrite ZMap.gso; eauto.
-
assert (Hneq: proc_id (uRData l) ≠ tid´).
{ eapply regset_map_None_Some_neq´; eauto. }
exploit ts_lessdef_exists_neq´; try eassumption.
intros (rs´0 & Hrs´0 & Hless).
exploit annot_arguments_disjoint_union; eauto.
intros (vargs´ & Hargs & Hless_list).
exploit (exec_external_disjoint_union (L:=L)); eauto.
intros (gm´ & vl´ & Hexe & Hdis & Hnb & Hless´).
refine_split´.
+ eapply star_one.
eapply eexec_step_annot; eauto.
eapply regset_lessdef_eq; eauto. congruence.
{
erewrite <- H5.
rewrite ZMap.gso; auto.
}
+ eapply mem_disjoint_union_commutativity; eauto.
+ intros.
rewrite zmap_set_commutative; eauto.
eapply ts_lessdef_gss; eauto.
constructor; eauto.
regset_lessdef_solve_tac.
+ eapply ZMap_gss_forall´; eauto.
+ eauto.
+ rewrite ZMap.gso; eauto.
-
assert (Hneq: proc_id (uRData l) ≠ tid´).
{ eapply regset_map_None_Some_neq´; eauto. }
exploit ts_lessdef_exists_neq´; try eassumption.
intros (rs´0 & Hrs´0 & Hless).
exploit extcall_arguments_disjoint_union; eauto.
intros (vargs´ & Hargs & Hless_list).
exploit (exec_external_disjoint_union´ (L:=L)); eauto.
{ eapply ef_id_imply; eapply NON_YIELD. }
intros (gm´ & vl´ & Hexe & Hdis & Hnb & Hless´).
refine_split´.
+ eapply star_one.
eapply eexec_step_external; eauto.
{ eapply regset_lessdef_eq; eauto. congruence. }
{ destruct ef; eauto.
case_eq (peq name thread_yield); intros; [subst; rewrite peq_true in NON_YIELD; contradiction |].
case_eq (peq name thread_sleep); intros; [subst; rewrite peq_true in NON_YIELD; contradiction |].
case_eq (has_event name); intros Hhas_event; rewrite peq_false in NON_YIELD; auto;
rewrite peq_false in NON_YIELD; auto; rewrite Hhas_event in NON_YIELD; auto.
destruct NON_YIELD as (largs & choice & Hlargs & Hch & Hl);
∃ largs; ∃ choice; eauto; split.
eapply val2Lval_list_lessdef; eauto.
split; eauto. }
{
intros. exploit STACK; eauto.
eapply regset_lessdef_eq´; eauto.
intros (Hst1 & Hst2).
split; trivial.
lift_unfold.
pose proof (mem_disjoint_union_nextblock _ _ _ H2).
xomega.
}
{ eapply regset_lessdef_neq; eauto. }
{ eapply regset_lessdef_neq; eauto. }
{
erewrite <- H5.
rewrite ZMap.gso; auto.
}
+ eapply mem_disjoint_union_commutativity; eauto.
+ intros.
rewrite zmap_set_commutative; eauto.
eapply ts_lessdef_gss; eauto.
constructor; eauto.
regset_lessdef_solve_tac.
+ eapply ZMap_gss_forall´; eauto.
+ eauto.
+ rewrite ZMap.gso; eauto.
-
assert (Hneq: proc_id (uRData l) ≠ tid´).
{ eapply regset_map_None_Some_neq´; eauto. }
exploit ts_lessdef_exists_neq´; try eassumption.
intros (rs´0 & Hrs´0 & Hless).
exploit exec_primitive_disjoint_union; eauto.
{ eapply ef_id_imply; eapply NON_YIELD. }
intros (gm´ & rs0´0 & Hexe & Hunion & Hnb & Hregset_less).
refine_split´.
+ apply star_one.
eapply eexec_step_prim_call; eauto.
eapply regset_lessdef_eq; eauto. congruence.
{
erewrite <- H5.
rewrite ZMap.gso; auto.
}
+ eapply mem_disjoint_union_commutativity; eauto.
+ intros.
rewrite zmap_set_commutative; eauto.
eapply ts_lessdef_gss; eauto.
constructor; eauto.
+ eapply ZMap_gss_forall´; eauto.
+ eauto.
+ rewrite ZMap.gso; eauto.
Qed.
Lemma star_step_disjoint_union´:
∀ ge s1 t s2,
star estep ge s1 t s2 →
P_DIS ge s1 t s2.
Proof.
induction 1.
- unfold P_DIS. intros; subst. inv H0.
refine_split´; eauto.
eapply star_refl.
- pose proof H as Hone.
pose proof H as Hone´.
pose proof H0 as Hstar.
eapply one_step_disjoint_union in Hone´; eauto.
unfold P_DIS in ×.
intros; subst.
destruct s2.
eapply star_step_log_incr in H0.
eapply one_step_log_incr in H.
destruct H0 as (l1 & Hl).
destruct H as (l2 & Hl2).
eapply list_eq_bidirection in Hl; eauto. clear Hl2. subst.
eapply one_step_log_same in Hone; subst.
exploit Hone´; eauto.
intros (gm1 & rsm1 & dp1 & Hstar1 & Hdis1 & Hreg1 & Hdp1 & Hnb1 & Hnone1).
exploit IHstar; eauto.
intros (gm2 & rsm2 & dp2 & Hstar2 & Hdis2 & Hreg2 & Hdp2 & Hnb2 & Hnone2).
refine_split´; eauto.
eapply star_trans; eauto.
Qed.
Lemma star_step_disjoint_union:
∀ ge m m´ m0 gm l rsm rsm0 rsm´ tid tid´ dp dp´ dp0 ts d E0,
star estep ge
(EState tid rsm m dp l) E0 (EState tid rsm´ m´ dp´ l) →
mem_disjoint_union m0 m gm →
(Mem.nextblock m0 ≤ Mem.nextblock m)%positive →
(∀ i, ts_lessdef (ZMap.get i (ZMap.set tid´ ts rsm))
(ZMap.get i rsm0)) →
(∀ i,
ZMap.get i (ZMap.set tid´ (Some d) dp) = ZMap.get i dp0) →
ZMap.get tid´ rsm = Environment →
∃ gm´ rsm0´ dp0´,
star estep ge
(EState tid rsm0 gm dp0 l) E0 (EState tid rsm0´ gm´ dp0´ l)
∧ mem_disjoint_union m0 m´ gm´
∧ (∀ i, ts_lessdef (ZMap.get i (ZMap.set tid´ ts rsm´))
(ZMap.get i rsm0´))
∧ (∀ i,
ZMap.get i (ZMap.set tid´ (Some d) dp´) = ZMap.get i dp0´)
∧ (Mem.nextblock m0 ≤ Mem.nextblock m´)%positive
∧ ZMap.get tid´ rsm´ = Environment.
Proof.
intros. eapply star_step_disjoint_union´; eauto.
Qed.
End STAR_DIS.
Lemma list_append_e_impl:
∀ {A : Type} l (e e´: A),
(∃ l0, e :: l = l0 ++ e´::l) →
e´ = e.
Proof.
intros.
destruct H as (l0 & Heq).
destruct l0.
- inv Heq. trivial.
- inversion Heq. eapply list_append_neq in H1. inv H1.
Qed.
Section STAR_PROP2.
Variable step_prop: genv → (estate (mem:= mem)) → (estate (mem:=mem)) → Prop.
Hypothesis one_step_prop:
∀ ge s1 s2,
estep ge s1 E0 s2 →
step_prop ge s1 s2.
Hypothesis prop_refl:
∀ ge s,
step_prop ge s s.
Hypothesis prop_trans:
∀ ge s0 s1 s2,
step_prop ge s0 s1 →
step_prop ge s1 s2 →
step_prop ge s0 s2.
Lemma star_step_prop2:
∀ ge s1 s2,
star estep ge s1 E0 s2 →
step_prop ge s1 s2.
Proof.
intros ge.
eapply star_E0_ind; eauto.
Qed.
End STAR_PROP2.
Section STAR_init.
Definition P_init (ge: genv) (s: estate (mem:= mem)) (s´: estate (mem:= mem)):=
∀ ts rsm´ curid curid´ tid m m´ d dp´ l l´,
ts ≠ Environment →
s = (EState curid (ZMap.set tid ts (ZMap.init Environment)) m
(ZMap.set tid (Some d) (ZMap.init None)) l) →
s´ = EState curid´ rsm´ m´ dp´ l´ →
∃ ts0 d0,
rsm´ = ZMap.set tid ts0 (ZMap.init Environment)
∧ dp´ = ZMap.set tid (Some d0) (ZMap.init None)
∧ ts0 ≠ Environment.
Lemma one_step_init_aux:
∀ {B:Type} tid tid´ ts ts´´ ts´ ts0 (d´ d0: B),
ZMap.get tid´ (ZMap.set tid ts (ZMap.init Environment)) = ts´ →
ts ≠ Environment →
ts´ ≠ Environment →
ts´´ ≠ Environment →
ts0 ≠ Environment →
∃ ts1 d1,
ZMap.set tid´ ts´´ (ZMap.set tid ts0 (ZMap.init Environment)) =
ZMap.set tid ts1 (ZMap.init Environment) ∧
ZMap.set tid´ (Some d´) (ZMap.set tid (Some d0) (ZMap.init None)) =
ZMap.set tid (Some d1) (ZMap.init None) ∧
ts1 ≠ Environment.
Proof.
intros.
destruct (zeq tid tid´); subst.
+ repeat rewrite ZMap.set2. eauto.
+ rewrite !ZMap.gso, !ZMap.gi in *; eauto.
congruence.
Qed.
Lemma one_step_init´:
∀ ge s s´,
estep ge s E0 s´ →
P_init ge s s´.
Proof.
unfold P_init; intros. subst.
inv H;
try eapply one_step_init_aux; eauto; try congruence.
-
destruct (zeq tid (proc_id (uRData l))); subst.
+ repeat rewrite ZMap.set2.
repeat econstructor.
congruence.
+ rewrite !ZMap.gso, !ZMap.gi in *; eauto.
destruct H9 as [[? ?] | ?]; discriminate.
Qed.
Lemma one_step_init:
∀ ge ts rsm´ curid curid´ tid m m´ d dp´ l l´,
estep ge (EState curid (ZMap.set tid ts (ZMap.init Environment)) m
(ZMap.set tid (Some d) (ZMap.init None)) l) E0
(EState curid´ rsm´ m´ dp´ l´) →
ts ≠ Environment →
∃ ts0 d0,
rsm´ = ZMap.set tid ts0 (ZMap.init Environment)
∧ dp´ = ZMap.set tid (Some d0) (ZMap.init None)
∧ ts0 ≠ Environment.
Proof.
intros. eapply one_step_init´; eauto.
Qed.
Lemma star_step_init´:
∀ ge s s´,
star estep ge s E0 s´ →
P_init ge s s´.
Proof.
eapply star_step_prop2; eauto.
- eapply one_step_init´; eauto.
- unfold P_init; intros; subst.
inv H1. eauto.
- unfold P_init; intros.
destruct s1.
exploit H; eauto.
intros (ts0 & d0 & ? & ? & ?); subst.
eapply H0; eauto.
Qed.
Lemma star_step_init:
∀ ge ts rsm´ curid curid´ tid m m´ d dp´ l l´,
star estep ge (EState curid (ZMap.set tid ts (ZMap.init Environment)) m
(ZMap.set tid (Some d) (ZMap.init None)) l) E0
(EState curid´ rsm´ m´ dp´ l´) →
ts ≠ Environment →
∃ ts0 d0,
rsm´ = ZMap.set tid ts0 (ZMap.init Environment)
∧ dp´ = ZMap.set tid (Some d0) (ZMap.init None)
∧ ts0 ≠ Environment.
Proof.
intros. eapply star_step_init´; eauto.
Qed.
End STAR_init.
Definition yield_condition (tid: Z) (l: Log):=
(∃ a l´, l = a :: l´
∧ proc_id (uRData l´) = tid
∧ getLogEventType a = LogYieldTy).
Definition active_condition (tid: Z) (l: Log):=
(proc_id (uRData l) = tid ∧ lastEvType l ≠ Some LogYieldTy)
∨ yield_condition tid l.
Definition inyield_condition (l: Log) rsm :=
(∃ a l´, l = a :: l´
∧ ZMap.get (proc_id (uRData l´)) rsm ≠ Environment
∧ getLogEventType a = LogYieldTy).
Definition inactive_condition (l: Log) rsm :=
(ZMap.get (proc_id (uRData l)) rsm ≠ Environment ∧
lastEvType l ≠ Some LogYieldTy)
∨ inyield_condition l rsm.
Lemma active_condition_same_neq:
∀ i l
(Heq: proc_id (uRData l) = i)
(Hneq: lastEvType l ≠ Some LogYieldTy),
active_condition i l.
Proof.
intros. unfold active_condition. left; eauto.
Qed.
Lemma inactive_condition_diff_neq:
∀ l rsm
(Heq: ZMap.get (proc_id (uRData l)) rsm = Environment
∧ lastEvType l ≠ Some LogYieldTy),
¬ inactive_condition l rsm.
Proof.
intros. unfold inactive_condition. red; intros.
destruct Heq as (Heq & Hneq).
inv H.
- destruct H0 as (? & ?). congruence.
- destruct H0 as (a & l´ & ? & _ & Hlast); subst.
rewrite lastEvType_tail in Hneq. congruence.
Qed.
Lemma inyield_condition_false:
∀ rsm l a
(Heq: ZMap.get (proc_id (uRData l)) rsm = Environment),
¬ inyield_condition (a :: l) rsm.
Proof.
unfold inyield_condition. intros. intro HF.
destruct HF as (a0 & l´ & Heq´ & Hid & He). inv Heq´.
congruence.
Qed.
Lemma inactive_condition_false:
∀ rsm l a
(Heq: ZMap.get (proc_id (uRData l)) rsm = Environment),
¬ inactive_condition (a :: l) rsm.
Proof.
unfold inactive_condition. intros. intro HF.
destruct HF.
- destruct H as (HF1 & HF2).
rewrite lastEvType_tail in HF2.
rewrite uRData_proc_id_eq in HF1. congruence.
destruct (getLogEventType a); trivial. congruence.
- destruct H as (a0 & l´ & Heq´ & Hid & He). inv Heq´.
congruence.
Qed.
Lemma yield_condition_false:
∀ i l a
(Heq: proc_id (uRData l) ≠ i),
¬ yield_condition i (a :: l).
Proof.
unfold yield_condition. intros. intro HF.
destruct HF as (a0 & l´ & Heq´ & Hid & He). inv Heq´.
congruence.
Qed.
Lemma active_condition_false:
∀ i l a
(Heq: proc_id (uRData l) ≠ i),
¬ active_condition i (a :: l).
Proof.
unfold active_condition. intros. intro HF.
destruct HF.
- destruct H as (HF1 & HF2).
rewrite lastEvType_tail in HF2.
rewrite uRData_proc_id_eq in HF1. congruence.
destruct (getLogEventType a); trivial. congruence.
- destruct H as (a0 & l´ & Heq´ & Hid & He). inv Heq´.
congruence.
Qed.
Lemma getLogEventNB_other_false:
∀ l e nb,
lastEvType l ≠ Some LogYieldTy →
last_op l = Some e →
getLogEventNB e = Some nb →
False.
Proof.
intros.
unfold lastEvType in ×.
rewrite H0 in H.
destruct e.
destruct l0; inv H1; elim H; simpl; trivial.
Qed.
Lemma list_append_e_or´:
∀ {A : Type} l l1 (e e´: A),
e :: l = l1 ++ e´ :: l →
e = e´ ∧ l1 = nil.
Proof.
destruct l1; intros.
- simpl in H. inv H. eauto.
- inversion H.
{ list_append_neq_tac. }
Qed.
Lemma active_condition_true:
∀ i l a
(Heq: proc_id (uRData l) = i)
(Hlast: getLogEventType a = LogYieldTy),
active_condition i (a :: l).
Proof.
intros. right. unfold yield_condition.
refine_split; trivial.
Qed.
Lemma active_condition_false2:
∀ i l
(Heq: proc_id (uRData l) ≠ i)
(Hneq: lastEvType l ≠ Some LogYieldTy),
¬ active_condition i l.
Proof.
intros. unfold active_condition.
intro HF. destruct HF.
- destruct H as (HF & _). congruence.
- destruct H as (a & l´ & Heq´ & Hid & Htype); subst.
unfold lastEvType in Hneq. simpl in Hneq. congruence.
Qed.
Lemma yield_condition_false2:
∀ l i
(Hneq: lastEvType l ≠ Some LogYieldTy),
¬ yield_condition i l.
Proof.
unfold yield_condition; intros.
intro HF. destruct HF as (a & l´ & Heq & Hid & Htype); subst.
unfold lastEvType in Hneq. simpl in Hneq. congruence.
Qed.
Lemma inyield_condition_false2:
∀ l rsm
(Hneq: lastEvType l ≠ Some LogYieldTy),
¬ inyield_condition l rsm.
Proof.
unfold inyield_condition; intros.
intro HF. destruct HF as (a & l´ & Heq & Hid & Htype); subst.
unfold lastEvType in Hneq. simpl in Hneq. congruence.
Qed.
Lemma yield_condition_dec:
∀ tid l,
{yield_condition tid l} + {¬ yield_condition tid l}.
Proof.
unfold yield_condition. intros.
destruct l.
- right. intro HF. destruct HF as (a & l´ & Heq & _). inv Heq.
- destruct (zeq (proc_id (uRData l0)) tid).
+ destruct (getLogEventType l) eqn: Htype.
× left. refine_split´; trivial.
× right. intro HF.
destruct HF as (a & l´ & Heq & _ & Htype´). inv Heq. congruence.
+ right. intro HF.
destruct HF as (a & l´ & Heq & Heq´ & _). inv Heq. congruence.
Qed.
Lemma active_condition_imply_neg:
∀ tid a l
(Hnac: ¬ active_condition tid (a :: l))
(Htype : getLogEventType a = LogOtherTy),
¬ active_condition tid l ∨ yield_condition tid l.
Proof.
intros. unfold active_condition in ×.
destruct (yield_condition_dec tid l).
- right. trivial.
- left. intro HF. elim Hnac.
destruct HF; try congruence.
left. destruct H as (? & ?).
rewrite uRData_proc_id_eq; trivial.
split; trivial. unfold lastEvType; simpl; congruence.
Qed.
Lemma inyield_condition_dec:
∀ l rsm,
{inyield_condition l rsm} + {¬ inyield_condition l rsm}.
Proof.
unfold inyield_condition. intros.
destruct l.
- right. intro HF. destruct HF as (a & l´ & Heq & _). inv Heq.
- destruct (ZMap.get (proc_id (uRData l0)) rsm) eqn: Hrsm.
+ right. intro HF.
destruct HF as (a & l´ & Heq & Heq´ & _). inv Heq. congruence.
+ destruct (getLogEventType l) eqn: Htype.
× left. refine_split´; trivial. congruence.
× right. intro HF.
destruct HF as (a & l´ & Heq & _ & Htype´). inv Heq. congruence.
+ destruct (getLogEventType l) eqn: Htype.
× left. refine_split´; trivial. congruence.
× right. intro HF.
destruct HF as (a & l´ & Heq & _ & Htype´). inv Heq. congruence.
Qed.
Lemma inactive_condition_imply_neg:
∀ rsm a l
(Hnac: ¬ inactive_condition (a :: l) rsm)
(Htype : getLogEventType a = LogOtherTy),
¬ inactive_condition l rsm ∨ inyield_condition l rsm.
Proof.
intros. unfold inactive_condition in ×.
destruct (inyield_condition_dec l rsm).
- right. trivial.
- left. intro HF. elim Hnac.
destruct HF; try congruence.
left. destruct H as (? & ?).
rewrite uRData_proc_id_eq; trivial.
split; trivial. unfold lastEvType; simpl; congruence.
Qed.
Lemma le_and_trans:
∀ a b c d,
(c ≤ d) % positive →
(a ≤ c ∧ b ≤ c) % positive →
(a ≤ d ∧ b ≤ d) % positive.
Proof.
intros. destruct H0 as (? & ?).
split; xomega.
Qed.
Lemma one_step_last_nb:
∀ ge tid tid´ rsm rsm´ m m´ dp dp´ a l
(Hone: estep ge (EState tid rsm m dp l) E0
(EState tid´ rsm´ m´ dp´ (a :: l)))
(Hrsm: ZMap.get tid rsm ≠ Environment)
(Hneq: lastEvType l ≠ Some LogYieldTy)
(Ha: getLogEventType a = LogYieldTy),
Mem.nextblock m´ = last_nb (a :: l).
Proof.
intros. inversion Hone; try subst; try congruence; list_append_neq_tac.
- exploit ef_id_imply_or; try eapply NON_YIELD.
intros HT.
destruct HT as [HT2 | HT2]; list_append_neq_tac; auto.
destruct HT2 as (id & sg & Hef & Hl); subst.
destruct (has_event id); list_append_neq_tac; eauto.
destruct Hl as (largs & choice & Hlargs & Hch & Hl).
inv Hl. simpl in Ha. congruence.
- exploit ef_id_imply_or; try eapply NON_YIELD.
intros HT.
destruct HT as [HT2 | HT2]; list_append_neq_tac; auto.
destruct HT2 as (id & sg & Hef & Hl); subst.
destruct (has_event id); list_append_neq_tac; eauto.
inv Hl. simpl in Ha. congruence.
- inv H15. simpl. trivial.
- inv H15. simpl. trivial.
- inv H13. simpl in Ha. congruence.
Qed.
Lemma star_step_last_yield:
∀ ge tid tid´ rsm rsm´ m m´ dp dp´ l
(Hone: star estep ge (EState tid rsm m dp l) E0
(EState tid´ rsm´ m´ dp´ l))
(Hneq: lastEvType l = Some LogYieldTy),
m´ = m.
Proof.
intros ? ? ? ? ? ? ? ? ? ?.
generalize (eq_refl (EState tid´ rsm´ m´ dp´ l)).
generalize (eq_refl (EState tid rsm m dp l)).
generalize (EState tid´ rsm´ m´ dp´ l) at 1 3 as s´.
generalize (EState tid rsm m dp l) at 1 3 as s.
intros s s´ Hs Hs´ H Hl.
revert tid rsm m dp tid´ rsm´ m´ dp´ Hs Hs´.
induction H; try congruence.
intros tid1 rsm1 m1 dp1 tid3 rsm3 m3 dp3 Hs1 Hs3.
subst.
destruct s2 as [tid2 rsm2 m2 dp2 l2].
exploit star_step_log_incr; eauto.
intros (l23 & Heq1).
exploit one_step_log_incr; eauto.
intros (l12 & Heq2).
eapply list_eq_bidirection in Heq1; eauto. subst. clear Heq2.
inversion H; try congruence; list_append_neq_tac.
Qed.
End RefinementLibrary.