Changeset 2080 for src/ASM/CPP2012-policy

Ignore:
Timestamp:
Jun 14, 2012, 11:57:51 AM (8 years ago)
Message:
• added references to SDCC and gcc (thanks, Dominic)
• updated sigma policy specification
• changed description of SDCC algorithm to actual SDCC behaviour
Location:
src/ASM/CPP2012-policy
Files:
3 edited

Unmodified
Added
Removed
• src/ASM/CPP2012-policy/algorithm.tex

 r2064 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 MCS-51 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 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 MCS-51 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
• src/ASM/CPP2012-policy/biblio.bib

 r2064 } @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} }
• src/ASM/CPP2012-policy/proof.tex

 r2065 \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} 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$.
Note: See TracChangeset for help on using the changeset viewer.