diff options
Diffstat (limited to 'chapters/scheduling.tex')
| -rw-r--r-- | chapters/scheduling.tex | 24 |
1 files changed, 11 insertions, 13 deletions
diff --git a/chapters/scheduling.tex b/chapters/scheduling.tex index 662d877..15850ce 100644 --- a/chapters/scheduling.tex +++ b/chapters/scheduling.tex @@ -51,12 +51,10 @@ flexible scheduling operations that could be beneficial to various different bac the key points of this paper are the following: \startitemize -\item -Description of how hyperblocks are introduced for improved scheduling of instructions, and how these -can be built and translated back to instructions without predicates. -\item -Description of the implementation and correctness proof of a \infull{SDC} (\SDC) scheduling -algorithm, which can be adapted to various different scheduling strategies. +\item Description of how hyperblocks are introduced for improved scheduling of instructions, and how + these can be built and translated back to instructions without predicates. +\item Description of the implementation and correctness proof of a \SDC\ scheduling algorithm, which + can be adapted to various different scheduling strategies. \stopitemize \section[sec:scheduling]{Implementation of Hyperblocks in CompCert} @@ -322,8 +320,8 @@ proven correct in Coq to prove the scheduling translation correct. The SAT solv be verified, because it could otherwise not be used in the proof of correctness. The DPLL algorithm is used to implement the SAT solver. This means that the SAT solver takes in a -\infull{CNF} (\CNF) formula. The conversion from a recursive predicate type into a \CNF formula is -done by recursively expanding the predicate in equivalent \CNF formulas. +\CNF\ formula. The conversion from a recursive predicate type into a \CNF\ formula is done by +recursively expanding the predicate in equivalent \CNF\ formulas. The SAT solver is implemented in Coq and proven to be sound and complete. The soundness and completeness of an algorithm to check whether a predicate is satisfiable or not also directly @@ -413,8 +411,7 @@ Section~\goto{3}[abstr_interp], the formally verified SAT solver described in Section~\goto{4.2}[verified_sat] can be used prove that if the two predicated expression lists are equivalent, that they will always evaluate to the same value. -\section[implementation-details-of-static-sdc-scheduling]{Implementation Details of Static \SDC - Scheduling} +\section[implementation-details-of-static-sdc-scheduling]{\SDC\ Scheduling Implementation Details} This section describes the implementation details of the static \SDC\ scheduling algorithm used, and also describes some of the details of the basic block generation as well as the if-conversion pass @@ -437,9 +434,10 @@ that do not support predicates, which are most the default back ends included in \subsection[static-sdc-scheduling]{Static \SDC\ Scheduling} -\Word{\infull{SDC}} (\SDC) scheduling~ is a flexible algorithm to perform scheduling of -instructions, especially if the target is hardware directly. It allows for flexible definitions of -optimisation functions in terms of latencies and dependencies of the operations in the basic block. +\Word{\infull{SDC}} (\SDC) scheduling~\cite[cong06_sdc] is a flexible algorithm to perform +scheduling of instructions, especially if the target is hardware directly. It allows for flexible +definitions of optimisation functions in terms of latencies and dependencies of the operations in +the basic block. \section[performance-comparison]{Performance Comparison} |