aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--scheduling/BTL.v81
-rw-r--r--scheduling/BTL_SEtheory.v18
-rw-r--r--scheduling/BTLtoRTLproof.v6
-rw-r--r--scheduling/RTLtoBTLproof.v6
4 files changed, 92 insertions, 19 deletions
diff --git a/scheduling/BTL.v b/scheduling/BTL.v
index 10a000a8..cb60fed1 100644
--- a/scheduling/BTL.v
+++ b/scheduling/BTL.v
@@ -83,7 +83,7 @@ Coercion BF: final >-> iblock.
Record iblock_info := {
entry: iblock;
- input_regs: Regset.t (* extra liveness information ignored by BTL semantics *)
+ input_regs: Regset.t (* extra liveness information for BTL functional semantics *)
}.
Definition code: Type := PTree.t iblock_info.
@@ -161,6 +161,9 @@ Record outcome := out {
Section RELSEM.
+(* final_step is parametrized by a function to transfer regset on each exit *)
+Variable tr_exit: function -> exit -> regset -> regset.
+
Variable ge: genv.
Definition find_function (ros: reg + ident) (rs: regset) : option fundef :=
@@ -274,7 +277,7 @@ Qed.
Inductive final_step stack f sp rs m: final -> trace -> state -> Prop :=
| exec_Bgoto pc:
final_step stack f sp rs m (Bgoto pc) E0
- (State stack f sp pc rs m)
+ (State stack f sp pc (tr_exit f pc rs) m)
| exec_Breturn or stk m':
sp = (Vptr stk Ptrofs.zero) ->
Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
@@ -284,7 +287,7 @@ Inductive final_step stack f sp rs m: final -> trace -> state -> Prop :=
find_function ros rs = Some fd ->
funsig fd = sig ->
final_step stack f sp rs m (Bcall sig ros args res pc')
- E0 (Callstate (Stackframe res f sp pc' rs :: stack) fd rs##args m)
+ E0 (Callstate (Stackframe res f sp pc' (tr_exit f pc' rs) :: stack) fd rs##args m)
| exec_Btailcall sig ros args stk m' fd:
find_function ros rs = Some fd ->
funsig fd = sig ->
@@ -296,12 +299,12 @@ Inductive final_step stack f sp rs m: final -> trace -> state -> Prop :=
eval_builtin_args ge (fun r => rs#r) sp m args vargs ->
external_call ef ge vargs m t vres m' ->
final_step stack f sp rs m (Bbuiltin ef args res pc')
- t (State stack f sp pc' (regmap_setres res vres rs) m')
+ t (State stack f sp pc' (tr_exit f pc' (regmap_setres res vres rs)) m')
| exec_Bjumptable arg tbl n pc':
rs#arg = Vint n ->
list_nth_z tbl (Int.unsigned n) = Some pc' ->
final_step stack f sp rs m (Bjumptable arg tbl)
- E0 (State stack f sp pc' rs m)
+ E0 (State stack f sp pc' (tr_exit f pc' rs) m)
.
(** big-step execution of one iblock *)
@@ -358,11 +361,75 @@ Inductive final_state: state -> int -> Prop :=
| final_state_intro: forall r m,
final_state (Returnstate nil (Vint r) m) r.
-(** The small-step semantics for a program. *)
+(** The basic small-step semantics for a BTL program. *)
+
+(* tid = transfer_identity *)
+Definition tid (_:function) (_:exit) (rs:regset) := rs.
Definition semantics (p: program) :=
- Semantics step (initial_state p) final_state (Genv.globalenv p).
+ Semantics (step tid) (initial_state p) final_state (Genv.globalenv p).
+
+(** The "functional" small-step semantics for a BTL program.
+ at each exit, we only transfer register in "input_regs" (i.e. "alive" registers).
+*)
+
+Definition transfer_regs (inputs: list reg) (rs: regset): regset :=
+ init_regs (rs##inputs) inputs.
+
+Lemma transfer_regs_inputs inputs rs r:
+ List.In r inputs -> (transfer_regs inputs rs)#r = rs#r.
+Proof.
+ unfold transfer_regs; induction inputs; simpl; intuition subst.
+ - rewrite Regmap.gss; auto.
+ - destruct (Pos.eq_dec a r).
+ + subst; rewrite Regmap.gss; auto.
+ + rewrite Regmap.gso; auto.
+Qed.
+
+Lemma transfer_regs_dead inputs rs r:
+ ~List.In r inputs -> (transfer_regs inputs rs)#r = Vundef.
+Proof.
+ unfold transfer_regs; induction inputs; simpl; intuition subst.
+ - rewrite Regmap.gi; auto.
+ - rewrite Regmap.gso; auto.
+Qed.
+
+Definition inputs_exit (f:function) (pc: exit) : Regset.t :=
+ match f.(fn_code)!pc with
+ | None => Regset.empty
+ | Some ib => ib.(input_regs)
+ end.
+
+Definition tr_inputs (f:function) (pc: exit): regset -> regset
+ := transfer_regs (Regset.elements (inputs_exit f pc)).
+
+(* TODO: move this elsewhere *)
+Lemma SetoidList_InA_eq_equiv A (l: list A): forall x,
+ SetoidList.InA (fun x y => x = y) x l <-> List.In x l.
+Proof.
+ intros x; split.
+ - induction 1; simpl; eauto.
+ - induction l; simpl; intuition.
+Qed.
+
+Lemma tr_inputs_exit f pc rs r:
+ Regset.In r (inputs_exit f pc) -> (tr_inputs f pc rs)#r = rs#r.
+Proof.
+ intros; eapply transfer_regs_inputs.
+ rewrite <- SetoidList_InA_eq_equiv.
+ eapply Regset.elements_1; eauto.
+Qed.
+
+Lemma tr_inputs_dead f pc rs r:
+ ~(Regset.In r (inputs_exit f pc)) -> (tr_inputs f pc rs)#r = Vundef.
+Proof.
+ intros X; eapply transfer_regs_dead; intuition eauto.
+ eapply X. eapply Regset.elements_2.
+ rewrite -> SetoidList_InA_eq_equiv; eauto.
+Qed.
+Definition fsem (p: program) :=
+ Semantics (step tr_inputs) (initial_state p) final_state (Genv.globalenv p).
(** TODO: est-ce qu'il faudrait déplacer ceci dans une librairie du genre "BTLlib" ? *)
diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v
index b9a05a8a..5125ea3c 100644
--- a/scheduling/BTL_SEtheory.v
+++ b/scheduling/BTL_SEtheory.v
@@ -4,6 +4,8 @@ NB: an efficient implementation with hash-consing will be defined in another fil
*)
+(* TODO: A REVOIR - remplacer les [tid] par [tr_inputs] pour montrer la bisimulation avec [fsem] plutôt. *)
+
Require Import Coqlib Maps Floats.
Require Import AST Integers Values Events Memory Globalenvs Smallstep.
Require Import Op Registers.
@@ -580,7 +582,7 @@ Local Hint Constructors sem_sfval: core.
Lemma sexec_final_svf_correct ctx i sis t rs m s:
sem_sistate ctx sis rs m ->
- final_step (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs m i t s ->
+ final_step tid (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs m i t s ->
sem_sfval ctx (sexec_final_sfv i sis) rs m t s.
Proof.
intros (PRE&MEM&REG).
@@ -604,10 +606,12 @@ Local Hint Resolve seval_builtin_args_exact: core.
Lemma sexec_final_svf_exact ctx i sis t rs m s:
sem_sistate ctx sis rs m ->
sem_sfval ctx (sexec_final_sfv i sis) rs m t s
- -> final_step (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs m i t s.
+ -> final_step tid (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs m i t s.
Proof.
intros (PRE&MEM&REG).
destruct i; simpl; intros LAST; inv LAST; eauto.
+ + (* Bgoto *)
+ econstructor.
+ (* Breturn *)
enough (v=regmap_optget res Vundef rs) as ->; eauto.
destruct res; simpl in *; congruence.
@@ -621,6 +625,8 @@ Proof.
intros; eapply exec_Btailcall; eauto.
destruct fn; simpl in * |- *; auto.
rewrite REG in * |- ; auto.
+ + (* Bbuiltin *)
+ eapply (exec_Bbuiltin tid); eauto.
+ (* Bjumptable *)
eapply exec_Bjumptable; eauto.
congruence.
@@ -799,7 +805,7 @@ Lemma sexec_rec_correct ctx t s ib rs m rs1 m1 ofin
(SIS: sem_sistate ctx sis rs m)
(CONT: match ofin with
| None => forall sis', sem_sistate ctx sis' rs1 m1 -> sem_sstate ctx t s (k sis')
- | Some fin => final_step (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs1 m1 fin t s
+ | Some fin => final_step tid (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs1 m1 fin t s
end),
sem_sstate ctx t s (sexec_rec ib sis k).
Proof.
@@ -816,7 +822,7 @@ Qed.
(sexec is a correct over-approximation)
*)
Theorem sexec_correct ctx ib t s:
- iblock_step (cge ctx) (cstk ctx) (cf ctx) (csp ctx) (crs0 ctx) (cm0 ctx) ib t s ->
+ iblock_step tid (cge ctx) (cstk ctx) (cf ctx) (csp ctx) (crs0 ctx) (cm0 ctx) ib t s ->
sem_sstate ctx t s (sexec ib).
Proof.
destruct 1 as (rs' & m' & fin & ISTEP & FSTEP).
@@ -1049,7 +1055,7 @@ Lemma sexec_rec_exact ctx ib t s1: forall sis k
,
match iblock_istep_run (cge ctx) (csp ctx) ib rs m with
| Some (out rs' m' (Some fin)) =>
- exists s2, final_step (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs' m' fin t s2 /\ equiv_state s1 s2
+ exists s2, final_step tid (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs' m' fin t s2 /\ equiv_state s1 s2
| Some (out rs' m' None) => exists sis', (sem_sstate ctx t s1 (k sis')) /\ (sem_sistate ctx sis' rs' m')
| None => False
end.
@@ -1095,7 +1101,7 @@ Qed.
*)
Theorem sexec_exact ctx ib t s1:
sem_sstate ctx t s1 (sexec ib) ->
- exists s2, iblock_step (cge ctx) (cstk ctx) (cf ctx) (csp ctx) (crs0 ctx) (cm0 ctx) ib t s2
+ exists s2, iblock_step tid (cge ctx) (cstk ctx) (cf ctx) (csp ctx) (crs0 ctx) (cm0 ctx) ib t s2
/\ equiv_state s1 s2.
Proof.
intros; exploit sexec_rec_exact; eauto.
diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v
index 08a77ae4..bbb984c4 100644
--- a/scheduling/BTLtoRTLproof.v
+++ b/scheduling/BTLtoRTLproof.v
@@ -292,7 +292,7 @@ Qed.
Lemma final_simu_except_goto sp dupmap stack stack' f f' rs1 m1 pc1 fin t s
(STACKS : list_forall2 match_stackframes stack stack')
(TRANSF : match_function dupmap f f')
- (FS : final_step ge stack f sp rs1 m1 fin t s)
+ (FS : final_step tid ge stack f sp rs1 m1 fin t s)
(i : instruction)
(ATpc1 : (RTL.fn_code f') ! pc1 = Some i)
(MF : match_final_inst dupmap fin i)
@@ -338,7 +338,7 @@ Lemma iblock_step_simulation sp dupmap stack stack' f f' ib rs0 m0 rs1 m1 pc0 fi
(TRANSF: match_function dupmap f f')
(IBIS: iblock_istep ge sp rs0 m0 ib rs1 m1 (Some fin))
(MIB : match_iblock dupmap (RTL.fn_code f') true pc0 ib None)
- (FS : final_step ge stack f sp rs1 m1 fin t s)
+ (FS : final_step tid ge stack f sp rs1 m1 fin t s)
: exists s', plus RTL.step tge (RTL.State stack' f' sp pc0 rs0 m0) t s' /\ match_states s s'.
Proof.
intros; exploit iblock_istep_simulation; eauto.
@@ -359,7 +359,7 @@ Proof.
Qed.
Theorem plus_simulation s1 t s1':
- step ge s1 t s1' ->
+ step tid ge s1 t s1' ->
forall s2 (MS: match_states s1 s2),
exists s2',
plus RTL.step tge s2 t s2'
diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v
index 633e1b8e..60edea49 100644
--- a/scheduling/RTLtoBTLproof.v
+++ b/scheduling/RTLtoBTLproof.v
@@ -492,7 +492,7 @@ Lemma match_strong_state_simu
(MSS2 : match_strong_state dupmap st st' f f' sp rs2 m2 rs0 m0 pcB0 pcR0 pcR2 ib2 ib0 false)
(MES : measure ib2 < n)
: exists (oib' : option iblock),
- (exists s2', step tge (State st' f' sp pcB0 rs0 m0) E0 s2'
+ (exists s2', step tid tge (State st' f' sp pcB0 rs0 m0) E0 s2'
/\ match_states oib' (RTL.State st f sp pcR2 rs2 m2) s2')
\/ (omeasure oib' < n /\ E0=E0
/\ match_states oib' (RTL.State st f sp pcR2 rs2 m2) (State st' f' sp pcB0 rs0 m0)).
@@ -523,7 +523,7 @@ Lemma opt_simu_intro
(MSTRONG : match_strong_state dupmap st st' f f' sp rs m rs0 m0 pcB0 pcR0 pcR1 ib ib0 isfst)
(NGOTO : is_goto ib = false)
: exists (oib' : option iblock),
- (exists s2', step tge (State st' f' sp pcB0 rs0 m0) t s2' /\ match_states oib' s1' s2')
+ (exists s2', step tid tge (State st' f' sp pcB0 rs0 m0) t s2' /\ match_states oib' s1' s2')
\/ (omeasure oib' < omeasure (Some ib) /\ t=E0 /\ match_states oib' s1' (State st' f' sp pcB0 rs0 m0)).
Proof.
inversion MSTRONG; subst. inv MIB.
@@ -677,7 +677,7 @@ Theorem opt_simu s1 t s1' oib s2:
RTL.step ge s1 t s1' ->
match_states oib s1 s2 ->
exists (oib' : option iblock),
- (exists s2', step tge s2 t s2' /\ match_states oib' s1' s2')
+ (exists s2', step tid tge s2 t s2' /\ match_states oib' s1' s2')
\/ (omeasure oib' < omeasure oib /\ t=E0 /\ match_states oib' s1' s2)
.
Proof.
generated by cgit (git 2.34.1) at 2024-06-02 15:52:25 +0000