 Timestamp:
 Jun 14, 2012, 11:57:51 AM (9 years ago)
 Location:
 src/ASM/CPP2012policy
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/CPP2012policy/algorithm.tex
r2064 r2080 7 7 potentially take a great amount of time. 8 8 9 The {\tt gcc} compiler suite, for the x86 architecture, uses a greatest fix 10 point algorithm. In other words, it starts off with all jumps encoded as the 11 largest jumps possible, and then tries to reduce jumps as much as possible. 9 The SDCC compiler~\cite{SDCC2011}, which has the MCS51 among its target 10 instruction sets, simply encodes every jump as a long jump without taking the 11 distance into account. While certainly correct (the long jump can reach any 12 destination in memory) and rapid, it does result in a less than optimal 13 solution. 14 15 The {\tt gcc} compiler suite~\cite{GCC2012}, while compiling C on the x86 16 architecture, uses a greatest fix point algorithm. In other words, it starts 17 off with all jumps encoded as the largest jumps available, and then tries to 18 reduce jumps as much as possible. 12 19 13 20 Such an algorithm has the advantage that any intermediate results it returns … … 20 27 The result, however, is not necessarily optimal, even if the algorithm is run 21 28 until it terminates naturally: the fixed point reached is the {\em greatest} 22 fixed point, not the least fixed point. 29 fixed point, not the least fixed point. Furthermore, {\tt gcc} (at least for 30 the x86 architecture) only uses short and long jumps. This makes the algorithm 31 more rapid, as shown in the previous section, but also results in a less 32 optimal solution. 23 33 24 The SDCC compiler, which has the MCS51 among its target instruction sets, uses 25 a least fix point algorithm, but does not take the presence of medium jumps 26 into account. This makes the algorithm run in linear time with respect to the 27 number of jumps in the program: starting out with every jump encoded as a 28 short jump, each jump can be switched to a long jump once, but no jump ever 29 goes back from long to short. This algorithm must be run until a fixed point 30 is reached, because the intermediate solutions are not necessarily correct. 31 32 This algorithm results in a least fixed point, which means its solution is 33 potentially more optimal then the one reached by the {\tt gcc} algorithm. 34 However, the solution is still not optimal, since there might be jumps whose 35 destination is in the same segment. These jumps could be encoded as medium 36 jumps, which are smaller than long jumps. 37 38 Our first attempt at an algorithm was a least fixed point algorithm that took 39 medium jumps into account. 34 In the CerCo assembler, we opted at first for a least fixed point algorithm, 35 taking medium jumps into account. 40 36 41 37 Here, we ran into a problem with proving termination: whereas the SDCC 
src/ASM/CPP2012policy/biblio.bib
r2064 r2080 56 56 } 57 57 58 @misc{SDCC2011, 59 title = {Small Device {C} Compiler 3.1.0}, 60 howpublished = {\url{http://sdcc.sourceforge.net/}}, 61 year = {2011} 62 } 63 64 @misc{GCC2012, 65 title = {GNU Compiler Collection 4.7.0}, 66 howpublished = {\url{http://gcc.gnu.org/}}, 67 year = {2012} 68 } 
src/ASM/CPP2012policy/proof.tex
r2065 r2080 81 81 82 82 \begin{lstlisting} 83 definition jump_expansion': 84 $\forall$program:preamble $\times$ ($\Sigma$l:list labelled_instruction.S (l) < 2^16). 85 option ($\Sigma$sigma:Word → Word $\times$ bool. 86 $\forall$ppc: Word.$\forall$ppc_ok. 87 let pc := \fst (sigma ppc) in 88 let labels := \fst (create_label_cost_map (\snd program)) in 89 let lookup_labels := 90 $\lambda$x.bitvector_of_nat ? (lookup_def ?? labels x 0) in 91 let instruction := 92 \fst (fetch_pseudo_instruction (\snd program) ppc ppc_ok) in 93 let next_pc := \fst (sigma (add ? ppc (bitvector_of_nat ? 1))) in 94 And (nat_of_bitvector $\ldots$ ppc $\leq$ \snd program → 95 next_pc = add ? pc (bitvector_of_nat $\ldots$ 96 (instruction_size lookup_labels ($\lambda$x.\fst (sigma x)) 97 ($\lambda$x.\snd (sigma x)) ppc instruction)) 98 ) 99 (Or (nat_of_bitvector $\ldots$ ppc < \snd program → 100 nat_of_bitvector $\ldots$ pc < nat_of_bitvector $\ldots$ next_pc) 101 (nat_of_bitvector $\ldots$ ppc = \snd program → next_pc = (zero $\ldots$)))) 83 definition sigma_policy_specification :=: 84 $\lambda$program: pseudo_assembly_program. 85 $\lambda$sigma: Word → Word. 86 $\lambda$policy: Word → bool. 87 sigma (zero $\ldots$) = zero $\ldots$ $\wedge$ 88 $\forall$ppc: Word.$\forall$ppc_ok. 89 let instr_list := \snd program in 90 let pc ≝ sigma ppc in 91 let labels := \fst (create_label_cost_map (\snd program)) in 92 let lookup_labels := 93 $\lambda$x.bitvector_of_nat ? (lookup_def ?? labels x 0) in 94 let instruction := 95 \fst (fetch_pseudo_instruction (\snd program) ppc ppc_ok) in 96 let next_pc := \fst (sigma (add ? ppc (bitvector_of_nat ? 1))) in 97 (nat_of_bitvector $\ldots$ ppc ≤ instr_list → 98 next_pc = add 16 pc (bitvector_of_nat $\ldots$ 99 (instruction_size lookup_labels sigma policy ppc instruction))) 100 $\wedge$ 101 ((nat_of_bitvector $\ldots$ ppc < instr_list → 102 nat_of_bitvector $\ldots$ pc < nat_of_bitvector $\ldots$ next_pc) 103 $\vee$ (nat_of_bitvector $\ldots$ ppc = instr_list → next_pc = (zero $\ldots$))). 102 104 \end{lstlisting} 103 105 … … 113 115 address can be zero (this is the case where the program size is exactly equal 114 116 to the amount of memory). 117 118 And finally, we enforce that the program starts at address 0, i.e. 119 $\sigma(0) = 0$.
Note: See TracChangeset
for help on using the changeset viewer.