Changeset 2054 for src/ASM/CPP2012policy
 Timestamp:
 Jun 13, 2012, 11:58:55 AM (8 years ago)
 Location:
 src/ASM/CPP2012policy
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/CPP2012policy/algorithm.tex
r2049 r2054 69 69 70 70 This 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 71 jump can correctly be encoded as a medium jump (a short jump can bridge 72 segments, whereas a medium jump cannot). Therefore, in this situation 72 73 we decide to encode the jump as a long jump, which is always correct. 73 74 … … 75 76 from {\tt gcc} and SDCC, and potentially better. Its complexity remains 76 77 linear (though with a higher constant than SDCC). 78 79 \subsection{The algorithm in detail} 80 81 The branch displacement algorithm forms part of the translation from 82 pseudocode to assembler. More specifically, it is used by the function that 83 translates pseudoaddresses (natural numbers indicating the position of the 84 instruction in the program) to actual addresses in memory. 85 86 The 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 89 function $\sigma: \mathbb{N} \rightarrow \mathtt{Word}$ to associate 90 pseudoaddresses to actual addresses. $\sigma$ would use $\mathtt{policy}$ to 91 determine the size of jump instructions. 92 93 This turned out to be suboptimal from the algorithmic point of view and 94 impossible to prove correct. 95 96 From the algorithmic point of view, in order to create the $\mathtt{policy}$ 97 function, we must necessarily have a translation from pseudoaddresses 98 to actual addresses (i.e. a $\sigma$ function): in order to judge the distance 99 between a jump and its destination, we must know their memory locations. 100 Conversely, 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 102 instructions in the program. 103 104 Much the same problem appears when we try to prove the algorithm correct: the 105 correctness of $\mathtt{policy}$ depends on the correctness of $\sigma$, and 106 the correctness of $\sigma$ depends on the correctness of $\mathtt{policy}$. 107 108 We solved this problem by integrating the $\mathtt{policy}$ and $\sigma$ 109 algorithms. We now have a function 110 $\sigma: \mathbb{N} \rightarrow \mathtt{Word} \times \mathtt{bool}$ which 111 associates a pseudoaddress to an actual address. The boolean denotes a forced 112 long jump; as noted in the previous section, if during the fixed point 113 computation a medium jump needs to be reencoded as a short jump, the result 114 is actually a long jump. It might therefore be the case that jumps are encoded 115 as long jumps without this actually being necessary. 116 117 The assembler function encodes the jumps by checking the distance between 118 source and destination according to $\sigma$, so it could select a medium 119 jump in a situation where there should be a long jump. The boolean is there 120 to prevent this from happening by indicating the locations where a long jump 121 should be encoded, even if a shorter jump is possible. This has no effect on 122 correctness, since a long jump is applicable in any situation. 123 124 \begin{figure} 125 \begin{algorithmic} 126 \Function{jump\_expansion\_step}{x} 127 \EndFunction 128 \end{algorithmic} 129 \caption{The heart of the algorithm} 130 \label{f:jump_expansion_step} 131 \end{figure} 
src/ASM/CPP2012policy/main.tex
r1889 r2054 1 1 \documentclass[a4paper]{llncs} 2 \usepackage{algpseudocode} 2 3 \usepackage{alltt} 4 \usepackage{amsfonts} 3 5 \usepackage[utf8]{inputenc} 4 6 
src/ASM/CPP2012policy/problem.tex
r2049 r2054 1 \section{ The problem}1 \section{Introduction} 2 2 3 3 The problem of branch displacement optimisation, also known as jump encoding, is
Note: See TracChangeset
for help on using the changeset viewer.