diff options
Diffstat (limited to 'docs/scheduler.org')
| -rw-r--r-- | docs/scheduler.org | 54 |
1 files changed, 38 insertions, 16 deletions
diff --git a/docs/scheduler.org b/docs/scheduler.org index 018633c..c8b00ff 100644 --- a/docs/scheduler.org +++ b/docs/scheduler.org @@ -909,18 +909,19 @@ Require Import vericert.hls.Predicate. Require Import vericert.hls.Abstr. Import NE.NonEmptyNotation. -(** * RTLPar Generation *) - #[local] Open Scope positive. #[local] Open Scope forest. #[local] Open Scope pred_op. +#+end_src -(** ** Abstract Computations +** Abstract Computations Define the abstract computation using the [update] function, which will set each register to its symbolic value. First we need to define a few helper functions to correctly translate the -predicates. *) +predicates. +#+name: rtlpargen-generation +#+begin_src coq Fixpoint list_translation (l : list reg) (f : forest) {struct l} : list pred_expr := match l with | nil => nil @@ -1014,18 +1015,25 @@ Definition app_predicated {A: Type} (p: option pred_op) (a b: predicated A) := Definition pred_ret {A: Type} (a: A) : predicated A := NE.singleton (T, a). -(** *** Update Function +#+end_src -The [update] function will generate a new forest given an existing forest and a new instruction, -so that it can evaluate a symbolic expression by folding over a list of instructions. The main -problem is that predicates need to be merged as well, so that: +*** Update Function +:PROPERTIES: +:CUSTOM_ID: update-function +:END: + +The [update] function will generate a new forest given an existing forest and a new instruction, so +that it can evaluate a symbolic expression by folding over a list of instructions. The main problem +is that predicates need to be merged as well, so that: 1. The predicates are *independent*. 2. The expression assigned to the register should still be correct. This is done by multiplying the predicates together, and assigning the negation of the expression to -the other predicates. *) +the other predicates. +#+name: rtlpargen-update-function +#+begin_src coq Definition update (f : forest) (i : instr) : forest := match i with | RBnop => f @@ -1055,28 +1063,37 @@ Definition update (f : forest) (i : instr) : forest := (f # (Pred p)) (map_predicated (pred_ret (Esetpred c)) (merge (list_translation args f)))) end. +#+end_src -(** Implementing which are necessary to show the correctness of the translation validation by +Implementing which are necessary to show the correctness of the translation validation by showing that there aren't any more effects in the resultant RTLPar code than in the RTLBlock code. -Get a sequence from the basic block. *) +Get a sequence from the basic block. +#+name: rtlpargen-abstract-seq +#+begin_src coq Fixpoint abstract_sequence (f : forest) (b : list instr) : forest := match b with | nil => f | i :: l => abstract_sequence (update f i) l end. +#+end_src -(** Check equivalence of control flow instructions. As none of the basic blocks should have been +Check equivalence of control flow instructions. As none of the basic blocks should have been moved, none of the labels should be different, meaning the control-flow instructions should match -exactly. *) +exactly. +#+name: rtlpargen-check-functions +#+begin_src coq Definition check_control_flow_instr (c1 c2: cf_instr) : bool := if cf_instr_eq c1 c2 then true else false. +#+end_src -(** We define the top-level oracle that will check if two basic blocks are equivalent after a -scheduling transformation. *) +We define the top-level oracle that will check if two basic blocks are equivalent after a +scheduling transformation. +#+name: rtlpargen-top-check-functions +#+begin_src coq Definition empty_trees (bb: RTLBlock.bb) (bbt: RTLPar.bb) : bool := match bb with | nil => @@ -1116,8 +1133,12 @@ Lemma check_scheduled_trees_correct2: PTree.get x f2 = None. Proof. solve_scheduled_trees_correct. Qed. -(** ** Top-level Functions *) +#+end_src + +** Top-level Functions +#+name: rtlpargen-top-level-functions +#+begin_src coq Parameter schedule : RTLBlock.function -> RTLPar.function. Definition transl_function (f: RTLBlock.function) : Errors.res RTLPar.function := @@ -1136,6 +1157,7 @@ Definition transl_fundef := transf_partial_fundef transl_function. Definition transl_program (p : RTLBlock.program) : Errors.res RTLPar.program := transform_partial_program transl_fundef p. #+end_src + * RTLPargenproof :PROPERTIES: :header-args:coq: :comments noweb :noweb no-export :padline yes :tangle ../src/hls/RTLPargenproof.v |