Changeset 2064
 Timestamp:
 Jun 13, 2012, 5:29:11 PM (7 years ago)
 Location:
 src/ASM/CPP2012policy
 Files:

 3 added
 4 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/CPP2012policy/algorithm.tex
r2054 r2064 124 124 \begin{figure} 125 125 \begin{algorithmic} 126 \Function{jump\_expansion\_step}{x} 126 \Function{f}{$labels$,$old\_sigma$,$instr$,$ppc$,$acc$} 127 \State $\langle added, pc, sigma \rangle \gets acc$ 128 \If {$instr$ is a backward jump to $j$} 129 \State $length \gets \mathrm{jump\_size}(pc,sigma_1(labels(j)))$ 130 \ElsIf {$instr$ is a forward jump to $j$} 131 \State $length \gets \mathrm{jump\_size}(pc,old\_sigma_1(labels(j))+added)$ 132 \Else 133 \State $length \gets \mathtt{short\_jump}$ 134 \EndIf 135 \State $old\_length \gets \mathrm{old\_sigma_1}(ppc)$ 136 \State $new\_length \gets \mathrm{max}(old\_length, length)$ 137 \State $old\_size \gets \mathrm{old\_sigma_2}(ppc)$ 138 \State $new\_size \gets \mathrm{instruction\_size}(instr,new\_length)$ 139 \State $new\_added \gets added+(new\_sizeold\_size)$ 140 \State $new\_sigma_1(ppc+1) \gets pc+new\_size$ 141 \State $new\_sigma_2(ppc) \gets new\_length$ \\ 142 \Return $\langle new\_added, pc+new\_size, new\_sigma \rangle$ 127 143 \EndFunction 128 144 \end{algorithmic} … … 130 146 \label{f:jump_expansion_step} 131 147 \end{figure} 148 149 The algorithm, shown in figure~\ref{f:jump_expansion_step}, works by folding the 150 function {\sc f} over the entire program, thus gradually constructing $sigma$. 151 This constitutes one step in the fixed point calculation; successive steps 152 repeat the fold until a fixed point is reached. 153 154 Parameters of the function {\sc f} are: 155 \begin{itemize} 156 \item a function $labels$ that associates a label to its pseudoaddress; 157 \item $old\_sigma$, the $\sigma$ function returned by the previous 158 iteration of the fixed point calculcation; 159 \item $instr$, the instruction currently under consideration; 160 \item $ppc$, the pseudoaddress of $instr$; 161 \item $acc$, the fold accumulator, which contains $pc$ (the highest memory 162 address reached so far), $added$ (the number of bytes added to the program 163 size with respect to the previous iteration), and of course $sigma$, the 164 $\sigma$ function under construction. 165 \end{itemize} 166 167 The first two are parameters that remain the same through one iteration, the 168 last three are standard parameters for a fold function (including $ppc$, 169 which is simply the number of instructions of the program already processed). 170 171 The $\sigma$ functions used by {\sc f} are not of the same type as the final 172 $\sigma$ function: they are of type 173 $\sigma: \mathbb{N} \rightarrow \mathbb{N} \times \{\mathtt{short\_jump}, 174 \mathtt{medium\_jump},\mathtt{long\_jump}\}$; a function that associates a 175 pseudoaddress with an memory address and a jump length. We do this to be able 176 to more easily compare the jump lengths between iterations. In the algorithm, 177 we use the notation $sigma_1(x)$ to denote the memory address corresponding to 178 $x$, and $sigma_2(x)$ to denote the jump length corresponding to $x$. 179 180 Note that the $\sigma$ function used for label lookup varies depending on 181 whether the label is behind our current position or ahead of it. For 182 backward jumps, where the label is behind our current position, we can use 183 $sigma$ for lookup, since its memory address is already known. However, for 184 forward jumps, the memory address of the address of the label is not yet 185 known, so we must use $old\_sigma$. 186 187 We cannot use $old\_sigma$ without change: it might be the case that we have 188 already changed some jumps before, making the program longer. We must therefore 189 compensate for this by adding the size increase of the program to the label's 190 memory address according to $old\_sigma$, so that jump distances do not get 191 compromised. 192 193 Note also that we add the pc to $sigma$ at location $ppc+1$, whereas we add the 194 jump length at location $ppc$. We do this so that $sigma(ppc)$ will always 195 return a couple with the start address of the instruction at $ppc$ and the 196 length of its jump; the end address of the program can be found at $sigma(n+1)$, 197 where $n$ is the number of instructions in the program. 
src/ASM/CPP2012policy/biblio.bib
r1889 r2064 47 47 bibsource = {DBLP, http://dblp.unitrier.de} 48 48 } 49 50 @inproceedings{Sozeau2006, 51 author = {Matthieu Sozeau}, 52 title = {Subset Coercions in {Coq}}, 53 booktitle = {{TYPES}}, 54 pages = {237252}, 55 year = {2006} 56 } 57 
src/ASM/CPP2012policy/main.tex
r2054 r2064 3 3 \usepackage{alltt} 4 4 \usepackage{amsfonts} 5 \usepackage[british]{babel} 5 6 \usepackage[utf8]{inputenc} 7 \usepackage{listings} 8 9 \renewcommand{\verb}{\lstinline} 10 \def\lstlanguagefiles{lstgrafite.tex} 11 \lstset{language=Grafite} 6 12 7 13 \begin{document} … … 31 37 \input{problem} 32 38 \input{algorithm} 39 \input{proof} 40 \input{conclusion} 33 41 34 42 \bibliography{biblio} 
src/ASM/CPP2012policy/problem.tex
r2054 r2064 67 67 68 68 The canonical solution, as shown in~\cite{Szymanski1978} or more recently 69 in~\cite{Dickson2008} for the x86 instruction set, is to use a fix point69 in~\cite{Dickson2008} for the x86 instruction set, is to use a fixed point 70 70 algorithm that starts out with the shortest possible encoding (all jumps 71 71 encoded as short jumps, which is very probably not a correct solution) and then … … 79 79 can be used; above this value the jump must be encoded as a long jump. 80 80 81 Here, termination of the smallest fix point algorithm is easy to prove. All81 Here, termination of the smallest fixed point algorithm is easy to prove. All 82 82 jumps start out encoded as short jumps, which means that the distance between 83 83 any jump and its target is as short as possible. If we therefore need to encode … … 86 86 reasoning holds throughout the subsequent iterations of the algorithms: short 87 87 jumps can change into long jumps, but not vice versa. Hence, the algorithm 88 either terminates when a fix point is reached or when all short jumps have been89 changed into long jumps.88 either terminates when a fixed point is reached or when all short jumps have 89 been changed into long jumps. 90 90 91 91 Also, we can be certain that we have reached an optimal solution: a short jump … … 147 147 as medium jumps. Depending on the relative sizes of long and medium jumps, this 148 148 solution might actually be smaller than the one reached by the smallest 149 fix point algorithm.149 fixed point algorithm. 150 150 151 151 \begin{figure}[h]
Note: See TracChangeset
for help on using the changeset viewer.