Require Import Coqlib.
Require Import Relations.Relation_Operators.
Require Import Wellfounded.
Require Import Integers.
Require Import Values.
Require Import Pointers.
Require Import Events.
Require Import Mem.
Require Import Ast.
Require Import Globalenvs.
Require Import Maps.
Require Import Simulations.
Require Import Floats.
Require Import TSOmachine.
Require Import Memcomp.
Require Import Memeq.
Require Import Traces.
Require Import MCsimulation.
Require Import Libtactics.
Generic results about the TSO machine
Section TSOresults.
Variables (
Sem :
SEM).
Let tsolts ge := (
mklts event_labels (
Comp.step tso_mm Sem ge)).
Let lts ge := (
mklts thread_labels (
SEM_step Sem ge)).
Hint Constructors tso_step :
myhints.
Hint Constructors Comp.mm_arglist :
myhints.
Hint Constructors Comp.mm_arglist_fail :
myhints.
Hint Constructors Comp.mm_ext_arglist :
myhints.
Hint Constructors Comp.mm_ext_arglist_fail :
myhints.
Hint Constructors Val.lessdef_list.
Hint Extern 0 (
MM_step _ _ _ _) =>
simpl.
Lemma stuck_threads_empty_buff_impl_stuck_tso:
forall ge stso sthr
(
FINSUP:
tso_fin_sup stso)
(
STUCK:
(
exists t,
exists ts,
exists e,
exists ts',
sthr !
t =
Some ts /\
e =
TEext Efail /\
SEM_step _ ge ts e ts') \/
forall t,
sthr !
t =
None)
(
BE:
forall t,
stso.(
tso_buffers)
t =
nil),
stuck_or_error (
tsolts ge) (
stso,
sthr).
Proof.
destruct 2
as [(
t &
ts &
e &
ts' &
ST &
Eerr &
ERR) |
STUCK];
intros.
destruct e;
try destruct ev;
simpl in Eerr;
try done.
right;
exists (
stso,
sthr !
t <-
ts');
exists (
Evisible Efail);
split; [
done|].
by simpl;
eapply Comp.step_ext;
eauto.
exploit (
strong_in_dec_prop (
fun (
x:
thread_id *
_) =>
~ (
exists l',
exists s',
SEM_step _ ge (
snd x)
l'
s'))).
-
intros [
tid s];
simpl.
destruct (
SEM_progress_dec _ ge s)
as [
NO|]; [|
by right].
eby left;
intros (? & ? & ?);
ecase NO.
instantiate (1 := (
PTree.elements sthr)).
intros [[[
tid ?] [
IN NOST]]|
ALL];
simpl in *.
-
eapply PTree.elements_complete in IN.
right;
eexists (
_,
_);
exists (
Evisible Efail);
split; [
done|];
simpl.
eapply Comp.step_thread_stuck;
try eassumption.
eby intros l'
s'
STEP;
elim NOST;
do 2
eexists.
left;
intros s'
l'
ST.
(
comp_step_cases (
inv ST)
Case);
try by rewrite STUCK in *.
Case "
step_unbuf";
by inv tsoSTEP;
rewrite BE in *.
Qed.
Less-defined memories, buffers, and tso states
Inductive lessdef_mem (
m m' :
mem) :=
|
lessdef_mem_cons:
forall
(
LVS:
mem_lessdef m m')
(
RAS:
arange_eq (
fun _ =>
true)
m m'),
lessdef_mem m m'.
Definition lessdef_buffer_item (
bi bi' :
buffer_item) :
Prop :=
match bi,
bi'
with
|
BufferedWrite p c v,
BufferedWrite p'
c'
v' =>
p =
p' /\
c =
c' /\
Val.lessdef v v'
|
_,
_ =>
bi =
bi'
end.
Inductive lessdef_tso :
tso_state ->
tso_state ->
Prop :=
|
lessdef_tso_cons:
forall b m b'
m'
(
LDM :
lessdef_mem m m')
(
LDB :
forall t,
list_forall2 lessdef_buffer_item (
b t) (
b'
t)),
lessdef_tso (
mktsostate b m) (
mktsostate b'
m').
Lemma lessdef_buffer_item_refl:
forall bi,
lessdef_buffer_item bi bi.
Proof.
by intros []. Qed.
Lemma lessdef_mem_refl:
forall t,
lessdef_mem t t.
Proof.
Hint Resolve lessdef_buffer_item_refl.
Hint Resolve lessdef_mem_refl.
Lemma lessdef_listsum_pfx:
forall {
A l l'} (
h :
A +
val)
(
LD :
Val.lessdef_listsum l l') ,
Val.lessdef_listsum (
h ::
l) (
h ::
l').
Proof.
by intros; destruct h; vauto. Qed.
Lemma lessdef_listsum_refl:
forall {
A} (
l :
list (
A +
val)),
Val.lessdef_listsum l l.
Proof.
by induction l as [|[|]]; constructor. Qed.
Lemma list_forall2_app:
forall A B (
P :
A ->
B ->
Prop)
l1 l2 l1'
l2'
(
LFA :
list_forall2 P l1 l2)
(
LFA':
list_forall2 P l1'
l2'),
list_forall2 P (
l1 ++
l1') (
l2 ++
l2').
Proof.
intros until l1.
induction l1 as [|
h l1 IH];
intros;
inv LFA.
done.
rewrite <- !
app_comm_cons.
by constructor;
auto.
Qed.
Lemma alloc_lessdef_mem:
forall {
m m'}
r k
(
LDM :
lessdef_mem m m'),
match alloc_ptr r k m,
alloc_ptr r k m'
with
|
Some nm,
Some nm' =>
lessdef_mem nm nm'
|
None,
None =>
True
|
_,
_ =>
False
end.
Proof.
Lemma free_lessdef_mem:
forall {
m m'}
p k
(
LDM :
lessdef_mem m m'),
match free_ptr p k m,
free_ptr p k m'
with
|
Some nm,
Some nm' =>
lessdef_mem nm nm'
|
None,
None =>
True
|
_,
_ =>
False
end.
Proof.
Lemma store_lessdef_mem:
forall {
m m'
v v'}
c p
(
LDM :
lessdef_mem m m')
(
LDV :
Val.lessdef v v'),
match store_ptr c m p v,
store_ptr c m'
p v'
with
|
Some nm,
Some nm' =>
lessdef_mem nm nm'
|
None,
None =>
True
|
_,
_ =>
False
end.
Proof.
Lemma apply_buffer_item_lessdef_mem:
forall {
m m'
bi bi'}
(
LDM :
lessdef_mem m m')
(
LDV :
lessdef_buffer_item bi bi'),
match apply_buffer_item bi m,
apply_buffer_item bi'
m'
with
|
Some nm,
Some nm' =>
lessdef_mem nm nm'
|
None,
None =>
True
|
_,
_ =>
False
end.
Proof.
Lemma apply_buffer_lessdef_mem:
forall {
m m'
b b'}
(
LDM :
lessdef_mem m m')
(
LDB :
list_forall2 lessdef_buffer_item b b'),
match apply_buffer b m,
apply_buffer b'
m'
with
|
Some nm,
Some nm' =>
lessdef_mem nm nm'
|
None,
None =>
True
|
_,
_ =>
False
end.
Proof.
intros m m'
b;
revert m m'.
induction b as [|
bi b IH];
intros.
by inv LDB.
inversion LDB as [|
bi1 bt1 bi2 bt2 LDBI LDBF E1 E2].
subst.
pose proof (
apply_buffer_item_lessdef_mem LDM LDBI)
as LDM'.
simpl.
destruct (
apply_buffer_item bi m)
as [
nm|]
_eqn :
ABI;
destruct (
apply_buffer_item bi2 m')
as [
nm'|]
_eqn :
ABI';
try done; [].
by apply IH.
Qed.
Lemma unbuffer_lessdef_tso:
forall b m bi bt nm b'
m'
bi'
bt'
nm'
t
(
LD :
lessdef_tso (
mktsostate b m) (
mktsostate b'
m'))
(
BD :
b t =
bi ::
bt)
(
ABI :
apply_buffer_item bi m =
Some nm)
(
BD' :
b'
t =
bi' ::
bt')
(
ABI':
apply_buffer_item bi'
m' =
Some nm'),
lessdef_tso (
mktsostate (
tupdate t bt b)
nm)
(
mktsostate (
tupdate t bt'
b')
nm').
Proof.
intros.
inversion LD.
subst.
assert (
LDBt :=
LDB t).
rewrite BD,
BD'
in LDBt.
inversion LDBt as [|
bi1 bt1 bi2 bt2 LDBI LDBF E1 E2].
subst.
constructor.
assert (
LDM' :=
apply_buffer_item_lessdef_mem LDM LDBI).
by rewrite ABI,
ABI'
in LDM'.
by intro t';
destruct (
peq t'
t)
as [-> |
N];
[
rewrite !
tupdate_s |
rewrite !
tupdate_o].
Qed.
Lemma buffer_insert_lessdef_tso:
forall {
tso tso'
bi bi'}
t
(
LD :
lessdef_tso tso tso')
(
LDBI :
lessdef_buffer_item bi bi'),
lessdef_tso (
buffer_insert tso t bi) (
buffer_insert tso'
t bi').
Proof.
intros.
inv LD.
constructor.
done.
intros t'.
specialize (
LDB t').
destruct (
peq t'
t)
as [-> |
N].
rewrite !
tupdate_s.
apply list_forall2_app.
done.
by constructor;
vauto.
by rewrite !
tupdate_o.
Qed.
Lemma load_lessdef_mem:
forall {
m m'}
p c
(
LD :
lessdef_mem m m'),
match load_ptr c m p,
load_ptr c m'
p with
|
Some v,
Some v' =>
Val.lessdef v v'
|
None,
None =>
True
|
_,
_ =>
False
end.
Proof.
intros.
pose proof (
load_chunk_allocated_spec c m p)
as LS.
pose proof (
load_chunk_allocated_spec c m'
p)
as LS'.
inv LD.
specialize (
LVS p c).
destruct (
load_ptr c m p)
as [
v|]
_eqn :
Ev;
destruct (
load_ptr c m'
p)
as [
v'|]
_eqn :
Ev';
simpl in *;
try done.
destruct LS'
as [[
r [
k (
RI &
RA)]]
ALG].
apply RAS in RA; [|
done].
elim LS.
by split;
vauto.
Qed.
Unbuffer safety does not depend on value definedness.
Lemma unbuffer_safe_lessdef:
forall t t',
lessdef_tso t t' ->
unbuffer_safe t' ->
unbuffer_safe t.
Proof.
intros tso tso'
LD US.
revert tso LD.
induction US;
intros;
inversion LD;
subst.
constructor;
simpl in *.
-
intros t bi bt BD.
specialize (
LDB t).
rewrite BD in LDB.
inversion LDB as [|
bi1 bt1 bi2 bt2 LDBI LDBF E1 E2].
subst.
exploit ABIS.
eby symmetry.
intros [
nm'
ABInm'].
assert (
LDMn :=
apply_buffer_item_lessdef_mem LDM LDBI).
destruct (
apply_buffer_item bi m)
as [
nm|]
_eqn:
ABInm;
rewrite ABInm'
in LDMn; [|
done].
eby eexists.
-
intros t bi bt nm BD ABInm.
specialize (
LDB t).
rewrite BD in LDB.
inversion LDB as [|
bi1 bt1 bi2 bt2 LDBI LDBF E1 E2].
subst.
exploit ABIS.
eby symmetry.
intros [
nm'
ABInm'].
assert (
LDMn :=
apply_buffer_item_lessdef_mem LDM LDBI).
rewrite ABInm',
ABInm in LDMn.
eapply H.
eby symmetry.
edone.
apply sym_eq in E2.
eby eapply unbuffer_lessdef_tso.
Qed.
Lemma unbuffer_safe_lessdef_rev:
forall t t',
lessdef_tso t'
t ->
unbuffer_safe t' ->
unbuffer_safe t.
Proof.
intros tso tso'
LD US.
revert tso LD.
induction US;
intros;
inversion LD;
subst.
constructor;
simpl in *.
-
intros t bi bt BD.
specialize (
LDB t).
rewrite BD in LDB.
inversion LDB as [|
bi1 bt1 bi2 bt2 LDBI LDBF E1 E2].
subst.
exploit ABIS.
eby symmetry.
intros [
nm'
ABInm'].
assert (
LDMn :=
apply_buffer_item_lessdef_mem LDM LDBI).
destruct (
apply_buffer_item bi m')
as [
nm|]
_eqn:
ABInm;
rewrite ABInm'
in LDMn; [|
done].
eby eexists.
-
intros t bi bt nm BD ABInm.
specialize (
LDB t).
rewrite BD in LDB.
inversion LDB as [|
bi1 bt1 bi2 bt2 LDBI LDBF E1 E2].
subst.
exploit ABIS.
eby symmetry.
intros [
nm'
ABInm'].
assert (
LDMn :=
apply_buffer_item_lessdef_mem LDM LDBI).
rewrite ABInm',
ABInm in LDMn.
eapply H.
eby symmetry.
edone.
apply sym_eq in E1.
eby eapply unbuffer_lessdef_tso.
Qed.
Lemma unbuffer_safe_lessdef_iff:
forall t t',
lessdef_tso t'
t ->
(
unbuffer_safe t <->
unbuffer_safe t').
Proof.
Lemma ldo_step_simulation:
forall {
stso ttso t ev ttso'
l'}
(
LD :
lessdef_tso stso ttso)
(
TSOST:
tso_step ttso (
MMmem t ev)
ttso')
(
LDO :
te_ldo l' (
TEmem ev)),
exists ev',
exists stso',
l' =
TEmem ev' /\
tso_step stso (
MMmem t ev')
stso' /\
lessdef_tso stso'
ttso'.
Proof.
Lemma tso_step_ldi:
forall {
stso ttso t ev ttso'}
(
LD :
lessdef_tso stso ttso)
(
TST:
tso_step ttso (
MMmem t ev)
ttso'),
exists ev',
exists stso',
te_ldi (
TEmem ev') (
TEmem ev) /\
tso_step stso (
MMmem t ev')
stso' /\
lessdef_tso stso'
ttso'.
Proof.
Lemma tso_step_arglist:
forall tlocs stso ttso ttso'
slocs t tvals
(
LD :
lessdef_tso stso ttso)
(
LDlocs :
Val.lessdef_listsum slocs tlocs)
(
MA :
Comp.mm_arglist tso_mm ttso t tlocs tvals ttso'),
exists stso',
exists svals,
Val.lessdef_list svals tvals /\
Comp.mm_arglist tso_mm stso t slocs svals stso' /\
lessdef_tso stso'
ttso'.
Proof.
induction tlocs as [|
h tlocs IH];
intros.
inv LDlocs.
inv MA.
by eauto 8
with myhints.
inversion LDlocs as [|
hslocs tslocks htlocks ttlocks LDh LDt];
subst.
inv MA.
destruct hslocs as [|
v'].
done.
destruct (
IH _ _ _ _ _ _ LD LDt MA0)
as [
stso' [
svals (
LD' &
MA' &
LDtso')]].
by eauto 8
with myhints.
destruct hslocs as [[
p'
c']|]; [|
done].
inv LDh.
inv RD.
destruct (
IH _ _ _ _ _ _ LD LDt MA0)
as [
stso' [
svals (
LD' &
MA' &
LDtso')]].
inversion LD;
subst.
pose proof (
apply_buffer_lessdef_mem LDM (
LDB t))
as ABLD.
simpl in AB.
rewrite AB in ABLD.
destruct (
apply_buffer (
b t)
m)
as [
nm|]
_eqn :
AB'; [|
done].
pose proof (
load_lessdef_mem p c ABLD)
as LDLD.
rewrite LD0 in LDLD.
destruct (
load_ptr c nm p)
as [
v'|]
_eqn :
LDx; [|
done].
by eauto 9
with myhints.
Qed.
Lemma tso_step_arglist_fail:
forall tlocs stso ttso slocs t
(
LD :
lessdef_tso stso ttso)
(
LDlocs :
Val.lessdef_listsum slocs tlocs)
(
MA :
Comp.mm_arglist_fail tso_mm ttso t tlocs),
Comp.mm_arglist_fail tso_mm stso t slocs.
Proof.
induction tlocs as [|
h tlocs IH];
intros.
inv LDlocs.
inv MA.
inversion LDlocs as [|
hslocs tslocks htlocks ttlocks LDh LDt];
subst.
inv MA.
destruct hslocs as [[
p'
c']|]; [|
done].
inv LDh.
inv TST.
inversion LD;
subst.
simpl in Bemp.
pose proof (
apply_buffer_lessdef_mem LDM (
LDB t))
as ABLD.
pose proof (
LDB t)
as LDBt.
rewrite Bemp in *.
inv LDBt.
replace (
b t)
with (@
nil buffer_item)
in ABLD.
simpl in *.
pose proof (
load_lessdef_mem p c ABLD)
as LDLD.
rewrite LD0 in LDLD.
by destruct (
load_ptr c m p)
as []
_eqn :
LDs;
eauto with myhints.
destruct hslocs as [|
v'].
done.
specialize (
IH _ _ _ _ LD LDt MA0).
by constructor.
destruct hslocs as [[
p'
c']|]; [|
done].
inv LDh.
inv RD.
specialize (
IH _ _ _ _ LD LDt MA0).
inversion LD;
subst.
pose proof (
apply_buffer_lessdef_mem LDM (
LDB t))
as ABLD.
simpl in AB.
rewrite AB in ABLD.
destruct (
apply_buffer (
b t)
m)
as [
nm|]
_eqn :
AB'; [|
done].
pose proof (
load_lessdef_mem p c ABLD)
as LDLD.
rewrite LD0 in LDLD.
destruct (
load_ptr c nm p)
as [
v'|]
_eqn :
LDx; [|
done].
eauto with myhints.
Qed.
Lemma tso_step_ext_arglist_fail:
forall stso ttso locs t
(
LD :
lessdef_tso stso ttso)
(
MA :
Comp.mm_ext_arglist_fail tso_mm ttso t locs),
Comp.mm_ext_arglist_fail tso_mm stso t locs.
Proof.
induction locs as [|
h locs IH];
intros.
by inv MA.
inv MA;
eauto with myhints.
inv TST.
inversion LD;
subst.
simpl in Bemp.
pose proof (
apply_buffer_lessdef_mem LDM (
LDB t))
as ABLD.
pose proof (
LDB t)
as LDBt.
rewrite Bemp in *.
inv LDBt.
replace (
b t)
with (@
nil buffer_item)
in ABLD.
simpl in *.
pose proof (
load_lessdef_mem p c ABLD)
as LDLD.
rewrite LD0 in LDLD.
by destruct (
load_ptr c m p)
as []
_eqn;
eauto with myhints.
inv TST.
inversion LD;
subst.
pose proof (
apply_buffer_lessdef_mem LDM (
LDB t))
as ABLD.
simpl in AB.
rewrite AB in ABLD.
destruct (
apply_buffer (
b t)
m)
as [
nm|]
_eqn :
AB'; [|
done].
pose proof (
load_lessdef_mem p c ABLD)
as LDLD.
rewrite LD0 in LDLD.
destruct (
load_ptr c nm p)
as [
v'|]
_eqn :
LDx; [|
done].
inv LDLD;
eapply Comp.mm_ext_arglist_fail_everr;
vauto;
try done;
by intros [].
inv RD.
inversion LD;
subst.
pose proof (
apply_buffer_lessdef_mem LDM (
LDB t))
as ABLD.
simpl in AB.
rewrite AB in ABLD.
destruct (
apply_buffer (
b t)
m)
as [
nm|]
_eqn :
AB'; [|
done].
pose proof (
load_lessdef_mem p c ABLD)
as LDLD.
rewrite LD0 in LDLD.
by destruct (
load_ptr c nm p)
as []
_eqn;
eauto with myhints.
Qed.
Lemma tso_step_ext_arglist:
forall stso ttso ttso'
locs t vals
(
LD :
lessdef_tso stso ttso)
(
MA :
Comp.mm_ext_arglist tso_mm ttso t locs vals ttso'),
Comp.mm_ext_arglist_fail tso_mm stso t locs \/
exists stso',
Comp.mm_ext_arglist tso_mm stso t locs vals stso' /\
lessdef_tso stso'
ttso'.
Proof.
induction locs as [|
h locs IH];
intros;
inv MA;
eauto with myhints.
-
by destruct (
IH _ _ LD MA0)
as [
FAIL | [
stso' (
MA' &
LDtso')]];
eauto with myhints.
inv RD.
inversion LD;
subst.
pose proof (
apply_buffer_lessdef_mem LDM (
LDB t))
as ABLD.
simpl in AB.
rewrite AB in ABLD.
destruct (
apply_buffer (
b t)
m)
as [
nm|]
_eqn :
AB'; [|
done].
pose proof (
load_lessdef_mem p c ABLD)
as LDLD.
rewrite LD0 in LDLD.
destruct (
load_ptr c nm p)
as [
v'|]
_eqn :
LDx; [|
done].
destruct (
IH _ _ LD MA0)
as [
FAIL | [
stso' (
MA' &
LDtso')]];
[
by eauto with myhints|].
destruct (
val_of_eval_dec v')
as [[
ev' <-] |
NVOE]; [|
by eauto with myhints].
apply lessdef_val_of_eval,
val_of_eval_eq in LDLD.
subst ev'.
by right;
eauto 8
with myhints.
Qed.
Lemma tso_step_nomem_sim:
forall {
stso ttso ev ttso'}
(
LD :
lessdef_tso stso ttso)
(
TST:
tso_step ttso ev ttso')
(
NM :
match ev with MMmem _ _ =>
False |
_ =>
True end),
exists stso',
tso_step stso ev stso' /\
lessdef_tso stso'
ttso'.
Proof.
intros.
inv TST;
try done;
try (
by exists stso;
split; [|
assumption];
econstructor; [
edone|];
intro US;
elim UNS;
refine (
unbuffer_safe_lessdef_rev _ _ _ US);
by apply buffer_insert_lessdef_tso).
exists stso;
split; [|
assumption];
econstructor;
inv LD;
simpl in *.
-
specialize (
LDB t).
rewrite Bemp in LDB.
by inv LDB.
-
pose proof (
load_lessdef_mem p c LDM)
as LDLD.
rewrite LD0 in LDLD.
by destruct (
load_ptr c m p).
exists stso;
split; [|
assumption];
econstructor;
inv LD;
simpl in *.
-
by generalize (
LDB t);
rewrite Bemp;
inversion 1.
pose proof (
free_lessdef_mem p k LDM).
do 2 (
destruct free_ptr;
clarify);
des.
eexists tid'.
specialize (
LDB tid').
destruct (
b'
tid');
clarify.
destruct (
b tid')
as [|[]];
inv LDB;
clarify.
pose proof (
apply_buffer_item_lessdef_mem H H4);
simpl in *.
repeat eexists;
try done.
by do 2 (
destruct store_ptr;
clarify).
exists stso;
split; [|
assumption];
econstructor.
intros p US.
elim (
OOM p).
refine (
unbuffer_safe_lessdef_rev _ _ _ US);
by apply buffer_insert_lessdef_tso.
inversion LD;
subst.
specialize (
LDB t).
simpl in *.
rewrite EQbufs in LDB.
inversion LDB as [|
bi1 bt1 bi2 bt2 LDBI LDBF E1 E2].
subst.
pose proof (
apply_buffer_item_lessdef_mem LDM LDBI)
as LDAB.
rewrite AB in LDAB.
destruct (
apply_buffer_item bi1 m)
as [
nm'|]
_eqn :
ABI'; [|
done].
eexists.
split.
econstructor;
try edone;
eby symmetry.
by eapply unbuffer_lessdef_tso;
try edone.
eexists;
split; [
by vauto|].
inv LD.
split.
done.
intro t';
destruct (
peq t'
newtid)
as [<- |
N].
rewrite !
tupdate_s.
by constructor.
by rewrite !
tupdate_o;
auto.
eexists;
split.
econstructor.
inv LD.
simpl in *.
specialize (
LDB t).
by rewrite Bemp in LDB;
inv LDB.
done.
Qed.
End TSOresults.
TSO backward simulation from per-thread backward simulation
Module TSOsim_with_undefs.
Section TSObackwardsim.
Variables (
Src Tgt :
SEM).
Let as assume that there is a relation on global environments and
a simulation relation on states.
Variable genv_rel :
Src.(
SEM_GE) ->
Tgt.(
SEM_GE) ->
Prop.
Variable st_rel :
Src.(
SEM_GE) ->
Tgt.(
SEM_GE) ->
Tgt.(
SEM_ST) ->
Src.(
SEM_ST) ->
Prop.
Variable st_order :
Src.(
SEM_GE) ->
Tgt.(
SEM_GE) ->
Tgt.(
SEM_ST) ->
Tgt.(
SEM_ST) ->
Prop.
Variable match_prg :
Src.(
SEM_PRG) ->
Tgt.(
SEM_PRG) ->
Prop.
Related environments have the same main function.
Hypothesis main_ptr_eq:
forall src_prog tgt_prog,
forall sge tge
(
MP :
match_prg src_prog tgt_prog)
(
GENVR:
genv_rel sge tge),
Src.(
SEM_find_symbol)
sge (
Src.(
SEM_main_fn_id)
src_prog) =
Tgt.(
SEM_find_symbol)
tge (
Tgt.(
SEM_main_fn_id)
tgt_prog).
We assume that for any intial global environment of the transformed
program there is a related initial env of the source program.
Hypothesis ge_init_related :
forall src_prog tgt_prog,
forall tge m
(
MP :
match_prg src_prog tgt_prog)
(
INIT:
Tgt.(
SEM_ge_init)
tgt_prog tge m),
exists sge,
Src.(
SEM_ge_init)
src_prog sge m /\
genv_rel sge tge.
Suppose that the initial states of threads spawned in related
environments are related.
Hypothesis thread_init_related:
forall sge tge tgt_init fnp args args'
(
GENVR :
genv_rel sge tge)
(
INIT :
Tgt.(
SEM_init)
tge fnp args =
Some tgt_init)
(
LD :
Val.lessdef_list args'
args),
exists src_init,
Src.(
SEM_init)
sge fnp args' =
Some src_init /\
st_rel sge tge tgt_init src_init.
Hypothesis thread_init_related_none:
forall sge tge fnp args args'
(
GENVR :
genv_rel sge tge)
(
INITF :
Tgt.(
SEM_init)
tge fnp args =
None)
(
LD :
Val.lessdef_list args'
args),
Src.(
SEM_init)
sge fnp args' =
None.
... and assume that there is a per-thread backward simulation in
related environments.
Hypothesis thread_backward_sim:
forall sge tge
(
GENR :
genv_rel sge tge),
backward_sim_with_undefs
(
mklts thread_labels (
Src.(
SEM_step)
sge))
(
mklts thread_labels (
Tgt.(
SEM_step)
tge))
te_ldo
te_ldi
(
st_rel sge tge)
(
st_order sge tge).
We extend this simulation to the simulation on the tso_states
Definition tso_rel sge tge (
sst :
Comp.state tso_mm Src) (
tst :
Comp.state tso_mm Tgt) :=
let '((
stso,
srct), (
ttso,
tgtt)) := (
sst,
tst)
in
lessdef_tso stso ttso /\
forall t,
srct !
t =
None /\
tgtt !
t =
None \/
exists ss,
exists ts,
srct !
t =
Some ss /\
tgtt !
t =
Some ts /\
st_rel sge tge ts ss.
Definition tso_order sge tge (
t1 t2 :
Comp.state tso_mm _) :=
PTree.order (
st_order sge tge) (
snd t1) (
snd t2) /\
fst t1 =
fst t2.
For each intial state of the target TSO there is a corresponding
initial state of the source machine.
Theorem tso_init_related:
forall src_prog tgt_prog args tge tstate,
match_prg src_prog tgt_prog ->
Comp.init _ _ tgt_prog args tge tstate ->
exists sge,
exists sstate,
Comp.init _ _ src_prog args sge sstate /\
genv_rel sge tge /\
tso_rel sge tge sstate tstate.
Proof.
Lemma wf_tso_order:
forall sge tge (
GREL:
genv_rel sge tge),
well_founded (
tso_order sge tge).
Proof.
Section TSObackwardsim1.
Variables (
sge :
Src.(
SEM_GE)) (
tge :
Tgt.(
SEM_GE)).
Variable (
sge_tge_rel :
genv_rel sge tge).
Let srctsolts := (
mklts event_labels (
Comp.step tso_mm _ sge)).
Let tgttsolts := (
mklts event_labels (
Comp.step tso_mm _ tge)).
Let srclts := (
mklts thread_labels (
SEM_step _ sge)).
Let tgtlts := (
mklts thread_labels (
SEM_step _ tge)).
Lemma tso_rel_buff_empty:
forall {
ttso tthr stso sthr t},
tso_rel sge tge (
stso,
sthr) (
ttso,
tthr) ->
tso_buffers ttso t =
nil ->
tso_buffers stso t =
nil.
Proof.
destruct 1 as [[] _].
simpl. specialize (LDB t). intro E. rewrite E in LDB. by inv LDB.
Qed.
Hint Resolve taustar_refl.
Lemma stuck_rel_tau_stuck_aux:
forall (
tl :
list thread_id)
stso ttso sthr tthr,
(
forall t ts,
tthr!
t =
Some ts ->
False) ->
tso_rel sge tge (
stso,
sthr) (
ttso,
tthr) ->
exists thr',
taustar srctsolts (
stso,
sthr) (
stso,
thr') /\
((
exists t,
exists ts,
exists e,
exists ts',
thr' !
t =
Some ts /\
e =
TEext Efail /\
Src.(
SEM_step)
sge ts e ts') \/
forall t,
(
sthr !
t =
None /\
thr' !
t =
None) \/
(~
In t tl /\
sthr !
t =
thr' !
t)).
Proof.
intros tl stso ttso sthr tthr TSTUCK REL.
induction tl as [|
it irest IH].
exists sthr;
split;
try done.
by right;
right;
auto.
destruct IH as [
thri [
TST [
ERR |
IH]]].
exists thri.
split;
auto.
destruct (
tthr !
it)
as [
tits|]
_eqn :
Etit.
by pose proof (
TSTUCK it tits Etit).
exists thri.
split;
try done.
right.
intro t.
destruct (
IH t)
as [[
SN TN] | [
NI E]];
try (
repeat (
try (
left;
tauto);
right);
fail).
destruct (
tid_eq_dec it t)
as [
Eitt |
Neitt].
subst.
destruct (
proj2 REL t)
as [[
RELN _]|[
sit [
tst [
Esit [
Etst RELs]]]]].
left.
rewrite <-
E;
split;
auto.
by rewrite Etit in Etst.
right;
split;
auto.
intro NINit.
destruct (
in_inv NINit);
subst;
auto.
Qed.
Lemma stuck_rel_tau_stuck:
forall stso ttso sthr tthr,
(
forall t ts,
tthr!
t =
Some ts ->
False) ->
tso_rel sge tge (
stso,
sthr) (
ttso,
tthr) ->
exists thr',
taustar srctsolts (
stso,
sthr) (
stso,
thr') /\
((
exists t,
exists ts,
exists e,
exists ts',
thr' !
t =
Some ts /\
e =
TEext Efail /\
SEM_step _ sge ts e ts') \/
forall t,
thr' !
t =
None).
Proof.
intros stso ttso sthr tthr STUCK REL.
destruct (
stuck_rel_tau_stuck_aux (
ptkeys sthr)
_ _ _ _ STUCK REL)
as
[
tso' [
TAU [
ERR |
SP]]].
by exists tso';
split; [|
left].
exists tso'.
split.
auto.
right.
intro t.
destruct (
SP t)
as [
H |[
H E]];
try (
repeat (
try (
try left;
tauto);
right);
fail).
destruct (
sthr !
t)
as [
sit|]
_eqn :
Esit;
try done.
elim H.
apply (
proj2 (
ptkeys_spec _ _)).
by rewrite Esit.
Qed.
Lemma backward_sim_sandwich_step:
forall sthr stso tthr ttso tso'
stso'
t ss ss1 ss'
ts e
(
STREL:
st_rel sge tge ts ss')
(
TSOREL:
tso_rel sge tge (
stso,
sthr) (
ttso,
tthr))
(
Ess:
sthr !
t =
Some ss)
(
TGTST:
Comp.step _ _ tge (
ttso,
tthr)
e (
tso',
tthr !
t <-
ts))
(
TAU1:
taustar srclts ss ss1)
(
TLD:
lessdef_tso stso'
tso')
(
MST:
forall thr',
thr' !
t =
Some ss1 ->
(
forall t',
t <>
t' ->
sthr !
t' =
thr' !
t') ->
Comp.step _ _ sge (
stso,
thr')
e (
stso',
thr' !
t <-
ss')),
exists srcs,
taustep srctsolts (
stso,
sthr)
e srcs /\
tso_rel sge tge srcs (
tso',
tthr !
t <-
ts).
Proof.
intros.
destruct (
taustar_to_comp _ _ stso Ess TAU1)
as [
sthr1 [
STAU1 [
SP1 ST1]]].
pose proof (
MST sthr1 ST1 SP1)
as SSTEP1.
eexists.
split.
by econstructor;
econstructor;
eauto.
split; [
done|].
intro ot.
destruct (
tid_eq_dec ot t).
subst.
by right;
eexists ss';
exists ts;
rewrite !
PTree.gss.
by rewrite !
PTree.gso, <-
SP1;
auto;
apply (
proj2 TSOREL).
Qed.
The main theorem for converting a thread-local simulation to a TSO simulation
Lemma tso_backward_sim:
well_founded (
tso_order sge tge) /\
(
forall s t,
stuck tgttsolts t ->
tso_rel sge tge s t ->
Comp.consistent _ _ s ->
Comp.consistent _ _ t ->
exists s',
taustar srctsolts s s' /\
stuck_or_error _ s') /\
(
forall s t l t',
stepr tgttsolts t l t' ->
tso_rel sge tge s t ->
Comp.consistent _ _ s ->
Comp.consistent _ _ t ->
(
exists s',
taustep srctsolts s l s' /\
tso_rel sge tge s'
t') \/
(
l =
tau _ /\
tso_rel sge tge s t' /\
tso_order sge tge t'
t) \/
(
exists s',
taustar srctsolts s s' /\
can_do_error _ s')).
Proof.
split; [
by apply wf_tso_order|].
split.
intros [
stso sthr] [
ttso tthr]
STUCK REL sCONS tCONS.
pose proof (
Comp.stuck_imp_no_threads _ _ _ _ tCONS (
fun l s' =>
STUCK s'
l))
as STK.
eexists;
split;
try done.
left;
red;
simpl;
intros.
eapply (
Comp.no_threads_stuck _ _ _ _ _ _ sCONS);
eauto;
simpl in *.
eapply PTree.ext;
intro t;
clarify.
by destruct (
proj2 REL t);
des;
rewrite PTree.gempty in *.
intros [
stso sthr] [
ttso tthr]
l t'
TSTEP TREL sCONS tCONS;
simpl in *.
pose proof TREL as [
LD REL].
destruct (
thread_backward_sim _ _ sge_tge_rel)
as [
_ [
SS BS]].
(
comp_step_cases (
inversion TSTEP
as [
os os'
ev ot tso tso'
st st'
SST TST TG TS |
os os'
ev tso st st'
ot SST TG TS |
tso tso'
st TST |
os os'
ot tso st st'
SST TG TS |
os os'
newtid p v ot tso tso'
st st'
sinit SST TST TG TGN TS IN |
os os'
p v ot tso st SST TG IN |
os os'
ot tso tso'
st SST TST TG |
os os'
ot tso tso'
st st'
p c v SST TST TG TS |
os os'
ot tso tso'
st st'
p c v SST TST TG TS |
os os'
ot tso tso'
st st'
p k SST TST TG TS |
os os'
ot tso tso'
st st'
p c v instr SST TST TG TS |
os ot tso st NO_STEP TG |
os os'
ot tso tso'
st st'
p n k SST TST TG TS |
os os'
ot tso st st'
SST TG TS |
os os'
largs args ot tso tso'
st st'
id SST TST TG TS |
os os'
largs ot tso st st'
id SST TST TG TS |
os os'
args ot tso tso'
tso''
st st'
v sinit newtid fn p SST TST TST2 TG TGN TS IN |
os os'
args ot tso st st'
fn SST TST TG TS |
os os'
ot tso st st'
lfn largs fn args tso'
SST TST TG IN TS])
Case);
subst;
first [
Case "
step_unbuf" |
destruct (
REL ot)
as [[? ?] | [
ss [
ts [
Est [
Ett RELs]]]]]];
try rewrite TG in *;
clarify;
try destruct (
BS _ _ _ _ SST RELs)
as [[
ISTAU [
NREL ORD]] |
[
ERROR |
[[
ts' [
l' (
LDO & [
ts1 (
TAU1 &
MST)] &
RELts')]] |
LDIIMPL]]];
try (
eby right;
right;
destruct TREL;
eapply thread_ev_stuck_to_comp_tau_error);
try (
by pose proof LDO as _;
destruct l'
as [|[]| | | | | |]);
try (
by destruct (
LDIIMPL _ (
ldi_refl _))
as [
ts' [[
ts1 (
TAU1 &
MST)]
RELts']];
try destruct (
tso_step_nomem_sim LD TST I)
as [
stso' [
TST'
LD']];
left;
eapply backward_sim_sandwich_step;
try eassumption; [];
vauto).
Case "
step_ord".
by left;
destruct (
ldo_step_simulation LD TST LDO)
as [
ev' [
stso' (-> &
TST' &
LD')]];
eapply backward_sim_sandwich_step;
try eassumption; [];
vauto.
left.
destruct (
tso_step_ldi LD TST)
as [
ev' [
stso' (
LDI &
TST' &
LD')]].
destruct (
LDIIMPL _ LDI)
as [
ts' [[
ts1 (
TAU1 &
MST)]
RELts']].
by eapply backward_sim_sandwich_step;
try eassumption; [];
vauto.
Case "
step_unbuf".
destruct (
tso_step_nomem_sim LD TST I)
as [
stso' [
TST'
LD']].
assert (
WS :
taustep srctsolts (
stso,
sthr)
Etau (
stso',
sthr)).
by eapply step_taustep;
simpl;
vauto.
left;
eexists (
_,
_);
split.
edone.
split.
done.
apply REL.
Case "
step_tau".
right;
left.
split.
done.
split.
split.
by apply (
proj1 TREL).
intro xt.
destruct (
tid_eq_dec xt ot).
subst.
right.
exists ss.
exists os'.
rewrite PTree.gss;
auto.
repeat rewrite PTree.gso;
auto.
by split;
try done;
apply (
PTree.order_set_lt _ _ _ _ TG ORD).
Case "
step_start".
left.
destruct (
tso_step_nomem_sim LD TST I)
as [
stso' [
TST'
LD']].
destruct l'
as [| [] | | |
p'
v' | | |];
try done.
destruct LDO as [->
LDv].
destruct (
taustar_to_comp tso_mm _ stso Est TAU1)
as [
sthr1 [
STAU1 [
SP1 ST1]]].
destruct (
thread_init_related _ _ _ _ _ _ sge_tge_rel IN LDv)
as [
inits [
INITS INREL]].
destruct (
REL newtid)
as [[
NTIDN _] | [
ds [
dt [
_ [
Edt _]]]]];
try (
rewrite Edt in TGN;
discriminate).
destruct (
tid_eq_dec ot newtid)
as [
NTE |
NTNE].
rewrite NTE,
NTIDN in Est;
discriminate.
rewrite SP1 in NTIDN;
auto.
pose proof (
Comp.step_start tso_mm _ _ _ _ _ _ _ _ _ _ _ _ _
MST TST'
ST1 NTIDN (
refl_equal _)
INITS)
as STARTST.
set (
sthr' := (
sthr1 !
ot <-
ts') !
newtid <-
inits).
assert (
ETS2:
sthr' !
ot =
Some ts').
by unfold sthr';
rewrite PTree.gso,
PTree.gss;
auto.
econstructor.
split.
eexists.
split.
apply STAU1.
by vauto.
split;
try done.
intro t.
destruct (
tid_eq_dec t ot).
subst.
by right;
exists ts';
exists os';
repeat rewrite PTree.gso,
PTree.gss.
unfold sthr'
in *.
destruct (
tid_eq_dec t newtid).
subst.
by right;
exists inits;
exists sinit;
rewrite !
PTree.gss.
by rewrite !
PTree.gso, <-
SP1;
auto;
apply (
proj2 REL).
destruct (
tso_step_nomem_sim LD TST I)
as [
stso' [
TST'
LD']].
destruct (
LDIIMPL _ (
ldi_refl _))
as [
ts' [[
ts1 (
TAU1 &
MST)]
RELts']].
left.
destruct (
taustar_to_comp tso_mm _ stso Est TAU1)
as [
sthr1 [
STAU1 [
SP1 ST1]]].
destruct (
thread_init_related _ _ _ _ _ _ sge_tge_rel IN
(
Val.lessdef_list_refl _))
as [
inits [
INITS INREL]].
destruct (
REL newtid)
as [[
NTIDN _] | [
ds [
dt [
_ [
Edt _]]]]];
try (
rewrite Edt in TGN;
discriminate).
destruct (
tid_eq_dec ot newtid)
as [
NTE |
NTNE].
rewrite NTE,
NTIDN in Est;
discriminate.
rewrite SP1 in NTIDN;
auto.
pose proof (
Comp.step_start tso_mm _ _ _ _ _ _ _ _ _ _ _ _ _
MST TST'
ST1 NTIDN (
refl_equal _)
INITS)
as STARTST.
set (
sthr' := (
sthr1 !
ot <-
ts') !
newtid <-
inits).
assert (
ETS2:
sthr' !
ot =
Some ts').
by unfold sthr';
rewrite PTree.gso,
PTree.gss;
auto.
econstructor.
split.
eexists.
split.
apply STAU1.
by vauto.
split;
try done.
intro t.
destruct (
tid_eq_dec t ot).
subst.
by right;
exists ts';
exists os';
repeat rewrite PTree.gso,
PTree.gss.
unfold sthr'
in *.
destruct (
tid_eq_dec t newtid).
subst.
by right;
exists inits;
exists sinit;
rewrite !
PTree.gss.
by rewrite !
PTree.gso, <-
SP1;
auto;
apply (
proj2 REL).
Case "
step_start_fail".
destruct l'
as [| [] | | |
p'
v'| | |];
try done.
destruct LDO as [->
LDv].
left.
eapply (
backward_sim_sandwich_step);
try eassumption.
intros thr'
TS1 _.
pose proof (
thread_init_related_none _ _ _ _ _ sge_tge_rel IN LDv)
as IN'.
eby eapply Comp.step_start_fail.
destruct (
LDIIMPL _ (
ldi_refl _))
as [
ts' [[
ts1 (
TAU1 &
MST)]
RELts']].
left.
eapply (
backward_sim_sandwich_step);
try eassumption.
intros thr'
TS1 _.
pose proof (
thread_init_related_none _ _ _ _ _ sge_tge_rel IN
(
Val.lessdef_list_refl _))
as IN'.
eby eapply Comp.step_start_fail.
Case "
step_exit".
destruct (
tso_step_nomem_sim LD TST I)
as [
stso' [
TST'
LD']].
destruct (
LDIIMPL _ (
ldi_refl _))
as [
ts' [[
ts1 (
TAU1 &
MST)]
RELts']].
left.
destruct (
taustar_to_comp tso_mm _ stso Est TAU1)
as [
sthr1 [
STAU1 [
SP1 ST1]]].
pose proof (
Comp.step_exit tso_mm _ _ _ _ _ _ _ _
MST TST'
ST1)
as EXITST.
econstructor.
split.
eby eexists;
eexists.
split; [
done|].
intro t.
destruct (
tid_eq_dec t ot);
clarify.
by left;
rewrite !
PTree.grs.
by rewrite !
PTree.gro, <-
SP1;
auto;
apply (
proj2 REL).
Case "
step_write_fail".
left.
destruct l'
as [|[]| | | | | |];
try done.
destruct LDO as [-> [->
LDV]].
inv TST.
assert(
TST' :
tso_step stso (
MMreadfail ot p c)
stso).
econstructor;
try edone.
-
eby eapply tso_rel_buff_empty.
revert LD0;
destruct LD;
simpl.
by generalize (
load_lessdef_mem p c LDM);
clear;
do 2 (
destruct load_ptr;
clarify).
by eapply backward_sim_sandwich_step;
try eassumption; [];
vauto.
Case "
step_free_fail".
destruct (
LDIIMPL _ (
ldi_refl _))
as [
ts' [[
ts1 (
TAU1 &
MST)]
RELts']].
destruct (
taustar_to_comp tso_mm _ stso Est TAU1)
as [
sthr1 [
STAU1 [
SP1 ST1]]].
eapply tso_step_nomem_sim in TST;
try edone;
des.
right;
right;
eexists;
split;
try edone.
by eexists (
_,
_);
exists (
Evisible Efail);
split;
simpl;
vauto.
Case "
step_thread_stuck".
exploit SS; [|
apply RELs|
intros ERROR].
-
by intros s'
l'
STEP;
specialize (
NO_STEP _ _ STEP).
eby right;
right;
destruct TREL;
eapply thread_ev_stuck_to_comp_tau_error.
Case "
step_extcallmem".
destruct (
LDIIMPL _ (
ldi_refl _))
as [
ts' [[
ts1 (
TAU1 &
MST)]
RELts']].
destruct (
tso_step_ext_arglist _ _ _ _ _ _ LD TST)
as [
FAIL | [
stso' (
MEA' &
LD')]].
right.
right.
destruct (
taustar_to_comp tso_mm _ stso Est TAU1)
as [
sthr1 [
STAU1 [
SP1 ST1]]].
eexists.
split.
edone.
eexists (
_,
_).
exists (
Evisible Efail).
split.
done.
simpl.
eby eapply Comp.step_extcallmem_fail.
left.
eapply backward_sim_sandwich_step;
try eassumption;
vauto.
Case "
step_extcallmem_fail".
destruct (
LDIIMPL _ (
ldi_refl _))
as [
ts' [[
ts1 (
TAU1 &
MST)]
RELts']].
pose proof (
tso_step_ext_arglist_fail _ _ _ _ LD TST)
as FAIL.
right;
right.
destruct (
taustar_to_comp tso_mm _ stso Est TAU1)
as [
sthr1 [
STAU1 [
SP1 ST1]]].
eexists.
split.
edone.
eexists (
_,
_).
exists (
Evisible Efail).
split.
done.
simpl.
eby eapply Comp.step_extcallmem_fail.
Case "
step_startmem".
destruct l'
as [| [] | | | | |
fn'
args'|];
try done.
destruct LDO as [->
LDargs].
pose proof (
lessdef_listsum_pfx fn LDargs)
as LDfnargs.
destruct (
tso_step_arglist _ _ _ _ _ _ _ LD LDfnargs TST)
as [
stsoi [
svals (
LDsvals &
MAi &
LDstsoi)]].
destruct (
tso_step_nomem_sim LDstsoi TST2 I)
as [
stso' [
TST'
LD']].
destruct (
taustar_to_comp tso_mm _ stso Est TAU1)
as [
sthr1 [
STAU1 [
SP1 ST1]]].
inversion LDsvals as [|
hsvals ?
tsvals ?
LDhsvals LDtsvals];
subst.
destruct (
thread_init_related _ _ _ _ _ _ sge_tge_rel IN LDtsvals)
as [
inits [
INITS INREL]].
destruct (
REL newtid)
as [[
NTIDN _] | [
ds [
dt [
_ [
Edt _]]]]];
try (
rewrite Edt in TGN;
discriminate).
destruct (
tid_eq_dec ot newtid)
as [
NTE |
NTNE].
rewrite NTE,
NTIDN in Est;
discriminate.
rewrite SP1 in NTIDN;
auto.
inv LDhsvals.
pose proof (
Comp.step_startmem tso_mm _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
MST MAi TST'
ST1 NTIDN (
refl_equal _)
INITS)
as STARTST.
set (
sthr' := (
sthr1 !
ot <-
ts') !
newtid <-
inits).
assert (
ETS2:
sthr' !
ot =
Some ts').
by unfold sthr';
rewrite PTree.gso,
PTree.gss;
auto.
left;
econstructor.
split.
eexists.
split.
apply STAU1.
by vauto.
split;
try done.
intro t.
destruct (
tid_eq_dec t ot).
subst.
by right;
exists ts';
exists os';
repeat rewrite PTree.gso,
PTree.gss.
unfold sthr'
in *.
destruct (
tid_eq_dec t newtid).
subst.
by right;
exists inits;
exists sinit;
rewrite !
PTree.gss.
by rewrite !
PTree.gso, <-
SP1;
auto;
apply (
proj2 REL).
right;
right.
eexists.
split.
edone.
eexists (
_,
_);
exists (
Evisible Efail).
split.
done.
simpl.
eby eapply Comp.step_startmem_spawn_fail.
destruct (
LDIIMPL _ (
ldi_refl _))
as [
ts' [[
ts1 (
TAU1 &
MST)]
RELts']].
pose proof (
lessdef_listsum_refl (
fn ::
args))
as LDfnargs.
destruct (
tso_step_arglist _ _ _ _ _ _ _ LD LDfnargs TST)
as [
stsoi [
svals (
LDsvals &
MAi &
LDstsoi)]].
destruct (
tso_step_nomem_sim LDstsoi TST2 I)
as [
stso' [
TST'
LD']].
destruct (
taustar_to_comp tso_mm _ stso Est TAU1)
as [
sthr1 [
STAU1 [
SP1 ST1]]].
inversion LDsvals as [|
hsvals ?
tsvals ?
LDhsvals LDtsvals];
subst.
destruct (
thread_init_related _ _ _ _ _ _ sge_tge_rel IN LDtsvals)
as [
inits [
INITS INREL]].
destruct (
REL newtid)
as [[
NTIDN _] | [
ds [
dt [
_ [
Edt _]]]]];
try (
rewrite Edt in TGN;
discriminate).
destruct (
tid_eq_dec ot newtid)
as [
NTE |
NTNE].
rewrite NTE,
NTIDN in Est;
discriminate.
rewrite SP1 in NTIDN;
auto.
inv LDhsvals.
pose proof (
Comp.step_startmem _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
MST MAi TST'
ST1 NTIDN (
refl_equal _)
INITS)
as STARTST.
set (
sthr' := (
sthr1 !
ot <-
ts') !
newtid <-
inits).
assert (
ETS2:
sthr' !
ot =
Some ts').
by unfold sthr';
rewrite PTree.gso,
PTree.gss;
auto.
left;
econstructor.
split.
eexists.
split.
apply STAU1.
by vauto.
split;
try done.
intro t.
destruct (
tid_eq_dec t ot).
subst.
by right;
exists ts';
exists os';
repeat rewrite PTree.gso,
PTree.gss.
unfold sthr'
in *.
destruct (
tid_eq_dec t newtid).
subst.
by right;
exists inits;
exists sinit;
rewrite !
PTree.gss.
by rewrite !
PTree.gso, <-
SP1;
auto;
apply (
proj2 REL).
right;
right.
eexists.
split.
edone.
eexists (
_,
_);
exists (
Evisible Efail).
split.
done.
simpl.
eby eapply Comp.step_startmem_spawn_fail.
Case "
step_startmem_read_fail".
destruct l'
as [| [] | | | | |
fn'
args'|];
try done.
destruct LDO as [->
LDargs].
pose proof (
lessdef_listsum_pfx fn LDargs)
as LDfnargs.
destruct (
taustar_to_comp tso_mm _ stso Est TAU1)
as [
sthr1 [
STAU1 [
SP1 ST1]]].
right;
right.
eexists.
split.
edone.
pose proof (
tso_step_arglist_fail _ _ _ _ _ LD LDfnargs TST)
as FAIL.
eexists (
_,
_);
exists (
Evisible Efail).
split.
done.
simpl.
eby eapply Comp.step_startmem_read_fail.
destruct (
LDIIMPL _ (
ldi_refl _))
as [
ts' [[
ts1 (
TAU1 &
MST)]
RELts']].
pose proof (
lessdef_listsum_refl (
fn ::
args))
as LDfnargs.
destruct (
taustar_to_comp tso_mm _ stso Est TAU1)
as [
sthr1 [
STAU1 [
SP1 ST1]]].
right;
right.
eexists.
split.
edone.
pose proof (
tso_step_arglist_fail _ _ _ _ _ LD LDfnargs TST)
as FAIL.
eexists (
_,
_);
exists (
Evisible Efail).
split.
done.
simpl.
eby eapply Comp.step_startmem_read_fail.
Case "
step_startmem_spawn_fail".
destruct l'
as [| [] | | | | |
fn'
args'|];
try done.
destruct LDO as [->
LDargs].
pose proof (
lessdef_listsum_pfx lfn LDargs)
as LDfnargs.
destruct (
tso_step_arglist _ _ _ _ _ _ _ LD LDfnargs TST)
as [
stsoi [
svals (
LDsvals &
MAi &
LDstsoi)]].
destruct (
taustar_to_comp tso_mm _ stso Est TAU1)
as [
sthr1 [
STAU1 [
SP1 ST1]]].
inversion LDsvals as [|
hsvals ?
tsvals ?
LDhsvals LDtsvals];
subst.
right;
right.
eexists.
split.
edone.
eexists (
_,
_);
exists (
Evisible Efail).
split.
done.
simpl.
eapply Comp.step_startmem_spawn_fail;
try edone; [].
inv LDhsvals.
destruct fn;
try done.
eby eapply thread_init_related_none.
done.
destruct (
LDIIMPL _ (
ldi_refl _))
as [
ts' [[
ts1 (
TAU1 &
MST)]
RELts']].
pose proof (
lessdef_listsum_refl (
lfn ::
largs))
as LDfnargs.
destruct (
tso_step_arglist _ _ _ _ _ _ _ LD LDfnargs TST)
as [
stsoi [
svals (
LDsvals &
MAi &
LDstsoi)]].
destruct (
taustar_to_comp tso_mm _ stso Est TAU1)
as [
sthr1 [
STAU1 [
SP1 ST1]]].
inversion LDsvals as [|
hsvals ?
tsvals ?
LDhsvals LDtsvals];
subst.
right;
right.
eexists.
split.
edone.
eexists (
_,
_);
exists (
Evisible Efail).
split.
done.
simpl.
eapply Comp.step_startmem_spawn_fail;
try edone; [].
inv LDhsvals.
destruct fn;
try done.
eby eapply thread_init_related_none.
done.
Qed.
End TSObackwardsim1.
Packaging everything into a sim structure.
Definition bsim :
Bsim.sim tso_mm tso_mm Src Tgt match_prg.
Proof.
apply (@
Bsim.make _ _ Src Tgt match_prg
(
fun sge tge s t =>
genv_rel sge tge /\
tso_rel sge tge s t)
(
fun sge tge t t' =>
genv_rel sge tge /\
tso_order sge tge t'
t)).
-
intros ? ? [? ?] [? ?] (
_ &
_ &
A) ? ?;
simpl.
by intro X;
eapply PTree.ext;
intro tid;
generalize (
A tid);
rewrite X, !
PTree.gempty;
intros [(? & ?)|(? & ? & ? & ? &
_)].
-
eby intros;
exploit tso_init_related.
-
intros;
des.
exploit tso_backward_sim;
try edone; [].
intros [
_ [
_ X]];
exploit X;
try edone;
intro;
des;
eauto.
eby right;
left;
eexists.
by right;
right;
vauto.
Defined.
Theorem sim :
Sim.sim tso_mm tso_mm Src Tgt match_prg.
Proof.
End TSObackwardsim.
End TSOsim_with_undefs.