Proof.
Proof.
Proof.
Proof.
Proof.
Proof.
Proof.
Proof.
Proof.
Proof.
Proof.
Proof.
Proof.
Proof.
Proof.
fp0 are the accumulated footprints since the last switch point,
and fp are footprints recorded by current module local simulation
Proof.
Proof.
intros i fpS fpT fpS0 fpT0 spc tpc H spc'
fpS'
H0 Hatom.
destruct spc as [
sthdp stid sm sbit].
destruct spc'
as [
sthdp'
stid'
sm'
sbit'].
destruct tpc as [
tthdp ttid tm tbit].
pose proof (
tp_match _ _ _ _ _ _ _ H)
as Htp.
destruct Htp as [
Htp H'].
destruct H'.
inversion H1.
simpl in *.
subst tbit.
clear pc1 pc2 H4 H5 H1.
inversion H2.
simpl in *.
subst ttid.
clear pc1 pc2 H3 H4 H2.
inversion Htp.
subst;
simpl in *.
clear Htp.
rename H3 into Htp.
rename H0 into Hsstep.
inversion Hsstep;
subst;
simpl in *.
core-step *) {
assert (
exists scs,
ThreadPool.get_cs sthdp stid' =
Some scs /\
CallStack.top scs =
Some c)
as H_tp_scs.
{
apply get_top_in_cs;
auto. }
destruct H_tp_scs as (
scs &
H_tp_scs &
H_scs_c).
assert (
exists tc,
ThreadPool.get_top tthdp stid' =
Some tc)
as H_tp_core_tgt.
{
eapply ocs_match_top_exists;
eauto. }
destruct H_tp_core_tgt as (
tc &
H_tp_core_tgt).
assert (
exists tcs,
ThreadPool.get_cs tthdp stid' =
Some tcs /\
CallStack.top tcs =
Some tc)
as H_tp_tcs.
{
repeat solv_thread.
destruct ((
ThreadPool.content tthdp) !!
stid'); [
eexists;
split;
eauto|
discriminate]. }
destruct H_tp_tcs as (
tcs &
H_tp_tcs &
H_tcs_tc).
destruct i as [
index index_order Hwf i].
pose proof (
tp_cur_sim _ _ _ _ _ _ _ H scs H_tp_scs)
as Hlsim_cur;
simpl in Hlsim_cur.
destruct Hlsim_cur as (
tcs' &
H_tp_tcs' &
Hlsim_cur).
rewrite H_tp_tcs in H_tp_tcs'.
inversion H_tp_tcs'.
subst tcs'.
clear H_tp_tcs'.
inversion Hlsim_cur.
solv_thread'.
subst.
clear Hlsim_cur.
inversion H0.
destruct core_config_sim_current0 as (
R&
Hlsim_top&
Hmatch).
inversion H_scs_c.
subst.
inversion H_tcs_tc.
subst.
eapply (
AuxLDSim.match_tau_step _ _ _ _ _ _ _ _ _ Hlsim_top)
in Hmatch;
eauto.
destruct Hmatch as [
Hnostep |
Hplus].
{
right.
destruct Hnostep as (
i'&
Hdecr&
Hmatch).
exists (
i_wrap _ _ Hwf i').
split.
constructor;
auto.
constructor;
simpl in *.
** src_fwd *)
generalize H H_core_step GE_mod_wd_src.
clear.
intros.
specialize (
GE_mod_wd_src (
Core.i c)).
inversion GE_mod_wd_src.
apply step_forward in H_core_step.
eapply GMem.forward_trans;
eauto.
inversion H;
auto.
** tgt_fwd *)
inversion H;
auto.
** src mem inv *) {
eapply GE_mod_wd_tp_inv_mem in Hsstep;
eauto.
inversion H;
auto.
inversion H;
auto. }
** tgt mem inv *) {
inversion H;
auto. }
** tp_match *) {
split; [|
split;
constructor;
auto].
econstructor;
eauto;
simpl.
subst.
intro.
generalize H_tp_upd Htp H_tp_scs.
clear.
intros.
eapply stp_upd_ocs_match;
eauto.
}
** LFPG *) {
pose proof (
fp_match _ _ _ _ _ _ _ H).
destruct H2 as (
HLFPG&
Hfpsubs&
Hfpsubt).
split.
apply LFPG_union_S.
inversion H.
destruct fp_match0;
auto.
split;
auto.
apply FP.union2_subset.
auto. }
** tp_inv src *) {
eapply GE_mod_wd_tp_inv in Hsstep;
inversion H;
eauto. }
** tp_inv tgt *) {
inversion H;
auto. }
** sim_invs cur *) {
intros.
exists (
tc ::
tcs0).
split;
auto.
destruct scs.
exfalso.
eapply thdp_upd_get_nil_false;
eauto.
constructor.
current top sim *) {
assert (
c' =
t).
{
apply thdp_upd_get in H_tp_upd.
destruct H_tp_upd as (
c0&
cs&
H'&
H'').
solv_eq. }
subst t.
constructor.
dealing with dependent types... *)
inversion H_core_upd.
simpl in *;
subst.
exists R.
auto.
rewrite <-
sg_eq_current0.
inversion H_core_upd;
subst;
auto.
}
current tail sim *) {
assert (
scs0 =
scs).
{
apply thdp_upd_get in H_tp_upd.
destruct H_tp_upd as (?&?&?&?).
solv_eq. }
subst.
assert (
GMem.forward sm sm').
{
eapply GE_mod_wd_forward in Hsstep;
auto. }
/by step and HG we know forward and unchg_on *)
assert (
forall fi,
let:
fl := (
FLists.get_fl (
GlobEnv.freelists SGE)
fi)
in
fi <> (
Core.F c) ->
unchg_freelist fl sm sm').
{
apply step_local_eff,
LEffect_unchanged_on in H_core_step.
intros.
eapply GMem.unchanged_on_implies;
eauto.
intros.
simpl.
intro.
eapply match_HG in Hmatch;
eauto.
destruct Hmatch.
destruct H7.
unfold LDSimDefs.fpG in H7.
specialize (
H7 b).
assert (
Bset.belongsto (
FP.blocks (
FP.union fpS fpS'))
b).
{
generalize H6;
clear;
intro.
exists ofs.
solv_belongsto. }
specialize (
H7 H9);
clear H8 H9.
destruct H7.
b in S *)
unfold no_overlap in Hfl_mu_disj_src.
unfold in_fl in H5.
destruct H5.
specialize (
Hfl_mu_disj_src _ _ _ H5).
apply Hfl_mu_disj_src.
auto.
b in F *)
destruct H7,
H5.
rewrite <-
H5 in H7.
eapply (
FLists.flist_disj _ (
GlobEnv.wd_fl _ GE_wd_src))
in H4;
eauto.
destruct H4.
eapply H4;
eauto.
eapply GE_mod_wd_src;
eauto.
}
assert (
ThreadPool.inv sthdp').
{
apply GE_mod_wd_tp_inv in Hsstep;
auto.
inversion H;
auto. }
assert (
forall score',
In score'
scs ->
Core.F score' <>
Core.F c).
{
apply ThreadPool.cs_inv in H_tp_scs.
destruct H_tp_scs.
intros.
intro.
apply In_nth_error in H6.
destruct H6.
symmetry in H7.
specialize (
fid_disjoint 0%
nat (
S x)
c score'
eq_refl H6 H7).
inversion fid_disjoint.
inversion H;
auto.
}
generalize H1 H3 H4 H5 H6 GE_wd_src.
clear;
intros.
induction H1.
constructor.
specialize (
IHCallStack_sim_tail H3 H4).
econstructor;
eauto.
inversion H.
econstructor;
eauto.
destruct mem_rely_src0.
split;
auto.
eapply GMem.forward_trans;
eauto.
eapply GMem.unchanged_on_trans;
eauto.
apply H4.
/by wd GE *)
apply H6;
simpl;
auto.
apply IHCallStack_sim_tail.
intros.
apply H6.
apply in_cons.
auto.
}
}
** sim_invs other *) {
intros.
/by step and HG we know forward and unchg_on *)
assert (
GMem.forward sm sm').
{
eapply GE_mod_wd_forward in Hsstep;
auto. }
assert (
forall fi,
let:
fl := (
FLists.get_fl (
GlobEnv.freelists SGE)
fi)
in
fi <> (
Core.F c) ->
unchg_freelist fl sm sm').
{
apply step_local_eff,
LEffect_unchanged_on in H_core_step.
intros.
eapply GMem.unchanged_on_implies;
eauto.
intros.
simpl.
intro.
eapply match_HG in Hmatch;
eauto.
destruct Hmatch.
destruct H9.
unfold LDSimDefs.fpG in H9.
specialize (
H9 b).
assert (
Bset.belongsto (
FP.blocks (
FP.union fpS fpS'))
b).
{
exists ofs.
solv_belongsto. }
specialize (
H9 H11);
clear H10 H11.
destruct H9.
b in S *)
unfold no_overlap in Hfl_mu_disj_src.
unfold in_fl in H7.
destruct H7.
specialize (
Hfl_mu_disj_src _ _ _ H7).
apply Hfl_mu_disj_src.
auto.
b in F *)
destruct H7,
H9.
rewrite <-
H9 in H7.
eapply (
FLists.flist_disj _ (
GlobEnv.wd_fl _ GE_wd_src))
in H6;
eauto.
destruct H6.
eapply H6;
eauto.
eapply GE_mod_wd_src;
eauto.
}
assert (
ThreadPool.inv sthdp').
{
eapply ThreadPool.upd_top_inv;
eauto.
inversion H;
auto. }
assert (
forall score',
In score'
scs ->
Core.F score' <>
Core.F c).
{
intros.
destruct H7.
apply cs_inv in H3.
destruct H3.
apply fid_belongsto in H8.
assert (
In c (
c ::
scs0))
by (
simpl;
auto).
eapply ThreadPool.fid_belongsto in H3.
Focus 2.
apply ThreadPool.cs_inv;
eauto.
inversion H;
eauto.
unfold FLists.fbelongsto in *.
destruct H8,
H3.
rewrite <-
H7, <-
H3.
eapply FLists.thread_fl_disj in H2;
eauto.
eapply GlobEnv.wd_fl;
eauto.
}
assert (
ThreadPool.get_cs sthdp t =
Some scs).
{
generalize H2 H_tp_upd H3.
clear.
intros.
solv_thread.
destruct peq;
congruence. }
pose proof (
tp_other_sim _ _ _ _ _ _ _ H t scs tcs H2 H9 H4).
generalize H10 H5 H6 H7 H8.
clear;
intros.
destruct H10;
econstructor.
inversion H.
econstructor;
eauto.
clear core_config_sim_block0 mem_rely_tgt_block0.
destruct mem_rely_src_block0.
split.
eapply GMem.forward_trans;
eauto.
eapply unchg_freelist_trans;
eauto.
apply H6,
H8.
simpl;
auto.
clear H.
induction H0.
constructor.
inversion H.
econstructor;
eauto.
econstructor;
eauto.
destruct mem_rely_src0.
split.
eapply GMem.forward_trans;
eauto.
eapply unchg_freelist_trans;
eauto.
apply H6,
H8;
simpl;
auto.
apply IHCallStack_sim_tail;
auto.
intros.
apply H8.
destruct H1;
simpl;
auto.
}
}
{
left.
destruct Hplus as (
i'&
fpT'&
tcc'&
tm'&
Hplus&
HLfpG&
Hmatch).
assert (
exists tc',
Core.update tc tcc'
tc')
as H_tcore_upd.
{
clear.
destruct tc;
simpl in *.
exists (
Core.Build_t i tcc'
sg F).
constructor;
auto. }
destruct H_tcore_upd as (
tc'&
H_tcore_upd).
assert (
exists tthdp',
ThreadPool.update tthdp stid'
tc'
tthdp')
as H_tp_upd_tgt.
{
generalize H_tp_core_tgt H_tcore_upd.
clear;
intros.
unfold ThreadPool.get_top in H_tp_core_tgt.
assert (
exists cs,
ThreadPool.get_cs tthdp stid' =
Some cs).
{
destruct ThreadPool.get_cs;
eauto.
discriminate. }
destruct H as [
cs H].
rewrite H in H_tp_core_tgt.
assert (
exists cs',
CallStack.update cs tc'
cs').
{
destruct cs;
inversion H_tp_core_tgt.
subst.
exists (
tc'::
cs).
econstructor;
eauto. }
destruct H0 as [
cs'
H0].
eexists.
econstructor;
eauto. }
destruct H_tp_upd_tgt as [
tthdp'
H_tp_upd_tgt].
exists {|
thread_pool:=
tthdp';
cur_tid:=
stid';
gm:=
tm';
atom_bit:=
sbit'|},
fpT', (
i_wrap index index_order Hwf i'), (
FP.union fpS fpS'), (
FP.union fpT fpT').
* plus step *) /lemma, core plus step -> glob plus tau step *)
assert (
ETrace.tau_plus np_step
{|
thread_pool :=
tthdp;
cur_tid :=
stid';
gm :=
tm;
atom_bit :=
sbit' |}
fpT'
{|
thread_pool :=
tthdp';
cur_tid :=
stid';
gm :=
tm';
atom_bit :=
sbit' |})
as Htstep.
{
generalize H_tp_tcs Hplus H_tcore_upd H_tp_upd_tgt H_tp_core_tgt.
clear.
destruct tc.
do 3
intro .
inversion H_tcore_upd.
subst;
simpl in *.
generalize dependent H_tcore_upd.
generalize dependent tcs0.
generalize dependent tthdp.
induction Hplus;
intros.
constructor.
econstructor;
eauto.
eapply core_step_np_step in H.
destruct H as (?&?&?).
eapply ETrace.tau_plus_cons.
eauto.
eapply IHHplus;
eauto;
clear IHHplus.
solv_thread.
econstructor;
eauto.
econstructor;
eauto.
solv_thread.
econstructor;
eauto.
econstructor;
eauto.
solv_thread.
rewrite PMap.set2.
solv_thread.
solv_thread.
eauto.
}
split.
auto.
split.
* LFPG *)
destruct (
fp_match _ _ _ _ _ _ _ H).
destruct H3.
apply LFPG_union_T.
apply LFPG_union_S.
auto.
apply LfpG'
_subset_T with (
fpT':=
fpT')
in HLfpG.
inversion HLfpG.
apply LFPG_subset_S with (
fpS :=
FP.union fpS fpS').
split;
auto.
/lemma LDSimDefs.fpG -> fpG *)
constructor.
intros.
specialize (
H6 b).
/lemma locs belongsto bset belongsto *)
assert (
Blockset.Bset.belongsto (
FP.blocks fpT')
b).
{
exists ofs.
solv_belongsto. }
apply H6 in H8.
destruct H8;
auto.
destruct H8.
right.
unfold FLists.bbelongsto.
unfold FLists.get_tfblock,
FLists.get_block,
FLists.get_tfl in *.
/lemma by wd GE, ..*)
assert (
exists n,
FLists.get_tfid (
GlobEnv.freelists TGE)
stid'
n =
Core.F tc).
{
eapply ThreadPool.fid_belongsto.
eapply ThreadPool.cs_inv.
inversion H;
eauto.
eauto.
simpl;
auto.
}
destruct H9.
exists x0,
x.
rewrite H9.
auto.
apply FP.union2_subset.
auto.
/lemma eq subset *) {
clear.
constructor;
simpl;
intros b ofs H;
solv_belongsto. }
* match state *)
assert (
GMem.forward sm sm').
{
eapply GE_mod_wd_forward in Hsstep;
eauto. }
assert (
GMem.forward tm tm').
{
generalize Htstep GE_mod_wd_tgt;
clear;
intros.
eapply GE_mod_wd_plus_forward in Htstep;
eauto.
}
constructor;
simpl in *.
** src_fwd *)
eapply GMem.forward_trans;
eauto.
inversion H;
auto.
** tgt_fwd *)
eapply GMem.forward_trans;
eauto.
inversion H;
auto.
** src mem inv *) {
eapply GE_mod_wd_tp_inv_mem in Hsstep;
eauto.
inversion H;
auto.
inversion H;
auto.
}
** tgt mem inv *) {
eapply GE_mod_wd_plus_tp_inv_mem in Htstep;
eauto.
inversion H;
auto.
inversion H;
auto.
}
** tp_match *) {
split.
/need lemma for upd and dom_eq/ *)
econstructor;
eauto;
simpl.
intro.
eapply sttp_upd_ocs_match;
eauto.
split;
constructor;
auto.
}
** LFPG *) {
pose proof (
fp_match _ _ _ _ _ _ _ H).
destruct H4 as (
HLFPG&
Hfpsubs&
Hfpsubt).
split.
apply LFPG_union_T;
auto.
apply LFPG_union_S;
auto.
split.
destruct HLfpG.
eapply fp_match_subset_T'.
eapply fp_match_subset_S'.
eapply H4.
apply FP.union2_subset.
auto.
/ lemma x subset (x U y) *) {
clear.
constructor;
simpl;
intros b ofs H;
solv_belongsto. }
destruct HLfpG.
/ need lemma for local fpG to glob fpG *)
unfold LDSimDefs.fpG in H5.
constructor.
intros.
specialize (
H5 b).
assert (
Bset.belongsto (
FP.blocks (
FP.union fpT fpT'))
b)
by (
exists ofs;
solv_belongsto).
specialize (
H5 H7).
destruct H5;
auto.
destruct H5.
right.
unfold FLists.bbelongsto.
assert (
In tc (
tc::
tcs0))
by (
simpl;
auto).
eapply ThreadPool.fid_belongsto in H8.
unfold FLists.fbelongsto in H8.
destruct H8.
exists x0,
x.
rewrite <-
H8 in H5.
rewrite <-
H5.
unfold FLists.get_tfblock,
FLists.get_block,
FLists.get_tfl.
eauto.
eapply ThreadPool.cs_inv.
inversion H;
eauto.
auto.
*** fp subsets *)
split;
apply FP.union2_subset;
auto. }
** tp_inv src *) {
eapply GE_mod_wd_tp_inv in Hsstep;
eauto.
inversion H;
auto. }
** tp_inv tgt *) {
eapply GE_mod_wd_plus_tp_inv in Htstep;
eauto.
inversion H;
auto. }
** sim_invs cur *) {
intros.
exists (
tc' ::
tcs0).
split;
auto.
inversion H_tp_upd_tgt.
subst.
unfold ThreadPool.get_cs.
simpl.
rewrite PMap.gsspec.
destruct peq;
try congruence.
inversion H6.
subst.
rewrite H_tp_tcs in H5.
inversion H5.
auto.
destruct scs.
/need lemma for upd and thread pool dom *)
exfalso.
inversion H_tp_upd.
subst.
unfold ThreadPool.get_cs in H4.
simpl in H4.
rewrite PMap.gsspec in H4.
destruct peq;
try congruence.
inversion H4.
subst.
inversion H6.
constructor.
current top sim *) {
assert (
c' =
t).
{
inversion H_tp_upd.
subst.
unfold ThreadPool.get_cs in H4.
simpl in H4.
rewrite Maps.PMap.gsspec in H4.
destruct peq;
try congruence.
inversion H4.
subst.
inversion H6.
auto. }
subst t.
dealing with dependent types... *)
inversion H_core_upd;
inversion H_tcore_upd.
simpl in *;
subst.
constructor.
exists R.
auto.
simpl.
auto.
}
current tail sim *) {
assert (
scs0 =
scs).
{
inversion H_tp_upd.
subst.
unfold ThreadPool.get_cs in H4.
simpl in H4.
rewrite Maps.PMap.gsspec in H4.
destruct peq;
try congruence.
inversion H4.
subst.
destruct cs.
inversion H6.
inversion H6.
subst.
rewrite H_tp_scs in H5.
inversion H5.
auto. }
subst.
/by step and HG we know forward and unchg_on *)
assert (
forall fi,
let:
fl := (
FLists.get_fl (
GlobEnv.freelists SGE)
fi)
in
fi <> (
Core.F c) ->
unchg_freelist fl sm sm').
{
apply step_local_eff,
LEffect_unchanged_on in H_core_step.
intros.
eapply GMem.unchanged_on_implies;
eauto.
intros.
simpl.
intro.
eapply match_HG in Hmatch;
eauto.
destruct Hmatch.
destruct H8.
unfold LDSimDefs.fpG in H8.
specialize (
H8 b).
assert (
Bset.belongsto (
FP.blocks (
FP.union fpS fpS'))
b).
{
exists ofs.
solv_belongsto. }
specialize (
H8 H10);
clear H10 H9.
destruct H8.
b in S *)
unfold no_overlap in Hfl_mu_disj_src.
unfold in_fl in H6.
destruct H6.
specialize (
Hfl_mu_disj_src _ _ _ H6).
apply Hfl_mu_disj_src.
auto.
b in F *)
destruct H8,
H6.
rewrite <-
H6 in H8.
eapply (
FLists.flist_disj _ (
GlobEnv.wd_fl _ GE_wd_src))
in H5;
eauto.
destruct H5.
eapply H5;
eauto.
eapply GE_mod_wd_src;
eauto.
}
assert (
forall fi,
let:
fl := (
FLists.get_fl (
GlobEnv.freelists TGE)
fi)
in
fi <> (
Core.F tc) ->
unchg_freelist fl tm tm').
{
/ lemma for plus-step local-effect *)
assert (
GMem.unchanged_on (
fun b ofs => ~
Locs.belongsto (
FP.locs fpT')
b ofs)
tm tm')
as Htleffect.
{
generalize Hplus GE_mod_wd_tgt;
clear;
intros.
induction Hplus.
apply step_local_eff,
LEffect_unchanged_on in H;
auto.
eapply GMem.unchanged_on_trans with (
m2:=
m');
eauto.
eapply GMem.unchanged_on_implies;
eauto.
apply step_local_eff,
LEffect_unchanged_on in H;
eauto.
clear.
intros.
intro.
apply H.
clear H.
solv_belongsto.
eapply GMem.unchanged_on_implies;
eauto.
clear.
intros.
intro.
apply H.
clear H.
solv_belongsto.
}
intros.
eapply GMem.unchanged_on_implies;
eauto.
intros.
simpl.
intro.
generalize HLfpG H6 H7 H8 GE_wd_tgt Hfl_mu_disj_tgt.
clear ;
intros.
destruct HLfpG.
clear H.
unfold LDSimDefs.fpG in H0.
specialize (
H0 b).
assert (
Bset.belongsto (
FP.blocks (
FP.union fpT fpT'))
b).
{
exists ofs;
solv_belongsto. }
specialize (
H0 H);
clear H H8.
destruct H7.
destruct H0.
b in S *)
unfold no_overlap in Hfl_mu_disj_tgt.
specialize (
Hfl_mu_disj_tgt _ _ _ H).
apply Hfl_mu_disj_tgt.
auto.
b in F *)
destruct H0.
rewrite <-
H0 in H.
eapply (
FLists.flist_disj _ (
GlobEnv.wd_fl _ GE_wd_tgt))
in H6;
eauto.
destruct H6.
eapply H1;
eauto.
}
assert (
forall score',
In score'
scs ->
Core.F score' <>
Core.F c).
{
apply ThreadPool.cs_inv in H_tp_scs.
destruct H_tp_scs.
intros.
intro.
apply In_nth_error in H7.
destruct H7.
symmetry in H8.
specialize (
fid_disjoint 0%
nat (
S x)
c score'
eq_refl H7 H8).
inversion fid_disjoint.
inversion H;
auto.
}
assert (
forall tcore',
In tcore'
tcs0 ->
Core.F tcore' <>
Core.F tc).
{
apply ThreadPool.cs_inv in H_tp_tcs.
destruct H_tp_tcs.
intros.
intro.
apply In_nth_error in H8.
destruct H8.
symmetry in H9.
specialize (
fid_disjoint 0%
nat (
S x)
tc tcore'
eq_refl H8 H9).
inversion fid_disjoint.
inversion H;
auto.
}
assert (
ThreadPool.inv sthdp').
{
apply GE_mod_wd_tp_inv in Hsstep;
auto.
inversion H;
auto. }
assert (
ThreadPool.inv tthdp').
{
apply GE_mod_wd_plus_tp_inv in Htstep;
auto.
inversion H;
auto. }
generalize H1 H2 H3 H5 H6 H7 H8 H9 H10 GE_wd_src.
clear;
intros.
induction H1.
constructor.
specialize (
IHCallStack_sim_tail H2 H3 H5 H6).
econstructor;
eauto.
inversion H.
econstructor;
eauto.
destruct mem_rely_src0.
split;
auto.
eapply GMem.forward_trans;
eauto.
eapply GMem.unchanged_on_trans;
eauto.
specialize (
H7 sCore (
or_introl eq_refl)).
apply H5.
auto.
destruct mem_rely_tgt0.
split;
auto.
eapply GMem.forward_trans;
eauto.
eapply GMem.unchanged_on_trans;
eauto.
specialize (
H8 tCore (
or_introl eq_refl)).
apply H6.
auto.
apply IHCallStack_sim_tail;
intros.
apply H7.
apply in_cons.
auto.
apply H8.
apply in_cons.
auto.
}
}
** sim_invs other *) {
intros.
/by step and HG we know forward and unchg_on *)
assert (
forall fi,
let:
fl := (
FLists.get_fl (
GlobEnv.freelists SGE)
fi)
in
fi <> (
Core.F c) ->
unchg_freelist fl sm sm').
{
apply step_local_eff,
LEffect_unchanged_on in H_core_step.
intros.
eapply GMem.unchanged_on_implies;
eauto.
intros.
simpl.
intro.
eapply match_HG in Hmatch;
eauto.
destruct Hmatch.
destruct H10.
unfold LDSimDefs.fpG in H10.
specialize (
H10 b).
assert (
Bset.belongsto (
FP.blocks (
FP.union fpS fpS'))
b).
{
exists ofs;
solv_belongsto. }
specialize (
H10 H12);
clear H11 H12.
destruct H10.
b in S *)
unfold no_overlap in Hfl_mu_disj_src.
unfold in_fl in H8.
destruct H8.
specialize (
Hfl_mu_disj_src _ _ _ H8).
apply Hfl_mu_disj_src.
auto.
b in F *)
destruct H10,
H8.
rewrite <-
H8 in H10.
eapply (
FLists.flist_disj _ (
GlobEnv.wd_fl _ GE_wd_src))
in H7;
eauto.
destruct H7.
eapply H7;
eauto.
eapply GE_mod_wd_src;
eauto.
}
assert (
forall fi,
let:
fl := (
FLists.get_fl (
GlobEnv.freelists TGE)
fi)
in
fi <> (
Core.F tc) ->
unchg_freelist fl tm tm').
{
/ lemma for plus-step local-effect *)
assert (
GMem.unchanged_on (
fun b ofs => ~
Locs.belongsto (
FP.locs fpT')
b ofs)
tm tm')
as Htleffect.
{
generalize Hplus GE_mod_wd_tgt;
clear;
intros.
induction Hplus.
apply step_local_eff,
LEffect_unchanged_on in H;
auto.
eapply GMem.unchanged_on_trans with (
m2:=
m');
eauto.
eapply GMem.unchanged_on_implies;
eauto.
apply step_local_eff,
LEffect_unchanged_on in H;
eauto.
clear.
intros.
intro.
apply H.
clear H.
solv_belongsto.
eapply GMem.unchanged_on_implies;
eauto.
clear.
intros.
intro.
apply H.
clear H.
solv_belongsto.
}
intros.
eapply GMem.unchanged_on_implies;
eauto.
intros.
simpl.
intro.
generalize HLfpG H8 H9 H10 GE_wd_tgt Hfl_mu_disj_tgt.
clear ;
intros.
destruct HLfpG.
clear H.
unfold LDSimDefs.fpG in H0.
specialize (
H0 b).
assert (
Bset.belongsto (
FP.blocks (
FP.union fpT fpT'))
b).
{
exists ofs.
solv_belongsto. }
specialize (
H0 H);
clear H.
destruct H9.
destruct H0.
b in S *)
eapply Hfl_mu_disj_tgt;
eauto.
b in F *)
destruct H0.
solv_eq.
eapply FLists.flist_disj;
eauto.
inversion GE_wd_tgt;
eauto.
}
assert (
forall score',
In score'
scs ->
Core.F score' <>
Core.F c).
{
intros.
apply ThreadPool.cs_inv in H5.
apply ThreadPool.cs_inv in H_tp_scs.
destruct H5,
H_tp_scs.
apply fid_belongsto in H9.
assert (
In c (
c ::
scs0))
by (
simpl;
auto).
apply fid_belongsto0 in H5.
unfold FLists.fbelongsto in *.
destruct H9,
H5.
rewrite <-
H9, <-
H5.
eapply FLists.thread_fl_disj in H4;
eauto.
eapply GlobEnv.wd_fl;
eauto.
inversion H;
auto.
apply GE_mod_wd_tp_inv in Hsstep;
auto.
inversion H;
auto.
}
assert (
forall tcore',
In tcore'
tcs ->
Core.F tcore' <>
Core.F tc).
{
intros.
apply ThreadPool.cs_inv in H6.
apply ThreadPool.cs_inv in H_tp_tcs.
destruct H6,
H_tp_tcs.
apply fid_belongsto in H10.
assert (
In tc (
tc ::
tcs0))
by (
simpl;
auto).
apply fid_belongsto0 in H6.
unfold FLists.fbelongsto in *.
destruct H10,
H6.
rewrite <-
H10, <-
H6.
eapply FLists.thread_fl_disj in H4;
eauto.
eapply GlobEnv.wd_fl;
eauto.
inversion H;
auto.
apply GE_mod_wd_plus_tp_inv in Htstep;
auto.
inversion H;
auto.
}
assert (
ThreadPool.get_cs sthdp t =
Some scs).
{
generalize H_tp_upd H4 H5.
clear.
intros.
unfold ThreadPool.get_cs in *.
inversion H_tp_upd;
subst;
simpl in *.
rewrite PMap.gsspec in *.
destruct peq;
congruence.
}
assert (
ThreadPool.get_cs tthdp t =
Some tcs).
{
generalize H_tp_upd_tgt H4 H6.
clear.
intros.
unfold ThreadPool.get_cs in *.
inversion H_tp_upd_tgt;
subst;
simpl in *.
rewrite PMap.gsspec in *.
destruct peq;
congruence.
}
pose proof (
tp_other_sim _ _ _ _ _ _ _ H t _ _ H4 H11 H12).
generalize H2 H3 H4 H7 H8 H9 H10 H13.
clear;
intros.
destruct H13;
econstructor.
inversion H.
econstructor;
eauto.
destruct mem_rely_src_block0.
split.
eapply GMem.forward_trans;
eauto.
eapply unchg_freelist_trans;
eauto.
apply H7,
H9.
simpl;
auto.
destruct mem_rely_tgt_block0.
split.
eapply GMem.forward_trans;
eauto.
eapply unchg_freelist_trans;
eauto.
apply H8,
H10.
simpl;
auto.
clear H.
induction H0.
constructor.
econstructor;
eauto.
inversion H.
econstructor;
eauto.
destruct mem_rely_src0.
split.
eapply GMem.forward_trans;
eauto.
eapply unchg_freelist_trans;
eauto.
apply H7,
H9.
simpl;
auto.
destruct mem_rely_tgt0.
split.
eapply GMem.forward_trans;
eauto.
eapply unchg_freelist_trans;
eauto.
apply H8,
H10;
simpl;
auto.
apply IHCallStack_sim_tail;
auto.
intros.
apply H9.
destruct H1;
simpl;
auto.
intros.
apply H10.
destruct H1;
simpl;
auto.
}
}
}
call ext *) {
left.
destruct i eqn:
Hi.
arguments related arg_rel (inj mu) args args' *)
assert (
exists scs,
ThreadPool.get_cs sthdp stid' =
Some (
c ::
scs))
as H_tp_cs.
{
generalize H_tp_core;
clear;
intro.
unfold ThreadPool.get_top in H_tp_core.
destruct ThreadPool.get_cs;
inversion H_tp_core.
unfold CallStack.top in H0.
destruct t;
inversion H0.
eauto. }
decompose_ex H_tp_cs.
destruct (
tp_cur_sim _ _ _ _ _ _ _ H _ H_tp_cs)
as (
tcs &
H_tp_cs' &
Hsim_cur_cs).
destruct tcs as [ |
tc ]; [
inversion Hsim_cur_cs | ].
inversion Hsim_cur_cs;
subst.
rename H9 into Hsim_cur_other.
clear Hsim_cur_cs.
assert (
ThreadPool.get_top tthdp stid' =
Some tc)
as H_tp_core'.
{
unfold ThreadPool.get_top.
rewrite H_tp_cs';
auto. }
destruct H8 as [
core_config_sim Hsg].
destruct core_config_sim as [
R_top [
Hldsim_top Hmatch_top] ].
pose proof Hldsim_top as Hldsim_top'.
eapply match_at_external in Hldsim_top;
eauto.
destruct Hldsim_top as [
GARG [
i0' [
args'
Hldsim_top] ] ].
destruct Hldsim_top as (
H_core_atext' &
Hargs &
HLG &
match_top').
destruct tc eqn:
Htc;
simpl in *.
by simulation on modules in SGE and TGE,
we could init a related target core *)
set (
ThreadPool.next_fmap sthdp stid')
as sfnum.
set (
FLists.get_tfid (
GlobEnv.freelists SGE)
stid'
sfnum)
as sfid.
set (
ThreadPool.next_fmap tthdp stid')
as tfnum.
set (
FLists.get_tfid (
GlobEnv.freelists TGE)
stid'
tfnum)
as tfid.
destruct (
HGE_sim funid new_ix sfid tfid H_mod_id)
as
(
new_ix' &
H_mod_id' &
Hmod_sim_new).
destruct Hmod_sim_new as (
index' &
index_order' &
R_new &
Hmod_sim_new).
edestruct (
Hmod_sim_new funid args args')
as (
tcc'' &
H_new_core' &
Htmp);
eauto.
exploit (
Htmp sm_init tm_init).
{
inversion H_init_sm.
eauto. }
{
inversion H_init_tm.
eauto. }
{
constructor;
auto.
eapply FLists.freelist_norepeat;
eauto.
eapply GlobEnv.wd_fl;
eauto.
eapply FLists.freelist_norepeat;
eauto.
eapply GlobEnv.wd_fl;
eauto. }
{
instantiate (2:=
sm').
instantiate (1:=
tm).
inversion HLG.
inversion H0.
constructor;
auto.
constructor;
auto.
inv H;
auto.
TODO: lemma : freelist free -> unchg_freelist
apply freelist_free_unchg_freelist;
auto.
inv H.
inv fl_inv_src0.
eauto.
eapply match_HG in Hmatch_top;
eauto.
destruct Hmatch_top.
destruct H5.
auto.
constructor;
auto.
inv H;
auto.
apply freelist_free_unchg_freelist;
auto.
inv H.
inv fl_inv_tgt0.
eauto.
}
intros (
i0'' &
Hsim_new &
Hmatch_new).
eapply match_init
inversion H. eapply ThreadPool.tp_valid_freelist_free; eauto.
inversion H. eapply ThreadPool.tp_valid_freelist_free; eauto.
eapply FLists.freelist_norepeat; eauto. eapply GlobEnv.wd_fl; eauto.
eapply FLists.freelist_norepeat; eauto. eapply GlobEnv.wd_fl; eauto.
eapply match_HG; eauto. }
H_init_sm H_init_tm). sm' tm) as (index' & index_order' & R_new & i0'' &
Hsim_new & Hmatch_new); eauto.
*)
clear Htmp.
assert (
exists tthdp'',
ThreadPool.push tthdp stid'
new_ix'
tcc''
sg =
Some tthdp'')
as H_tp_push'.
{
generalize H_tp_core'.
clear.
intro.
repeat solv_thread'. }
destruct H_tp_push'
as [
tthdp''
H_tp_push''].
exists ([[
tthdp'',
stid',
tm,
O ]]),
FP.emp.
unshelve eexists (
i_wrap index'
index_order'
_ i0'').
{
eapply AuxLDSim.index_wf;
eauto. }
exists FP.emp,
FP.emp.
assert (
tau_plus np_step
{|
thread_pool :=
tthdp;
cur_tid :=
stid';
gm :=
tm;
atom_bit :=
O |}
FP.emp
{|
thread_pool :=
tthdp'';
cur_tid :=
stid';
gm :=
tm;
atom_bit :=
O |})
as Htplus.
{
eapply tau_plus_1.
eapply Call with (
c1:= (<<
i,
c0,
sg0,
F >>));
eauto. }
split;
auto.
split.
{
* LFPG *)
destruct (
fp_match _ _ _ _ _ _ _ H).
destruct H1.
apply LFPG_union.
auto.
clear.
constructor.
constructor;
constructor;
intros;
inversion H0.
apply fpG_emp.
}
{
constructor;
simpl in *.
** src_fwd *)
inversion H;
auto.
** tgt_fwd *)
inversion H;
auto.
** src mem inv *) {
eapply GE_mod_wd_tp_inv_mem in Hsstep;
eauto.
inversion H;
auto.
inversion H;
auto.
}
** tgt mem inv *) {
eapply GE_mod_wd_plus_tp_inv_mem in Htplus;
eauto.
simpl.
inversion H;
auto.
simpl.
inversion H;
auto.
}
** tp_match *) {
split; [|
split;
constructor;
auto].
/need lemma for upd and dom_eq/ *)
econstructor;
eauto;
simpl.
intro t.
generalize H_tp_push,
H_tp_push'',
H.
clear;
intros.
apply tp_match in H.
destruct H as [?
_].
inversion H;
subst.
unfold ThreadPool.get_cs in *;
simpl in *.
specialize (
H2 t).
eapply tp_push_ocs_match in H2;
eauto.
}
** LFPG *) {
pose proof (
fp_match _ _ _ _ _ _ _ H).
destruct H0 as (
HLFPG&
Hfpsubs&
Hfpsubt).
split.
apply LFPG_union.
auto.
clear.
constructor.
constructor;
constructor;
intros;
inversion H0.
apply fpG_emp.
clear.
split;
constructor;
intros b ofs H;
solv_belongsto.
}
** tp_inv src *) {
eapply GE_mod_wd_tp_inv in Hsstep;
eauto.
inversion H;
auto. }
** tp_inv tgt *) {
eapply GE_mod_wd_plus_tp_inv in Htplus;
eauto.
inversion H;
auto. }
** sim_invs cur *) {
intros.
inversion H_tp_push.
unfold ThreadPool.push in H2.
unfold ThreadPool.get_cs in H_tp_cs,
H0.
rewrite H_tp_cs in H2.
inversion H2;
subst;
clear H2;
simpl in *.
rewrite PMap.gsspec in H0.
destruct peq; [|
contradiction].
inversion H0;
clear H0;
subst.
unfold CallStack.push.
unfold ThreadPool.push in H_tp_push''.
exists ({|
Core.c:=
tcc'';
Core.sg:=
sg;
Core.F:=
FLists.get_tfid (
GlobEnv.freelists TGE)
stid'
(
ThreadPool.next_fmap tthdp stid') |}
:: {|
Core.c:=
c0;
Core.sg:=
Core.sg c;
Core.F:=
F |} ::
tcs).
split.
{
generalize H_tp_push'',
H_tp_cs'.
clear.
intros.
solv_thread'.
solv_pmap.
auto.
discriminate. }
constructor.
current top sim *) {
constructor;
simpl in *;
auto.
eexists;
eauto. }
current tail sim *) {
caller core *)
econstructor;
eauto.
econstructor.
eexists.
eauto.
split;[
apply GMem.forward_refl|
apply GMem.unchanged_on_refl].
split;[
apply GMem.forward_refl|
apply GMem.unchanged_on_refl].
auto.
}
}
** sim_invs other *) {
intros.
/by step and HG we know forward and unchg_on *)
assert (
ThreadPool.get_cs sthdp t =
Some scs0).
{
generalize H_tp_push H0 H1.
clear.
intros.
solv_thread'.
solv_pmap.
auto. }
assert (
ThreadPool.get_cs tthdp t =
Some tcs0).
{
generalize H_tp_push''
H0 H2.
clear.
intros.
solv_thread';
solv_pmap;
auto. }
pose proof (
tp_other_sim _ _ _ _ _ _ _ H t _ _ H0 H3 H4).
generalize H1 H2 H5.
clear;
intros.
destruct H5;
econstructor;
eauto.
}
}
}
return *) {
left.
assert (
exists scs,
ThreadPool.get_cs sthdp stid' =
Some (
c ::
c' ::
scs))
as H_tp_scs.
{
apply get_top_in_cs in H_tp_core;
auto.
destruct H_tp_core as (
cs &
Htpcs &
Htop).
destruct cs;
inversion Htop.
subst.
unfold ThreadPool.pop in H_tp_pop.
unfold ThreadPool.get_cs in Htpcs.
rewrite Htpcs in H_tp_pop;
simpl in *.
inversion H_tp_pop;
subst.
unfold ThreadPool.get_top,
ThreadPool.get_cs in H_tp_caller;
simpl in *.
rewrite PMap.gsspec in H_tp_caller.
destruct peq; [|
contradiction].
destruct cs;
inversion H_tp_caller;
subst.
exists cs;
auto.
}
destruct H_tp_scs as (
scs &
H_tp_scs).
assert (
exists tc tc'
tcs,
ThreadPool.get_cs tthdp stid' =
Some (
tc ::
tc' ::
tcs))
as H_tp_tcs.
{
apply tp_match in H.
destruct H as [
H _].
inversion H;
subst.
specialize (
H2 stid');
inversion H2.
congruence.
solv_eq;
subst;
repeat match goal with
|
H:
cs_match (
cons _ _)
_ |-
_ =>
inversion H;
subst;
clear H
|
H:
CallStack.is_emp (
cons _ _) |-
_ =>
inversion H
end.
repeat eexists;
eauto. }
destruct H_tp_tcs as (
tc &
tc' &
tcs &
H_tp_tcs).
destruct i as [
index index_order Hwf i].
pose proof (
tp_cur_sim _ _ _ _ _ _ _ H _ H_tp_scs)
as Hlsim_cur;
simpl in Hlsim_cur.
destruct Hlsim_cur as (
tcs' &
H_tp_tcs' &
Hlsim_cur).
rewrite H_tp_tcs in H_tp_tcs'.
inversion H_tp_tcs'.
subst tcs'.
clear H_tp_tcs'.
inversion Hlsim_cur as
[|
sCore sm tCore tm0 scs0 tcs0 H0 H1'
Hsim_cur_top Hsim_cur_other H3 H2'].
subst.
clear Hlsim_cur.
inversion Hsim_cur_top.
destruct core_config_sim_current0 as (
R&
Hlsim_top&
Hmatch).
pose proof Hmatch as Hmatch'.
eapply (
AuxLDSim.match_halt _ _ _ _ _ _ _ _ _ Hlsim_top)
in Hmatch;
eauto.
destruct tc as [
tix_top tcc sg F]
eqn:
Htc;
simpl in *.
destruct Hmatch as (
H_res_src &
resT &
H_core_halt' &
Hres_rel &
HLG).
inversion Hsim_cur_other as
[|
sm0 tm0 sm tm1 scs0 tcs0 index0 index_order0 i0
sCore tCore Hsim_caller Hsim_cur_other'
H0 H1'
H3 H2'].
subst.
clear Hsim_cur_other.
construct return step in target *)
inversion Hsim_caller.
clear Hsim_caller.
destruct core_config_sim0 as (
R_caller &
Hsim_caller &
Hmatch_caller).
auto.
pose proof Hsim_caller as Hcaller_after_sim.
eapply match_after_external in Hcaller_after_sim;
eauto.
instantiate (1:=
res_sg (
Core.sg c)
resT)
in Hcaller_after_sim.
Focus 2.
destruct (
res_sg _ res)
eqn:
Htmp;
simpl;
auto.
inversion Htmp.
unfold res_sg in H1.
destruct AST.sig_res;
congruence.
destruct Hcaller_after_sim as (
tcc'' &
H_core_aftext' &
Hmatch_after).
TODO:
1. is signature preserved across all compilation passes ?
A: propably yes, at leat for Selection.v
2. if so, need additional condition in Config_sim for eq_sig
3. what about the entry signature? main_sg?
A: seems it does not matter what signature is recoreded in the bottom core,
both source and target program could initialize the core with [ sg_main ].
4. Do we need additional conditions in mod_lsim?
A: no, signature checks only return values when a core halts. mod_lsim
deals with core initialization, has nothing to do with sg.
*)
TODO:
It seems that the has_type relation is not preserved by value injection ...
Sol:
1. we could add condition on returning type?
i.e.
halted c = Some (v, typ) -> has_type v typ /\
check typ when returning in globsem /\
require return type matches in simulation
need lemma for:
res_has_type res ty ->
val_inj res res' ->
res_has_type res' ty *)
Solved:
additional type information in interaction semantics *)
assert (
exists tthdp',
ThreadPool.pop tthdp stid' =
Some tthdp').
{
generalize H_tp_tcs.
clear.
intros.
solv_thread'. }
destruct H0 as [
tthdp'
H_tp_pop'].
assert (
exists tthdp'',
ThreadPool.update tthdp'
stid'
{|
Core.c:=
tcc'';
Core.sg :=
Core.sg tc';
Core.F :=
Core.F tc' |}
tthdp'').
{
generalize H_tp_pop'
H_tp_tcs.
clear.
intros.
solv_thread'.
eexists.
econstructor;
eauto.
solv_thread.
repeat (
econstructor;
eauto). }
destruct H0 as [
tthdp''
H_tp_upd'].
assert (
np_step {|
thread_pool :=
tthdp;
cur_tid :=
stid';
gm :=
tm;
atom_bit :=
O|}
tau FP.emp
{|
thread_pool :=
tthdp'';
cur_tid :=
stid';
gm :=
tm;
atom_bit :=
O|}
)
as Htreturn.
{
inversion H_tp_upd'
as [
cs cs'
thdp'0
H0'
H1'
H2'
H3'].
inversion H1'
as [
c0 cs0 cc c'0
H0''
H1''
H2''
H3''].
subst;
simpl in *.
eapply Return with (
c1:=(<<
tix_top,
tcc,
Core.sg c,
F>>));
eauto.
{
find_relatives tthdp.
clear.
intros.
solv_thread'. }
{
find_relatives tthdp'.
clear;
intros.
solv_thread'.
solv_pmap.
congruence. }
{
simpl.
dependent types....... *)
assert (
tc' =
c0).
{
generalize H0'
H_tp_pop'
H_tp_tcs.
clear.
intros.
solv_thread'.
solv_pmap.
congruence. }
subst c0.
constructor.
auto.
}
}
assert (
well_founded index_order0)
as wf0.
{
inversion Hsim_caller;
auto. }
destruct (
Hmatch_after sm'
tm)
as (
i0' &
Hmatch_caller').
{
eapply match_HG in Hlsim_top;
eauto.
generalize Hlsim_top HLG mem_rely_src0 mem_rely_tgt0;
clear;
intros.
destruct mem_rely_src0,
mem_rely_tgt0,
HLG,
Hlsim_top.
destruct H3,
H6.
constructor;
auto;
constructor;
auto. }
clear Hmatch_after.
eexists _,
FP.emp, (
i_wrap _ _ wf0 i0'),
FP.emp,
FP.emp.
split.
econstructor;
eauto.
split.
do 2
rewrite fp_union_emp_r.
apply fp_match in H.
destruct H.
auto.
sim *)
do 2
rewrite fp_union_emp_r.
constructor;
simpl.
{
inversion H;
auto. }
{
inversion H;
auto. }
{
inversion H;
eapply GE_mod_wd_tp_inv_mem in Hsstep;
eauto. }
{
inversion H;
eapply GE_mod_wd_tp_inv_mem in Htreturn;
eauto. }
{
split; [|
split;
constructor;
auto].
econstructor;
eauto;
simpl.
apply tp_match in H;
destruct H as [
H _].
generalize H H_tp_pop H_tp_upd H_tp_pop'
H_tp_upd'
H_tp_scs H_tp_tcs;
clear;
intros.
inversion H;
simpl in *;
subst.
eapply sttp_upd_ocs_match; [|
eauto|
eauto].
eapply tp_pop_ocs_match in H2;
eauto.
}
{
??? the same routine with the caller sim case
split; [|
clear;
split;
constructor;
intros b ofs H;
inversion H].
apply fp_match in H.
destruct H;
auto.
}
tp invs
{
eapply GE_mod_wd_tp_inv in Hsstep;
inversion H;
eauto. }
{
inversion H;
eapply GE_mod_wd_tp_inv in Htreturn;
eauto;
eapply GE_mod_wd_star_tp_inv in Htstar';
eauto. }
sim cur
{
intros.
solv_eq.
assert (
ThreadPool.get_cs sthdp'
stid' =
Some (
c'' ::
scs)).
{
generalize H_tp_scs,
H_tp_pop,
H_tp_upd.
clear.
intros.
solv_thread'.
solv_pmap.
inversion H.
auto. }
assert (
ThreadPool.get_cs tthdp''
stid' =
Some ({|
Core.c:=
tcc'';
Core.sg:=
Core.sg tc';
Core.F :=
Core.F tc' |} ::
tcs)).
{
find_relatives tthdp''.
clear;
intros.
solv_thread'.
solv_pmap.
f_equal.
congruence. }
eexists;
split;
eauto.
rewrite H1 in H0.
inversion H0;
clear H0.
subst.
constructor.
{
why do i have to deal with dependent types? *)
destruct c'
as [
i_c'
c_c'
sg_c'
F_c'].
destruct c''
as [
i_c''
c_c''
sg_c''
F_c''].
assert (
i_c' =
i_c'' /\
F_c' =
F_c'' /\
sg_c' =
sg_c'').
{
generalize H_core_upd;
clear;
intro H;
inversion H;
simpl in *.
inversion H0.
auto. }
destruct H0 as [
H0 [
H3 H4] ];
subst i_c''
F_c'';
simpl in *.
assert (
c_c'' =
cc'').
{
inversion H_core_upd.
subst.
inversion H0.
rewrite eq_sigT_iff_eq_dep in H4.
apply Eqdep.EqdepTheory.eq_dep_eq in H4.
trivial. }
subst c_c''
sg_c''.
constructor;
simpl in *;
auto.
exists R_caller.
split;
auto.
}
{
assumption.
}
}
sim other
{
intros.
assert (
ThreadPool.get_cs sthdp'
t =
ThreadPool.get_cs sthdp t).
{
generalize H_tp_upd,
H_tp_pop,
H0;
clear;
intros.
solv_thread'.
solv_pmap.
auto. }
assert (
ThreadPool.get_cs tthdp''
t =
ThreadPool.get_cs tthdp t).
{
generalize H_tp_upd',
H_tp_pop',
H0;
clear;
intros.
solv_thread'.
solv_pmap.
auto. }
eapply tp_other_sim in H.
generalize H2 H3 H4 H0 H1 H.
clear;
intros.
eapply H;
eauto;
congruence.
}
ores_rel
generalize Hres_rel.
clear;
intros.
unfold ores_rel,
res_sg.
destruct (
Core.sg c);
simpl in *.
destruct sig_res;
auto.
}
halt *) {
left.
assert (
ThreadPool.get_cs sthdp stid' =
Some (
c ::
nil))
as H_tp_scs.
{
generalize H_tp_core H_tp_pop H_thread_halt;
clear;
intros.
solv_thread'.
solv_pmap.
inversion H.
auto. }
assert (
exists tc,
ThreadPool.get_cs tthdp stid' =
Some (
tc ::
nil))
as H_tp_tcs.
{
apply tp_match in H.
destruct H as [
H _].
inversion H;
subst.
specialize (
H2 stid');
inversion H2.
congruence.
solv_eq;
subst.
inversion H3;
subst.
inversion H0.
eexists;
eauto.
inversion H6.
subst.
inversion H4.
auto. }
destruct H_tp_tcs as (
tc &
H_tp_tcs).
destruct i as [
index index_order Hwf i].
pose proof (
tp_cur_sim _ _ _ _ _ _ _ H _ H_tp_scs)
as Hlsim_cur;
simpl in Hlsim_cur.
destruct Hlsim_cur as (
tcs' &
H_tp_tcs' &
Hlsim_cur).
rewrite H_tp_tcs in H_tp_tcs'.
inversion H_tp_tcs'.
subst tcs'.
clear H_tp_tcs'.
inversion Hlsim_cur as
[|
sCore sm tCore tm0 scs0 tcs0 H0 H1'
Hsim_cur_top Hsim_cur_other H3 H2'].
subst.
clear Hlsim_cur.
inversion Hsim_cur_top.
destruct core_config_sim_current0 as (
R&
Hlsim_top&
Hmatch).
pose proof Hmatch as Hmatch'.
eapply (
AuxLDSim.match_halt _ _ _ _ _ _ _ _ _ Hlsim_top)
in Hmatch;
eauto.
destruct tc as [
tix_top tcc sg F]
eqn:
Htc;
simpl in *.
destruct Hmatch as (
H_res_src &
resT &
H_core_halt' &
Hres_rel &
HLG).
construct return step in target *)
assert (
exists tthdp',
ThreadPool.pop tthdp stid' =
Some tthdp').
{
generalize H_tp_tcs.
clear.
intros.
solv_thread'. }
destruct H0 as [
tthdp'
H_tp_pop'].
assert (
ThreadPool.halted tthdp'
stid')
as H_therad_halt.
{
find_relatives tthdp'.
clear.
intros.
solv_thread'.
econstructor;
eauto;
solv_thread'.
solv_pmap.
eauto. }
assert (
forall t',
ThreadPool.valid_tid tthdp'
t' ->
ThreadPool.halted tthdp'
t')
as H_all_thread_halted'.
{
assert (
ThreadPool.inv sthdp').
{
inversion H.
eapply ThreadPool.pop_inv;
eauto. }
assert (
ThreadPool.inv tthdp').
{
inversion H.
eapply ThreadPool.pop_inv;
eauto. }
intro.
rewrite valid_tid_get_cs;
auto.
destruct 1
as (
cs' &
Hcs').
generalize H H_all_thread_halted H_thread_halt H_tp_pop H_tp_pop'
Hcs'
H0.
clear;
intros.
apply tp_match in H.
destruct H as [
H _].
inversion H;
subst.
eapply tp_pop_ocs_match with (
i:=
t')
in H3;
eauto.
eapply ThreadPool.Halted;
eauto.
rewrite Hcs'
in H3.
inversion H3.
subst.
inversion H4; [
auto|].
subst.
exfalso.
clear H2 H4.
assert (
ThreadPool.valid_tid sthdp'
t').
{
rewrite valid_tid_get_cs;
auto.
rewrite <-
H1.
eauto. }
apply H_all_thread_halted in H2.
inversion H2.
inversion H5.
subst.
congruence.
}
assert (
np_step {|
thread_pool :=
tthdp;
cur_tid :=
stid';
gm :=
tm;
atom_bit :=
O|}
tau FP.emp
{|
thread_pool :=
tthdp';
cur_tid :=
stid';
gm :=
tm;
atom_bit :=
O|}
)
as Htreturn.
{
eapply Halt with (
c0:=
tc);
subst;
eauto.
generalize H_tp_tcs;
clear;
intros;
solv_thread'. }
eexists _,
FP.emp, (
i_wrap _ _ Hwf i),
FP.emp,
FP.emp.
split.
econstructor;
eauto.
split.
do 2
rewrite fp_union_emp_r.
apply fp_match in H.
destruct H.
auto.
sim *)
do 2
rewrite fp_union_emp_r.
constructor;
simpl.
{
inversion H;
auto. }
{
inversion H;
auto. }
{
inversion H;
eapply GE_mod_wd_tp_inv_mem in Hsstep;
eauto. }
{
inversion H;
eapply GE_mod_wd_tp_inv_mem in Htreturn;
eauto. }
{
split; [|
split;
constructor;
auto].
econstructor;
eauto;
simpl.
apply tp_match in H;
destruct H as [
H _].
generalize H H_tp_pop H_tp_pop'
H_tp_scs H_tp_tcs;
clear;
intros.
inversion H;
simpl in *;
subst.
eapply tp_pop_ocs_match in H2;
eauto.
}
{
WTF??? the same routine with the caller sim case
split; [|
clear;
split;
constructor;
intros b ofs H;
inversion H].
apply fp_match in H.
destruct H;
auto.
}
tp invs
{
eapply GE_mod_wd_tp_inv in Hsstep;
inversion H;
eauto. }
{
inversion H;
eapply GE_mod_wd_tp_inv in Htreturn;
eauto;
eapply GE_mod_wd_star_tp_inv in Htstar';
eauto. }
sim cur
{
intros.
exists nil.
split.
find_relatives tthdp';
clear;
intros.
solv_thread'.
assert (
scs =
nil)
by (
find_relatives sthdp';
clear;
intros;
solv_thread').
subst.
econstructor.
auto.
}
sim other
{
intros.
assert (
ThreadPool.get_cs sthdp'
t =
ThreadPool.get_cs sthdp t).
{
generalize H_tp_pop,
H0;
clear;
intros.
solv_thread'.
solv_pmap.
auto. }
assert (
ThreadPool.get_cs tthdp'
t =
ThreadPool.get_cs tthdp t).
{
generalize H_tp_pop',
H0;
clear;
intros.
solv_thread'.
solv_pmap.
auto. }
eapply tp_other_sim in H.
generalize H2 H3 H4 H0 H1 H.
clear;
intros.
eapply H;
eauto;
congruence.
}
}
Qed.
Proof.
Proof.
Proof.