From 839ae9a65535e25e52207d46e274385e0709a90f Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 4 Jul 2022 13:56:29 +0100 Subject: Working on scheduling proof --- src/hls/Gible.v | 13 +++ src/hls/GiblePar.v | 4 +- src/hls/GiblePargenproof.v | 200 +++++++++++++++++++++++++++++++++------------ src/hls/GibleSeq.v | 62 ++++++++++++++ 4 files changed, 224 insertions(+), 55 deletions(-) (limited to 'src') diff --git a/src/hls/Gible.v b/src/hls/Gible.v index 8971535..cacca85 100644 --- a/src/hls/Gible.v +++ b/src/hls/Gible.v @@ -344,6 +344,19 @@ Inductive step_list2 {A} (step_i: val -> istate -> A -> istate -> Prop): | exec_RBnil2 : forall sp i, step_list2 step_i sp i nil i. +Inductive step_list_inter {A} (step_i: val -> istate -> A -> istate -> Prop): + val -> istate -> list A -> istate -> Prop := +| exec_term_RBcons : + forall i0 i1 i2 i instrs sp, + step_i sp (Iexec i0) i i1 -> + step_list_inter step_i sp i1 instrs i2 -> + step_list_inter step_i sp (Iexec i0) (i :: instrs) i2 +| exec_term_RBnil : + forall sp i, step_list_inter step_i sp i nil i +| exec_term_RBcons_term : + forall i cf l sp, + step_list_inter step_i sp (Iterm i cf) l (Iterm i cf). + (*| Top-Level Type Definitions ========================== diff --git a/src/hls/GiblePar.v b/src/hls/GiblePar.v index fcfb3d0..69afc27 100644 --- a/src/hls/GiblePar.v +++ b/src/hls/GiblePar.v @@ -50,8 +50,8 @@ Module ParBB <: BlockType. Context {A B: Type} (ge: Genv.t A B). - Definition step_instr_list := step_list (step_instr ge). - Definition step_instr_seq := step_list step_instr_list. + Definition step_instr_list := step_list_inter (step_instr ge). + Definition step_instr_seq := step_list_inter step_instr_list. Definition step_instr_block := step_list step_instr_seq. (*| diff --git a/src/hls/GiblePargenproof.v b/src/hls/GiblePargenproof.v index 99b5b98..eaf0c32 100644 --- a/src/hls/GiblePargenproof.v +++ b/src/hls/GiblePargenproof.v @@ -787,49 +787,49 @@ Proof. repeat match goal with | H: match_states _ _ |- _ => inv H end. do 2 econstructor; eauto. econstructor; congruence. -Qed.*)Admitted. +Qed.*)Admitted.*) -Definition match_prog (prog : RTLBlock.program) (tprog : RTLPar.program) := +Definition match_prog (prog : GibleSeq.program) (tprog : GiblePar.program) := match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq prog tprog. (* TODO: Fix the `bb` and add matches for them. *) -Inductive match_stackframes: RTLBlock.stackframe -> RTLPar.stackframe -> Prop := +Inductive match_stackframes: GibleSeq.stackframe -> GiblePar.stackframe -> Prop := | match_stackframe: forall f tf res sp pc rs rs' ps ps', transl_function f = OK tf -> (forall x, rs !! x = rs' !! x) -> (forall x, ps !! x = ps' !! x) -> - match_stackframes (Stackframe res f sp pc rs ps) + match_stackframes (GibleSeq.Stackframe res f sp pc rs ps) (Stackframe res tf sp pc rs' ps'). -Inductive match_states: RTLBlock.state -> RTLPar.state -> Prop := +Inductive match_states: GibleSeq.state -> GiblePar.state -> Prop := | match_state: forall sf f sp pc rs rs' m sf' tf ps ps' (TRANSL: transl_function f = OK tf) (STACKS: list_forall2 match_stackframes sf sf') (REG: forall x, rs !! x = rs' !! x) (REG: forall x, ps !! x = ps' !! x), - match_states (State sf f sp pc rs ps m) + match_states (GibleSeq.State sf f sp pc rs ps m) (State sf' tf sp pc rs' ps' m) | match_returnstate: forall stack stack' v m (STACKS: list_forall2 match_stackframes stack stack'), - match_states (Returnstate stack v m) + match_states (GibleSeq.Returnstate stack v m) (Returnstate stack' v m) | match_callstate: forall stack stack' f tf args m (TRANSL: transl_fundef f = OK tf) (STACKS: list_forall2 match_stackframes stack stack'), - match_states (Callstate stack f args m) + match_states (GibleSeq.Callstate stack f args m) (Callstate stack' tf args m). Section CORRECTNESS. - Context (prog: RTLBlock.program) (tprog : RTLPar.program). + Context (prog: GibleSeq.program) (tprog : GiblePar.program). Context (TRANSL: match_prog prog tprog). - Let ge : RTLBlock.genv := Globalenvs.Genv.globalenv prog. - Let tge : RTLPar.genv := Globalenvs.Genv.globalenv tprog. + Let ge : GibleSeq.genv := Globalenvs.Genv.globalenv prog. + Let tge : GiblePar.genv := Globalenvs.Genv.globalenv tprog. Lemma symbols_preserved: forall (s: AST.ident), Genv.find_symbol tge s = Genv.find_symbol ge s. @@ -837,7 +837,7 @@ Section CORRECTNESS. Hint Resolve symbols_preserved : rtlgp. Lemma function_ptr_translated: - forall (b: Values.block) (f: RTLBlock.fundef), + forall (b: Values.block) (f: GibleSeq.fundef), Genv.find_funct_ptr ge b = Some f -> exists tf, Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = Errors.OK tf. @@ -847,7 +847,7 @@ Section CORRECTNESS. Qed. Lemma functions_translated: - forall (v: Values.val) (f: RTLBlock.fundef), + forall (v: Values.val) (f: GibleSeq.fundef), Genv.find_funct ge v = Some f -> exists tf, Genv.find_funct tge v = Some tf /\ transl_fundef f = Errors.OK tf. @@ -862,9 +862,9 @@ Section CORRECTNESS. Hint Resolve senv_preserved : rtlgp. Lemma sig_transl_function: - forall (f: RTLBlock.fundef) (tf: RTLPar.fundef), + forall (f: GibleSeq.fundef) (tf: GiblePar.fundef), transl_fundef f = OK tf -> - funsig tf = funsig f. + funsig tf = GibleSeq.funsig f. Proof using . unfold transl_fundef, transf_partial_fundef, transl_function; intros; repeat destruct_match; crush; @@ -878,7 +878,7 @@ Section CORRECTNESS. Lemma find_function_translated: forall ros rs rs' f, (forall x, rs !! x = rs' !! x) -> - find_function ge ros rs = Some f -> + GibleSeq.find_function ge ros rs = Some f -> exists tf, find_function tge ros rs' = Some tf /\ transl_fundef f = OK tf. Proof using TRANSL. @@ -898,18 +898,16 @@ Section CORRECTNESS. Qed. Lemma schedule_oracle_nil: - forall bb cfi, - schedule_oracle {| bb_body := nil; bb_exit := cfi |} bb = true -> - bb_body bb = nil /\ bb_exit bb = cfi. + forall bb, + schedule_oracle nil bb = true -> + bb = nil. Proof using . unfold schedule_oracle, check_control_flow_instr. simplify; repeat destruct_match; crush. Qed. Lemma schedule_oracle_nil2: - forall cfi, - schedule_oracle {| bb_body := nil; bb_exit := cfi |} - {| bb_body := nil; bb_exit := cfi |} = true. + schedule_oracle nil nil = true. Proof using . unfold schedule_oracle, check_control_flow_instr. simplify; repeat destruct_match; crush. @@ -982,14 +980,14 @@ Section CORRECTNESS. learn H as H2; unfold transl_function in H2; destruct (check_scheduled_trees - (@fn_code RTLBlock.bb f) - (@fn_code RTLPar.bb (schedule f))) eqn:?; + (GibleSeq.fn_code f) + (fn_code (schedule f))) eqn:?; [| discriminate ]; inv H2 | [ H: context[check_scheduled_trees] |- _ ] => let H2 := fresh "CHECK" in learn H as H2; eapply check_scheduled_trees_correct in H2; [| solve [eauto] ] - | [ H: schedule_oracle {| bb_body := nil; bb_exit := _ |} ?bb = true |- _ ] => + | [ H: schedule_oracle nil ?bb = true |- _ ] => let H2 := fresh "SCHED" in learn H as H2; apply schedule_oracle_nil in H2 @@ -1041,7 +1039,7 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. (* TODO: Fix these proofs, now the cf_instr is in the State. *) Lemma step_cf_instr_correct: forall t s s' cf, - step_cf_instr ge s cf t s' -> + GibleSeq.step_cf_instr ge s cf t s' -> forall r, match_states s r -> exists r', step_cf_instr tge r cf t r' /\ match_states s' r'. @@ -1068,7 +1066,112 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. repeat (try erewrite match_states_list; eauto; econstructor; eauto with rtlgp). erewrite eval_predf_pr_equiv; eauto. } - Qed.*) Admitted.*) + Qed.*) Admitted. + + #[local] Hint Resolve Events.external_call_symbols_preserved : core. + #[local] Hint Resolve eval_builtin_args_eq : core. + #[local] Hint Resolve symbols_preserved : core. + #[local] Hint Resolve senv_preserved : core. + #[local] Hint Resolve eval_op_eq : core. + #[local] Hint Resolve eval_addressing_eq : core. + + Lemma step_instr_ge : + forall sp a i i', + step_instr ge sp i a i' -> + step_instr tge sp i a i'. + Proof. + inversion 1; subst; simplify; try solve [econstructor; eauto]. + - constructor; auto; rewrite <- eval_op_eq; eauto. + - econstructor; eauto; rewrite <- eval_addressing_eq; eauto. + - econstructor; eauto; rewrite <- eval_addressing_eq; eauto. + Qed. + #[local] Hint Resolve step_instr_ge : core. + + Lemma seqbb_step_step_instr_list : + forall sp a i i', + SeqBB.step ge sp i a i' -> + ParBB.step_instr_list tge sp i a i'. + Proof. + induction a; simplify; inv H. + econstructor; eauto. eapply IHa; eauto. + econstructor; eauto. constructor. + Qed. + #[local] Hint Resolve seqbb_step_step_instr_list : core. + + Lemma step_list2_step_instr_list : + forall sp a i i', + step_list2 (step_instr ge) sp i a i' -> + ParBB.step_instr_list tge sp i a i'. + Proof. + induction a; simplify; inv H. + econstructor; eauto. + destruct i; try solve [inv H4]. + econstructor; eauto. apply IHa; auto. + Qed. + #[local] Hint Resolve step_list2_step_instr_list : core. + + Lemma seqbb_step_step_instr_seq : + forall sp x i i' cf, + SeqBB.step ge sp (Iexec i) (concat x) (Iterm i' cf) -> + ParBB.step_instr_seq tge sp (Iexec i) x (Iterm i' cf). + Proof. + induction x; crush. inv H. eapply step_options in H. + inv H. econstructor. eauto. constructor. + simplify. econstructor; eauto. + eapply IHx; eauto. + Qed. + + Lemma step_list2_step_instr_seq : + forall sp x i i', + step_list2 (step_instr ge) sp (Iexec i) (concat x) (Iexec i') -> + ParBB.step_instr_seq tge sp (Iexec i) x (Iexec i'). + Proof. + induction x; crush. inv H. constructor. + eapply step_options2 in H. simplify. + econstructor; eauto. + eapply IHx; eauto. + Qed. + + Lemma seqbb_step_parbb_step : + forall sp x i i' cf, + SeqBB.step ge sp (Iexec i) (concat (concat x)) (Iterm i' cf) -> + ParBB.step tge sp (Iexec i) x (Iterm i' cf). + Proof. + induction x; crush. inv H. + rewrite concat_app in H. + eapply step_options in H. inv H. + constructor. eapply seqbb_step_step_instr_seq; eauto. + simplify. econstructor. + eapply step_list2_step_instr_seq; eauto. + eapply IHx; eauto. + Qed. + + Lemma schedule_oracle_correct : + forall x y sp i i' ti cf, + schedule_oracle x y = true -> + SeqBB.step ge sp (Iexec i) x (Iterm i' cf) -> + state_lessdef i ti -> + exists ti', ParBB.step tge sp (Iexec ti) y (Iterm ti' cf) + /\ state_lessdef i' ti'. + Proof. Admitted. + + Lemma step_cf_correct : + forall cf ts s s' t, + GibleSeq.step_cf_instr ge s cf t s' -> + match_states s ts -> + exists ts', step_cf_instr tge ts cf t ts' + /\ match_states s' ts'. + Proof. Admitted. + + Lemma match_states_stepBB : + forall s f sp pc rs pr m sf' f' trs tps tm rs' pr' m' trs' tpr' tm', + match_states (GibleSeq.State s f sp pc rs pr m) (State sf' f' sp pc trs tps tm) -> + state_lessdef (mk_instr_state rs' pr' m') (mk_instr_state trs' tpr' tm') -> + match_states (GibleSeq.State s f sp pc rs' pr' m') (State sf' f' sp pc trs' tpr' tm'). + Proof. + inversion 1; subst; simplify. + inv H0. econstructor; eauto. + Qed. Theorem transl_step_correct : forall (S1 : GibleSeq.state) t S2, @@ -1077,40 +1180,31 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. match_states S1 R1 -> exists R2, Smallstep.plus GiblePar.step tge R1 t R2 /\ match_states S2 R2. Proof. - - (*induction 1; repeat semantics_simpl. - - { destruct bb; destruct x. - assert (bb_exit = bb_exit0). - { unfold schedule_oracle in *. simplify. - n unfold check_control_flow_instr in *. - destruct_match; crush. - } - subst. - - exploit abstract_execution_correct; try eassumption. eapply ge_preserved_lem. - econstructor; eauto. - simplify. destruct x. inv H7. - - exploit step_cf_instr_correct; try eassumption. econstructor; eauto. - simplify. - - econstructor. econstructor. eapply Smallstep.plus_one. econstructor. - eauto. eauto. simplify. eauto. eauto. } + induction 1; repeat semantics_simpl. + { + exploit schedule_oracle_correct; eauto. constructor; eauto. simplify. + destruct x0. + pose proof H2 as X. eapply match_states_stepBB in X; eauto. + exploit step_cf_correct; eauto. simplify. + eexists; split. apply Smallstep.plus_one. + econstructor; eauto. auto. + } { unfold bind in *. inv TRANSL0. clear Learn. inv H0. destruct_match; crush. inv H2. unfold transl_function in Heqr. destruct_match; crush. inv Heqr. repeat econstructor; eauto. unfold bind in *. destruct_match; crush. } - { inv TRANSL0. repeat econstructor; eauto using Events.external_call_symbols_preserved, symbols_preserved, senv_preserved, Events.E0_right. } + { inv TRANSL0. + repeat econstructor; + eauto using Events.E0_right. } { inv STACKS. inv H2. repeat econstructor; eauto. intros. apply PTree_matches; eauto. } - Qed.*) Admitted. + Qed. Lemma transl_initial_states: forall S, - RTLBlock.initial_state prog S -> - exists R, RTLPar.initial_state tprog R /\ match_states S R. + GibleSeq.initial_state prog S -> + exists R, GiblePar.initial_state tprog R /\ match_states S R. Proof. induction 1. exploit function_ptr_translated; eauto. intros [tf [A B]]. @@ -1125,13 +1219,13 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. Lemma transl_final_states: forall S R r, - match_states S R -> RTLBlock.final_state S r -> RTLPar.final_state R r. + match_states S R -> GibleSeq.final_state S r -> GiblePar.final_state R r. Proof. intros. inv H0. inv H. inv STACKS. constructor. Qed. Theorem transf_program_correct: - Smallstep.forward_simulation (RTLBlock.semantics prog) (RTLPar.semantics tprog). + Smallstep.forward_simulation (GibleSeq.semantics prog) (GiblePar.semantics tprog). Proof. eapply Smallstep.forward_simulation_plus. apply senv_preserved. diff --git a/src/hls/GibleSeq.v b/src/hls/GibleSeq.v index 45095f3..793eb5d 100644 --- a/src/hls/GibleSeq.v +++ b/src/hls/GibleSeq.v @@ -247,3 +247,65 @@ Proof. unfold all_successors, SeqBB.foldl; intros. eapply in_cf_all_successors'; eauto. Qed. + +Lemma eq_stepBB : + forall A B (ge: Genv.t A B) sp l i1 i2 i2', + SeqBB.step ge sp i1 l i2 -> + SeqBB.step ge sp i1 l i2' -> + i2 = i2'. +Proof. + induction l; crush. inv H. + inv H; inv H0. + assert (Iexec state' = Iexec state'0). + { eapply exec_determ; eauto. } + inv H. eauto. + assert (Iexec state' = Iterm state'0 cf0). + { eapply exec_determ; eauto. } + discriminate. + assert (Iterm state' cf = Iexec state'0). + { eapply exec_determ; eauto. } + discriminate. + eapply exec_determ; eauto. +Qed. + +Lemma step_options : + forall A B (ge: Genv.t A B) a b i1 i2 cf sp, + SeqBB.step ge sp (Iexec i1) (a ++ b) (Iterm i2 cf) -> + (SeqBB.step ge sp (Iexec i1) a (Iterm i2 cf) \/ + exists i1', step_list2 (step_instr ge) sp (Iexec i1) a (Iexec i1') + /\ SeqBB.step ge sp (Iexec i1') b (Iterm i2 cf)). +Proof. + induction a; crush. right; eexists; split; [constructor|auto]. + inv H. exploit IHa; eauto; intros. inv H. + left; econstructor; eauto. + simplify. + right. eexists; split; eauto. econstructor; eauto. + left. constructor; eauto. +Qed. + +Lemma step_options2' : + forall A B (ge: Genv.t A B) a b i1 i2 sp, + step_list2 (step_instr ge) sp (Iexec i1) (a ++ b) (Iexec i2) -> + (step_list2 (step_instr ge) sp (Iexec i1) a (Iexec i2) \/ + exists i1', step_list2 (step_instr ge) sp (Iexec i1) a (Iexec i1') + /\ step_list2 (step_instr ge) sp (Iexec i1') b (Iexec i2)). +Proof. + induction a; crush. right; eexists; split; [constructor|auto]. + inv H. destruct i3; [|exfalso; eapply step_list2_false; eauto]. exploit IHa; eauto; intros. inv H. + left; econstructor; eauto. + simplify. + right. eexists; split; eauto. econstructor; eauto. +Qed. + +Lemma step_options2 : + forall A B (ge: Genv.t A B) a b i1 i2 sp, + step_list2 (step_instr ge) sp (Iexec i1) (a ++ b) (Iexec i2) -> + exists i', step_list2 (step_instr ge) sp (Iexec i1) a (Iexec i') + /\ step_list2 (step_instr ge) sp (Iexec i') b (Iexec i2). +Proof. + induction a; crush. eexists; split; eauto. + constructor. + inv H. destruct i3; [|exfalso; eapply step_list2_false; eauto]. + exploit IHa; eauto; simplify. + eexists; split; eauto. econstructor; eauto. +Qed. -- cgit