Changeset 2054

Ignore:
Timestamp:
Jun 13, 2012, 11:58:55 AM (8 years ago)
Message:
• progress
Location:
src/ASM/CPP2012-policy
Files:
3 edited

Legend:

Unmodified
 r2049 This is not necessarily correct, however: it is not the case that any short jump can correctly be encoded as a medium jump. Therefore, in this situation jump can correctly be encoded as a medium jump (a short jump can bridge segments, whereas a medium jump cannot). Therefore, in this situation we decide to encode the jump as a long jump, which is always correct. from {\tt gcc} and SDCC, and potentially better. Its complexity remains linear (though with a higher constant than SDCC). \subsection{The algorithm in detail} The branch displacement algorithm forms part of the translation from pseudo-code to assembler. More specifically, it is used by the function that translates pseudo-addresses (natural numbers indicating the position of the instruction in the program) to actual addresses in memory. The original intention was to have two different functions, one function $\mathtt{policy}: \mathbb{N} \rightarrow \{\mathtt{short}, \mathtt{medium}, \mathtt{long}\}$ to associate jumps to their intended translation, and a function $\sigma: \mathbb{N} \rightarrow \mathtt{Word}$ to associate pseudo-addresses to actual addresses. $\sigma$ would use $\mathtt{policy}$ to determine the size of jump instructions. This turned out to be suboptimal from the algorithmic point of view and impossible to prove correct. From the algorithmic point of view, in order to create the $\mathtt{policy}$ function, we must necessarily have a translation from pseudo-addresses to actual addresses (i.e. a $\sigma$ function): in order to judge the distance between a jump and its destination, we must know their memory locations. Conversely, in order to create the $\sigma$ function, we need to have the $\mathtt{policy}$ function, otherwise we do not know the sizes of the jump instructions in the program. Much the same problem appears when we try to prove the algorithm correct: the correctness of $\mathtt{policy}$ depends on the correctness of $\sigma$, and the correctness of $\sigma$ depends on the correctness of $\mathtt{policy}$. We solved this problem by integrating the $\mathtt{policy}$ and $\sigma$ algorithms. We now have a function $\sigma: \mathbb{N} \rightarrow \mathtt{Word} \times \mathtt{bool}$ which associates a pseudo-address to an actual address. The boolean denotes a forced long jump; as noted in the previous section, if during the fixed point computation a medium jump needs to be re-encoded as a short jump, the result is actually a long jump. It might therefore be the case that jumps are encoded as long jumps without this actually being necessary. The assembler function encodes the jumps by checking the distance between source and destination according to $\sigma$, so it could select a medium jump in a situation where there should be a long jump. The boolean is there to prevent this from happening by indicating the locations where a long jump should be encoded, even if a shorter jump is possible. This has no effect on correctness, since a long jump is applicable in any situation. \begin{figure} \begin{algorithmic} \Function{jump\_expansion\_step}{x} \EndFunction \end{algorithmic} \caption{The heart of the algorithm} \label{f:jump_expansion_step} \end{figure}