Changeset 2080 for src/ASM

Jun 14, 2012, 11:57:51 AM (9 years ago)
  • added references to SDCC and gcc (thanks, Dominic)
  • updated sigma policy specification
  • changed description of SDCC algorithm to actual SDCC behaviour
3 edited


  • src/ASM/CPP2012-policy/algorithm.tex

    r2064 r2080  
    77potentially take a great amount of time.
    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.
     9The SDCC compiler~\cite{SDCC2011}, which has the MCS-51 among its target
     10instruction sets, simply encodes every jump as a long jump without taking the
     11distance into account. While certainly correct (the long jump can reach any
     12destination in memory) and rapid, it does result in a less than optimal
     15The {\tt gcc} compiler suite~\cite{GCC2012}, while compiling C on the x86
     16architecture, uses a greatest fix point algorithm. In other words, it starts
     17off with all jumps encoded as the largest jumps available, and then tries to
     18reduce jumps as much as possible.
    1320Such an algorithm has the advantage that any intermediate results it returns
    2027The result, however, is not necessarily optimal, even if the algorithm is run
    2128until it terminates naturally: the fixed point reached is the {\em greatest}
    22 fixed point, not the least fixed point.
     29fixed point, not the least fixed point. Furthermore, {\tt gcc} (at least for
     30the x86 architecture) only uses short and long jumps. This makes the algorithm
     31more rapid, as shown in the previous section, but also results in a less
     32optimal solution.
    24 The SDCC compiler, which has the MCS-51 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.
    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.
    38 Our first attempt at an algorithm was a least fixed point algorithm that took
    39 medium jumps into account.
     34In the CerCo assembler, we opted at first for a least fixed point algorithm,
     35taking medium jumps into account.
    4137Here, we ran into a problem with proving termination: whereas the SDCC
  • src/ASM/CPP2012-policy/biblio.bib

    r2064 r2080  
     59  title = {Small Device {C} Compiler 3.1.0},
     60  howpublished = {\url{}},
     61  year = {2011}
     65        title = {GNU Compiler Collection 4.7.0},
     66        howpublished = {\url{}},
     67        year = {2012}
  • src/ASM/CPP2012-policy/proof.tex

    r2065 r2080  
    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$))))
     83definition 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$))).
    113115address can be zero (this is the case where the program size is exactly equal
    114116to the amount of memory).
     118And 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.