From aeb7b75278c6affa9499b03f592f6869ae2ca19f Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 15 Apr 2022 22:33:49 +0100 Subject: Add text to lsr --- chapters/scheduling.tex | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) (limited to 'chapters/scheduling.tex') diff --git a/chapters/scheduling.tex b/chapters/scheduling.tex index 2201f72..662d877 100644 --- a/chapters/scheduling.tex +++ b/chapters/scheduling.tex @@ -52,11 +52,11 @@ 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. +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 system of difference constraints - (SDC) scheduling algorithm, which can be adapted to various different scheduling strategies. +Description of the implementation and correctness proof of a \infull{SDC} (\SDC) scheduling +algorithm, which can be adapted to various different scheduling strategies. \stopitemize \section[sec:scheduling]{Implementation of Hyperblocks in CompCert} @@ -310,7 +310,7 @@ is because predicated instructions can be executed in many different orders, and used to calculate dependence information and therefore also determine the order of operations. Instead, comparing predicates can be done by checking logical equivalence of the predicates using a -formally verified SAT solver. This ensures that the predicates will always evaluate to the same +formally verified \SAT solver. This ensures that the predicates will always evaluate to the same value, thereby making it a fair comparison. \subsection[verified_sat]{Verified Decidable DPLL SAT Solver} @@ -322,8 +322,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 -conjunctive normal form (CNF) formula. The conversion from a recursive predicate type into a CNF -formula is done by recursively expanding the predicate in equivalent CNF formulas. +\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. 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,10 +413,10 @@ 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 +\section[implementation-details-of-static-sdc-scheduling]{Implementation Details of Static \SDC Scheduling} -This section describes the implementation details of the static SDC scheduling algorithm used, and +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 which generates the predicated instructions. @@ -435,9 +435,9 @@ using a process called reverse if-conversion, which creates branches out of the groups these together again. This allows for hyperblock scheduling to also be used with back ends that do not support predicates, which are most the default back ends included in CompCert. -\subsection[static-sdc-scheduling]{Static SDC Scheduling} +\subsection[static-sdc-scheduling]{Static \SDC\ Scheduling} -System of difference constraints (SDC) scheduling~ is a flexible algorithm to perform scheduling of +\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. -- cgit