From 870d0cf9d06f453e2ba3cbdaf0184bc1f657c04b Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 15 Jun 2021 17:11:25 +0200 Subject: some advance in sched proof --- scheduling/BTL_Schedulerproof.v | 116 +++++++++++++++++++++++++++++++--------- 1 file changed, 92 insertions(+), 24 deletions(-) (limited to 'scheduling') diff --git a/scheduling/BTL_Schedulerproof.v b/scheduling/BTL_Schedulerproof.v index aaa2bf80..c7ecb0dc 100644 --- a/scheduling/BTL_Schedulerproof.v +++ b/scheduling/BTL_Schedulerproof.v @@ -40,9 +40,10 @@ Inductive match_fundef: fundef -> fundef -> Prop := Inductive match_stackframes: stackframe -> stackframe -> Prop := | match_stackframe_intro - res f sp pc rs f' + res f sp pc rs rs' f' + (EQREGS: forall r, rs # r = rs' # r) (TRANSF: match_function f f') - : match_stackframes (BTL.Stackframe res f sp pc rs) (BTL.Stackframe res f' sp pc rs). + : match_stackframes (BTL.Stackframe res f sp pc rs) (BTL.Stackframe res f' sp pc rs'). Inductive match_states: state -> state -> Prop := | match_states_intro @@ -62,6 +63,24 @@ Inductive match_states: state -> state -> Prop := : match_states (Returnstate st v m) (Returnstate st' v m) . +Lemma match_stack_equiv stk1 stk2: + list_forall2 match_stackframes stk1 stk2 -> + forall stk3, list_forall2 equiv_stackframe stk2 stk3 -> + list_forall2 match_stackframes stk1 stk3. +Proof. + (*Local Hint Resolve match_stackframes_equiv: core.*) + induction 1; intros stk3 EQ; inv EQ; constructor; eauto. + inv H3; inv H; econstructor; eauto. + intros; rewrite <- EQUIV; auto. +Qed. + +Lemma match_states_equiv s1 s2 s3: match_states s1 s2 -> equiv_state s2 s3 -> match_states s1 s3. +Proof. + Local Hint Resolve match_stack_equiv: core. + destruct 1; intros EQ; inv EQ; econstructor; eauto. + intros; rewrite <- EQUIV; auto. +Qed. + Lemma transf_function_correct f f': transf_function f = OK f' -> match_function f f'. Proof. @@ -113,43 +132,89 @@ Proof. intros. inv H0. inv H. inv STACKS. constructor. Qed. -(* TODO gourdinl - generalize with a None version of the lemma *) -Lemma iblock_istep_simulation stk1 stk2 f f' sp pc fin rs1 m rs1' m' rs2 ib1 t s +Theorem symbolic_simu_ssem stk1 stk2 f1 f2 ib1 ib2: + forall (ctx: simu_proof_context f1 f2) t s, + sem_sstate (bctx1 ctx) stk1 t s (sexec f1 ib1) -> + exists s', + sem_sstate (bctx2 ctx) stk2 t s' (sexec f2 ib2) + /\ match_states s s'. +Admitted. + +Theorem symbolic_simu_correct stk1 stk2 f1 f2 ib1 ib2: + symbolic_simu f1 f2 ib1 ib2 -> + forall (ctx: simu_proof_context f1 f2) t s, iblock_step tr_inputs (sge1 ctx) stk1 f1 (ssp ctx) (srs0 ctx) (sm0 ctx) ib1 t s -> + exists s', + iblock_step tr_inputs (sge2 ctx) stk2 f2 (ssp ctx) (srs0 ctx) (sm0 ctx) ib2 t s' + /\ match_states s s'. +Proof. + unfold symbolic_simu, sstate_simu. + intros SIMU ctx t s1 STEP1. + exploit (sexec_correct (bctx1 ctx)); simpl; eauto. + intros SST1. exploit sem_sstate_run; eauto. + intros (sis1 & sfv1 & rs & m & OUTC1 & SIS1 & SV1). + exploit sem_si_ok; eauto. intros SOK. + intros; exploit SIMU; eauto. + intros (sis2 & sfv2 & OUTC2 & SSIMU & SEM). + exploit symbolic_simu_ssem; eauto. + intros (s2 & SST2 & MS). + exploit (sexec_exact (bctx2 ctx)); simpl; eauto. + intros (s3 & STEP & EQUIV). + exists s3. intuition eauto. + eapply match_states_equiv; eauto. +Qed. + +(* +Lemma iblock_istep_simulation_None stk1 stk2 f f' sp pc rs1 m rs1' m' rs2 ib1 ibf2 s + (ISTEP: iblock_istep pge sp rs1 m ib1 rs1' m' None) + (PC: (fn_code f') ! pc = Some ibf2) + (EQREGS: forall r : positive, rs1 # r = rs2 # r) + (STACKS: list_forall2 match_stackframes stk1 stk2) + (TRANSF: match_function f f') + :exists rs2' s', + iblock_istep_run tpge sp ibf2.(entry) rs2 m = Some (out rs2' m' None) + /\ match_states s s'. +Proof. + induction ib1; inv ISTEP; eauto. +Admitted. + +Lemma iblock_istep_simulation_Some stk1 stk2 f f' sp ib1: forall fin ibf2 rs1 m rs1' m' rs2 pc t s (ISTEP: iblock_istep pge sp rs1 m ib1 rs1' m' (Some fin)) - (FSTEP : final_step tr_inputs pge stk1 f sp rs1' m' fin t s) + (FSTEP: final_step tr_inputs pge stk1 f sp rs1' m' fin t s) + (PC: (fn_code f') ! pc = Some ibf2) (EQREGS: forall r : positive, rs1 # r = rs2 # r) - (STACKS : list_forall2 match_stackframes stk1 stk2) - (TRANSF : match_function f f') - :exists ib2 rs2' s', - (fn_code f') ! pc = Some ib2 - /\ iblock_istep tpge sp rs2 m ib2.(entry) rs2' m' (Some fin) + (STACKS: list_forall2 match_stackframes stk1 stk2) + (TRANSF: match_function f f'), + exists rs2' s', + iblock_istep_run tpge sp ibf2.(entry) rs2 m = Some (out rs2' m' (Some fin)) /\ final_step tr_inputs tpge stk2 f' sp rs2' m' fin t s' /\ match_states s s'. Proof. - induction ib1; inv ISTEP; eauto. + induction ib1; simpl; try_simplify_someHyps; inv ISTEP; eauto; intros. - (* BF *) admit. - (* Bseq continue *) - eauto. + exploit iblock_istep_simulation_None; eauto. + intros (rs2' & s' & ISTEP & MS). + admit. + - Admitted. - -Lemma iblock_step_simulation stk1 stk2 f f' sp rs rs' m ibf t s1 pc - (STEP: iblock_step tr_inputs pge stk1 f sp rs m ibf.(entry) t s1) + *) +Lemma iblock_step_simulation stk1 stk2 f f' sp rs rs' m ibf t s pc + (STEP: iblock_step tr_inputs pge stk1 f sp rs m ibf.(entry) t s) (PC: (fn_code f) ! pc = Some ibf) (EQREGS: forall r : positive, rs # r = rs' # r) (STACKS: list_forall2 match_stackframes stk1 stk2) (TRANSF: match_function f f') - :exists ibf' s2, - (fn_code f') ! pc = Some ibf' /\ - iblock_step tr_inputs tpge stk2 f' sp rs' m ibf'.(entry) t s2 /\ - match_states s1 s2. + :exists ibf' s', + (fn_code f') ! pc = Some ibf' + /\ iblock_step tr_inputs tpge stk2 f' sp rs' m ibf'.(entry) t s' + /\ match_states s s'. Proof. destruct STEP as (rs1 & m1 & fin & ISTEP & FSTEP). - exploit iblock_istep_simulation; eauto. - intros (ibf2 & rs2' & s' & PC' & ISTEP' & FSTEP' & MS'). - repeat eexists; eauto. -Qed. + inversion TRANSF. apply symbolic_simu_ok in PC as SYMB. + destruct SYMB as (ibf2 & PC' & SYMBS). clear symbolic_simu_ok. + unfold symbolic_simu, sstate_simu in SYMBS. +Admitted. Local Hint Constructors step: core. @@ -181,6 +246,9 @@ Proof. eexists; split. + econstructor. + inv H1. econstructor; eauto. + intros; destruct (Pos.eq_dec res' r); subst. + * rewrite !Regmap.gss; reflexivity. + * rewrite !Regmap.gso; auto. Qed. Theorem transf_program_correct: -- cgit