Ignore:
Timestamp:
Sep 27, 2012, 5:36:44 PM (7 years ago)
Author:
sacerdot
Message:

New 3.3. Maybe worse than the previous one.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/cpp-asm-2012/cpp-2012-asm.tex

    r2362 r2363  
    308308As a consequence, we allow the programmer to mangle, change and generally adjust addresses as they want, under the proviso that the translation process may not be able to preserve the semantics of programs that do this.
    309309The only limitation introduced by this approach is that the size of
    310 assembly programs is bounded by $2^16$.
     310assembly programs is bounded by $2^{16}$.
    311311This will be further discussed in Subsect.~\ref{subsect.total.correctness.for.well.behaved.assembly.programs}.
    312312
     
    317317\subsection{The assembler}
    318318\label{subsect.the.assembler}
     319The assembler takes in input an assembly program to expand and a
     320branch displacement policy for it.
     321It returns both the assembled program (a list of bytes to be
     322loaded in code memory for execution) and the costing of the source program.
    319323
    320324Conceptually the assembler works in two passes.
    321 The first pass expands every pseudoinstruction into a list of machine code instructions using the function \texttt{expand\_pseudo\_instruction}.
     325The first pass expands every pseudoinstruction into a list of machine code instructions using the function \texttt{expand\_pseudo\_instruction}. The policy
     326determines which expansion among the alternatives will be choosed for
     327pseudo-jumps and pseudo-calls. Once the expansion is performed, the cost
     328of the pseudoinstruction is defined as the cost of the expansion.
    322329The second pass encodes as a list of bytes the expanded instruction list by mapping the function \texttt{assembly1} across the list, and then flattening.
    323 The program obtained as a list of bytes is ready to be loaded in code memory
    324 for execution.
    325330\begin{displaymath}
    326331\hspace{-0.5cm}
    327332\mbox{\fontsize{7}{9}\selectfont$[\mathtt{P_1}, \ldots \mathtt{P_n}]$} \underset{\mbox{\fontsize{7}{9}\selectfont$\mathtt{assembly}$}}{\xrightarrow{\left(P_i \underset{\mbox{\fontsize{7}{9}\selectfont$\mathtt{assembly\_1\_pseudo\_instruction}$}}{\xrightarrow{\mathtt{P_i} \xrightarrow{\mbox{\fontsize{7}{9}\selectfont$\mathtt{expand\_pseudo\_instruction}$}} \mathtt{[I^1_i, \ldots I^q_i]} \xrightarrow{\mbox{\fontsize{7}{9}\selectfont$\mathtt{~~~~~~~~assembly1^{*}~~~~~~~~}$}} \mathtt{[0110]}}} \mathtt{[0110]}\right)^{*}}} \mbox{\fontsize{7}{9}\selectfont$\mathtt{[\ldots0110\ldots]}$}
    328333\end{displaymath}
    329 The most complex of the two passes is the first, which expands pseudoinstructions and must perform the task of branch displacement~\cite{hyde:branch:2006}.
    330 The function \texttt{assembly\_1\_pseudo\_instruction} used in the body of the paper is essentially the composition of the two passes.
    331 
    332 The branch displacement problem refers to the task of expanding pseudojumps into their concrete counterparts, preferably as efficiently as possible.
    333 For instance, the MCS-51 features three unconditional jump instructions: \texttt{LJMP} and \texttt{SJMP}---`long jump' and `short jump' respectively---and an 11-bit oddity of the MCS-51, \texttt{AJMP}.
    334 Each of these three instructions expects arguments in different sizes and behaves in markedly different ways: \texttt{SJMP} may only perform a `local jump'; \texttt{LJMP} may jump to any address in the MCS-51's memory space and \texttt{AJMP} may jump to any address in the current memory page.
    335 Consequently, the size of each opcode is different, and to squeeze as much code as possible into the MCS-51's limited code memory, the smallest possible opcode that will suffice should be selected.
     334In order to understand the type for the policy, we briefly hint at the
     335branch displacement problem for the MCS-51. A detailed description is found
     336in~\cite{boender:correctness:2012}.
     337The MCS-51 features three unconditional jump instructions: \texttt{LJMP} and \texttt{SJMP}---`long jump' and `short jump' respectively---and an 11-bit oddity of the MCS-51, \texttt{AJMP}.
     338Each of these three instructions expects arguments in different sizes and behaves in markedly different ways: \texttt{SJMP} may only perform a `local jump' to an address closer then $2^{7}$ bytes; \texttt{LJMP} may jump to any address in the MCS-51's memory space and \texttt{AJMP} may jump to any address in the current memory page. Memory pages partition the code memory into $2^8$ disjoint areas.
     339The size of each opcode is different, with long jumps being larger than the
     340other two. Because of the presence of \texttt{AJMP}, an optimal global solution
     341may be locally unoptimal, employing a long jump where a shorter one could be
     342used to force later jumps to stay inside single memory pages.
    336343
    337344Similarly, a conditional pseudojump must be translated potentially into a configuration of machine code instructions, depending on the distance to the jump's target.
     
    347354\end{array}
    348355\end{displaymath}}}
    349 Here, if \texttt{JZ} fails, we fall through to the \texttt{SJMP} which jumps over the \texttt{LJMP}.
    350356Naturally, if \texttt{label} is `close enough', a conditional jump pseudoinstruction is mapped directly to a conditional jump machine instruction; the above translation only applies if \texttt{label} is not sufficiently local.
    351357
    352 In order to implement branch displacement it is impossible to really make the \texttt{expand\_pseudo\_instruction} function completely independent of the encoding function.
    353 This is due to branch displacement requiring the distance in bytes of the target of the jump.
    354 Moreover the standard solutions for solving the branch displacement problem find their solutions iteratively, by either starting from a solution where all jumps are long, and shrinking them when possible, or starting from a state where all jumps are short and increasing their length as needed.
    355 Proving the correctness of such algorithms is already quite involved and the correctness of the assembler as a whole does not depend on the `quality' of the solution found to a branch displacement problem.
    356 For this reason, we try to isolate the computation of a branch displacement problem from the proof of correctness for the assembler by parameterising our \texttt{expand\_pseudo\_instruction} by a `policy'.
    357 
    358 \begin{lstlisting}
    359 definition expand_pseudo_instruction:
    360  $\forall$lookup_labels: Identifier $\rightarrow$ Word.
    361  $\forall$policy.
    362  $\forall$ppc: Word.
    363  $\forall$lookup_datalabels: Identifier $\rightarrow$ Word.
    364  $\forall$pi: pseudo_instruction.
    365   list instruction := ...
    366 \end{lstlisting}
    367 Here, the functions \texttt{lookup\_labels} and \texttt{lookup\_datalabels} are the functions that map labels and datalabels to program counters respectively, both of them used in the semantics of assembly.
    368 The input \texttt{pi} is the pseudoinstruction to be expanded and is found at address \texttt{ppc} in the assembly program.
    369 The function takes \texttt{policy} as an input.
    370 In reality, this is a pair of functions, but for the purposes of this paper we simplify.
    371 The \texttt{policy} maps pseudo-program counters to program counters: the encoding of the expansion of the pseudoinstruction found at address \texttt{a} in the assembly code should be placed into code memory at address \texttt{policy(a)}.
    372 Of course this is possible only if the policy is correct, which means that the encoding of consecutive assembly instructions must be consecutive in code memory.
    373 \begin{displaymath}
    374 \texttt{policy}(\texttt{ppc} + 1) = \texttt{pc} + \texttt{current\_instruction\_size}
    375 \end{displaymath}
    376 Here, \texttt{current\_instruction\_size} is the size in bytes of the encoding of the expanded pseudoinstruction found at \texttt{ppc}.
    377 Note that the entanglement we hinted at is only partially solved in this way: the assembler code can ignore the implementation details of the algorithm that finds a policy;
    378 however, the algorithm that finds a policy must know the exact behaviour of the assembly program because it needs to predict the way the assembly will expand and encode pseudoinstructions, once fed with a policy.
    379 A companion submission to this one~\cite{boender:correctness:2012} certifies an algorithm that finds branch displacement policies for the assembler described in this paper.
    380 
    381 The \texttt{expand\_pseudo\_instruction} function uses the \texttt{policy} map to determine the size of jump required when expanding pseudojumps, computing the jump size by examining the size of the differences between program counters.
    382 For instance, if at address \texttt{ppc} in the assembly program we found \texttt{Jmp l} such that \texttt{lookup\_labels l = a}, if the offset \texttt{d = policy(a) - policy(ppc + 1)} is such that \texttt{d} $< 128$ then \texttt{Jmp l} is normally translated to the best local solution, the short jump \texttt{SJMP d}.
    383 A global best solution to the branch displacement problem, however, is not always made of locally best solutions.
    384 Therefore, in some circumstances, it is necessary to force the assembler to expand jumps into larger ones.
    385 This is achieved by another boolean-valued function such that if the function applied to \texttt{ppc} returns true then a \texttt{Jmp l} at address \texttt{ppc} is always translated to a long jump.
    386 An essentially identical mechanism exists for call instructions.
     358%In order to implement branch displacement it is impossible to really make the \texttt{expand\_pseudo\_instruction} function completely independent of the encoding function.
     359%This is due to branch displacement requiring the distance in bytes of the target of the jump.
     360%Moreover the standard solutions for solving the branch displacement problem find their solutions iteratively, by either starting from a solution where all jumps are long, and shrinking them when possible, or starting from a state where all jumps are short and increasing their length as needed.
     361%Proving the correctness of such algorithms is already quite involved and the correctness of the assembler as a whole does not depend on the `quality' of the solution found to a branch displacement problem.
     362%For this reason, we try to isolate the computation of a branch displacement problem from the proof of correctness for the assembler by parameterising our \texttt{expand\_pseudo\_instruction} by a `policy'.
     363
     364The \texttt{expand\_pseudo\_instruction} function is driven by a policy
     365in the choice of expansion of pseudoinstructions. The simplest idea
     366is then to define policies as functions that maps jumps to their size.
     367This simple idea, however, is impractical because short jumps require the
     368offset of the target. For instance, suppose that at address \texttt{ppc} in
     369the assembly program we found \texttt{Jmp l} such that $l$ is associated to the
     370pseudo-address \texttt{a} and the policy wants the \texttt{Jmp} to become a
     371\texttt{SJMP $\delta$}. To compute $\delta$, we need to know what the addresses
     372\texttt{ppc+1} and \texttt{a} will become in the assembled program to compute
     373their difference.
     374The address \texttt{a} will be associated to is a function of the expansion
     375of all the pseudoinstructions between \texttt{ppc} and \texttt{a}, which is
     376still to be performed when expanding the instruction at \texttt{ppc}.
     377
     378To solve the issue, we define the policy \texttt{policy} as a maps
     379from a valid pseudoaddress to the corresponding address in the assembled
     380program.
     381Therefore, $\delta$ in the example above can be computed simply as
     382\texttt{sigma(a) - sigma(ppc + 1)}. Moreover, the \texttt{expand\_pseudo\_instruction} emits a \texttt{SJMP} only after verifying for each \texttt{Jmp} that
     383$\delta < 128$. When this is not the case, the function emits an
     384\texttt{AJMP} if possible, or an \texttt{LJMP} otherwise, therefore always
     385picking the locally best solution.
     386In order to accomodate those optimal solutions that require local sub-optimal
     387choices, the policy may also return a boolean used to force
     388the translation of a \texttt{Jmp} into a \texttt{LJMP} even if
     389$\delta < 128$. An essentially identical mechanism exists for call
     390instructions and conditional jumps.
     391
     392In order for the translation of a jump to be correct, the address associated to
     393\texttt{a} by the policy and by the assembler must coincide. The latter is
     394the sum of the size of all the expansions of the pseudo-instructions that
     395preceed the one at address \texttt{a}: the assembler just concatenates all
     396expansions one after another. To grant this property, we impose a
     397correctness criterion over policies. A policy is correct when for all
     398valid pseudoaddresses \texttt{ppc}
     399$${\texttt{policy(ppc+1) = policy(ppc) + instruction\_size(ppc)}}$$
     400Here \texttt{instruction\_size(ppc)} is the size in bytes of the expansion
     401of the pseudoinstruction found at \texttt{pcc}, i.e. the length of
     402$\texttt{assembly\_1\_pseudo\_instruction(ppc)}$.
     403
    387404
    388405% ---------------------------------------------------------------------------- %
Note: See TracChangeset for help on using the changeset viewer.