From mathcomp.ssreflect Require Import fintype ssrnat.
Require Import Coqlib Maps Axioms.
Require Import AST Integers Floats Values Events Globalenvs Smallstep.
Require Import Locations Stacklayout Conventions.
Require Import CUAST.
Require Import Footprint GMemory FMemory.
Require Import GAST GlobDefs ETrace Blockset DRF.
Require Import Languages.
Require Import GlobSemantics RGRels ClientSim ObjectSim.
Require Import ASM_local.
Require Import AsmLang.
Require Import InteractionSemantics.
Lemma taustar_etrace_star:
forall State step (
s s':
State)
fp,
tau_star step s fp s' ->
exists ls,
ETrace.star step s ls fp s'.
Proof.
induction 1. eexists. econstructor.
destruct IHtau_star. eexists. econstructor; eauto.
Qed.
Lemma etrace_star_star:
forall State step (
s1 s2:
State)
ls1 fp1,
ETrace.star step s1 ls1 fp1 s2 ->
forall ls2 fp2 s3,
ETrace.star step s2 ls2 fp2 s3 ->
ETrace.star step s1 (
ls1 ++
ls2) (
FP.union fp1 fp2)
s3.
Proof.
Lemma thdp_inv_upd:
forall ge (
tp : @
ThreadPool.t ge)
i
(
c' :
Core.t) (
tp' :
ThreadPool.t),
ThreadPool.inv tp ->
ThreadPool.update tp i c'
tp' ->
ThreadPool.inv tp'.
Proof.
clear.
intros.
inv H0.
inv H2.
inv H.
constructor;
simpl;
auto.
{
intros.
destruct (
peq i0 i).
subst.
apply tp_finite in H.
unfold ThreadPool.get_cs in *.
rewrite H in H1.
discriminate.
rewrite PMap.gso;
auto. }
{
intros.
destruct (
peq i0 i).
subst.
rewrite PMap.gss.
eauto.
rewrite PMap.gso;
eauto. }
{
intro i0.
destruct (
peq i0 i).
subst.
rewrite PMap.gss.
intros.
inv H.
eapply ThreadPool.cs_upd_inv_cs.
eapply cs_inv.
eauto.
econstructor.
eauto.
rewrite PMap.gso;
auto. }
Qed.
Lemma thdp_upd_next_tid:
forall GE (
tp: @
ThreadPool.t GE)
t c tp',
ThreadPool.update tp t c tp' ->
ThreadPool.next_tid tp' =
ThreadPool.next_tid tp.
Proof.
clear. intros. inv H. auto. Qed.
Lemma thdp_upd_next_fmap:
forall GE (
tp: @
ThreadPool.t GE)
t c tp',
ThreadPool.update tp t c tp' ->
forall t0,
ThreadPool.next_fmap tp'
t0 =
ThreadPool.next_fmap tp t0.
Proof.
clear. intros. inv H. auto. Qed.
Require GDefLemmas.
Lemma core_step_globstep:
forall GE i_x F c m fp c'
m',
let:
Mod :=
GlobEnv.modules GE i_x in
let:
lang :=
ModSem.lang Mod in
let:
Ge :=
ModSem.Ge Mod in
let:
fl :=
FLists.get_fl (
GlobEnv.freelists GE)
F in
step lang Ge fl c m fp c'
m' ->
forall (
tp: @
ThreadPool.t GE)
i sg b cs,
ThreadPool.get_cs tp i =
Some ((
Core.Build_t i_x c sg F)::
cs) ->
exists tp',
glob_step (
Build_ProgConfig GE tp i m b)
ETrace.tau fp
(
Build_ProgConfig GE tp'
i m'
b) /\
ThreadPool.update tp i (
Core.Build_t i_x c'
sg F)
tp'.
Proof.
clear;
intros.
assert (
exists tp',
ThreadPool.update
tp i
{|
Core.i :=
i_x;
Core.c :=
c';
Core.sg:=
sg;
Core.F :=
F |}
tp').
{
assert (
exists cs',
CallStack.update
({|
Core.c :=
c;
Core.sg:=
sg;
Core.F :=
F |}::
cs)
{|
Core.c :=
c';
Core.sg:=
sg;
Core.F :=
F |}
cs').
{
eexists.
econstructor;
eauto.
econstructor;
eauto. }
destruct H1 as (
cs' &
H_cs_upd).
eexists;
econstructor;
eauto.
}
destruct H1 as (
tp' &
H_tp_upd).
exists tp'.
split.
eapply Corestep;
eauto.
unfold ThreadPool.get_top.
rewrite H0.
simpl.
eauto.
eauto.
constructor;
auto.
auto.
Qed.
Lemma core_plus_globstep_plus:
forall GE i_x F c m fp c'
m',
let:
Mod :=
GlobEnv.modules GE i_x in
let:
lang :=
ModSem.lang Mod in
let:
Ge :=
ModSem.Ge Mod in
let:
fl :=
FLists.get_fl (
GlobEnv.freelists GE)
F in
plus (
step lang Ge fl)
c m fp c'
m' ->
forall (
tp: @
ThreadPool.t GE)
i sg b cs,
ThreadPool.get_cs tp i =
Some (
Core.Build_t i_x c sg F ::
cs) ->
exists tp',
tau_plus glob_step (
Build_ProgConfig GE tp i m b)
fp
(
Build_ProgConfig GE tp'
i m'
b) /\
ThreadPool.update tp i {|
Core.c:=
c';
Core.sg:=
sg;
Core.F:=
F |}
tp'.
Proof.
clear.
intros GE i_x F c m fp c'
m'
H.
induction H;
intros.
{
eapply core_step_globstep in H;
eauto.
destruct H as (
tp'&
Hstep &
Htp').
eexists;
split; [
econstructor|];
eauto.
}
{
eapply core_step_globstep in H;
eauto.
destruct H as (
tp' &
Hstep &
Htp').
instantiate (1:=
b)
in Hstep.
inversion Htp'.
rewrite H1 in H.
inversion H.
edestruct (
IHplus tp'
i sg b cs)
as [
tp'' [
Hplus'
Htp''] ].
subst.
unfold ThreadPool.get_cs;
simpl.
rewrite PMap.gsspec.
destruct peq; [|
congruence].
inversion H2.
auto.
exists tp''.
split.
eapply tau_plus_cons;
eauto.
inversion Htp''.
subst;
simpl in *;
clear Hplus'
IHplus H0 Hstep Htp''.
unfold ThreadPool.get_cs in H5;
simpl in H5;
rewrite PMap.gsspec in H5.
destruct peq; [|
congruence].
inversion H5;
subst.
repeat (
econstructor;
eauto).
f_equal.
inversion H7.
rewrite PMap.set2.
subst.
inversion H2;
auto.
}
Qed.
Lemma tau_plus_tau_star:
forall GE (
pc: @
ProgConfig GE)
fp pc',
tau_plus glob_step pc fp pc' ->
tau_star glob_step pc fp pc'.
Proof.
Lemma core_star_globstep_star:
forall GE i_x F c m fp c'
m',
let:
Mod :=
GlobEnv.modules GE i_x in
let:
lang :=
ModSem.lang Mod in
let:
Ge :=
ModSem.Ge Mod in
let:
fl :=
FLists.get_fl (
GlobEnv.freelists GE)
F in
star (
step lang Ge fl)
c m fp c'
m' ->
forall (
tp: @
ThreadPool.t GE)
i sg b cs,
ThreadPool.get_cs tp i =
Some ((
Core.Build_t i_x c sg F)::
cs) ->
exists tp',
tau_star glob_step (
Build_ProgConfig GE tp i m b)
fp
(
Build_ProgConfig GE tp'
i m'
b) /\
(
ThreadPool.update tp i (
Core.Build_t i_x c'
sg F)
tp' \/
m =
m' /\
c =
c' /\
tp =
tp' /\
fp =
FP.emp).
Proof.
Lemma range_perm_client_mem:
forall m b ofs size p,
Mem.range_perm m b ofs (
ofs +
size)
Memperm.Cur p ->
(
forall b'
ofs',
FMemOpFP.range_locset b ofs size b'
ofs' =
true ->
client_mem (
strip m)
b'
ofs').
Proof.
Lemma valid_access_client_mem:
forall m chunk b ofs p,
Mem.valid_access m chunk b ofs p ->
(
forall b'
ofs',
FMemOpFP.range_locset b ofs (
size_chunk chunk)
b'
ofs' =
true ->
client_mem (
strip m)
b'
ofs').
Proof.
Lemma loadv_loadv_fp_client_fp:
forall chunk m v v',
Mem.loadv chunk m v =
Some v' ->
client_fp (
strip m) (
strip m) (
FMemOpFP.loadv_fp chunk v).
Proof.
Lemma storev_storev_fp_client_fp:
forall chunk m v v'
m',
Mem.storev chunk m v v' =
Some m' ->
client_fp (
strip m) (
strip m') (
FMemOpFP.storev_fp chunk v).
Proof.
Lemma valid_pointer_client_mem:
forall m b ofs,
Mem.valid_pointer m b ofs =
true ->
client_mem (
strip m)
b ofs.
Proof.
Lemma valid_pointer_client_mem_range_locset:
forall m b ofs b'
ofs',
Mem.valid_pointer m b ofs =
true ->
FMemOpFP.range_locset b ofs 1
b'
ofs' =
true ->
client_mem (
strip m)
b'
ofs'.
Proof.
Lemma weak_valid_pointer_client_mem:
forall m b ofs b'
ofs',
Mem.weak_valid_pointer m b ofs =
true ->
FP.cmps (
FMemOpFP.weak_valid_pointer_fp m b ofs)
b'
ofs' =
true ->
exists ofs'',
client_mem (
strip m)
b'
ofs''.
Proof.
Lemma valid_pointer_valid_pointer_fp_client_fp:
forall m b ofs,
Mem.valid_pointer m b ofs =
true ->
client_fp (
strip m) (
strip m) (
FMemOpFP.valid_pointer_fp b ofs).
Proof.
Lemma weak_valid_pointer_weak_valid_pointer_fp_client_fp:
forall m b ofs,
Mem.weak_valid_pointer m b ofs =
true ->
client_fp (
strip m) (
strip m) (
FMemOpFP.weak_valid_pointer_fp m b ofs).
Proof.
Lemma alloc_client_or_unused:
forall m lo hi m'
b,
Mem.alloc m lo hi = (
m',
b) ->
forall ofs,
client_mem (
strip m')
b ofs \/
unused_mem (
strip m')
b ofs.
Proof.
Lemma alloc_obj_mem_unchg:
forall m lo hi m'
b,
Mem.alloc m lo hi = (
m',
b) ->
forall b'
ofs',
obj_mem (
strip m)
b'
ofs' <->
obj_mem (
strip m')
b'
ofs'.
Proof.
Lemma alloc_clt_mem_unchg:
forall m lo hi m'
b,
Mem.alloc m lo hi = (
m',
b) ->
forall b'
ofs',
b' <>
b ->
client_mem (
strip m)
b'
ofs' <->
client_mem (
strip m')
b'
ofs'.
Proof.
Lemma free_obj_mem_unchg:
forall m b lo hi m',
Mem.free m b lo hi =
Some m' ->
forall b'
ofs',
obj_mem (
strip m)
b'
ofs' <->
obj_mem (
strip m')
b'
ofs'.
Proof.
Lemma free_clt_mem':
forall m b lo hi m',
Mem.free m b lo hi =
Some m' ->
forall b'
ofs',
client_mem (
strip m')
b'
ofs' ->
client_mem (
strip m)
b'
ofs'.
Proof.
Lemma exec_load_client_fp_obj_unchg:
forall ge chunk m a rs r rs'
m',
sep_obj_client_block (
strip m) ->
exec_load ge chunk m a rs r =
AsmLang.Next rs'
m' ->
client_fp (
strip m) (
strip m') (
exec_load_fp ge chunk a rs) /\
(
forall b ofs,
obj_mem (
strip m)
b ofs <->
obj_mem (
strip m')
b ofs) /\
sep_obj_client_block (
strip m').
Proof.
Lemma exec_store_client_fp_obj_unchg:
forall ge chunk m a rs r lr rs'
m',
sep_obj_client_block (
strip m) ->
exec_store ge chunk m a rs r lr =
AsmLang.Next rs'
m' ->
client_fp (
strip m) (
strip m') (
exec_store_fp ge chunk a rs) /\
(
forall b ofs,
obj_mem (
strip m)
b ofs <->
obj_mem (
strip m')
b ofs) /\
sep_obj_client_block (
strip m').
Proof.
Lemma check_true_compare_ints_client_fp:
forall v1 v2 m,
sep_obj_client_block (
strip m) ->
check_compare_ints v1 v2 m =
true ->
client_fp (
strip m) (
strip m) (
compare_ints_fp v1 v2 m).
Proof.
Lemma test_compare_ints_client_fp:
forall v1 v2 m,
client_fp (
strip m) (
strip m) (
compare_ints_fp (
Val.and v1 v2)
Vzero m).
Proof.
Lemma compare_longs_client_fp:
forall v1 v2 m,
client_fp (
strip m) (
strip m) (
compare_longs_fp v1 v2 m).
Proof.
Lemma fp_locs_fp_union_locs_union_fp_locs:
forall fp1 fp2,
FP.locs (
FP.union fp1 fp2) =
Locs.union (
FP.locs fp1) (
FP.locs fp2).
Proof.
destruct fp1,
fp2.
unfold FP.locs.
simpl.
repeat rewrite <-
Locs.union_assoc_eq.
do 2 (
apply functional_extensionality;
intro).
Locs.unfolds.
repeat match goal with
| |- ?
a || ?
b =
_ =>
destruct a;
simpl;
auto with bool
| |-
_ = ?
a || ?
b =>
destruct a;
simpl;
auto with bool
end.
Qed.
Lemma eval_builtin_arg_fp_client_mem:
forall ge rs v m a b fp,
eval_builtin_arg ge rs v m a b ->
@
MemOpFP.eval_builtin_arg_fp Asm.preg ge rs v a fp ->
forall b'
ofs',
FP.locs fp b'
ofs' =
true ->
client_mem (
strip m)
b'
ofs'.
Proof.
Lemma extcall_arg_fp_client_mem:
forall rs m r b fp,
extcall_arg rs m r b ->
extcall_arg_fp rs r fp ->
forall b'
ofs',
FP.locs fp b'
ofs' =
true ->
client_mem (
strip m)
b'
ofs'.
Proof.
Lemma store_args_fmem_mem_validblock_eq:
forall m stk args tys m',
loadframe.store_args_fmem m stk args tys =
Some m' ->
Mem.validblocks m' =
Mem.validblocks m.
Proof.
Lemma store_args_fmem_mem_access_eq:
forall m stk args tys m',
loadframe.store_args_fmem m stk args tys =
Some m' ->
Mem.mem_access m' =
Mem.mem_access m.
Proof.
Lemma AsmLang_step_client_fp:
forall Ge fl c gm fp c'
gm',
sep_obj_client_block gm ->
step AsmLang Ge fl c gm fp c'
gm' ->
client_fp gm gm'
fp /\
(
forall b ofs,
obj_mem gm b ofs <->
obj_mem gm'
b ofs) /\
sep_obj_client_block gm'.
Proof.
clear.
intros Ge fl c gm fp c'
gm'
Hsep Hstep.
inv Hstep.
inv H.
inv H0.
{
revert Hsep H2 H3.
clear.
destruct i;
simpl;
unfold goto_label;
intros;
try discriminate;
eauto using exec_store_client_fp_obj_unchg,
exec_load_client_fp_obj_unchg;
repeat match goal with
|
H:
match ?
a with _ =>
_ end =
AsmLang.Next _ _ |-
_ =>
destruct a eqn:?;
inv H
|
H:
AsmLang.Next _ _ =
AsmLang.Next _ _ |-
_ =>
inv H
| |-
client_fp _ _ FP.emp /\
_ =>
split; [
apply client_emp_fp;
auto|
tauto]
| |-
client_fp _ _ (
compare_ints_fp _ _ _) /\
_ =>
split; [
auto using check_true_compare_ints_client_fp,
test_compare_ints_client_fp|
tauto]
| |-
client_fp _ _ (
compare_longs_fp _ _ _) /\
_ =>
split; [
auto using compare_longs_client_fp|
tauto]
end.
alloc *) {
pose proof (
Mem.fresh_block_alloc _ _ _ _ _ Heqp)
as Hfresh.
pose proof (
Mem.valid_new_block _ _ _ _ _ Heqp)
as Hvalid.
unfold strip,
obj_mem,
client_mem,
unused_mem.
simpl.
split.
{
apply client_alloc_fp.
unfold GMem.valid_block,
client_mem,
unused_mem.
simpl.
unfold FP.locs.
Locs.unfolds.
simpl.
intros.
red_boolean_true.
store cases *)
repeat rewrite Locs.emp_union_locs in H0.
Locs.unfolds.
red_boolean_true.
store ofs_link *)
apply FMemOpFP.range_locset_loc in H.
destruct H.
subst b0.
split.
auto.
split.
eapply Mem.store_valid_block_1.
eauto.
eapply Mem.store_valid_block_1;
eauto.
erewrite Mem.store_access;
eauto.
erewrite Mem.store_access;
eauto.
eapply alloc_client_or_unused;
eauto.
store ofs_ra *)
apply FMemOpFP.range_locset_loc in H.
destruct H.
subst b0.
split.
auto.
split.
eapply Mem.store_valid_block_1.
eauto.
eapply Mem.store_valid_block_1;
eauto.
erewrite Mem.store_access;
eauto.
erewrite Mem.store_access;
eauto.
eapply alloc_client_or_unused;
eauto.
alloc *)
repeat rewrite Locs.locs_union_emp in H0.
destruct peq; [|
discriminate];
subst b0.
exploit Mem.alloc_result;
eauto.
intro.
subst b.
split.
auto.
split.
eapply Mem.store_valid_block_1.
eauto.
eapply Mem.store_valid_block_1;
eauto.
erewrite Mem.store_access;
eauto.
erewrite Mem.store_access;
eauto.
eapply alloc_client_or_unused;
eauto.
}
{
split.
intros b'
ofs'.
erewrite (
Mem.store_access _ m1 _ _ _ m');
eauto.
erewrite (
Mem.store_access _ m0 _ _ _ m1);
eauto.
eapply alloc_obj_mem_unchg;
eauto.
unfold sep_obj_client_block.
intros b'
ofs1 ofs2.
unfold obj_mem,
client_mem.
simpl.
erewrite Mem.store_access;
eauto.
erewrite Mem.store_access;
eauto.
exploit alloc_obj_mem_unchg.
eauto.
unfold strip,
obj_mem,
client_mem.
simpl.
intro A.
rewrite <-
A.
clear A.
intro.
assert (
b' <>
b).
{
intro.
subst.
destruct H.
apply H.
exploit Mem.fresh_block_alloc;
eauto;
try contradiction.
exfalso.
apply H.
apply Mem.invalid_noaccess.
auto. }
exploit alloc_clt_mem_unchg.
eauto.
eauto.
unfold strip,
client_mem.
simpl.
intro A.
rewrite <-
A.
clear A.
intro.
eapply Hsep;
eauto.
}
}
free *) {
split.
{
apply client_valid_block_fp.
unfold strip,
obj_mem,
client_mem,
unused_mem.
simpl.
unfold FP.locs.
Locs.unfolds.
simpl.
Locs.unfolds.
simpl in *.
apply Mem.load_valid_access in Heqo.
apply Mem.load_valid_access in Heqo0.
apply Mem.free_range_perm in Heqo1.
intros.
red_boolean_true.
left.
eapply valid_access_client_mem in H0;
eauto.
unfold client_mem in H0.
eauto.
left.
eapply valid_access_client_mem in H0;
eauto.
unfold client_mem in H0.
eauto.
left.
eapply range_perm_client_mem in H0.
unfold client_mem,
strip in H0.
eauto.
rewrite Z.sub_0_r,
Z.add_0_l.
eauto. }
split.
eapply free_obj_mem_unchg;
eauto.
unfold sep_obj_client_block.
intros.
erewrite <-
free_obj_mem_unchg in H;
eauto.
eapply free_clt_mem'
in H0;
eauto.
}
}
{
split; [|
tauto].
apply client_valid_block_fp.
revert H4 H5.
clear.
generalize (
rs (
Asm.IR Asm.RSP))
m'
vargs fp.
clear.
induction args.
intros.
inv H5.
inv H.
intros v m'
vargs fp Heval Hevalfp b ofs H.
inv Heval.
inv Hevalfp.
rewrite fp_locs_fp_union_locs_union_fp_locs in H.
Locs.unfolds.
red_boolean_true.
left.
eapply eval_builtin_arg_fp_client_mem;
eauto.
eauto.
}
{
split; [|
tauto].
apply client_valid_block_fp.
revert H2 H3.
clear.
unfold extcall_arguments,
extcall_arguments_fp.
generalize (
loc_arguments (
ef_sig ef))
as typs,
m'
as m,
args as vl,
fp as FP.
clear.
induction typs;
intros.
inv H3.
inv H.
inv H2.
inv H3.
rewrite fp_locs_fp_union_locs_union_fp_locs in H.
Locs.unfolds.
red_boolean_true;
eauto.
clear IHtyps H5 H6.
revert H0 H4 H2.
clear.
intros.
destruct a.
inv H4;
inv H2.
left.
eapply extcall_arg_fp_client_mem;
eauto.
left.
inv H2;
inv H4.
rewrite fp_locs_fp_union_locs_union_fp_locs in H0.
Locs.unfolds.
red_boolean_true;
eauto using extcall_arg_fp_client_mem.
}
{
split; [
auto using client_emp_fp|
tauto]. }
{
split.
{
apply client_alloc_fp.
intros.
assert (
b =
stk).
{
rewrite fp_locs_fp_union_locs_union_fp_locs in H0.
Locs.unfolds.
red_boolean_true.
unfold FP.locs in *.
Locs.unfolds.
simpl in H2.
destruct peq; [
subst b|
discriminate].
exploit Mem.alloc_result.
eauto.
intro;
subst stk;
auto.
revert H2.
clear.
unfold loadframe.store_args_fp.
generalize 0.
induction tys.
intros.
inv H2.
intros.
simpl in H2.
destruct a;
repeat rewrite fp_locs_fp_union_locs_union_fp_locs in H2;
Locs.unfolds;
unfold loadframe.store_stack_fp,
FMemOpFP.storev_fp in H2;
repeat match goal with
|
H:
context[
match ?
a with _ =>
_ end] |-
_ =>
destruct a eqn:?;
inv H
end;
red_boolean_true;
auto;
try (
eapply IHtys;
eassumption;
fail);
repeat match goal with
|
H:
Val.offset_ptr (
Vptr _ _)
_ =
Vptr _ _ |-
_ =>
inv H
|
H:
context[
FP.union FP.emp _] |-
_ =>
rewrite FP.emp_union_fp in H
|
H:
context[
FP.union _ FP.emp] |-
_ =>
rewrite FP.fp_union_emp in H
|
H:
FP.locs (
FMemOpFP.store_fp _ _ _)
_ _ =
true |-
_ =>
unfold FP.locs,
FMemOpFP.store_fp in H;
simpl in H;
repeat rewrite Locs.locs_union_emp in H;
repeat rewrite Locs.emp_union_locs in H;
apply FMemOpFP.range_locset_loc in H;
intuition
end.
}
subst b.
split.
intro.
exploit Mem.fresh_block_alloc;
eauto.
split.
exploit Mem.valid_new_block;
eauto.
unfold Mem.valid_block.
apply store_args_fmem_mem_validblock_eq in H3;
eauto.
rewrite <-
H3.
auto.
unfold client_mem,
unused_mem.
simpl.
erewrite store_args_fmem_mem_access_eq;
eauto.
eapply alloc_client_or_unused;
eauto.
}
split.
{
intros b'
ofs'.
rewrite alloc_obj_mem_unchg;
eauto.
unfold obj_mem.
simpl.
eapply store_args_fmem_mem_access_eq in H3.
rewrite H3.
tauto.
}
{
unfold sep_obj_client_block.
unfold obj_mem,
client_mem in *.
simpl in *.
eapply store_args_fmem_mem_access_eq in H3.
rewrite H3.
clear H3.
intros b'
ofs1 ofs2.
exploit alloc_obj_mem_unchg.
eauto.
unfold strip,
obj_mem,
client_mem.
simpl.
intro A.
rewrite <-
A.
clear A.
intro.
assert (
b' <>
stk).
{
intro.
subst.
destruct H0.
apply H0.
exploit Mem.fresh_block_alloc;
eauto;
try contradiction.
exfalso.
apply H0.
apply Mem.invalid_noaccess.
eapply Mem.fresh_block_alloc.
eauto. }
exploit alloc_clt_mem_unchg.
eauto.
eauto.
unfold strip,
client_mem.
simpl.
intro A.
rewrite <-
A.
clear A.
intro.
eapply Hsep;
eauto.
}
}
Qed.
Lemma SpecLang_step_sep:
forall ge fl c m fp c'
m',
sep_obj_client_block m ->
step SpecLang.speclang ge fl c m fp c'
m' ->
sep_obj_client_block m'.
Proof.
Require Import Compositionality Soundness.
Inductive abort_behav :
behav ->
Prop :=
|
abort_imm:
abort_behav Behav_abort
|
abort_cons:
forall v B,
abort_behav B ->
abort_behav (
Behav_cons v B).
Lemma non_evt_star_star_step:
forall state step (
pc:
state)
fp pc',
non_evt_star step pc fp pc' ->
exists ll,
ETrace.star step pc ll fp pc'.
Proof.
induction 1. eexists. constructor.
destruct H.
destruct IHnon_evt_star. eexists. econstructor; eauto.
destruct IHnon_evt_star. eexists. econstructor; eauto.
Qed.
Lemma prog_refine_safety_preserved:
forall NL L ps pt,
@
prog_refine NL L ps pt ->
forall (
mu :
Injections.Mu) (
sgm :
gmem) (
sge :
GlobEnv.t)
(
spc :
ProgConfig) (
ts :
tid) (
tgm :
gmem) (
tge :
GlobEnv.t)
(
tpc :
ProgConfig) (
tt :
tid),
InitRel mu sge tge sgm tgm ->
init_config ps sgm sge spc ts ->
init_config pt tgm tge tpc tt ->
safe_state glob_step GlobSemantics.abort spc ->
safe_state glob_step GlobSemantics.abort tpc.
Proof.
intros NL L ps pt H.
inv H.
rename H0 into REF.
intros mu sgm sge spc ts tgm tge tpc tt H0 H1 H2 H3.
specialize (
REF mu sgm sge spc ts tgm tge tpc tt H0 H1 H2).
clear mu sgm tgm ts tt H0 H1 H2.
unfold safe_state in *.
intros.
intro Habort.
assert (
exists B,
Etr glob_step GlobSemantics.abort final_state tpc B /\
abort_behav B).
{
revert H Habort;
clear.
induction 1;
intros.
{
eexists.
split.
eapply Etr_abort.
eapply ne_star_refl.
auto.
constructor. }
{
apply IHstar in Habort.
destruct Habort as (
B &
HEtr &
Habort).
clear IHstar.
destruct e.
{
exists B.
split.
destruct Habort.
inv HEtr.
econstructor.
eapply ne_star_step.
eauto.
eauto.
eauto.
inv HEtr.
econstructor.
eapply ne_star_step.
eauto.
eauto.
eauto.
eauto.
eauto. }
{
exists B.
split.
destruct Habort.
inv HEtr.
econstructor.
eapply ne_star_step.
eauto.
eauto.
eauto.
inv HEtr.
econstructor.
eapply ne_star_step.
eauto.
eauto.
eauto.
eauto.
eauto. }
{
exists (
Behav_cons v B).
split.
assert (
fp1 =
FP.emp)
by (
inv H;
auto).
subst.
econstructor.
econstructor.
eauto.
eauto.
econstructor.
eauto. }
}
}
destruct H0 as (
B &
HEtr &
Habort').
apply REF in HEtr.
assert (
exists l'
fp'
spc',
ETrace.star glob_step spc l'
fp'
spc' /\
GlobSemantics.abort spc').
{
revert HEtr Habort'.
clear.
intros.
revert spc HEtr.
induction Habort';
intros.
inv HEtr.
eapply non_evt_star_star_step in H.
destruct H.
eauto.
inv HEtr.
eapply IHHabort'
in H3.
eapply non_evt_star_star_step in H1.
destruct H1.
destruct H3 as (? & ? & ? & ? & ?).
do 3
eexists.
split.
eapply etrace_star_star.
eauto.
eapply ETrace.star_step;
eauto.
eauto. }
destruct H0 as (
l' &
fp' &
spc' &
Hstar' &
Habort'').
eapply H3;
eauto.
Qed.
Lemma safety_preservation:
forall NL L scunits tcunits e comps,
wd_langs scunits ->
wd_langs tcunits ->
det_langs tcunits ->
rc_cunits scunits ->
cunits_transf comps scunits tcunits ->
@
seqs_correct NL L comps ->
drf (
scunits,
e) ->
safe_prog (
scunits,
e) ->
forall mu sgm sge spc ts tgm tge tpc tt,
InitRel mu sge tge sgm tgm ->
init_config (
scunits,
e)
sgm sge spc ts ->
init_config (
tcunits,
e)
tgm tge tpc tt ->
safe_state glob_step GlobSemantics.abort tpc.
Proof.
Lemma drf_preservation:
forall NL L scunits tcunits e comps,
wd_langs scunits ->
wd_langs tcunits ->
det_langs tcunits ->
rc_cunits scunits ->
cunits_transf comps scunits tcunits ->
@
seqs_correct NL L comps ->
drf (
scunits,
e) ->
safe_prog (
scunits,
e) ->
forall mu sgm sge spc ts tgm tge tpc tt,
InitRel mu sge tge sgm tgm ->
init_config (
scunits,
e)
sgm sge spc ts ->
init_config (
tcunits,
e)
tgm tge tpc tt ->
~
star_race_config tpc.
Proof.