Require Import InteractionSemantics GAST GlobUSim NPSemantics NPDRF.
Require Import ETrace GlobDefs Footprint Injections GSimDefs GlobSim USimDRF Classical Init.
Simulation implies Refinement
This file defines the lemma USim_NPDRF, which says when
source program simulates target program ( S > T ), and
source program is data-race-free (NPDRF(S)), then
target program is data-race-free (NPDRF(T)).
Local Notation "'[['
thdp ','
t ','
m ','
b ']]'" :=
({|
thread_pool:=
thdp;
cur_tid:=
t;
gm:=
m;
atom_bit:=
b |})
(
at level 70,
right associativity).
Local Notation "'[['
thdp ','
t ','
m ','
b ']]@'
G " :=
(
Build_ProgConfig G thdp t m b) (
at level 70,
right associativity).
Definition npdrfpc {
ge}(
pc:@
ProgConfig ge):
Prop:=
~
np_race_config pc /\ ~
np_star_race_config pc.
NPDRF Preservation(Lemma 6):
In the rule of data race, we always load the program P and the state \sigma to the world W first. Here spc is the source world and tpc is the target world. For convenience we write the load step explicitly.
Lemma USim_NPDRF_Config:
forall NL L sprog tprog mu sgm sge spc t tgm tge tpc,
Source program simulates and target program
@
GlobUSim NL L sprog tprog->
initM(mu,GE,sgm,tgm) the relation of initial memory
InitRel mu sge tge sgm tgm->
load step: (sprog,sgm) ==load==> spc
init_config sprog sgm sge spc t->
load step: (tprog,tgm) ==load==> tpc
init_config tprog tgm tge tpc t->
source program configuration is data-race-free
npdrfpc spc->
Conclusion: target program configuration is data-race-free
npdrfpc tpc.
Proof.