Changeset 1005 for src/ASM/CPP2011


Ignore:
Timestamp:
Jun 20, 2011, 5:41:06 PM (8 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

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

    r1004 r1005  
    175175That is, the shrinking process is not just related to optimisation, but also the completeness of the assembler.
    176176
    177 Thinking more, it is easy to imagine knotty, circular configurations of jumps developing, each jump occurrence only being shrinkable if every other is.
    178 Finding a solution to this `shrinking jumps' problem then involves us finding a method to break any vicious circularities that develop.
    179 
    180177How we went about resolving this problem affected the shape of our proof of correctness for the whole assembler in a rather profound way.
    181178We 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.
     
    184181Abandoning 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.
    185182Assuming the existence of a correct policy, we proved the implementation of the assembler correct.
    186 Further, we proved that the assembler fails to assemble an assembly program if and only if a correct policy does not exist.
    187 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.
    188 The first case would constitute a serious compiler error, and hopefully certifying the rest of the compiler would rule this possibility out.
    189 The second case is unavoidable---certified compiler or not, trying to load a huge program into a small code memory will break \emph{something}.
     183Further, we proved that the assembler fails to assemble an assembly program if and only if a correct policy does not exist. This is achieved by means of dependent types: the assembly function is total over a program, a policy and the proof
     184that the policy is correct for the program.
     185
     186Policies 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
     187best policy. The first case is an example of compiler error because of
     188ill-formedness of the input. It does not count for the compiler completeness.
     189We plan to employ dependent types in CerCo to restrict the domain of the
     190compiler to those programs that are semantically correct and should be compiled.
     191In particular, in CerCo we are also interested in completeness of compilation
     192whereas previous formalizations only focused on correctness.
    190193
    191194The rest of this paper is a detailed description of this proof.
Note: See TracChangeset for help on using the changeset viewer.