Changeset 2054

Jun 13, 2012, 11:58:55 AM (9 years ago)
  • progress
3 edited


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

    r2049 r2054  
    7070This is not necessarily correct, however: it is not the case that any short
    71 jump can correctly be encoded as a medium jump. Therefore, in this situation
     71jump can correctly be encoded as a medium jump (a short jump can bridge
     72segments, whereas a medium jump cannot). Therefore, in this situation
    7273we decide to encode the jump as a long jump, which is always correct.
    7576from {\tt gcc} and SDCC, and potentially better. Its complexity remains
    7677linear (though with a higher constant than SDCC).
     79\subsection{The algorithm in detail}
     81The branch displacement algorithm forms part of the translation from
     82pseudo-code to assembler. More specifically, it is used by the function that
     83translates pseudo-addresses (natural numbers indicating the position of the
     84instruction in the program) to actual addresses in memory.
     86The original intention was to have two different functions, one function
     87$\mathtt{policy}: \mathbb{N} \rightarrow \{\mathtt{short}, \mathtt{medium},
     88\mathtt{long}\}$ to associate jumps to their intended translation, and a
     89function $\sigma: \mathbb{N} \rightarrow \mathtt{Word}$ to associate
     90pseudo-addresses to actual addresses. $\sigma$ would use $\mathtt{policy}$ to
     91determine the size of jump instructions.
     93This turned out to be suboptimal from the algorithmic point of view and
     94impossible to prove correct.
     96From the algorithmic point of view, in order to create the $\mathtt{policy}$
     97function, we must necessarily have a translation from pseudo-addresses
     98to actual addresses (i.e. a $\sigma$ function): in order to judge the distance
     99between a jump and its destination, we must know their memory locations.
     100Conversely, in order to create the $\sigma$ function, we need to have the
     101$\mathtt{policy}$ function, otherwise we do not know the sizes of the jump
     102instructions in the program.
     104Much the same problem appears when we try to prove the algorithm correct: the
     105correctness of $\mathtt{policy}$ depends on the correctness of $\sigma$, and
     106the correctness of $\sigma$ depends on the correctness of $\mathtt{policy}$.
     108We solved this problem by integrating the $\mathtt{policy}$ and $\sigma$
     109algorithms. We now have a function
     110$\sigma: \mathbb{N} \rightarrow \mathtt{Word} \times \mathtt{bool}$ which
     111associates a pseudo-address to an actual address. The boolean denotes a forced
     112long jump; as noted in the previous section, if during the fixed point
     113computation a medium jump needs to be re-encoded as a short jump, the result
     114is actually a long jump. It might therefore be the case that jumps are encoded
     115as long jumps without this actually being necessary.
     117The assembler function encodes the jumps by checking the distance between
     118source and destination according to $\sigma$, so it could select a medium
     119jump in a situation where there should be a long jump. The boolean is there
     120to prevent this from happening by indicating the locations where a long jump
     121should be encoded, even if a shorter jump is possible. This has no effect on
     122correctness, since a long jump is applicable in any situation.
     129\caption{The heart of the algorithm}
  • src/ASM/CPP2012-policy/main.tex

    r1889 r2054  
  • src/ASM/CPP2012-policy/problem.tex

    r2049 r2054  
    1 \section{The problem}
    33The problem of branch displacement optimisation, also known as jump encoding, is
Note: See TracChangeset for help on using the changeset viewer.