Changeset 2340
 Timestamp:
 Sep 26, 2012, 1:53:30 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Papers/cppasm2012/cpp2012asm.tex
r2339 r2340 78 78 As a result our C compiler, to have any sort of hope of successfully compiling realistic programs for embedded devices, ought to produce `tight' machine code. 79 79 80 In order to do this, we must solve the `branch displacement' problemdeciding how best to expand pseudojumps to labels in assembly language to machine code jumps. 81 Clearly a correct but efficient strategy would be to expand all unconditional pseudojumps to the MCS51's \texttt{LJMP} instruction, and all conditional pseudojumps to a set configuration of jumps using \texttt{LJMP} instructions; this is inefficient and a waste of valuable code memory space. 82 Finding an efficient solution with this expansion process is not trivial, and is a wellknown problem for those writing assemblers targetting CISC architectures (for instance, see~\cite{hyde:branch:2006}). 80 In order to do this, we must solve the `branch displacement' problemdeciding how best to expand pseudojumps to labels in assembly language to machine code jumps. The branch displacement problem happears when pseudojumps can be expanded 81 in different ways to real machine instructions, but the different expansions 82 are not equivalent (e.g. do not have the same size or speed) and not always 83 correct (e.g. correctness is only up to global constraints over the compiled 84 code). For instance, some jump instructions (short jumps) are very small 85 and fast, but they can only reach destinations within a 86 certain distance from the current instruction. When the destinations are 87 too far away, larger and slower long jumps must be used. The use of a long jump may 88 augment the distance between another pseudojump and its target, forcing 89 another long jump use, in a cascading effect. The job of the optimizing 90 compiler (assembler) is to individually expand every pseudoinstruction in such a way 91 that all global constraints are satisfied and that the compiled program size 92 is minimal in size and faster in time. The problem is known to be particularly 93 complex for most CICS architectures (for instance, see~\cite{hyde:branch:2006}). 83 94 84 95 To free the CerCo C compiler from having to consider complications relating to branch displacement, we have chosen to implement an optimising assembler, whose input language the compiler will target. … … 86 97 We simplify the proof by assuming that all our assembly programs are prelinked (i.e. we do not formalise a linkerthis is left for future work). 87 98 88 Further, we must make sure that the assembly process does not change the timing characteristics of an assembly program for two reasons. 89 90 First, the semantics of some functions of the MCS51, notably I/O, depend on the microprocessor's clock. 91 Changing how long a particular program takes to execute can affect the semantics of a program. 92 This is undesirable. 93 94 Second, CerCo imposes a cost model on C programs or, more specifically, on simple blocks of instructions. 99 Another complication we have addressed is that of the cost model. 100 CerCo imposes a cost model on C programs or, more specifically, on simple blocks of instructions. 95 101 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. 96 102 In short, we aim to obtain a very precise costing for a program by embracing the compilation process, not ignoring it. 97 This, however, complicates the proof of correctness for the compiler proper, and we must prove that both the meaning and concrete complexity characteristics of the program are preserved for every translation pass in the compiler, including the assembler. 98 99 How we went about resolving this problem affected the shape of our proof of correctness for the whole assembler in a rather profound way. 100 We first attempted to synthesise a solution bottom up: starting with no solution, we gradually refine a solution using the same functions that implement the jump expansion process. 101 Using this technique, solutions can fail to exist, and the proof of correctness for the assembler quickly descends into a diabolical quagmire. 102 103 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. 104 Assuming the existence of a correct policy, we prove the implementation of the assembler correct. 105 Further, we proved that the assembler fails to assemble an assembly program if and only if a correct policy does not exist. 106 This is achieved by means of dependent types: the assembly function is total over a program, a policy and the proof that the policy is correct for that program. 107 108 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, even after shrinking jumps according to the policy. 109 The first circumstance is an example of a serious compiler error, as an illformed assembly program was generated, and does not (and should not) count as a mark against the completeness of the assembler. 103 At the assembler level, this is reflected by our need to induce a cost 104 model on the assembly code as a function of the assembly program and the 105 strategy used to solve the branch displacement problem. In particular, the 106 optimizing compiler should also return a map that assigns a cost (in clock 107 cycles) to every instruction in the source program. We expect the induced cost 108 to be preserved by the compiler: we will prove that the compiled code 109 tightly simulates the source code by taking exactly the predicted amount of 110 time. 111 112 Note that the temporal tightness of the simulation is a fundamental prerequisite 113 of the correctness of the simulation because some functions of the MCS51, 114 notably timers and I/O, depend on the microprocessor's clock. If the 115 pseudo and concrete clock differs, the result of an I/O operation may not be 116 preserved. 117 118 Branch displacement algorithms must have a deep knowledge of the way 119 the rest of the assembler works in order to build globally correct solutions. 120 Proving their correctness is quite a complex task (see, for instance, 121 the compaion paper~\cite{boender:correctness:2012}). 122 Nevertheless, the correctness of the whole assembler only depends on the 123 correctness of the branch displacement algorithm. 124 Therefore, in the rest of the paper, we abstract the assembler on the 125 existence of a correct policy, to be computed by a branch displacement 126 algorithm if it exists. A policy is the decision over how 127 any particular jump should be expanded; it is correct when the global 128 constraints are satisfied. 129 The assembler fails to assemble an assembly program if and only if a correct policy does not exist. This is stated in an elegant way in the dependent type of the assembler: the assembly function is total over a program, a policy and the proof that the policy is correct for that program. 110 130 111 131 The rest of this paper is a detailed description of our proof that is, in part, still a work in progress.
Note: See TracChangeset
for help on using the changeset viewer.