Add text to lsr

8 files changed, 252 insertions, 157 deletions

diff --git a/chapters/conclusion.tex b/chapters/conclusion.tex
index 91ca14f..ee816cb 100644
--- a/chapters/conclusion.tex
+++ b/chapters/conclusion.tex
@@ -1,7 +1,7 @@
 \environment fonts_env
 \environment lsr_env
 
-\startcomponent pipelining
+\startcomponent conclusion
 
 \chapter{Conclusion}
 
diff --git a/chapters/hls.tex b/chapters/hls.tex
index 8ff7143..fbaf41a 100644
--- a/chapters/hls.tex
+++ b/chapters/hls.tex
@@ -7,61 +7,15 @@
 
 \chapter[sec:hls]{High-Level Synthesis}
 
-\paragraph{Can you trust your high-level synthesis tool?} As latency, throughput, and energy
-efficiency become increasingly important, custom hardware accelerators are being designed for
-numerous applications.  Alas, designing these accelerators can be a tedious and error-prone process
-using a hardware description language (HDL) such as Verilog.  An attractive alternative is
-\emph{high-level synthesis} (HLS), in which hardware designs are automatically compiled from
-software written in a high-level language like C.  Modern HLS tools such as
-LegUp~\cite{canis11_legup}, Vivado HLS~\cite{xilinx20_vivad_high_synth}, Intel i++~\cite{intel_hls},
-and Bambu HLS~\cite{bambu_hls} promise designs with comparable performance and energy-efficiency to
-those hand-written in an HDL~\cite{homsirikamol+14, silexicahlshdl, 7818341}, while offering the
-convenient abstractions and rich ecosystems of software development.  But existing HLS tools cannot
-always guarantee that the hardware designs they produce are equivalent to the software they were
-given, and this undermines any reasoning conducted at the software level.
-
-Indeed, there are reasons to doubt that HLS tools actually \emph{do} always preserve equivalence.
-For instance, Vivado HLS has been shown to apply pipelining optimisations
-incorrectly\footnote{\goto{https://bit.ly/vivado-hls-pipeline-bug}[url(https://bit.ly/vivado-hls-pipeline-bug)]}
-or to silently generate wrong code should the programmer stray outside the fragment of C that it
-supports.\footnote{\goto{https://bit.ly/vivado-hls-pointer-bug}[url(https://bit.ly/vivado-hls-pointer-bug)]}
-Meanwhile, \cite{lidbury15_many_core_compil_fuzzin} had to abandon their attempt to fuzz-test
-Altera's (now Intel's) OpenCL compiler since it \quotation{either crashed or emitted an internal
-  compiler error} on so many of their test inputs.  More recently,
-\cite{herklotz21_empir_study_reliab_high_level_synth_tools} fuzz-tested three commercial HLS tools
-using Csmith~\cite{yang11_findin_under_bugs_c_compil}, and despite restricting the generated
-programs to the C fragment explicitly supported by all the tools, they still found that on average
-2.5\% of test-cases were compiled to designs that behaved incorrectly.
-
-\paragraph{Existing workarounds.} Aware of the reliability shortcomings of HLS tools, hardware
-designers routinely check the generated hardware for functional correctness. This is commonly done
-by simulating the generated design against a large test-bench. But unless the test-bench covers all
-inputs exhaustively -- which is often infeasible -- there is a risk that bugs remain.
-
-One alternative is to use \emph{translation validation}~\cite{pnueli98_trans} to prove equivalence
-between the input program and the output design. Translation validation has been successfully
-applied to several HLS
-optimisations~\cite{kim04_autom_fsmd,karfa06_formal_verif_method_sched_high_synth,chouksey20_verif_sched_condit_behav_high_level_synth,banerjee14_verif_code_motion_techn_using_value_propag,chouksey19_trans_valid_code_motion_trans_invol_loops}.
-Nevertheless, it is an expensive task, especially for large designs, and it must be repeated every
-time the compiler is invoked.  For example, the translation validation for Catapult
-C~\cite{mentor20_catap_high_level_synth} may require several rounds of expert
-`adjustments'~\cite[alternative=authoryear,right={, p.~3)}][slec_whitepaper] to the input C program
-before validation succeeds. And even when it succeeds, translation validation does not provide
-watertight guarantees unless the validator itself has been mechanically proven
-correct~\cite[tristan08_formal_verif_trans_valid], which has not been the case in HLS tools to date.
-
-Our position is that none of the above workarounds are necessary if the HLS tool can simply be
-trusted to work correctly.
-
-\paragraph{Our solution.} We have designed a new HLS tool in the Coq theorem prover and proved that
-any output design it produces always has the same behaviour as its input program. Our tool, called
-Vericert, is automatically extracted to an OCaml program from Coq, which ensures that the object of
-the proof is the same as the implementation of the tool. Vericert is built by extending the CompCert
-verified C compiler~\cite[leroy09_formal_verif_realis_compil] with a new hardware-specific
-intermediate language and a Verilog back end. It supports most C constructs, including integer
-operations, function calls (which are all inlined), local arrays, structs, unions, and general
-control-flow statements, but currently excludes support for case statements, function pointers,
-recursive function calls, non-32-bit integers, floats, and global variables.
+We have designed a new HLS tool in the Coq theorem prover and proved that any output design it
+produces always has the same behaviour as its input program. Our tool, called Vericert, is
+automatically extracted to an OCaml program from Coq, which ensures that the object of the proof is
+the same as the implementation of the tool. Vericert is built by extending the CompCert verified C
+compiler~\cite[leroy09_formal_verif_realis_compil] with a new hardware-specific intermediate
+language and a Verilog back end. It supports most C constructs, including integer operations,
+function calls (which are all inlined), local arrays, structs, unions, and general control-flow
+statements, but currently excludes support for case statements, function pointers, recursive
+function calls, non-32-bit integers, floats, and global variables.
 
 \paragraph{Contributions and Outline.} The contributions of this paper are as follows:
 
@@ -1255,33 +1209,40 @@ Fig.~\goto{{[}fig:inference_module{]}}[fig:inference_module].~◻
 
 \subsection[coq-mechanisation]{Coq Mechanisation}
 
-lrrrrr & {\bf Coq code} & & {\bf Spec} & & {\bf Total}\crlf
-Data structures and libraries & 280 & --- & --- & 500 & 780\crlf
-Integers and values & 98 & --- & 15 & 968 & 1081\crlf
-HTL semantics & 50 & --- & 181 & 65 & 296\crlf
-HTL generation & 590 & --- & 66 & 3069 & 3725\crlf
-RAM generation & 253 & --- & --- & 2793 & 3046\crlf
-Verilog semantics & 78 & --- & 431 & 235 & 744\crlf
-Verilog generation & 104 & --- & --- & 486 & 590\crlf
-Top-level driver, pretty printers & 318 & 775 & --- & 189 & 1282\crlf
-{\bf Total} & 1721 & 775 & 693 & 8355 & 11544\crlf
+\startplacetable[reference=tab:proof-statistics]
+  \starttabulate[|l|r|r|r|r|r|]
+    \HL
+    \NC \NC {\bf Coq code} \NC \NC {\bf Spec} \NC \NC {\bf Total} \NC \NR
+    \HL
+    \NC Data structures and libraries \NC 280 \NC --- \NC --- \NC 500 \NC 780 \NC \NR
+    \NC Integers and values \NC 98 \NC --- \NC 15 \NC 968 \NC 1081 \NC \NR
+    \NC HTL semantics \NC 50 \NC --- \NC 181 \NC 65 \NC 296 \NC \NR
+    \NC HTL generation \NC 590 \NC --- \NC 66 \NC 3069 \NC 3725 \NC \NR
+    \NC RAM generation \NC 253 \NC --- \NC --- \NC 2793 \NC 3046 \NC \NR
+    \NC Verilog semantics \NC 78 \NC --- \NC 431 \NC 235 \NC 744 \NC \NR
+    \NC Verilog generation \NC 104 \NC --- \NC --- \NC 486 \NC 590 \NC \NR
+    \NC Top-level driver, pretty printers \NC 318 \NC 775 \NC --- \NC 189 \NC 1282 \NC \NR
+    \HL
+    \NC {\bf Total} \NC 1721 \NC 775 \NC 693 \NC 8355 \NC 11544 \NC \NR
+    \HL
+  \stoptabulate
+\stopplacetable
 
 The lines of code for the implementation and proof of can be found in
-Table~\goto{{[}tab:proof_statistics{]}}[tab:proof_statistics]. Overall, it took about 1.5
-person-years to build -- about three person-months on implementation and 15 person-months on
-proofs. The largest proof is the correctness proof for the HTL generation, which required
-equivalence proofs between all integer operations supported by and those supported in hardware. From
-the 3069 lines of proof code in the HTL generation, 1189 are for the correctness proof of just the
-load and store instructions. These were tedious to prove correct because of the substantial
-difference between the memory models used, and the need to prove properties such as stores outside
-of the allocated memory being undefined, so that a finite array could be used. In addition to that,
-since pointers in HTL and Verilog are represented as integers, instead of as a separate
-\quote{pointer} type like in the semantics, it was painful to reason about them. Many new theorems
-had to be proven about them in to prove the conversion from pointer to integer. Moreover, the
-second-largest proof of the correct RAM generation includes many proofs about the extensional
-equality of array operations, such as merging arrays with different assignments. As the negative
-edge implies that two merges take place every clock cycle, the proofs about the equality of the
-contents in memory and in the merged arrays become more tedious too.
+\in{Table}[tab:proof-statistics]. Overall, it took about 1.5 person-years to build -- about three
+person-months on implementation and 15 person-months on proofs. The largest proof is the correctness
+proof for the HTL generation, which required equivalence proofs between all integer operations
+supported by and those supported in hardware. From the 3069 lines of proof code in the HTL
+generation, 1189 are for the correctness proof of just the load and store instructions. These were
+tedious to prove correct because of the substantial difference between the memory models used, and
+the need to prove properties such as stores outside of the allocated memory being undefined, so that
+a finite array could be used. In addition to that, since pointers in HTL and Verilog are represented
+as integers, instead of as a separate \quote{pointer} type like in the semantics, it was painful to
+reason about them. Many new theorems had to be proven about them in to prove the conversion from
+pointer to integer. Moreover, the second-largest proof of the correct RAM generation includes many
+proofs about the extensional equality of array operations, such as merging arrays with different
+assignments. As the negative edge implies that two merges take place every clock cycle, the proofs
+about the equality of the contents in memory and in the merged arrays become more tedious too.
 
 Looking at the trusted computing base of , the Verilog semantics is 431 lines of code. This and the
 Clight semantics from are the only parts of the compiler that need to be trusted. The Verilog
diff --git a/chapters/introduction.tex b/chapters/introduction.tex
index 623b56a..d96ff55 100644
--- a/chapters/introduction.tex
+++ b/chapters/introduction.tex
@@ -2,4 +2,54 @@
 
 \chapter{Introduction}
 
+\startthesis
+An optimising high-level synthesis tool can be proven correct using an interactive theorem prover
+while also remaining practical.
+\stopthesis
+
+\noindent As latency, throughput, and energy efficiency become increasingly important, custom
+hardware accelerators are being designed for numerous applications.  Alas, designing these
+accelerators can be a tedious and error-prone process using a hardware description language (HDL)
+such as Verilog.  An attractive alternative is \emph{high-level synthesis} (HLS), in which hardware
+designs are automatically compiled from software written in a high-level language like C.  Modern
+HLS tools such as LegUp~\cite{canis11_legup}, Vivado HLS~\cite{xilinx20_vivad_high_synth}, Intel
+i++~\cite{intel_hls}, and Bambu HLS~\cite{bambu_hls} promise designs with comparable performance and
+energy-efficiency to those hand-written in an HDL~\cite{homsirikamol+14, silexicahlshdl, 7818341},
+while offering the convenient abstractions and rich ecosystems of software development.  But
+existing HLS tools cannot always guarantee that the hardware designs they produce are equivalent to
+the software they were given, and this undermines any reasoning conducted at the software level.
+
+Indeed, there are reasons to doubt that HLS tools actually \emph{do} always preserve equivalence.
+For instance, Vivado HLS has been shown to apply pipelining optimisations
+incorrectly\footnote{\goto{bit.ly/vivado-hls-pipeline-bug}[url(https://bit.ly/vivado-hls-pipeline-bug)]}
+or to silently generate wrong code should the programmer stray outside the fragment of C that it
+supports.\footnote{\goto{bit.ly/vivado-hls-pointer-bug}[url(https://bit.ly/vivado-hls-pointer-bug)]}
+Meanwhile, \cite{lidbury15_many_core_compil_fuzzin} had to abandon their attempt to fuzz-test
+Altera's (now Intel's) OpenCL compiler since it \quotation{either crashed or emitted an internal
+  compiler error} on so many of their test inputs.  More recently,
+\cite{herklotz21_empir_study_reliab_high_level_synth_tools} fuzz-tested three commercial HLS tools
+using Csmith~\cite{yang11_findin_under_bugs_c_compil}, and despite restricting the generated
+programs to the C fragment explicitly supported by all the tools, they still found that on average
+2.5\% of test-cases were compiled to designs that behaved incorrectly.
+
+\paragraph{Existing workarounds.} Aware of the reliability shortcomings of HLS tools, hardware
+designers routinely check the generated hardware for functional correctness. This is commonly done
+by simulating the generated design against a large test-bench. But unless the test-bench covers all
+inputs exhaustively -- which is often infeasible -- there is a risk that bugs remain.
+
+One alternative is to use \emph{translation validation}~\cite{pnueli98_trans} to prove equivalence
+between the input program and the output design. Translation validation has been successfully
+applied to several HLS
+optimisations~\cite{kim04_autom_fsmd,karfa06_formal_verif_method_sched_high_synth,chouksey20_verif_sched_condit_behav_high_level_synth,banerjee14_verif_code_motion_techn_using_value_propag,chouksey19_trans_valid_code_motion_trans_invol_loops}.
+Nevertheless, it is an expensive task, especially for large designs, and it must be repeated every
+time the compiler is invoked.  For example, the translation validation for Catapult
+C~\cite{mentor20_catap_high_level_synth} may require several rounds of expert
+`adjustments'~\cite[alternative=authoryear,right={, p.~3)}][slec_whitepaper] to the input C program
+before validation succeeds. And even when it succeeds, translation validation does not provide
+watertight guarantees unless the validator itself has been mechanically proven
+correct~\cite[tristan08_formal_verif_trans_valid], which has not been the case in HLS tools to date.
+
+Our position is that none of the above workarounds are necessary if the HLS tool can simply be
+trusted to work correctly.
+
 \stopcomponent
diff --git a/chapters/schedule.tex b/chapters/schedule.tex
index 1711108..49d5251 100644
--- a/chapters/schedule.tex
+++ b/chapters/schedule.tex
@@ -1,7 +1,7 @@
 \environment fonts_env
 \environment lsr_env
 
-\startcomponent pipelining
+\startcomponent schedule
 
 \definecolor[hyperblockcolour][x=66C2A5]
 \definecolor[dynamiccolour][x=FC8D62]
@@ -31,7 +31,8 @@ work is still on going.
 
 \desc{Modulo scheduling} The second piece of work is described in \in{Chapter}[sec:pipelining] and
 describes the implementation of modulo scheduling to perform scheduling on loops.  This work will be
-based on existing work by \cite[alternative=authoryears][tristan10_simpl_verif_valid_softw_pipel].
+based on existing work by
+\cite[alternative=authoryears][tristan10_simpl_verif_valid_softw_pipel].
 However, it is worth noting that the proof by
 \cite[alternative=author][tristan10_simpl_verif_valid_softw_pipel] does include parts that are not
 completely verified in Coq, meaning there may be various improvements that could be done to the
@@ -46,13 +47,13 @@ optimisations of \SSA\ code, but it should also allow for a more straightforward
 hardware as the GSA code can just be viewed as a \DFG.  Instead of working on modulo scheduling, it
 could therefore be interesting to work on a formally verified dynamic scheduling translation.
 
-\startplacefigure[
+\startplacemarginfigure[
   title={Gantt chart describing the future plan for 2022 and 2023.  The main funding runs out
     mid-2023, so the plan is to finish the thesis writing by then as well.},
   reference={fig:future-gantt},
-  location=top,
+  location={top},
 ]
-  \hbox{\startgantt[xunitlength=17.5mm]{15}{6}
+  \startgantt[xunitlength=17.5mm]{15}{6}
     \startganttitle
       \numtitle{2022}{1}{2022}{4}
       \numtitle{2023}{1}{2023}{2}
@@ -74,8 +75,8 @@ could therefore be interesting to work on a formally verified dynamic scheduling
     \ganttcon{1}{9}{2}{11}
     \ganttgroup{\rmx Thesis}{4}{2}
     \ganttbar[color=thesiscolour]{\rmx Thesis Writing}{4}{2}
-  \stopgantt}
-\stopplacefigure
+  \stopgantt
+\stopplacemarginfigure
 
 \section{Detailed Work Plan}
 
@@ -85,7 +86,7 @@ a plan of either tackling dynamic scheduling or modulo scheduling.
 
 \subsection{Finishing Work on Hyperblock Scheduling}
 
-As described in \in{Chapter}{sec:scheduling}, the current milestone that needs to be achieved is
+As described in \in{Chapter}[sec:scheduling], the current milestone that needs to be achieved is
 proving hyperblock scheduling.  This requires proofs of the following translations:
 
 \desc{\sc RTL $\rightarrow$ RTLBlock} This translation generates basic blocks to ease the scheduling
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.
 
diff --git a/lsr_env.tex b/lsr_env.tex
index 4ce5761..d74cd82 100644
--- a/lsr_env.tex
+++ b/lsr_env.tex
@@ -18,6 +18,7 @@
     openaction=ToggleViewer,
     focus=width,
     click=yes,
+    style=\rm,
 ]
 %\placebookmarks[chapter,section,subsection,subsubsection][chapter,section]
 %\setupinteractionscreen[option=bookmark]
@@ -32,6 +33,19 @@
 \setuptolerance[stretch,tolerant]
 
 \setuplayout[
+  edgedistance=1cm,
+  backspace=2cm,
+  rightmargin=5cm,
+  leftmargin=0cm,
+  topspace=1cm,
+  header=1cm,
+  footer=1cm,
+  headerdistance=0.5cm,
+  width=fit,
+  height=fit,
+]
+
+\definelayout[wide][
   backspace=3cm,
   margin=2cm,
   topspace=1.25cm,
@@ -41,19 +55,36 @@
   width=middle,
 ]
 
+\setuphead[chapter][
+  style={\bfd},
+  header=empty,
+  align=flushright,
+  numbercommand=\marginhead,
+  after={\blank[4*line]},
+  before={\blank[2*line,force]},
+]
+
 \startsectionblockenvironment [backpart]
-\setuplayout[
-  backspace=3cm,
-  margin=2cm,
-  topspace=1.25cm,
-  header=1.25cm,
-  footer=1.25cm,
-  height=middle,
-  width=middle,
+\setuplayout[wide]
+\setupheads[chapter][
+  after=,
+  before=,
+  style={\bfd},
+  header=empty,
+  align=flushleft,
 ]
+\setuppagenumbering[location={footer,middle}]
 \stopsectionblockenvironment
 
 \startsectionblockenvironment [frontpart]
+\setuplayout[wide]
+\setupheads[chapter][
+  after=,
+  before=,
+  style={\bfd},
+  header=empty,
+  align=flushleft,
+]
 \setuppagenumbering[location={footer,middle}]
 \stopsectionblockenvironment
 
@@ -63,10 +94,6 @@
 % ==========================================================================
 % Headers
 % ==========================================================================
-\setuphead[chapter][
-  style={\bfd},
-  header=empty,
-]
 
 \startMPinclusions
   numeric ChapterPageDone[];
@@ -82,10 +109,10 @@
   if n > 0 : % ignore pages before the first chapter
     if unknown ChapterPageDone[n] : % This is the first page a new chapter
           draw (x,PaperHeight) -- (x,PaperHeight-TopSpace+Header-HeaderDistance-75)
-            withpen pencircle scaled 0.5mm;;
+            withpen pencircle scaled 0.5mm;
         ChapterPageDone[n] := 1 ;
     else :
-      draw (x2,PaperHeight) -- (x2,PaperHeight-TopSpace+Header)
+      draw (x2,PaperHeight) -- (x2,PaperHeight-TopSpace+Header);
     fi;
   fi;
   StopPage;
@@ -110,37 +137,17 @@
 
 \define[1]\marginhead{\margintitle[location=right]{\switchtobodyfont[30pt] #1}}
 
-\setuphead[section][style={\bfc}]
-\setuphead[subsection][style={\bfb}]
-\setuphead[subsubsection][style={\bfa},after={\blank[0.2cm]}]
+\setuphead[section][style={\bfb}]
+\setuphead[subsection][style={\bfa}]
+\setuphead[subsubsection][style={\bf},after={\blank[0.2cm]}]
+
+\setuppagenumbering[location=]
+\setuplabeltext[chapter=]
+\setupheadertexts[margin][][{{\it \getmarking[chapter]}\wordright{\pagenumber}}]
+\setupheadertexts[text][][{\someheadnumber[chapter][current]}]
+% \setupheader[text][style=smallcaps,after=\hrule]
+% \setupheader[margin][style=smallcaps]
 
-\startsectionblockenvironment [bodypart]
-\setuplayout[
-  edgedistance=1cm,
-  backspace=2cm,
-  rightmargin=5cm,
-  leftmargin=0cm,
-  topspace=1cm,
-  header=1cm,
-  footer=1cm,
-  headerdistance=0.5cm,
-  width=fit,
-  height=fit,
-]
-  \setuppagenumbering[location=]
-  \setuplabeltext[chapter=]
-  \setupheadertexts[margin][][{{\it \getmarking[chapter]}\wordright{\pagenumber}}]
-  \setupheadertexts[text][][{\someheadnumber[chapter][current]}]
-  %\setupheader[text][style=smallcaps,after=\hrule]
-  %\setupheader[margin][style=smallcaps]
-  \setuphead[chapter][
-    style={\bfd},
-    header=empty,
-    align=flushright,
-    numbercommand=\marginhead,
-    after={\blank[4*line]},
-    before={\blank[2*line,force]},
-  ]
 %\setuplabeltext[chapter=Chapter~]
 %\setuphead[chapter][
 %  style={\bfd},
@@ -150,6 +157,9 @@
 %  after={\blank[4*line]},
 %  before={\blank[4*big,force]},
 %]
+
+\startsectionblockenvironment [bodypart]
+\setuplayout[reset]
 \setcounter[userpage][1]
 \stopsectionblockenvironment
 
@@ -214,6 +224,15 @@
 \setupcaption[subfigure][numbercommand=\groupedcommand{(}{)},numberconversion=a,prefix=no,way=bytext]
 \setuplabeltext[subfigure=]
 
+\newdimen\LeftMarginSize
+\LeftMarginSize=\dimexpr \backspace + \rightmarginwidth + \rightmargindistance \relax
+\newdimen\TextAreaSize
+\TextAreaSize=\dimexpr \textwidth + \rightmarginwidth + \rightmargindistance \relax
+\definefloat[marginfigure][textmarginfigures]
+\setupfloat[marginfigure][location={inner},width=\TextAreaSize,number=figure]
+\setupcaptions[marginfigure][leftmargin=\dimexpr \LeftMarginSize / 2 \relax]
+\setuplabeltext[marginfigure=Figure~]
+
 %\definereferenceformat[sfig][left={\determineheadnumber[figure]\currentheadnumber.}]
 
 \appendvalue{stopplacefigure}{\resetcounter[subfigure]}
@@ -307,17 +326,17 @@
 
 \setupexternalfigures[location=default]
 
-\hyphenation{Comp-Cert}
-\hyphenation{Veri-cert}
-\hyphenation{Poly-Bench}
-\hyphenation{Leg-Up}
+\hyphenation{comp-cert}
+\hyphenation{veri-cert}
+\hyphenation{poly-bench}
+\hyphenation{leg-up}
 \hyphenation{straight-for-ward}
 \hyphenation{cor-re-la-tion}
 \hyphenation{gram-schmi-dt}
 \hyphenation{de-riche}
 
 \definedescription[desc][
-  headstyle=bold, style=normal, align=flushleft, alternative=hanging,
+  headstyle=bold, style=normal, align={yes,tolerant}, alternative=hanging,
   width=broad, margin=1cm]
 
 \definesynonyms[abbreviation][abbreviations][\infull]
@@ -329,7 +348,68 @@
 \abbreviation{DFG}{data-flow graph}
 \abbreviation{CFG}{control-flow graph}
 \abbreviation{CDFG}{control- and data-flow graph}
+\abbreviation{SDC}{system of difference constraints}
+\abbreviation{CNF}{conjunctive normal form}
+\abbreviation{SAT}{satisfiability}
+\abbreviation{SMT}{satisfiability modulo scheduling}
 
 \usemodule[gantt-s-tikz]
 
+\setupenumerations
+[ before={\blank[big]},
+  after={\blank[big]},
+  alternative=serried,
+  width=broad,
+  distance=0.5cm,
+  headstyle=bold,
+  titlestyle=bold,
+  way=bychapter,
+  conversion=numbers]
+
+\defineenumeration
+[thesis]
+[ text=Thesis,
+  number=no,
+  headalign=center,
+  alternative=top,
+  style=italic]
+
+\defineenumeration
+[theorem]
+[ text=Theorem,
+  title=yes,
+  style=italic,
+  list=all,
+  listtext={Theorem }]
+
+\defineenumeration
+[proof]
+[ text=Proof.,
+  number=no,
+  headstyle=italic,
+  title=no,
+  closesymbol={\mathematics{\square}},
+  style=normal]
+
+\defineenumeration
+[corollary]
+[ text=Corollary,
+  number=theorem,
+  list=all,
+  listtext={Corollary }]
+
+\defineenumeration
+[lemma]
+[ text=Corollary,
+  number=theorem,
+  list=all,
+  listtext={Lemma }]
+
+\definestartstop
+  [abstract]
+  [before={\midaligned{\bf Abstract}
+           \startnarrower[2*middle]},
+   after={\stopnarrower
+          \blank[big]}]
+
 \stopenvironment
diff --git a/main.tex b/main.tex
index d31609c..6538981 100644
--- a/main.tex
+++ b/main.tex
@@ -15,7 +15,7 @@
 % \showsetups
 % \showgrid
 % \showmakeup
-%\showframe
+% \showframe
 % \showbodyfontenvironment
 %\showbodyfont
 
@@ -37,9 +37,8 @@
 \stopbodymatter
 
 \startbackmatter
-  \startchapter[title=Bibliography]
-    \placelistofpublications
-  \stopchapter
+  \chapter{Bibliography}
+  \placelistofpublications
 \stopbackmatter
 
 \stopproduct
diff --git a/title.tex b/title.tex
index a73ea75..f0be037 100644
--- a/title.tex
+++ b/title.tex
@@ -1,3 +1,5 @@
+\setuplayout[wide]
+
 \startcomponent title
 \product main
 
@@ -12,14 +14,16 @@
   \blank[5cm]
 
   % http://wiki.contextgarden.net/Command/currentdate
+  {\bf Imperial College London}\blank
   \currentdate[month,year]
   \blank[5cm]
 
   \startalignment[flushleft]
-  \setupinterlinespace[line=3.8ex]\rma
-  \bold{Supervisor}: John Wickerson
-
-  \bold{CID}: 01062783
+    \setupinterlinespace[3.8ex]
+    \starttabulate[format={|l|l|}]
+      \NC \bold{Supervisor} \NC John Wickerson \NC \NR
+      \NC \bold{CID}        \NC 01062783       \NC \NR
+    \stoptabulate
   \stopalignment
 \stopmakeup