Changeset 2064 for src


Ignore:
Timestamp:
Jun 13, 2012, 5:29:11 PM (9 years ago)
Author:
boender
Message:
  • more progress
Location:
src/ASM/CPP2012-policy
Files:
3 added
4 edited

Legend:

Unmodified
Added
Removed

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

    r2054 r2064  
    124124\begin{figure}
    125125\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\_size-old\_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$
    127143\EndFunction
    128144\end{algorithmic}
    … …  
    130146\label{f:jump_expansion_step}
    131147\end{figure}
     148
     149The algorithm, shown in figure~\ref{f:jump_expansion_step}, works by folding the
     150function {\sc f} over the entire program, thus gradually constructing $sigma$.
     151This constitutes one step in the fixed point calculation; successive steps
     152repeat the fold until a fixed point is reached.
     153
     154Parameters of the function {\sc f} are:
     155\begin{itemize}
     156        \item a function $labels$ that associates a label to its pseudo-address;
     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 pseudo-address 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
     167The first two are parameters that remain the same through one iteration, the
     168last three are standard parameters for a fold function (including $ppc$,
     169which is simply the number of instructions of the program already processed).
     170
     171The $\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
     175pseudo-address with an memory address and a jump length. We do this to be able
     176to more easily compare the jump lengths between iterations. In the algorithm,
     177we 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
     180Note that the $\sigma$ function used for label lookup varies depending on
     181whether the label is behind our current position or ahead of it. For
     182backward 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
     184forward jumps, the memory address of the address of the label is not yet
     185known, so we must use $old\_sigma$.
     186
     187We cannot use $old\_sigma$ without change: it might be the case that we have
     188already changed some jumps before, making the program longer. We must therefore
     189compensate for this by adding the size increase of the program to the label's
     190memory address according to $old\_sigma$, so that jump distances do not get
     191compromised.
     192
     193Note also that we add the pc to $sigma$ at location $ppc+1$, whereas we add the
     194jump length at location $ppc$. We do this so that $sigma(ppc)$ will always
     195return a couple with the start address of the instruction at $ppc$ and the
     196length of its jump; the end address of the program can be found at $sigma(n+1)$,
     197where $n$ is the number of instructions in the program.

  • src/ASM/CPP2012-policy/biblio.bib

    r1889 r2064  
    4747  bibsource = {DBLP, http://dblp.uni-trier.de}
    4848}
     49
     50@inproceedings{Sozeau2006,
     51  author = {Matthieu Sozeau},
     52  title = {Subset Coercions in {Coq}},
     53  booktitle = {{TYPES}},
     54  pages = {237--252},
     55  year = {2006}
     56}
     57

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

    r2054 r2064  
    33\usepackage{alltt}
    44\usepackage{amsfonts}
     5\usepackage[british]{babel}
    56\usepackage[utf8]{inputenc}
     7\usepackage{listings}
     8
     9\renewcommand{\verb}{\lstinline}
     10\def\lstlanguagefiles{lst-grafite.tex}
     11\lstset{language=Grafite}
    612
    713\begin{document}
    … …  
    3137\input{problem}
    3238\input{algorithm}
     39\input{proof}
     40\input{conclusion}
    3341
    3442\bibliography{biblio}

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

    r2054 r2064  
    6767
    6868The canonical solution, as shown in~\cite{Szymanski1978} or more recently
    69 in~\cite{Dickson2008} for the x86 instruction set, is to use a fixpoint
     69in~\cite{Dickson2008} for the x86 instruction set, is to use a fixed point
    7070algorithm that starts out with the shortest possible encoding (all jumps
    7171encoded as short jumps, which is very probably not a correct solution) and then
    … …  
    7979can be used; above this value the jump must be encoded as a long jump.
    8080
    81 Here, termination of the smallest fixpoint algorithm is easy to prove. All
     81Here, termination of the smallest fixed point algorithm is easy to prove. All
    8282jumps start out encoded as short jumps, which means that the distance between
    8383any jump and its target is as short as possible. If we therefore need to encode
    … …  
    8686reasoning holds throughout the subsequent iterations of the algorithms: short
    8787jumps can change into long jumps, but not vice versa. Hence, the algorithm
    88 either terminates when a fixpoint is reached or when all short jumps have been
    89 changed into long jumps.
     88either terminates when a fixed point is reached or when all short jumps have
     89been changed into long jumps.
    9090
    9191Also, we can be certain that we have reached an optimal solution: a short jump
    … …  
    147147as medium jumps. Depending on the relative sizes of long and medium jumps, this
    148148solution might actually be smaller than the one reached by the smallest
    149 fixpoint algorithm.
     149fixed point algorithm.
    150150
    151151\begin{figure}[h]
Note: See TracChangeset for help on using the changeset viewer.