Require Import Footprint InteractionSemantics GAST GMemory
GlobDefs ETrace GlobSemantics NPSemantics TypedSemantics.
Require Import DRF USimDRF NPDRF .
Require Import FPLemmas PRaceLemmas Init SmileReorder ConflictReorder Init DRFLemmas RefineEquiv.
Require Import Classical.
Equivalence on safety and DRF definitions between preemptive and non-preemptive semantics
This file consists of results on np-semantics:
- Safe(S) <=> NPSafe(S)
- Safe(S) /\ WD_langs(S) => (NPDRF(S) <=> DRF(S))
Lemma drf_drfpc:
forall NL L p gm ge pc t,
@
init_config NL L p gm ge pc t->
drf p ->
drfpc pc.
Proof.
Local Notation "{-|
PC ,
T }" := ({|
thread_pool :=
thread_pool PC;
cur_tid :=
T;
gm :=
gm PC;
atom_bit :=
atom_bit PC |}) (
at level 70,
right associativity).
Lemma DRF_NP_Refine_Config:
forall NL L mu su tu e sgm sge spc st tgm tge tpc tt,
@
wd_langs NL L su ->
@
wd_langs NL L tu ->
(
forall t :
tid,
DRFLemmas.pc_valid_tid tpc t ->
np_safe_config ({-|
tpc,
t})) ->
InitRel mu sge tge sgm tgm->
init_config (
su,
e)
sgm sge spc st->
init_config (
tu,
e)
tgm tge tpc tt->
drf (
su,
e)->
drfpc tpc->
np_prog_refine (
su,
e)(
tu,
e)->
config_refine tpc spc.
Proof.
Equivalence between preemptive and non-preemptive safety definition
Lemma Safe_NPSafe:
forall NL L cus e,
@
wd_langs NL L cus ->
safe_prog (
cus,
e) ->
np_safe_prog (
cus,
e).
Proof.
intros.
econstructor.
intros.
apply H0 in H1 as ?.
apply Safe_eq.
unfold safe_state in *.
intros.
intro.
assert(
t=
cur_tid s).
inversion H1;
auto.
subst.
eapply star_abort_np_p in H4;
eauto.
Focus 2.
econstructor;
eauto.
Esimpl;
eauto.
apply np_star_glob_star in H3 as [].
eapply H2 in H3;
eauto.
Qed.
Lemma NPSafe_Safe:
forall NL L cus e,
@
wd_langs NL L cus ->
np_safe_prog (
cus,
e) ->
npdrf (
cus,
e) ->
safe_prog (
cus,
e).
Proof.
apply NPSafe_Safe';auto.
Qed.
Lemma NPDRF_config:
forall NL L p gm ge pc t,
npdrf p->
@
init_config NL L p gm ge pc t->
(
forall t,
GSimDefs.pc_valid_tid pc t->
npdrfpc ({-|
pc,
t})).
Proof.
intros.
assert(
t=
cur_tid pc).
inversion H0;
auto.
subst.
eapply init_free in H0;
eauto.
unfold npdrf in H.
unfold npdrfpc.
apply not_or_and.
intro.
contradict H.
destruct H2.
econstructor;
eauto.
econstructor 2;
eauto.
Qed.
Equivalence between DRF definitions between preemptive and non-preemptive program configurations
Lemma NPDRF_DRF_Config:
forall NL L p gm ge pc t,
@
wd_langs NL L (
fst p) ->
init_config p gm ge pc t ->
(
forall t,
GSimDefs.pc_valid_tid pc t->
np_safe_config ({-|
pc,
t})) ->
(
forall t,
GSimDefs.pc_valid_tid pc t ->
npdrfpc ({-|
pc,
t})) ->
drfpc pc.
Proof.
Lemma DRF_NPDRF_Config:
forall NL L p gm ge pc t,
@
wd_langs NL L (
fst p) ->
init_config p gm ge pc t ->
drfpc pc ->
npdrfpc pc.
Proof.