 Timestamp:
 Jun 15, 2011, 11:30:50 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/CPP2011/cpp2011.tex
r953 r954 79 79 80 80 In 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 noncompositional 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. 81 This cost model is induced by the compilation process itself, and its noncompositional nature allows us to assign different costs to identical blocks of instructions depending on how they are compiled. 82 In short, we aim to obtain a very precise costing for a program by embracing the compilation process, not ignoring it. 83 This, 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. 83 84 This also applies for the translation from assembly language to machine code. 85 84 86 How do we assign a cost to a pseudoinstruction? 85 86 There is one snag: how to expand jumps.87 87 As 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 a n 8bit relative offset of the program counter.89 To translate a jump to a label, a single conditional jump pseudoinstruction is potentiallytranslated into a block of three real instructions, as follows (here, \texttt{JZ} is `jump if accumulator is zero'):88 However, at the machine code level, conditional jumps are limited to jumping `locally', using a measly byte offset. 89 To 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'): 90 90 \begin{displaymath} 91 91 \begin{array}{r@{\quad}l@{\;\;}l@{\qquad}c@{\qquad}l@{\;\;}l} … … 98 98 \end{displaymath} 99 99 In 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 100 Naturally, 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. 102 101 This leaves the problem, addressed below, of calculating whether a label is indeed `close enough' for the simpler translation to be used. 103 102 … … 105 104 A conditional jump may be mapped to a single machine instruction or a block of three. 106 105 Perhaps 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}.106 Depending on the particular MCS51 derivative at hand, an \texttt{SJMP} could in theory take a different number of clock cycles to execute than an \texttt{LJMP}. 108 107 These issues must also be dealt with in order to prove that the translation pass preserves the concrete complexity of the code. 109 108 110 109 The 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: 110 To understand why this problem is not trivial, consider the following snippet of assembly code: 113 111 \begin{displaymath} 114 112 \text{dpm: finish me} 115 113 \end{displaymath} 114 116 115 As 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. 117 116 However, 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.117 In 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. 119 118 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. 119 How we went about resolving this problem affected the shape of our proof of correctness for the whole assembler in a rather profound way. 120 We 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. 123 121 Using this technique, solutions can fail to exist, and the proof quickly descends into a diabolical quagmire. 124 122 125 Abandoning this attempt, we instead split the `policy' , i.e. the decision over how any particular jump should be expanded, from the implementation.123 Abandoning this attempt, we instead split the `policy'the decision over how any particular jump should be expandedfrom the implementation that actually expands assembly programs into machine code. 126 124 Assuming 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 fileif and only if a correct policy does not exist.125 Further, we proved that the assembler fails to assemble an assembly program if and only if a correct policy does not exist. 128 126 Policies 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 unavoidablecertified compiler or not, trying to load a huge program into a small code memory will break \emph{something}. 127 The first case would constitute a serious compiler error, and hopefully certifying the rest of the compiler would rule this possibility out. 128 The second case is unavoidablecertified compiler or not, trying to load a huge program into a small code memory will break \emph{something}. 129 130 The rest of this paper is a detailed description of this proof. 130 131 131 132 %  %
Note: See TracChangeset
for help on using the changeset viewer.