Module ModSem
End Args.
Module Retv.
Inductive t: Type :=
| Cstyle
(v: val)
(m: mem)
| Asmstyle
(rs: Asm.regset)
(m: mem).
Definition get_m (retv: Retv.t): mem :=
match retv with
| Retv.Cstyle _ m => m
| Retv.Asmstyle _ m => m
end
.
Definition v (retv: Retv.t): val :=
match retv with
| Retv.Cstyle v _ => v
| Retv.Asmstyle _ _ => Vundef
end
.
Definition m (retv: Retv.t): mem :=
match retv with
| Retv.Cstyle _ m => m
| Retv.Asmstyle _ m => Mem.empty
end
.
Definition mk (v: val) (m: mem): t := Retv.Cstyle v m.
Definition is_cstyle (retv: t): bool :=
match retv with
| Cstyle _ _ => true
| _ => false
end
.
Lemma get_m_m: forall retv (CSTYLE: is_cstyle retv), retv.(get_m) = retv.(m). Proof. destruct retv; ss. Qed.
End Retv.
Hint Unfold Args.is_cstyle Args.mk Args.fptr Args.vs Args.m Retv.is_cstyle Retv.mk Retv.v Retv.m.
Hint Constructors Args.t Retv.t.
Module ModSem.
Record t: Type := mk {
state: Type;
genvtype: Type;
step (se: Senv.t) (ge: genvtype) (st0: state) (tr: trace) (st1: state): Prop;
at_external (st0: state) (args: Args.t): Prop;
initial_frame (args: Args.t) (st0: state): Prop;
final_frame (st0: state) (retv: Retv.t): Prop;
after_external (st0: state) (retv: Retv.t) (st1: state): Prop;
globalenv: genvtype;
skenv: SkEnv.t;
skenv_link: SkEnv.t;
at_external_dtm: forall st args0 args1
(AT0: at_external st args0)
(AT1: at_external st args1),
args0 = args1;
final_frame_dtm: forall st retv0 retv1
(FINAL0: final_frame st retv0)
(FINAL1: final_frame st retv1),
retv0 = retv1;
after_external_dtm: forall st_call retv st0 st1
(AFTER0: after_external st_call retv st0)
(AFTER0: after_external st_call retv st1),
st0 = st1;
is_call (st0: state): Prop := exists args, at_external st0 args;
is_step (st0: state): Prop := exists tr st1, step skenv_link globalenv st0 tr st1;
is_return (st0: state): Prop := exists retv, final_frame st0 retv;
call_step_disjoint: is_call /1\ is_step <1= bot1;
step_return_disjoint: is_step /1\ is_return <1= bot1;
call_return_disjoint: is_call /1\ is_return <1= bot1;
}.
Ltac tac :=
try( let TAC := u; esplits; eauto in
u in *; des_safe;
first[ exfalso; eapply ModSem.call_step_disjoint; TAC; fail
| exfalso; eapply ModSem.step_return_disjoint; TAC; fail
| exfalso; eapply ModSem.call_return_disjoint; TAC; fail]
).
Definition to_semantics (ms: t) :=
(Semantics_gen ms.(step) bot1 bot2 ms.(globalenv) ms.(skenv_link)).
Module Atomic.
Section Atomic.
Local Coercion ModSem.to_semantics: ModSem.t >-> Smallstep.semantics.
Variable ms: t.
Let state := (trace * ms.(state))%type.
Inductive step (se: Senv.t) (ge: ms.(genvtype)): state -> trace -> state -> Prop :=
| step_silent
st0 st1
(STEPSIL: Step ms st0 E0 st1):
step se ge (E0, st0) E0 (E0, st1)
| step_start
st0 st1 ev tr
(STEPEV: Step ms st0 (ev :: tr) st1):
step se ge (E0, st0) [ev] (tr, st1)
| step_continue
ev tr st0
(WBT: output_trace (ev :: tr)):
step se ge (ev :: tr, st0) [ev] (tr, st0).
Definition at_external (st0: state) (args: Args.t): Prop :=
st0.(fst) = [] /\ ms.(at_external) st0.(snd) args.
Definition initial_frame (args: Args.t) (st0: state): Prop :=
st0.(fst) = [] /\ ms.(initial_frame) args st0.(snd).
Definition final_frame (st0: state) (retv: Retv.t): Prop :=
st0.(fst) = [] /\ ms.(final_frame) st0.(snd) retv.
Definition after_external (st0: state) (retv: Retv.t) (st1: state): Prop :=
st0.(fst) = [] /\ ms.(after_external) st0.(snd) retv st1.(snd) /\ st1.(fst) = [].
Program Definition trans: t :=
mk step at_external initial_frame final_frame after_external
ms.(globalenv) ms.(skenv) ms.(skenv_link) _ _ _ _ _ _.
Next Obligation.
Next Obligation.
Next Obligation.
rr in AFTER0.
rr in AFTER1.
des.
destruct st0,
st1;
ss.
clarify.
f_equal.
eapply after_external_dtm;
eauto.
Qed.
Next Obligation.
ii.
des.
destruct x0,
st1;
ss.
rr in PR.
ss.
des.
clarify.
eapply call_step_disjoint;
eauto.
esplits;
eauto.
{
rr.
esplits;
eauto. }
{
rr.
inv PR0;
esplits;
eauto. }
Qed.
Next Obligation.
ii.
des.
destruct x0,
st1;
ss.
rr in PR0.
ss.
des.
clarify.
eapply step_return_disjoint;
eauto.
esplits;
eauto;
cycle 1.
{
rr.
esplits;
eauto. }
{
rr.
inv PR;
esplits;
eauto. }
Qed.
Next Obligation.
ii.
des.
destruct x0;
ss.
rr in PR.
rr in PR0.
ss.
des.
clarify.
eapply call_return_disjoint;
eauto.
esplits;
eauto;
rr;
esplits;
eauto.
Qed.
Lemma atomic_continue tr0 tr1 st_src0
(WBT: output_trace (tr1 ** tr0)):
star step (skenv_link ms) (globalenv ms) (tr1 ** tr0, st_src0) tr1 (tr0, st_src0).
Proof.
ginduction tr1; ii; ss.
{ econs; eauto. }
des. econs; eauto; cycle 1.
{ instantiate (1:= [_]). ss. }
econs; eauto. ss.
Qed.
Lemma atomic_lift_step st_src0 tr st_src1
(WBT: well_behaved_traces ms)
(STEP: Step ms st_src0 tr st_src1):
Star trans ([], st_src0) tr ([], st_src1).
Proof.
Lemma atomic_lift_star st_src0 tr st_src1
(WBT: well_behaved_traces ms)
(STAR: Star ms st_src0 tr st_src1):
Star trans ([], st_src0) tr ([], st_src1).
Proof.
End Atomic.
End Atomic.
End ModSem.
Hint Unfold ModSem.is_call ModSem.is_step ModSem.is_return.
Coercion ModSem.to_semantics: ModSem.t >-> semantics.