Ignore:
Timestamp:
Jun 15, 2012, 3:25:21 PM (7 years ago)
Author:
mulligan
Message:

Changes to the English for Jaap, and some tidying up and making consistent with the other CPP submission.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CPP2012-policy/problem.tex

    r2091 r2096  
    55fact that in many architecture sets, the encoding (and therefore size) of some
    66instructions depends on the distance to their operand (the instruction 'span').
    7 The branch displacement optimisation problem consists in encoding these
     7The branch displacement optimisation problem consists of encoding these
    88span-dependent instructions in such a way that the resulting program is as
    99small as possible.
     
    1111This problem is the subject of the present paper. After introducing the problem
    1212in more detail, we will discuss the solutions used by other compilers, present
    13 the algorithm used by us in the CerCo assembler, and discuss its verification,
    14 that is the proofs of termination and correctness using the Matita theorem
    15 prover~\cite{Asperti2007}.
     13the algorithm we use in the CerCo assembler, and discuss its verification,
     14that is the proofs of termination and correctness using the Matita proof
     15assistant~\cite{Asperti2007}.
    1616 
    1717The research presented in this paper has been executed within the CerCo project
     
    1919target architecture for this project is the MCS-51, whose instruction set
    2020contains span-dependent instructions. Furthermore, its maximum addressable
    21 memory size is very small (65 Kbytes), which makes it important to generate
     21memory size is very small (64 Kb), which makes it important to generate
    2222programs that are as small as possible.
    2323
     
    3131In most modern instruction sets that have them, the only span-dependent
    3232instructions are branch instructions. Taking the ubiquitous x86-64 instruction
    33 set as an example, we find that it contains are eleven different forms of the
     33set as an example, we find that it contains eleven different forms of the
    3434unconditional branch instruction, all with different ranges, instruction sizes
    3535and semantics (only six are valid in 64-bit mode, for example). Some examples
    36 are shown in figure~\ref{f:x86jumps}.
     36are shown in Figure~\ref{f:x86jumps}.
    3737
    3838\begin{figure}[h]
     
    5555The chosen target architecture of the CerCo project is the Intel MCS-51, which
    5656features three types of branch instructions (or jump instructions; the two terms
    57 are used interchangeably), as shown in figure~\ref{f:mcs51jumps}.
     57are used interchangeably), as shown in Figure~\ref{f:mcs51jumps}.
    5858
    5959\begin{figure}[h]
     
    7878encoded using three branch instructions (for instructions whose logical
    7979negation is available, it can be done with two branch instructions, but for
    80 some instructions, this opposite is not available); the call instruction is
     80some instructions this is not available); the call instruction is
    8181only available in absolute and long forms.
    8282
    83 Note that even though the MCS-51 architecture is much less advanced and more
    84 simple than the x86-64 architecture, the basic types of branch instruction
     83Note that even though the MCS-51 architecture is much less advanced and simpler
     84than the x86-64 architecture, the basic types of branch instruction
    8585remain the same: a short jump with a limited range, an intra-segment jump and a
    8686jump that can reach the entire available memory.
    8787 
    88 Generally, in the code that is sent to the assembler as input, the only
    89 difference made between branch instructions is by semantics, not by span. This
     88Generally, in code fed to the assembler as input, the only
     89difference between branch instructions is semantics, not span. This
    9090means that a distinction is made between an unconditional branch and the
    9191several kinds of conditional branch, but not between their short, absolute or
     
    9494The algorithm used by the assembler to encode these branch instructions into
    9595the different machine instructions is known as the {\em branch displacement
    96 algorithm}. The optimisation problem consists in using as small an encoding as
     96algorithm}. The optimisation problem consists of finding as small an encoding as
    9797possible, thus minimising program length and execution time.
    9898
     
    102102The canonical solution, as shown by Szymanski~\cite{Szymanski1978} or more
    103103recently by Dickson~\cite{Dickson2008} for the x86 instruction set, is to use a
    104 fixed point algorithm that starts out with the shortest possible encoding (all
    105 branch instruction encoded as short jumps, which is very probably not a correct
     104fixed point algorithm that starts with the shortest possible encoding (all
     105branch instruction encoded as short jumps, which is likely not a correct
    106106solution) and then iterates over the program to re-encode those branch
    107107instructions whose target is outside their range.
     
    120120situation where the span of $j$ is so small that it can be encoded as a short
    121121jump. This argument continues to hold throughout the subsequent iterations of
    122 the algorithm: short jumps can change into long jumps, but not vice versa
    123 (spans only increase). Hence, the algorithm either terminates when a fixed
     122the algorithm: short jumps can change into long jumps, but not \emph{vice versa},
     123as spans only increase. Hence, the algorithm either terminates early when a fixed
    124124point is reached or when all short jumps have been changed into long jumps.
    125125
     
    128128
    129129However, neither of these claims (termination nor optimality) hold when we add
    130 the absolute jump.
    131 
    132 The reason for this is that with absolute jumps, the encoding of a branch
     130the absolute jump, as with absolute jumps, the encoding of a branch
    133131instruction no longer depends only on the distance between the branch
    134132instruction and its target: in order for an absolute jump to be possible, they
     
    139137long if this is not the case).
    140138
    141 This invalidates the termination argument: a branch instruction, once encoded
     139\begin{figure}[ht]
     140\begin{alltt}
     141    jmp X
     142    \vdots
     143L\(\sb{0}\):
     144    \vdots
     145    jmp L\(\sb{0}\)
     146\end{alltt}
     147\caption{Example of a program where a long jump becomes absolute}
     148\label{f:term_example}
     149\end{figure}
     150
     151This invalidates our earlier termination argument: a branch instruction, once encoded
    142152as a long jump, can be re-encoded during a later iteration as an absolute jump.
    143 Consider the program shown in figure~\ref{f:term_example}. At the start of the
     153Consider the program shown in Figure~\ref{f:term_example}. At the start of the
    144154first iteration, both the branch to {\tt X} and the branch to $\mathtt{L}_{0}$
    145155are encoded as small jumps. Let us assume that in this case, the placement of
     
    156166Hence, in the third iteration, the branch to $\mathtt{L}_{0}$ can be encoded as
    157167an absolute jump. At first glance, there is nothing that prevents us from
    158 making a construction where two branch instructions interact in such a way as
    159 to keep switching between long and absolute encodings for an indefinite amount
    160 of iterations.
    161 
    162 \begin{figure}[h]
    163 \begin{alltt}
    164     jmp X
    165     \vdots
    166 L\(\sb{0}\):
    167     \vdots
    168     jmp L\(\sb{0}\)
    169 \end{alltt}
    170 \caption{Example of a program where a long jump becomes absolute}
    171 \label{f:term_example}
    172 \end{figure}
    173 
    174 In fact, this situation mirrors the explanation by
    175 Szymanski~\cite{Szymanski1978} of why the branch displacement optimisation
    176 problem is NP-complete. In this explanation, a condition for NP-completeness
    177 is the fact that programs be allowed to contain {\em pathological} jumps.
    178 These are branch instructions that can normally not be encoded as a short(er)
    179 jump, but gain this property when some other branch instructions are encoded as
    180 a long(er) jump. This is exactly what happens in figure~\ref{f:term_example}:
    181 by encoding the first branch instruction as a long jump, another branch
    182 instructions switches from long to absolute (which is shorter).
    183 
    184 The optimality argument no longer holds either. Let us consider the program
    185 shown in figure~\ref{f:opt_example}. Suppose that the distance between
     168constructing a configuration where two branch instructions interact in such a
     169way as to iterate indefinitely between long and absolute encodings.
     170
     171This situation mirrors the explanation by Szymanski~\cite{Szymanski1978} of why
     172the branch displacement optimisation problem is NP-complete. In this explanation,
     173a condition for NP-completeness is the fact that programs be allowed to contain
     174{\em pathological} jumps. These are branch instructions that can normally not be
     175encoded as a short(er) jump, but gain this property when some other branch
     176instructions are encoded as a long(er) jump. This is exactly what happens in
     177Figure~\ref{f:term_example}. By encoding the first branch instruction as a long
     178jump, another branch instruction switches from long to absolute (which is
     179shorter).
     180
     181In addition, our previous optimality argument no longer holds. Consider the program
     182shown in Figure~\ref{f:opt_example}. Suppose that the distance between
    186183$\mathtt{L}_{0}$ and $\mathtt{L}_{1}$ is such that if {\tt jmp X} is encoded
    187184as a short jump, there is a segment border just after $\mathtt{L}_{1}$. Let
     
    189186segment, but far enough away from $\mathtt{L}_{1}$ that they cannot be encoded
    190187as short jumps.
     188
     189\begin{figure}[ht]
     190\begin{alltt}
     191L\(\sb{0}\): jmp X
     192X:
     193    \vdots
     194L\(\sb{1}\):
     195    \vdots
     196    jmp L\(\sb{1}\)
     197    \vdots
     198    jmp L\(\sb{1}\)
     199    \vdots
     200    jmp L\(\sb{1}\)
     201    \vdots
     202\end{alltt}
     203\caption{Example of a program where the fixed-point algorithm is not optimal}
     204\label{f:opt_example}
     205\end{figure}
    191206
    192207Then, if {\tt jmp X} were to be encoded as a short jump, which is clearly
     
    198213this solution might actually be smaller than the one reached by the smallest
    199214fixed point algorithm.
    200 
    201 \begin{figure}[h]
    202 \begin{alltt}
    203 L\(\sb{0}\): jmp X
    204 X:
    205     \vdots
    206 L\(\sb{1}\):
    207     \vdots
    208     jmp L\(\sb{1}\)
    209     \vdots
    210     jmp L\(\sb{1}\)
    211     \vdots
    212     jmp L\(\sb{1}\)
    213     \vdots
    214 \end{alltt}
    215 \caption{Example of a program where the fixed-point algorithm is not optimal}
    216 \label{f:opt_example}
    217 \end{figure}
Note: See TracChangeset for help on using the changeset viewer.