Index: src/ASM/CPP2011/cpp2011.tex
===================================================================
 src/ASM/CPP2011/cpp2011.tex (revision 953)
+++ src/ASM/CPP2011/cpp2011.tex (revision 954)
@@ 79,13 +79,13 @@
In order to achieve this CerCo imposes a cost model on programs, or more specifically, on simple blocks of instructions.
This cost model is induced by the compilation process itself, and its noncompositional nature allows us to assign different costs to identical blocks of instructions depending on how they are compiled, obtaining a very precise costing for a program by embracing the compilation process, not ignoring it.
However, this complicates the proof of correctness for the compiler proper: for every translation pass from intermediate language to intermediate language, we must prove that not only has the meaning of a program been preserved, but also its complexity characteristics.
+This cost model is induced by the compilation process itself, and its noncompositional nature allows us to assign different costs to identical blocks of instructions depending on how they are compiled.
+In short, we aim to obtain a very precise costing for a program by embracing the compilation process, not ignoring it.
+This, however, complicates the proof of correctness for the compiler proper: for every translation pass from intermediate language to intermediate language, we must prove that not only has the meaning of a program been preserved, but also its complexity characteristics.
This also applies for the translation from assembly language to machine code.
+
How do we assign a cost to a pseudoinstruction?

There is one snag: how to expand jumps.
As mentioned, conditional jumps at the assembly level can jump to a label appearing anywhere in the program.
However, at the machine code level, conditional jumps are limited to jumping `locally', using an 8bit relative offset of the program counter.
To translate a jump to a label, a single conditional jump pseudoinstruction is potentially translated into a block of three real instructions, as follows (here, \texttt{JZ} is `jump if accumulator is zero'):
+However, at the machine code level, conditional jumps are limited to jumping `locally', using a measly byte offset.
+To translate a jump to a label, a single conditional jump pseudoinstruction may be translated into a block of three real instructions, as follows (here, \texttt{JZ} is `jump if accumulator is zero'):
\begin{displaymath}
\begin{array}{r@{\quad}l@{\;\;}l@{\qquad}c@{\qquad}l@{\;\;}l}
@@ 98,6 +98,5 @@
\end{displaymath}
In the translation, if \texttt{JZ} fails, we fall through to the \texttt{SJMP} which jumps over the \texttt{LJMP}.
Naturally, if \textit{label} is close enough, a conditional jump pseudoinstruction is mapped directly to a conditional jump instruction; the above translation only applies if \textit{label} is not sufficiently local.
Similarly, we must also work out whether to expand an unconditional jump pse
+Naturally, if \textit{label} is close enough, a conditional jump pseudoinstruction is mapped directly to a conditional jump machine instruction; the above translation only applies if \textit{label} is not sufficiently local.
This leaves the problem, addressed below, of calculating whether a label is indeed `close enough' for the simpler translation to be used.
@@ 105,27 +104,29 @@
A conditional jump may be mapped to a single machine instruction or a block of three.
Perhaps more insidious, the number of cycles needed to execute the instructions in the two branches of a translated conditional jump may be different.
Depending on the semiconductor manufacturer, an \texttt{SJMP} could in theory take a different number of clock cycles to execute than an \texttt{LJMP}.
+Depending on the particular MCS51 derivative at hand, an \texttt{SJMP} could in theory take a different number of clock cycles to execute than an \texttt{LJMP}.
These issues must also be dealt with in order to prove that the translation pass preserves the concrete complexity of the code.
The question remains: how do we decide whether to expand a jump into an \texttt{SJMP} or an \texttt{LJMP}?
This problem is far from trivial.
To understand why, consider the following snippet of assembly code:
+To understand why this problem is not trivial, consider the following snippet of assembly code:
\begin{displaymath}
\text{dpm: finish me}
\end{displaymath}
+
As our example shows, given an occurence $l$ of an \texttt{LJMP} instruction, it may be possible to shrink $l$ to an occurence of an \texttt{SJMP} providing we can shrink any \texttt{LJMP}s that exist between $l$ and its target location.
However, shrinking these \texttt{LJMP}s may in turn depend on shrinking $l$ to an \texttt{SJMP}, as it is perfectly possible to jump backwards.
In short, unless we can somehow break this loop of circularity, we are stuck with a suboptimal solution to the expanding jumps problem.
+In short, unless we can somehow break this loop of circularity, and similar knotty configurations of jumps, we are stuck with a suboptimal solution to the expanding jumps problem.
How we go about resolving this problem affected the shape of our proof of correctness for the whole assembler in a rather profound way.
We first attempted to synthesize a solution bottom up.
That is, starting with no solution, we gradually refine a solution using the same functions that implement the jump expansion.
+How we went about resolving this problem affected the shape of our proof of correctness for the whole assembler in a rather profound way.
+We first attempted to synthesize a solution bottom up: starting with no solution, we gradually refine a solution using the same functions that implement the jump expansion.
Using this technique, solutions can fail to exist, and the proof quickly descends into a diabolical quagmire.
Abandoning this attempt, we instead split the `policy', i.e. the decision over how any particular jump should be expanded, from the implementation.
+Abandoning this attempt, we instead split the `policy'the decision over how any particular jump should be expandedfrom the implementation that actually expands assembly programs into machine code.
Assuming the existence of a correct policy, we proved the implementation of the assembler correct.
Further, we proved that the assembler fails to assemble a file if and only if a correct policy does not exist.
+Further, we proved that the assembler fails to assemble an assembly program if and only if a correct policy does not exist.
Policies do not exist in only a limited number of circumstances: namely, if a pseudoinstruction attempts to jump to a label that does not exist, or the program is too large to fit in code memory.
The first case would constitute a serious compiler error, and hopefully certifying the rest of the compiler would rule this possibility out; the second case is unavoidablecertified compiler or not, trying to load a huge program into a small code memory will break \emph{something}.
+The first case would constitute a serious compiler error, and hopefully certifying the rest of the compiler would rule this possibility out.
+The second case is unavoidablecertified compiler or not, trying to load a huge program into a small code memory will break \emph{something}.
+
+The rest of this paper is a detailed description of this proof.
%  %