Changeset 954


Ignore:
Timestamp:
Jun 15, 2011, 11:30:50 AM (8 years ago)
Author:
mulligan
Message:

more changes to introduction

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CPP2011/cpp-2011.tex

    r953 r954  
    7979
    8080In order to achieve this CerCo imposes a cost model on programs, or more specifically, on simple blocks of instructions.
    81 This cost model is induced by the compilation process itself, and its non-compositional nature allows us to assign different costs to identical blocks of instructions depending on how they are compiled, obtaining a very precise costing for a program by embracing the compilation process, not ignoring it.
    82 However, this complicates the proof of correctness for the compiler proper: for every translation pass from intermediate language to intermediate language, we must prove that not only has the meaning of a program been preserved, but also its complexity characteristics.
     81This cost model is induced by the compilation process itself, and its non-compositional nature allows us to assign different costs to identical blocks of instructions depending on how they are compiled.
     82In short, we aim to obtain a very precise costing for a program by embracing the compilation process, not ignoring it.
     83This, however, complicates the proof of correctness for the compiler proper: for every translation pass from intermediate language to intermediate language, we must prove that not only has the meaning of a program been preserved, but also its complexity characteristics.
    8384This also applies for the translation from assembly language to machine code.
     85
    8486How do we assign a cost to a pseudoinstruction?
    85 
    86 There is one snag: how to expand jumps.
    8787As mentioned, conditional jumps at the assembly level can jump to a label appearing anywhere in the program.
    88 However, at the machine code level, conditional jumps are limited to jumping `locally', using an 8-bit relative offset of the program counter.
    89 To translate a jump to a label, a single conditional jump pseudoinstruction is potentially translated into a block of three real instructions, as follows (here, \texttt{JZ} is `jump if accumulator is zero'):
     88However, at the machine code level, conditional jumps are limited to jumping `locally', using a measly byte offset.
     89To translate a jump to a label, a single conditional jump pseudoinstruction may be translated into a block of three real instructions, as follows (here, \texttt{JZ} is `jump if accumulator is zero'):
    9090\begin{displaymath}
    9191\begin{array}{r@{\quad}l@{\;\;}l@{\qquad}c@{\qquad}l@{\;\;}l}
     
    9898\end{displaymath}
    9999In the translation, if \texttt{JZ} fails, we fall through to the \texttt{SJMP} which jumps over the \texttt{LJMP}.
    100 Naturally, if \textit{label} is close enough, a conditional jump pseudoinstruction is mapped directly to a conditional jump instruction; the above translation only applies if \textit{label} is not sufficiently local.
    101 Similarly, we must also work out whether to expand an unconditional jump pse
     100Naturally, if \textit{label} is close enough, a conditional jump pseudoinstruction is mapped directly to a conditional jump machine instruction; the above translation only applies if \textit{label} is not sufficiently local.
    102101This leaves the problem, addressed below, of calculating whether a label is indeed `close enough' for the simpler translation to be used.
    103102
     
    105104A conditional jump may be mapped to a single machine instruction or a block of three.
    106105Perhaps more insidious, the number of cycles needed to execute the instructions in the two branches of a translated conditional jump may be different.
    107 Depending on the semiconductor manufacturer, an \texttt{SJMP} could in theory take a different number of clock cycles to execute than an \texttt{LJMP}.
     106Depending on the particular MCS-51 derivative at hand, an \texttt{SJMP} could in theory take a different number of clock cycles to execute than an \texttt{LJMP}.
    108107These issues must also be dealt with in order to prove that the translation pass preserves the concrete complexity of the code.
    109108
    110109The question remains: how do we decide whether to expand a jump into an \texttt{SJMP} or an \texttt{LJMP}?
    111 This problem is far from trivial.
    112 To understand why, consider the following snippet of assembly code:
     110To understand why this problem is not trivial, consider the following snippet of assembly code:
    113111\begin{displaymath}
    114112\text{dpm: finish me}
    115113\end{displaymath}
     114
    116115As our example shows, given an occurence $l$ of an \texttt{LJMP} instruction, it may be possible to shrink $l$ to an occurence of an \texttt{SJMP} providing we can shrink any \texttt{LJMP}s that exist between $l$ and its target location.
    117116However, shrinking these \texttt{LJMP}s may in turn depend on shrinking $l$ to an \texttt{SJMP}, as it is perfectly possible to jump backwards.
    118 In short, unless we can somehow break this loop of circularity, we are stuck with a suboptimal solution to the expanding jumps problem.
     117In short, unless we can somehow break this loop of circularity, and similar knotty configurations of jumps, we are stuck with a suboptimal solution to the expanding jumps problem.
    119118
    120 How we go about resolving this problem affected the shape of our proof of correctness for the whole assembler in a rather profound way.
    121 We first attempted to synthesize a solution bottom up.
    122 That is, starting with no solution, we gradually refine a solution using the same functions that implement the jump expansion.
     119How we went about resolving this problem affected the shape of our proof of correctness for the whole assembler in a rather profound way.
     120We first attempted to synthesize a solution bottom up: starting with no solution, we gradually refine a solution using the same functions that implement the jump expansion.
    123121Using this technique, solutions can fail to exist, and the proof quickly descends into a diabolical quagmire.
    124122
    125 Abandoning this attempt, we instead split the `policy', i.e. the decision over how any particular jump should be expanded, from the implementation.
     123Abandoning this attempt, we instead split the `policy'---the decision over how any particular jump should be expanded---from the implementation that actually expands assembly programs into machine code.
    126124Assuming the existence of a correct policy, we proved the implementation of the assembler correct.
    127 Further, we proved that the assembler fails to assemble a file if and only if a correct policy does not exist.
     125Further, we proved that the assembler fails to assemble an assembly program if and only if a correct policy does not exist.
    128126Policies do not exist in only a limited number of circumstances: namely, if a pseudoinstruction attempts to jump to a label that does not exist, or the program is too large to fit in code memory.
    129 The first case would constitute a serious compiler error, and hopefully certifying the rest of the compiler would rule this possibility out; the second case is unavoidable---certified compiler or not, trying to load a huge program into a small code memory will break \emph{something}.
     127The first case would constitute a serious compiler error, and hopefully certifying the rest of the compiler would rule this possibility out.
     128The second case is unavoidable---certified compiler or not, trying to load a huge program into a small code memory will break \emph{something}.
     129
     130The rest of this paper is a detailed description of this proof.
    130131
    131132% ---------------------------------------------------------------------------- %
Note: See TracChangeset for help on using the changeset viewer.