Add text to lsr

1 files changed, 11 insertions, 11 deletions

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.