Changeset 3361


Ignore:
Timestamp:
Jun 17, 2013, 12:11:13 PM (4 years ago)
Author:
sacerdot
Message:

15 pages version

Location:
src/ASM/CPP2012-policy
Files:
4 edited

Legend:

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

    r3353 r3361  
    33\subsection{Design decisions}
    44
    5 Given the NP-completeness of the problem, to arrive at an optimal solution
    6 (using, for example, a constraint solver) will potentially take a great amount
    7 of time.
     5Given the NP-completeness of the problem, finding optimal solutions
     6(using, for example, a constraint solver) can potentially be very costly.
    87
    98The SDCC compiler~\cite{SDCC2011}, which has a backend targetting the MCS-51
     
    4645and long jumps indefinitely.
    4746
    48 In order to keep the algorithm in the same complexity class and more easily
     47To keep the algorithm in the same complexity class and more easily
    4948prove termination, we decided to explicitly enforce the `branch instructions
    5049must always grow longer' requirement: if a branch instruction is encoded as a
    5150long jump in one iteration, it will also be encoded as a long jump in all the
    52 following iterations. This means that the encoding of any branch instruction
     51following iterations. Therefore the encoding of any branch instruction
    5352can change at most two times: once from short to absolute (or long), and once
    5453from absolute to long.
     
    5756in step $n$ as an absolute jump, but in step $n+1$ it is determined that
    5857(because of changes elsewhere) it can now be encoded as a short jump. Due to
    59 the requirement that the branch instructions must always grow longer, this
    60 means that the branch encoding will be encoded as an absolute jump in step
     58the requirement that the branch instructions must always grow longer,
     59the branch encoding will be encoded as an absolute jump in step
    6160$n+1$ as well.
    6261
     
    118117correctness, since a long jump is applicable in any situation.
    119118
    120 \begin{figure}
     119\begin{figure}[t]
    121120\begin{algorithmic}
    122121\Function{f}{$labels$,$old\_sigma$,$instr$,$ppc$,$acc$}
  • src/ASM/CPP2012-policy/main.tex

    r3342 r3361  
    99\usepackage[utf8]{inputenc}
    1010\usepackage{listings}
     11\usepackage{subcaption}
    1112
    1213\renewcommand{\verb}{\lstinline}
     
    4849\input{conclusion}
    4950
    50 \clearpage
    5151\bibliography{biblio}
    5252\bibliographystyle{splncs03}
  • src/ASM/CPP2012-policy/problem.tex

    r3354 r3361  
    104104fixed point algorithm that starts with the shortest possible encoding (all
    105105branch instruction encoded as short jumps, which is likely not a correct
    106 solution) and then iterates over the program to re-encode those branch
     106solution) and then iterates over the source to re-encode those branch
    107107instructions whose target is outside their range.
    108108
     
    130130the absolute jump, as with absolute jumps, the encoding of a branch
    131131instruction no longer depends only on the distance between the branch
    132 instruction and its target: in order for an absolute jump to be possible, they
    133 need to be in the same segment (for the MCS-51, this means that the first 5
     132instruction and its target: an absolute jump is possible when they
     133are in the same segment (for the MCS-51, this means that the first 5
    134134bytes of their addresses have to be equal). It is therefore entirely possible
    135135for two branch instructions with the same span to be encoded in different ways
     
    137137long if this is not the case).
    138138
    139 \begin{figure}[ht]
     139\begin{figure}[t]
     140\begin{subfigure}[b]{.45\linewidth}
    140141\begin{alltt}
    141142    jmp X
    142     \vdots
    143 L\(\sb{0}\):
    144     \vdots
     143    \ldots
     144L\(\sb{0}\): \ldots
     145% Start of new segment if
     146% jmp X is encoded as short
     147    \ldots
    145148    jmp L\(\sb{0}\)
    146149\end{alltt}
    147150\caption{Example of a program where a long jump becomes absolute}
    148151\label{f:term_example}
     152\end{subfigure}
     153\hfill
     154\begin{subfigure}[b]{.45\linewidth}
     155\begin{alltt}
     156L\(\sb{0}\): jmp X
     157X:  \ldots
     158    \ldots
     159L\(\sb{1}\): \ldots
     160% Start of new segment if
     161% jmp X is encoded as short
     162    \ldots
     163    jmp L\(\sb{1}\)
     164    \ldots
     165    jmp L\(\sb{1}\)
     166    \ldots
     167    jmp L\(\sb{1}\)
     168    \ldots
     169\end{alltt}
     170\caption{Example of a program where the fixed-point algorithm is not optimal}
     171\label{f:opt_example}
     172\end{subfigure}
    149173\end{figure}
    150174
     
    187211as short jumps.
    188212
    189 \begin{figure}[ht]
    190 \begin{alltt}
    191 L\(\sb{0}\): jmp X
    192 X:
    193     \vdots
    194 L\(\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}
    206 
    207213Then, if {\tt jmp X} were to be encoded as a short jump, which is clearly
    208214possible, all of the branches to $\mathtt{L}_{1}$ would have to be encoded as
  • src/ASM/CPP2012-policy/proof.tex

    r3353 r3361  
    22
    33In this section, we present the correctness proof for the algorithm in more
    4 detail.  The main correctness statement is as follows (slightly simplified, here):
    5 
     4detail.  The main correctness statement is shown, slightly simplified, in~Figure~\cite{statement}.
     5
     6\begin{figure}[t]
    67\begin{alignat*}{6}
    78\mathtt{sigma}&\omit\rlap{$\mathtt{\_policy\_specification} \equiv
     
    2021        &&&&& pc + (\mathtt{instruction\_size}\ sigma\ policy\ ppc\ instruction = 2^{16}))
    2122\end{alignat*}
     23\caption{Main correctness statement\label{statement}}
     24\end{figure}
    2225
    2326Informally, this means that when fetching a pseudo-instruction at $ppc$, the
Note: See TracChangeset for help on using the changeset viewer.