Changeset 2340


Ignore:
Timestamp:
Sep 26, 2012, 1:53:30 PM (7 years ago)
Author:
sacerdot
Message:

Introduction rewritten.

File:
1 edited

Legend:

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

    r2339 r2340  
    7878As 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.
    7979
    80 In order to do this, we must solve the `branch displacement' problem---deciding 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 MCS-51'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 well-known problem for those writing assemblers targetting CISC architectures (for instance, see~\cite{hyde:branch:2006}).
     80In order to do this, we must solve the `branch displacement' problem---deciding how best to expand pseudojumps to labels in assembly language to machine code jumps. The branch displacement problem happears when pseudojumps can be expanded
     81in different ways to real machine instructions, but the different expansions
     82are not equivalent (e.g. do not have the same size or speed) and not always
     83correct (e.g. correctness is only up to global constraints over the compiled
     84code). For instance, some jump instructions (short jumps) are very small
     85and fast, but they can only reach destinations within a
     86certain distance from the current instruction. When the destinations are
     87too far away, larger and slower long jumps must be used. The use of a long jump may
     88augment the distance between another pseudojump and its target, forcing
     89another long jump use, in a cascading effect. The job of the optimizing
     90compiler (assembler) is to individually expand every pseudo-instruction in such a way
     91that all global constraints are satisfied and that the compiled program size
     92is minimal in size and faster in time. The problem is known to be particularly
     93complex for most CICS architectures (for instance, see~\cite{hyde:branch:2006}).
    8394
    8495To 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.
     
    8697We simplify the proof by assuming that all our assembly programs are pre-linked (i.e. we do not formalise a linker---this is left for future work).
    8798
    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 MCS-51, 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.
     99Another complication we have addressed is that of the cost model.
     100CerCo imposes a cost model on C programs or, more specifically, on simple blocks of instructions.
    95101This 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.
    96102In 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 expanded---from 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 ill-formed assembly program was generated, and does not (and should not) count as a mark against the completeness of the assembler.
     103At the assembler level, this is reflected by our need to induce a cost
     104model on the assembly code as a function of the assembly program and the
     105strategy used to solve the branch displacement problem. In particular, the
     106optimizing compiler should also return a map that assigns a cost (in clock
     107cycles) to every instruction in the source program. We expect the induced cost
     108to be preserved by the compiler: we will prove that the compiled code
     109tightly simulates the source code by taking exactly the predicted amount of
     110time.
     111
     112Note that the temporal tightness of the simulation is a fundamental prerequisite
     113of the correctness of the simulation because some functions of the MCS-51,
     114notably timers and I/O, depend on the microprocessor's clock. If the
     115pseudo and concrete clock differs, the result of an I/O operation may not be
     116preserved.
     117
     118Branch displacement algorithms must have a deep knowledge of the way
     119the rest of the assembler works in order to build globally correct solutions.
     120Proving their correctness is quite a complex task (see, for instance,
     121the compaion paper~\cite{boender:correctness:2012}).
     122Nevertheless, the correctness of the whole assembler only depends on the
     123correctness of the branch displacement algorithm.
     124Therefore, in the rest of the paper, we abstract the assembler on the
     125existence of a correct policy, to be computed by a branch displacement
     126algorithm if it exists. A policy is the decision over how
     127any particular jump should be expanded; it is correct when the global
     128constraints are satisfied.
     129The 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.
    110130
    111131The 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.