Require Import Coqlib.
Require Import Events.
Require Import Values.
Require Import Libtactics.
Set Implicit Arguments.
Labels structure
Record lbls :
Type :=
mklbls
{
labels :
Type
;
tau :
labels
;
pseudotau :
labels ->
Prop
;
fencetau :
labels ->
Prop
;
samekind :
labels ->
labels ->
Prop
;
tau_1_kind :
forall t,
samekind t tau ->
t =
tau
;
pseudo_kind :
forall l l',
pseudotau l' ->
samekind l l' ->
pseudotau l
;
not_pseudo_tau: ~
pseudotau tau
;
lbl_dec :
forall (
x y :
labels), {
x =
y} + {
x <>
y}
;
is_error :
labels ->
Prop
}.
Instantiate external events as labels for the simulations.
Definition event_error (
e :
fullevent) :
Prop :=
match e with
|
Evisible Efail =>
True
|
_ =>
False
end.
Program Definition event_labels :=
{|
labels :=
fullevent
;
tau :=
Etau
;
pseudotau e :=
False
;
fencetau e :=
False
;
samekind :=
event_samekind
;
is_error :=
event_error
;
lbl_dec :=
fullevent_dec |}.
Solve Obligations using (
by destruct t as [[]| |]).
Instantiate thread events as labels for the simulations.
Definition te_pseudotau (
e :
thread_event) :
Prop :=
match e with
|
TEmem (
MEread _ _ _) =>
True
|
_ =>
False
end.
Program Definition thread_labels :=
{|
tau :=
TEtau
;
pseudotau :=
te_pseudotau
;
fencetau x :=
x =
TEmem MEfence
;
samekind :=
te_samekind
;
is_error x :=
x =
TEext Efail
;
lbl_dec :=
thread_event_eq_dec |}.
Solve Obligations using
(
intros;
repeat (
match goal with t :
thread_event |-
_ =>
destruct t as [[]|[]| | | | | |];
clarify end) ).
Program Definition mm_event_labels :=
{|
tau :=
MMtau
;
pseudotau x :=
False
;
fencetau x :=
False
;
is_error x :=
False
;
samekind x y :=
x =
y
;
lbl_dec :=
mm_event_dec |}.
Label transition systems
Section LTS.
Set Implicit Arguments.
Variable (
lbl :
lbls).
Record lts :
Type :=
mklts
{
St :
Type
;
stepr :
St ->
labels lbl ->
St ->
Prop
}.
Variable ts :
lts.
Important definitions
An LTS is receptive if it can transition on any input.
Definition receptive :
Prop :=
forall l {
l'
s s'},
stepr ts s l s' ->
samekind lbl l'
l ->
exists s'',
stepr ts s l'
s''.
An LTS is determinate if (i) two transitions from the same state
imply that their labels are the same up to input value (i.e.,
samekind), (ii) if there are two transitions from the same state
with the same label, then their targets must be equal.
Definition determinate :
Prop :=
forall s {
s'
s''
l l'},
stepr ts s l s' ->
stepr ts s l'
s'' ->
(
samekind lbl l l' /\
(
l =
l' ->
s' =
s'')).
Zero or more tau transitions.
Inductive taustar :
St ts ->
St ts ->
Prop :=
|
taustar_refl:
forall s,
taustar s s
|
taustar_step:
forall {
s s'
s''},
stepr ts s (
tau lbl)
s' ->
taustar s'
s'' ->
taustar s s''.
Definition weakstep (
s :
St ts) (
l :
labels lbl) (
s' :
St ts) :
Prop :=
exists s1,
exists s2,
taustar s s1 /\
stepr ts s1 l s2 /\
taustar s2 s'.
Definition taustep (
s :
St ts) (
l :
labels lbl) (
s' :
St ts) :
Prop :=
exists s1,
taustar s s1 /\
stepr ts s1 l s'.
Definition taureach (
s :
St ts) (
s' :
St ts) :
Prop :=
taustar s s' \/
taustar s'
s.
Definition stuck (
s :
St ts) :
Prop :=
forall s'
l,
stepr ts s l s' ->
False.
Lemma taustar_trans:
forall {
s1 s2 s3},
taustar s1 s2 ->
taustar s2 s3 ->
taustar s1 s3.
Proof.
intros s1 s2 s3 TS1 TS2.
induction TS1 as [
s |
t1 t2 t3 TS1'
TS2'
IH];
try done.
by apply (
taustar_step TS1'),
IH.
Qed.
Lemma taureach_refl:
forall s,
taureach s s.
Proof.
Lemma taureach_sym:
forall s1 s2,
taureach s1 s2 ->
taureach s2 s1.
Proof.
by destruct 1; unfold taureach; tauto. Qed.
Lemma weakstep_not_stuck:
forall s l s',
weakstep s l s' ->
stuck s ->
False.
Proof.
eby intros s l s' (s1 & s2 & [] & ST & _) Stuck; eapply Stuck. Qed.
Lemma taustep_not_stuck:
forall s l s',
taustep s l s' ->
stuck s ->
False.
Proof.
eby intros s l s' (s1 & [] & ST) Stuck; eapply Stuck. Qed.
Lemma steptau_taustar:
forall s1 s2,
stepr ts s1 (
tau lbl)
s2 ->
taustar s1 s2.
Proof.
intros; vauto. Qed.
Lemma weaksteptau_decomp:
forall s1 s2,
weakstep s1 (
tau lbl)
s2 ->
exists s',
stepr ts s1 (
tau lbl)
s' /\
taustar s'
s2.
Proof.
intros s1 s2 WS.
destruct WS as [
is1 [
is2 [[
s |
t1 t2 t3 STt TSt] [
ST TS']]]].
exists is2.
tauto.
exists t2.
split.
assumption.
apply steptau_taustar in ST.
exact (
taustar_trans (
taustar_trans TSt ST)
TS').
Qed.
Lemma tausteptau_decomp:
forall s1 s2,
taustep s1 (
tau lbl)
s2 ->
exists s',
stepr ts s1 (
tau lbl)
s' /\
taustar s'
s2.
Proof.
intros s1 s2 WS.
destruct WS as [
is1 [[
s |
t1 t2 t3 STt TSt]
ST]].
by exists s2;
vauto.
exists t2;
split;
try done.
eby eapply taustar_trans,
steptau_taustar.
Qed.
Lemma weaksteptau_taustar:
forall s1 s2,
weakstep s1 (
tau lbl)
s2 ->
taustar s1 s2.
Proof.
Lemma tausteptau_taustar:
forall s1 s2,
taustep s1 (
tau lbl)
s2 ->
taustar s1 s2.
Proof.
intros s1 s2 (
s' &
TS &
ST);
eapply taustar_trans;
try edone;
vauto.
Qed.
Lemma taustar_weakstep:
forall s1 s2 s3 l,
taustar s1 s2 ->
weakstep s2 l s3 ->
weakstep s1 l s3.
Proof.
intros s1 s2 s3 l STT WS.
destruct WS as [
s' [
s'' [
TS1 [
ST TS2]]]].
exists s'.
exists s''.
repeat split;
try assumption.
exact (
taustar_trans STT TS1).
Qed.
Lemma taustar_taustep:
forall s1 s2 s3 l,
taustar s1 s2 ->
taustep s2 l s3 ->
taustep s1 l s3.
Proof.
intros s1 s2 s3 l STT [
s' [
TS1 ST]].
exists s';
split;
try done.
exact (
taustar_trans STT TS1).
Qed.
Lemma weakstep_taustar:
forall s1 s2 s3 l,
weakstep s1 l s2 ->
taustar s2 s3 ->
weakstep s1 l s3.
Proof.
intros s1 s2 s3 l [
s' [
s'' [
TS1 [
ST TS2]]]]
STT.
exists s'.
exists s''.
repeat split;
try assumption.
exact (
taustar_trans TS2 STT).
Qed.
Lemma steptau_weakstep:
forall s1 s2 s3 l,
stepr ts s1 (
tau lbl)
s2 ->
weakstep s2 l s3 ->
weakstep s1 l s3.
Proof.
intros s1 s2 s3 l STT WS.
destruct WS as [
s' [
s'' [
TS1 [
ST TS2]]]].
exists s'.
exists s''.
repeat split;
try assumption.
exact (
taustar_step STT TS1).
Qed.
Lemma step_taustar_weakstep:
forall s1 s2 s3 l,
stepr ts s1 l s2 ->
taustar s2 s3 ->
weakstep s1 l s3.
Proof.
intros;
eexists;
eexists.
repeat split;
[
apply taustar_refl |
eassumption |
eassumption];
done.
Qed.
Lemma step_weakstep:
forall s1 s2 l,
stepr ts s1 l s2 ->
weakstep s1 l s2.
Proof.
Lemma step_taustep:
forall s1 s2 l,
stepr ts s1 l s2 ->
taustep s1 l s2.
Proof.
intros; eexists; vauto. Qed.
Lemma steptau_taustar_taustep:
forall s1 s2 s3,
stepr ts s1 (
tau lbl)
s2 ->
taustar s2 s3 ->
taustep s1 (
tau lbl)
s3.
Proof.
intros s1 s2 s3 STEP TAU.
revert s1 STEP.
induction TAU;
intros; [
by eexists;
vauto|].
by eapply taustar_taustep,
IHTAU;
try eassumption;
vauto.
Qed.
Lemma tausteptau_taustar_taustep:
forall s1 s2 s3,
taustep s1 (
tau lbl)
s2 ->
taustar s2 s3 ->
taustep s1 (
tau lbl)
s3.
Proof.
Definition can_do_error s :=
exists s',
exists l,
is_error _ l /\
stepr ts s l s'.
Definition stuck_or_error s :=
stuck s \/
can_do_error s.
Eventually will get stuck or do an errror transition.
Inductive ev_stuck_or_error (
s:
St ts):
Prop :=
|
ev_stuck_or_error_stuck:
forall
(
STUCK:
stuck s),
ev_stuck_or_error s
|
ev_stuck_or_error_error:
forall l s' (
STEP:
stepr ts s l s')
(
ISERR:
is_error lbl l),
ev_stuck_or_error s
|
ev_stuck_or_error_tau:
forall s'
(
TAUSTEP:
stepr ts s (
tau lbl)
s')
(
ERR:
ev_stuck_or_error s'),
ev_stuck_or_error s
|
ev_stuck_or_error_pseudotau:
forall l
(
ISPSEUDO:
pseudotau lbl l)
s'
(
STEP:
stepr ts s l s')
(
ERR:
forall l s',
pseudotau lbl l ->
stepr ts s l s' ->
ev_stuck_or_error s'),
ev_stuck_or_error s.
Lemma ev_stuck_or_error_taustar:
forall s s' (
TAU:
taustar s s'),
ev_stuck_or_error s' ->
ev_stuck_or_error s.
Proof.
Lemma ev_stuck_or_error1:
forall s s',
taustar s s' ->
stuck_or_error s' ->
ev_stuck_or_error s.
Proof.
induction 1.
by intros [?|(? & ? & ? & ?)]; vauto.
by intro X; specialize (IHtaustar X); vauto.
Qed.
End LTS.
Forward and backward simulation correspondence
Section FBSimulations.
Variable lbl :
lbls.
Variables (
src tgt :
lts lbl).
Hypothesis source_receptive :
receptive src.
Hypothesis target_determinate :
determinate tgt.
Hypothesis source_dec_progress :
forall s,
stuck src s \/
(
exists l,
exists s',
stepr src s l s').
Section ForwardSim.
Variable r :
St src ->
St tgt ->
Prop.
Variable c :
St src ->
St src ->
Prop.
Normal (thread-local) forward simulation
Definition forward_sim :
Prop :=
well_founded c /\
(
forall s t l s',
stepr src s l s' ->
r s t ->
(
ev_stuck_or_error src s) \/
(
exists t',
weakstep tgt t l t' /\
r s'
t') \/
(
l =
tau _ /\
r s'
t /\
c s'
s)).
End ForwardSim.
Lockstep (thread-local) forward simulation with pseudotau actions
Definition lockstep_forward_sim (
allow_pseudotaus:
bool) (
r :
St src ->
St tgt ->
Prop):
Prop :=
(
forall s t l s',
stepr src s l s' ->
r s t ->
(
exists t',
stepr tgt t l t' /\
r s'
t') \/
(
allow_pseudotaus /\
pseudotau lbl l /\ (
exists t',
stepr tgt t (
tau lbl)
t' /\
(
forall l0 s0,
samekind lbl l0 l ->
stepr src s l0 s0 ->
r s0 t')))).
(Thread-local) backward simulation
Definition backward_sim (
allow_pseudotaus :
bool)
(
r :
St tgt ->
St src ->
Prop)
(
c :
St tgt ->
St tgt ->
Prop) :
Prop :=
well_founded c /\
(
forall s t,
stuck tgt t ->
r t s ->
ev_stuck_or_error src s) /\
(
forall s t l t',
stepr tgt t l t' ->
r t s ->
(
exists s',
taustep src s l s' /\
r t'
s') \/
(
l =
tau lbl /\
r t'
s /\
c t'
t) \/
(
allow_pseudotaus /\
l =
tau lbl /\ (
exists l0,
forall l',
samekind lbl l'
l0 ->
exists s',
taustep src s l'
s' /\
pseudotau lbl l' /\
r t'
s')) \/
(
fencetau lbl l /\ (
exists s',
taustep src s (
tau lbl)
s' /\
r t'
s')) \/
ev_stuck_or_error src s).
Dealing with lockstep pseudotau forward simulations
Section LockstepForwardToBackwardSim.
Variable allow_pseudotaus :
bool.
Variable fsr :
St src ->
St tgt ->
Prop.
Hypothesis fsim :
lockstep_forward_sim allow_pseudotaus fsr.
Theorem lockstep_forward_to_backward_sim:
backward_sim allow_pseudotaus (
fun x y =>
fsr y x) (
fun x y =>
False).
Proof.
End LockstepForwardToBackwardSim.
Converting normal forward simulations
Section ForwardToBackwardSim.
Variable fsr :
St src ->
St tgt ->
Prop.
Variable fsc :
St src ->
St src ->
Prop.
Hypothesis fsim :
forward_sim fsr fsc.
Lemma fsc_wf:
well_founded fsc.
Proof.
pose proof fsim.
unfold forward_sim in *.
tauto. Qed.
Backward simulation construction.
Definition bsr (
t :
St tgt) (
s :
St src) :
Prop :=
exists t',
fsr s t' /\
taureach tgt t t'.
Well-founded relation for the backward simulation.
Inductive bsc :
St tgt ->
St tgt ->
Prop :=
|
bsc_nontau :
forall t t'
t''
l,
stepr tgt t (
tau lbl)
t' ->
stepr tgt t'
l t'' ->
l <>
tau lbl ->
bsc t'
t
|
bsc_step :
forall t t'
t'',
stepr tgt t (
tau lbl)
t' ->
bsc t''
t' ->
bsc t'
t.
Lemma bsc_impl_taustar:
forall t t',
bsc t'
t ->
stepr tgt t (
tau lbl)
t'.
Proof.
intros t t' H.
induction H; auto.
Qed.
Lemma bsc_unique_pred:
forall t t'
t'',
bsc t'
t ->
bsc t''
t ->
t' =
t''.
Proof.
Lemma bsc_wf:
well_founded bsc.
Proof.
Lemma ltaustar_eq:
forall t1 t2 t3 l,
stepr tgt t1 l t2 ->
l <>
tau lbl ->
taustar tgt t1 t3 ->
t1 =
t3.
Proof.
intros t1 t2 t3 l ST Lntau TS.
destruct TS as [|
s1 s2 s3 H].
reflexivity.
pose proof (
proj1 (
target_determinate _ _ _ _ _ ST H))
as SKL.
apply tau_1_kind in SKL.
byContradiction;
auto.
Qed.
Lemma lweaktaustar:
forall t1 t2 t3 l,
weakstep tgt t1 l t2 ->
l <>
tau lbl ->
taustar tgt t1 t3 ->
weakstep tgt t3 l t2.
Proof.
intros t1 t2 t3 l WS Lntau TS.
destruct WS as [
t' [
t'' [
TS1 [
ST TS2]]]].
exists t'.
exists t''.
repeat split;
try assumption.
induction TS1 as [
t1 |
t1'
t2'
t3'
Stau TS'
IH].
rewrite <- (@
ltaustar_eq _ _ _ _ ST Lntau TS).
apply taustar_refl.
destruct TS as [
u |
u1 u2 u3 Htau Hts].
exact (
taustar_step Stau TS').
apply IH;
try assumption.
rewrite (
proj2 (
target_determinate _ _ _ _ _ Stau Htau));
auto.
Qed.
Lemma lweakbothtep:
forall t1 t2 t3 l,
taureach tgt t1 t2 ->
l <>
tau lbl ->
weakstep tgt t2 l t3 ->
weakstep tgt t1 l t3.
Proof.
intros t1 t2 t3 l TR Lntau WS.
destruct TR as [
TS |
TS].
destruct WS as [
t' [
t'' [
TS1 [
TS2 TS3]]]].
exists t'.
exists t''.
repeat split;
try assumption.
exact (
taustar_trans TS TS1).
apply (@
lweaktaustar _ _ _ _ WS Lntau TS).
Qed.
Lemma taustar2_taureach:
forall t1 t2 t3,
taustar tgt t1 t2 ->
taustar tgt t1 t3 ->
taureach tgt t2 t3.
Proof.
intros t1 t2 t3 TS1 TS2.
induction TS1 as [
t1 |
t1'
t2'
t3'
Stau TS'
IH].
left;
assumption.
destruct TS2 as [
t1 |
t1'
t2''
t3''
Stau'
TS''].
right.
apply (
taustar_step Stau TS').
rewrite (
proj2 (
target_determinate _ _ _ _ _ Stau Stau')
(
refl_equal (
tau lbl)))
in *.
apply IH.
assumption.
Qed.
Lemma taureach_taustar_taureach:
forall t1 t2 t3,
taureach tgt t1 t2 ->
taustar tgt t2 t3 ->
taureach tgt t1 t3.
Proof.
Lemma taustar_labels:
forall t1 t2 t3 t4 t5 l l',
l <>
tau lbl ->
l' <>
tau lbl ->
taustar tgt t1 t2 ->
stepr tgt t2 l t3 ->
taustar tgt t1 t4 ->
stepr tgt t4 l'
t5 ->
t2 =
t4 /\
samekind lbl l l' /\ (
l =
l' ->
t3 =
t5).
Proof.
intros t1 t2 t3 t4 t5 l l'
Lntau Lntau'
TS1 ST1 TS2 ST2.
pose proof (@
taustar2_taureach _ _ _ TS1 TS2)
as TR.
assert (
T2_eq_T4:
t2 =
t4).
destruct TR as [
TS3 |
TS3].
apply (@
ltaustar_eq _ _ _ _ ST1 Lntau TS3).
symmetry;
apply (@
ltaustar_eq _ _ _ _ ST2 Lntau'
TS3).
split.
assumption.
rewrite T2_eq_T4 in *.
exact (
target_determinate _ _ _ _ _ ST1 ST2).
Qed.
Lemma forward_progress:
forall s t
(
SIMst :
fsr s t),
(
ev_stuck_or_error src s \/
exists sm,
exists tm,
exists s',
exists t',
exists l,
taustar src s sm /\
stepr src sm l s' /\
taustar tgt t tm /\
weakstep tgt tm l t' /\
fsr sm tm /\
fsr s'
t').
Proof.
induction s as [
s IH]
using (
well_founded_ind fsc_wf);
intros.
destruct (
source_dec_progress s)
as [
Stuck |
Step].
by left;
eapply ev_stuck_or_error_stuck.
destruct Step as [
l [
s'
Step]].
destruct fsim as [
_ FS].
destruct (
FS s t l s'
Step SIMst)
as
[
Err | [[
t'
TStep] | [
Ltau [
FS'
FSCss]]]];
clear FS.
by left.
right.
exists s.
exists t.
exists s'.
exists t'.
exists l.
by repeat split;
try tauto;
apply taustar_refl.
specialize (
IH s'
FSCss t FS').
destruct IH as [
STUCK |
[
sm [
tm [
sp [
tp [
lp [
TSsp [
STp [
TStm [
WStp [
FSm FSp]]]]]]]]]]].
eby clarify;
left;
eapply ev_stuck_or_error_tau.
right.
exists sm.
exists tm.
exists sp.
exists tp.
exists lp.
repeat split;
try assumption.
by rewrite Ltau in Step;
apply (
taustar_step Step).
Qed.
This is the fundamental lemma that uses receptiveness to force
the source lts to do the same step as the target lts. All this is
wrapped up in an inductive argument to get around the pesky tau
actions (using the old trick with determinacy).
Lemma forward_progress_nontau_aux:
forall t1 t2,
taustar tgt t1 t2 ->
forall t3 s t l,
fsr s t ->
taustar tgt t1 t ->
stepr tgt t2 l t3 ->
l <>
tau lbl ->
ev_stuck_or_error src s \/
(
exists s1,
exists s2,
exists t5,
taustar src s s1 /\
stepr src s1 l s2 /\
taustar tgt t3 t5 /\
fsr s2 t5).
Proof.
Lemma sourcesim_nontau:
forall s t t1 t2 l,
fsr s t ->
l <>
tau lbl ->
taustar tgt t t1 ->
stepr tgt t1 l t2 ->
ev_stuck_or_error src s \/
(
exists s1,
exists s',
exists t',
taustar src s s1 /\
stepr src s1 l s' /\
taustar tgt t2 t' /\
fsr s'
t').
Proof.
Lemma stau_ts_impl_order:
forall t t'
t''
l
(
STEP:
stepr tgt t (
tau lbl)
t')
(
WS:
taustep tgt t'
l t''),
l <>
tau lbl ->
bsc t'
t.
Proof.
intros;
destruct WS as [
t1 [
TStt1 STt1t2]].
revert t STEP;
induction TStt1;
eauto using bsc.
Qed.
Lemma stau_ws_impl_order:
forall t t'
t''
l
(
STEP:
stepr tgt t (
tau lbl)
t')
(
WS:
weakstep tgt t'
l t''),
l <>
tau lbl ->
bsc t'
t.
Proof.
intros;
destruct WS as [
t1 [
t2 [
TStt1 [
STt1t2 _]]]].
revert t STEP;
induction TStt1;
eauto using bsc.
Qed.
Lemma taustar_stuck_sim:
forall s t ts,
fsr s ts ->
taustar tgt t ts ->
stuck tgt t ->
ev_stuck_or_error src s.
Proof.
Lemma taustar_stuck_sim2:
forall t t',
taustar tgt t t' ->
forall s ts,
fsr s ts ->
taustar tgt t ts ->
stuck tgt t' ->
ev_stuck_or_error src s.
Proof.
Lemma fsr_in_bsr:
forall s t,
fsr s t ->
bsr t s.
Proof.
intros; exists t; split; vauto.
Qed.
The main result: bsr and bsc are a backward simulation.
Theorem forward_to_backward_sim:
backward_sim false bsr bsc.
Proof.
End ForwardToBackwardSim.
End FBSimulations.
Simulation with undefs
Section ForwardToBackwardUndefSim.
Labels
Variable lbl :
lbls.
Source and target transition systems
Variables (
src tgt :
lts lbl).
Assumptions on the transition systems
Hypothesis source_receptive :
receptive src.
Hypothesis target_determinate :
determinate tgt.
Hypothesis source_dec_progress :
forall s,
stuck src s \/
(
exists l,
exists s',
stepr src s l s').
Less defined comparison in output values.
In essence, this only relates write of an undefined value to a write
of defined value to the same memory location.
Variable ldo :
labels lbl ->
labels lbl ->
Prop.
Less defined comparison in input labels. Note that unlike
ldo, ldi is reflexive.
Variable ldi :
labels lbl ->
labels lbl ->
Prop.
Assumptions on ldi and ldo.
Hypothesis ldo_samekind_eq:
forall l1 l2 l,
samekind _ l1 l2 ->
ldo l l2 ->
l1 =
l2.
Hypothesis ldo_not_tau:
forall l1,
ldo l1 (
tau _) ->
False.
Hypothesis ldi_refl:
forall l,
ldi l l.
Forward simulation with undefined values
Definition forward_sim_with_undefs
(
r :
St src ->
St tgt ->
Prop)
(
c :
St src ->
St src ->
Prop) :
Prop :=
well_founded c /\
(
forall s t l s',
stepr _ s l s' ->
r s t ->
(
ev_stuck_or_error _ s) \/
(
l =
tau _ /\
r s'
t /\
c s'
s) \/
(
exists t', (
exists l',
ldo l l' /\
weakstep tgt t l'
t' /\
r s'
t') \/
(
weakstep tgt t l t' /\
forall l'',
ldi l''
l ->
exists s'',
stepr _ s l''
s'' /\
r s''
t'))).
Backward simulation with undefined values
Definition backward_sim_with_undefs
(
r :
St tgt ->
St src ->
Prop)
(
c :
St tgt ->
St tgt ->
Prop) :
Prop :=
well_founded c /\
(
forall s t,
stuck tgt t ->
r t s ->
ev_stuck_or_error _ s) /\
(
forall s t l t',
stepr tgt t l t' ->
r t s ->
(
l =
tau lbl /\
r t'
s /\
c t'
t) \/
(
ev_stuck_or_error _ s) \/
(
exists s',
exists l',
ldo l'
l /\
taustep src s l'
s' /\
r t'
s') \/
(
forall l'',
ldi l''
l ->
exists s',
taustep src s l''
s' /\
r t'
s')).
Section ForwardToBackwardSim.
Let us assume that we have a forward simulation ...
Variable fsr :
St src ->
St tgt ->
Prop.
Variable fsc :
St src ->
St src ->
Prop.
Hypothesis fsim :
forward_sim_with_undefs fsr fsc.
Lemma fscu_wf:
well_founded fsc.
Proof.
pose proof fsim.
unfold forward_sim_with_undefs in *.
tauto. Qed.
Lemma forward_progress_with_undef:
forall s t,
fsr s t ->
(
ev_stuck_or_error _ s \/
exists sm,
exists tm,
exists t',
exists l,
taustar src s sm /\
taustar tgt t tm /\
fsr sm tm /\
weakstep tgt tm l t' /\
((
exists l',
exists s',
ldo l'
l /\
stepr src sm l'
s' /\
fsr s'
t') \/
(
forall l'',
ldi l''
l ->
exists s'',
stepr src sm l''
s'' /\
fsr s''
t'))).
Proof.
induction s as [
s IH]
using (
well_founded_ind fscu_wf).
intros t SIMst.
destruct (
source_dec_progress s)
as [
Stuck |
Step].
by vauto.
destruct Step as [
l [
s'
Step]].
destruct fsim as [
_ FS].
destruct (
FS s t l s'
Step SIMst)
as
[
Err | [[
Ltau [
FS'
FSCss]] | [
t'
TStep]]].
clear FS.
by vauto.
clear FS.
specialize (
IH s'
FSCss t FS').
destruct IH as [
Stuck |
[
sm [
tm [
tp [
lp [
TSsm [
TSt [
FSm [
WStp Cases]]]]]]]]].
left;
eapply ev_stuck_or_error_taustar,
Stuck;
subst.
exact (
taustar_step Step (
taustar_refl _ _)).
right.
exists sm.
exists tm.
exists tp.
exists lp.
repeat split;
try assumption.
rewrite Ltau in Step.
exact (
taustar_step Step TSsm).
right.
exists s.
exists t.
exists t'.
destruct TStep as [[
l'
LDOStep] | [
WStltp LDIStep]].
exists l'.
repeat split;
try tauto;
try apply taustar_refl.
left;
exists l;
exists s';
tauto.
exists l.
repeat split;
try tauto;
try apply taustar_refl.
Qed.
Lemma weakstep_samekind:
forall t1 t2 t3 l l',
l <>
tau lbl ->
l' <>
tau lbl ->
weakstep tgt t1 l t2 ->
weakstep tgt t1 l'
t3 ->
samekind lbl l l'.
Proof.
intros t1 t2 t3 l l'
Lntau Lpntau
[
t4 [
t5 [
TSt1t4 [
STt4 _]]]]
[
t6 [
t7 [
TSt1t6 [
STt6 _]]]].
by destruct (@
taustar_labels _ _ target_determinate _ _ _ _ _ _ _
Lntau Lpntau TSt1t4 STt4 TSt1t6 STt6)
as [
_ [
SK _]].
Qed.
Lemma forward_progress_nontau_aux_with_undef:
forall t1 t2,
taustar tgt t1 t2 ->
forall t3 s t l,
fsr s t ->
taustar tgt t1 t ->
stepr tgt t2 l t3 ->
l <>
tau lbl ->
ev_stuck_or_error _ s \/
(
exists s1,
exists t5,
taustar src s s1 /\
taustar tgt t3 t5 /\
((
exists l',
exists s2,
ldo l'
l /\
stepr src s1 l'
s2 /\
fsr s2 t5) \/
(
forall l',
ldi l'
l ->
exists s2,
stepr src s1 l'
s2 /\
fsr s2 t5))).
Proof.
set (
ltauseq := @
ltaustar_eq _ _ target_determinate).
intros t1 t2 TSt1t2.
induction TSt1t2 as [
t1 |
t1 t2 t3 STt1t2 TSt2t3 IH].
intros t4 s t l FSst TSt1t STt1t3 Lntau.
pose proof (@
ltaustar_eq _ _ target_determinate _ _ _ _ STt1t3 Lntau TSt1t)
as Eq_t1_t.
rewrite <-
Eq_t1_t in *.
destruct (@
forward_progress_with_undef _ _ FSst)
as [
Stuck |
[
sm [
tm [
t' [
l' [
TSssm [
TStm [
FSstm [
WStmt'
Cases]]]]]]]]].
by vauto.
destruct (
lbl_dec lbl l' (
tau lbl))
as [
Ltau' |
Lntau'].
rewrite Ltau'
in *.
destruct (
weaksteptau_decomp (
taustar_weakstep TStm WStmt'))
as [
it [
STit _]].
elim Lntau.
apply tau_1_kind.
apply (
proj1 (
target_determinate _ _ _ _ _ STt1t3 STit)).
assert (
WSt1_to_TSt4:
forall tx,
weakstep _ t1 l tx ->
taustar _ t4 tx).
intros tx WStx.
destruct WStx as [
tx1 [
tx2 [
TSt1tx1 [
STtx1tx2 TStx2tx]]]].
rewrite <- (
ltauseq _ _ _ _ STt1t3 Lntau TSt1tx1)
in STtx1tx2.
by rewrite <- (
proj2 (
target_determinate _ _ _ _ _ STt1t3 STtx1tx2)
(
refl_equal l))
in TStx2tx.
pose proof WStmt'
as WStmtp.
destruct (
WStmt')
as [
t5 [
t6 [
TSt1t5 [
STt5t6 TSt6t']]]].
pose proof (
ltauseq _ _ _ _ STt1t3 Lntau TStm)
as t1_eq_tm.
rewrite <-
t1_eq_tm in *.
pose proof (
ltauseq _ _ _ _ STt1t3 Lntau TSt1t5)
as t1_eq_t5.
rewrite <-
t1_eq_t5 in *.
pose proof (
proj1 (
target_determinate _ _ _ _ _ STt1t3 STt5t6))
as SK.
destruct Cases as [[
lp [
s' [
Ldo [
STsms'
FSstp]]]] |
LDI].
right.
exists sm.
exists t'.
rewrite (@
ldo_samekind_eq _ _ _ SK Ldo)
in *.
rewrite <- (
proj2 (
target_determinate _ _ _ _ _ STt1t3 STt5t6)
(
refl_equal l'))
in *.
repeat split;
try assumption;
try apply taustar_refl.
left.
exists lp.
exists s'.
repeat split;
try assumption.
destruct (
LDI _ (
ldi_refl l'))
as [
s'' [
STsmlpspp FSspptp]].
destruct (
source_receptive _ _ _ _ STsmlpspp SK)
as [
s2 STsms2].
destruct fsim as [
_ FS].
destruct (
FS sm t1 l s2 STsms2 FSstm)
as
[
Err |
[[
Ltau [
FS'
FSCss]] |
[
t2 [[
l2p [
LDO2 [
WSlp2 FSs2t2]]] | [
WSt1lt2 LDI2]]]]];
clear FS.
eby left;
eapply ev_stuck_or_error_taustar.
contradiction.
assert (
L2pntau:
l2p <>
tau _).
intro L2ptau.
rewrite L2ptau in *.
apply ldo_not_tau in LDO2.
assumption.
pose proof (@
ldo_samekind_eq _ _ _
(@
weakstep_samekind _ _ _ _ _ Lntau'
L2pntau WStmtp WSlp2)
LDO2)
as Eq_lp_l2p.
rewrite <-
Eq_lp_l2p in *.
pose proof (@
ldo_samekind_eq _ _ _ SK LDO2)
as Eq_l_lp.
rewrite <-
Eq_l_lp in *.
right.
exists sm.
exists t2.
rewrite <- (
proj2 (
target_determinate _ _ _ _ _ STt1t3 STt5t6)
(
refl_equal l))
in *.
repeat split.
assumption.
apply (
WSt1_to_TSt4 _ WSlp2).
left.
exists l.
exists s2.
repeat split;
try assumption.
right.
exists sm.
exists t2.
repeat split.
assumption.
apply (
WSt1_to_TSt4 _ WSt1lt2).
right.
assumption.
intros t4 s t l FSst TSt1t STt1t3 Lntau.
destruct (@
forward_progress_with_undef _ _ FSst)
as [
Stuck |
[
sm [
tm [
t' [
l' [
TSssm [
TStm [
FSstm [
WStmt'
Cases]]]]]]]]].
by vauto.
destruct (
lbl_dec lbl l' (
tau lbl))
as [
Ltau' |
Lntau'].
rewrite Ltau'
in *.
destruct (
weaksteptau_decomp (
taustar_weakstep TSt1t (
taustar_weakstep TStm WStmt')))
as [
it [
STit TSit]].
rewrite (
proj2 (
target_determinate _ _ _ _ _ STt1t2 STit)
(
refl_equal (
tau lbl)))
in *.
destruct Cases as [[
lp [
sp [
LDO _]]] |
WStmtp].
apply ldo_not_tau in LDO.
contradiction.
destruct (
WStmtp (
tau _) (
ldi_refl _))
as [
s' [
STsms'
FSst']].
specialize (
IH t4 s'
t'
l FSst'
TSit STt1t3 Lntau).
destruct IH as [
Stuck | [
sp1 [
tp1 [
TSsp1 [
TStp1 Cases]]]]].
left;
eapply ev_stuck_or_error_taustar,
Stuck.
exact (
taustar_trans TSssm (
taustar_step STsms' (
taustar_refl _ _))).
right.
exists sp1.
exists tp1.
repeat split;
try assumption.
exact (
taustar_trans TSssm (
taustar_step STsms'
TSsp1)).
pose proof WStmt'
as WStmtp.
destruct WStmt'
as [
t5 [
t6 [
TStmt5 [
STt5t6 TSt6t']]]].
pose proof (
taustar_step STt1t2 TSt2t3)
as TSt1t3.
pose proof (
taustar_trans TSt1t (
taustar_trans TStm TStmt5))
as TSt1t5.
pose proof (
proj1 (@
taustar_labels _ _ target_determinate _ _ _ _ _ _ _
Lntau Lntau'
TSt1t3 STt1t3 TSt1t5 STt5t6))
as t3_eq_t5.
rewrite t3_eq_t5 in *.
pose proof (
proj1 (
target_determinate _ _ _ _ _ STt1t3 STt5t6))
as SK.
destruct Cases as [[
lp [
s' [
Ldo [
STsms'
FSstp]]]] |
LDI].
right.
exists sm.
exists t'.
rewrite (@
ldo_samekind_eq _ _ _ SK Ldo)
in *.
rewrite <- (
proj2 (
target_determinate _ _ _ _ _ STt1t3 STt5t6)
(
refl_equal l'))
in *.
repeat split;
try assumption;
try apply taustar_refl.
left.
exists lp.
exists s'.
repeat split;
try assumption.
destruct (
LDI _ (
ldi_refl l'))
as [
s'' [
STsmlpspp FSspptp]].
destruct (
source_receptive _ _ _ _ STsmlpspp SK)
as [
s2 STsms2].
destruct fsim as [
_ FS].
destruct (
FS sm tm l s2 STsms2 FSstm)
as
[
Err |
[[
Ltau [
FS'
FSCss]] |
[
t2p [[
l2p [
LDO2 [
WSlp2 FSs2t2]]] | [
WSt1lt2 LDI2]]]]];
clear FS.
eby left;
eapply ev_stuck_or_error_taustar.
contradiction.
assert (
L2pntau:
l2p <>
tau _).
intro L2ptau.
rewrite L2ptau in *.
apply ldo_not_tau in LDO2.
assumption.
pose proof (@
ldo_samekind_eq _ _ _
(@
weakstep_samekind _ _ _ _ _ Lntau'
L2pntau WStmtp WSlp2)
LDO2)
as Eq_lp_l2p.
rewrite <-
Eq_lp_l2p in *.
pose proof (@
ldo_samekind_eq _ _ _ SK LDO2)
as Eq_l_lp.
rewrite <-
Eq_l_lp in *.
right.
exists sm.
exists t'.
rewrite <- (
proj2 (
target_determinate _ _ _ _ _ STt1t3 STt5t6)
(
refl_equal l))
in *.
repeat split;
try done;
try apply taustar_refl.
by right.
right.
exists sm.
exists t2p.
repeat split.
assumption.
destruct WSt1lt2 as [
tmx [
tmy [
TStmtmx [
STtmxtmy TStmyt2p]]]].
by rewrite (
proj2 (
proj2 (@
taustar_labels _ _ target_determinate _ _ _ _ _ _ _
Lntau Lntau TStmtmx STtmxtmy TStmt5 STt1t3)) (
refl_equal l))
in TStmyt2p.
by right.
Qed.
Lemma sourcesim_nontau_with_undefs:
forall s t t1 t2 l,
fsr s t ->
l <>
tau lbl ->
taustar tgt t t1 ->
stepr tgt t1 l t2 ->
ev_stuck_or_error _ s \/
(
exists s1,
exists t',
taustar src s s1 /\
taustar tgt t2 t' /\
((
exists l',
exists s',
ldo l'
l /\
stepr src s1 l'
s' /\
fsr s'
t') \/
(
forall l',
ldi l'
l ->
exists s',
stepr src s1 l'
s' /\
fsr s'
t'))).
Proof.
Lemma taustar_stuck_sim_with_undefs:
forall s t ts,
fsr s ts ->
taustar tgt t ts ->
stuck tgt t ->
ev_stuck_or_error _ s.
Proof.
Lemma taustar_stuck_sim2_with_undef:
forall t t',
taustar tgt t t' ->
forall s ts,
fsr s ts ->
taustar tgt t ts ->
stuck tgt t' ->
ev_stuck_or_error _ s.
Proof.
The main result: bsr and bsc are backward simulation with undefs.
Theorem forward_to_backward_sim_with_undefs:
backward_sim_with_undefs (@
bsr _ _ _ fsr) (@
bsc _ _).
Proof.
End ForwardToBackwardSim.
End ForwardToBackwardUndefSim.
Simpler interface to per-thread forward simulation
Section ForwardThreadEventUndefSim.
Variable src tgt :
lts thread_labels.
Variable r :
St src ->
St tgt ->
Prop.
Variable c :
St src ->
St src ->
Prop.
Definition forward_sim_with_undefs2 :=
forall s t l s',
stepr _ s l s' ->
r s t ->
(
ev_stuck_or_error _ s) \/
(
match l with
|
TEmem (
MEread p c v) =>
(
exists t',
weakstep tgt t (
TEmem (
MEread p c v))
t'
/\
forall v',
Val.lessdef v'
v ->
exists s'',
stepr _ s (
TEmem (
MEread p c v'))
s'' /\
r s''
t')
|
TEmem (
MErmw p c v f) =>
(
exists t',
weakstep tgt t (
TEmem (
MErmw p c v f))
t'
/\
forall v',
Val.lessdef v'
v ->
exists s'',
stepr _ s (
TEmem (
MErmw p c v'
f))
s'' /\
r s''
t')
|
TEtau => (
c s'
s /\
r s'
t) \/ (
exists t',
weakstep tgt t TEtau t' /\
r s'
t')
|
TEmem (
MEwrite p c v) =>
(
exists t',
exists v',
Val.lessdef v v'
/\
weakstep tgt t (
TEmem (
MEwrite p c v'))
t' /\
r s'
t')
|
TEstart p v =>
(
exists t',
exists v',
Val.lessdef_list v v'
/\
weakstep tgt t (
TEstart p v')
t' /\
r s'
t')
|
TEstartmem p v =>
(
exists t',
exists v',
Val.lessdef_listsum v v'
/\
weakstep tgt t (
TEstartmem p v')
t' /\
r s'
t')
|
_ => (
exists t',
weakstep tgt t l t' /\
r s'
t')
end).
Lemma mk_forward_sim_with_undefs:
forall
(
WF:
well_founded c)
(
FSIM:
forward_sim_with_undefs2),
@
forward_sim_with_undefs thread_labels src tgt te_ldo te_ldi r c.
Proof.
split; [
done|].
intros s t l s'
H1 H2.
specialize (
FSIM s t l s'
H1 H2).
case FSIM;
clear FSIM;
intro FSIM; [
left;
done|
right];
simpl.
(
destruct l as [[]|[]| | | | | |]);
simpl;
try
(
by revert FSIM;
intros [
t' [
WS R]];
right;
exists t';
right;
split; [
apply WS|];
intros [[]|[]| | | | | |];
try done;
simpl;
intros;
clarify;
repeat match goal with H:
_ /\
_ |-
_ =>
destruct H end;
clarify;
eauto).
Case "
MEwrite".
revert FSIM;
intros [
t' [
v' [? [? ?]]]].
eby right;
exists t';
left;
eexists (
TEmem (
MEwrite _ _ v'));
repeat split.
Case "
TEtau".
destruct FSIM as [[? ?]|[
t' [? ?]]]; [
left;
done|].
right;
exists t';
right;
split; [
done|].
eby intros [[]|[]| | | | | |];
try done;
simpl;
intros;
clarify;
eexists.
Case "
TEstart".
revert FSIM;
intros [
t' [
v' [? [? ?]]]].
eby right;
exists t';
left;
eexists (
TEstart _ v');
repeat split.
Case "
TEstartmem".
revert FSIM;
intros [
t' [
v' [? [? ?]]]].
eby right;
exists t';
left;
eexists (
TEstartmem _ v');
repeat split.
Qed.
End ForwardThreadEventUndefSim.