Index: /src/ASM/CPP2012policy/algorithm.tex
===================================================================
 /src/ASM/CPP2012policy/algorithm.tex (revision 2079)
+++ /src/ASM/CPP2012policy/algorithm.tex (revision 2080)
@@ 7,7 +7,14 @@
potentially take a great amount of time.
The {\tt gcc} compiler suite, for the x86 architecture, uses a greatest fix
point algorithm. In other words, it starts off with all jumps encoded as the
largest jumps possible, and then tries to reduce jumps as much as possible.
+The SDCC compiler~\cite{SDCC2011}, which has the MCS51 among its target
+instruction sets, simply encodes every jump as a long jump without taking the
+distance into account. While certainly correct (the long jump can reach any
+destination in memory) and rapid, it does result in a less than optimal
+solution.
+
+The {\tt gcc} compiler suite~\cite{GCC2012}, while compiling C on the x86
+architecture, uses a greatest fix point algorithm. In other words, it starts
+off with all jumps encoded as the largest jumps available, and then tries to
+reduce jumps as much as possible.
Such an algorithm has the advantage that any intermediate results it returns
@@ 20,22 +27,11 @@
The result, however, is not necessarily optimal, even if the algorithm is run
until it terminates naturally: the fixed point reached is the {\em greatest}
fixed point, not the least fixed point.
+fixed point, not the least fixed point. Furthermore, {\tt gcc} (at least for
+the x86 architecture) only uses short and long jumps. This makes the algorithm
+more rapid, as shown in the previous section, but also results in a less
+optimal solution.
The SDCC compiler, which has the MCS51 among its target instruction sets, uses
a least fix point algorithm, but does not take the presence of medium jumps
into account. This makes the algorithm run in linear time with respect to the
number of jumps in the program: starting out with every jump encoded as a
short jump, each jump can be switched to a long jump once, but no jump ever
goes back from long to short. This algorithm must be run until a fixed point
is reached, because the intermediate solutions are not necessarily correct.

This algorithm results in a least fixed point, which means its solution is
potentially more optimal then the one reached by the {\tt gcc} algorithm.
However, the solution is still not optimal, since there might be jumps whose
destination is in the same segment. These jumps could be encoded as medium
jumps, which are smaller than long jumps.

Our first attempt at an algorithm was a least fixed point algorithm that took
medium jumps into account.
+In the CerCo assembler, we opted at first for a least fixed point algorithm,
+taking medium jumps into account.
Here, we ran into a problem with proving termination: whereas the SDCC
Index: /src/ASM/CPP2012policy/biblio.bib
===================================================================
 /src/ASM/CPP2012policy/biblio.bib (revision 2079)
+++ /src/ASM/CPP2012policy/biblio.bib (revision 2080)
@@ 56,2 +56,13 @@
}
+@misc{SDCC2011,
+ title = {Small Device {C} Compiler 3.1.0},
+ howpublished = {\url{http://sdcc.sourceforge.net/}},
+ year = {2011}
+}
+
+@misc{GCC2012,
+ title = {GNU Compiler Collection 4.7.0},
+ howpublished = {\url{http://gcc.gnu.org/}},
+ year = {2012}
+}
Index: /src/ASM/CPP2012policy/proof.tex
===================================================================
 /src/ASM/CPP2012policy/proof.tex (revision 2079)
+++ /src/ASM/CPP2012policy/proof.tex (revision 2080)
@@ 81,23 +81,25 @@
\begin{lstlisting}
definition jump_expansion':
$\forall$program:preamble $\times$ ($\Sigma$l:list labelled_instruction.S (l) < 2^16).
 option ($\Sigma$sigma:Word → Word $\times$ bool.
 $\forall$ppc: Word.$\forall$ppc_ok.
 let pc := \fst (sigma ppc) in
 let labels := \fst (create_label_cost_map (\snd program)) in
 let lookup_labels :=
 $\lambda$x.bitvector_of_nat ? (lookup_def ?? labels x 0) in
 let instruction :=
 \fst (fetch_pseudo_instruction (\snd program) ppc ppc_ok) in
 let next_pc := \fst (sigma (add ? ppc (bitvector_of_nat ? 1))) in
 And (nat_of_bitvector $\ldots$ ppc $\leq$ \snd program →
 next_pc = add ? pc (bitvector_of_nat $\ldots$
 (instruction_size lookup_labels ($\lambda$x.\fst (sigma x))
 ($\lambda$x.\snd (sigma x)) ppc instruction))
 )
 (Or (nat_of_bitvector $\ldots$ ppc < \snd program →
 nat_of_bitvector $\ldots$ pc < nat_of_bitvector $\ldots$ next_pc)
 (nat_of_bitvector $\ldots$ ppc = \snd program → next_pc = (zero $\ldots$))))
+definition sigma_policy_specification :=:
+$\lambda$program: pseudo_assembly_program.
+$\lambda$sigma: Word → Word.
+$\lambda$policy: Word → bool.
+ sigma (zero $\ldots$) = zero $\ldots$ $\wedge$
+ $\forall$ppc: Word.$\forall$ppc_ok.
+ let instr_list := \snd program in
+ let pc ≝ sigma ppc in
+ let labels := \fst (create_label_cost_map (\snd program)) in
+ let lookup_labels :=
+ $\lambda$x.bitvector_of_nat ? (lookup_def ?? labels x 0) in
+ let instruction :=
+ \fst (fetch_pseudo_instruction (\snd program) ppc ppc_ok) in
+ let next_pc := \fst (sigma (add ? ppc (bitvector_of_nat ? 1))) in
+ (nat_of_bitvector $\ldots$ ppc ≤ instr_list →
+ next_pc = add 16 pc (bitvector_of_nat $\ldots$
+ (instruction_size lookup_labels sigma policy ppc instruction)))
+ $\wedge$
+ ((nat_of_bitvector $\ldots$ ppc < instr_list →
+ nat_of_bitvector $\ldots$ pc < nat_of_bitvector $\ldots$ next_pc)
+ $\vee$ (nat_of_bitvector $\ldots$ ppc = instr_list → next_pc = (zero $\ldots$))).
\end{lstlisting}
@@ 113,2 +115,5 @@
address can be zero (this is the case where the program size is exactly equal
to the amount of memory).
+
+And finally, we enforce that the program starts at address 0, i.e.
+$\sigma(0) = 0$.