Ignore:
Timestamp:
Jun 21, 2011, 12:47:27 PM (9 years ago)
Author:
mulligan
Message:

final version? under 16 pages

File:
1 edited

Legend:

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

    r1025 r1026  
    6969This formalisation forms a major component of the EU-funded CerCo project~\cite{cerco:2011}, concering the construction and formalisation of a concrete complexity preserving compiler for a large subset of the C programming language.
    7070
    71 The MCS-51 dates from the early 1980s and is commonly called the 8051/8052.\footnote{Being strict, the 8051 and 8052 are two different microprocessors, though the features that the 8052 added over the 8051 are minor, and largely irrelevant for our formalisation project.}
     71The MCS-51 dates from the early 1980s and is commonly called the 8051/8052.
    7272Despite the microprocessor's age, derivatives are still widely manufactured by a number of semiconductor foundries.
    7373As a result the processor is widely used, especially in embedded systems development, where well-tested, cheap, predictable microprocessors find their niche.
     
    8080
    8181This predicability of timing information is especially attractive to the CerCo consortium.
    82 We are in the process of constructing a certified, concrete complexity compiler for a realistic processor, and not for building and formalising the worst case execution time tools (WCET---see~\cite{yan:wcet:2008} and~\cite{bate:wcet:2011}, amongst many others, for an application of WCET technology to microprocessors with more complex designs) that would be necessary to achieve the same result with, for example, a modern ARM or PowerPC microprocessor.
     82We are in the process of constructing a certified, concrete complexity compiler for a realistic processor, and not for building and formalising the worst case execution time tools (WCET---see~\cite{bate:wcet:2011}, amongst many others, for an application of WCET technology to microprocessors with more complex designs) that would be necessary to achieve the same result with, for example, a modern ARM or PowerPC microprocessor.
    8383
    8484As in most things, what one hand giveth, the other taketh away: the MCS-51's paucity of features, though an advantage in many respects, also quickly become a hindrance, and successfully compiling high-level code for this architecture is a cumbrous and involved process.
     
    118118
    119119Second, as mentioned, the CerCo consortium is in the business of constructing a verified compiler for the C programming language.
    120 However, unlike CompCert~\cite{compcert:2011,leroy:formal:2009,leroy:formally:2009}---which currently represents the state of the art for `industrial grade' verified compilers---CerCo considers not just the \emph{extensional correctness} of the compiler, but also its \emph{intensional correctness}.
     120However, unlike CompCert~\cite{compcert:2011,leroy:formal:2009}---which currently represents the state of the art for `industrial grade' verified compilers---CerCo considers not just the \emph{extensional correctness} of the compiler, but also its \emph{intensional correctness}.
    121121That is, CompCert focusses solely on the preservation of the \emph{meaning} of a program during the compilation process, guaranteeing that the program's meaning does not change as it is gradually transformed into assembly code.
    122122However in any realistic compiler (even the CompCert compiler!) there is no guarantee that the program's time properties are preserved during the compilation process; a compiler's `optimisations' could, in theory, even conspire to degrade the concrete complexity of certain classes of programs.
     
    128128This 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.
    129129In short, we aim to obtain a very precise costing for a program by embracing the compilation process, not ignoring it.
    130 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 concrete complexity characteristics.
     130This, however, complicates the proof of correctness for the compiler proper.
     131In each translation pass from intermediate language to intermediate language, we must prove that both the meaning and concrete complexity characteristics of the program are preserved.
    131132This also applies for the translation from assembly language to machine code.
    132133
     
    145146\end{array}
    146147\end{displaymath}}}
    147 In the translation, if \texttt{JZ} fails, we fall through to the \texttt{SJMP} which jumps over the \texttt{LJMP}.
     148Here, if \texttt{JZ} fails, we fall through to the \texttt{SJMP} which jumps over the \texttt{LJMP}.
    148149Naturally, if \texttt{label} is close enough, a conditional jump pseudoinstruction is mapped directly to a conditional jump machine instruction; the above translation only applies if \texttt{label} is not sufficiently local.
    149 This leaves the problem, addressed below, of calculating whether a label is indeed `close enough' for the simpler translation to be used.
     150We address the calculation of whether a label is indeed `close enough' for the simpler translation to be used below.
    150151
    151152Crucially, the above translation demonstrates the difficulty in predicting how many clock cycles a pseudoinstruction will take to execute.
     
    237238We merely describe enough here to understand the rest of the proof.
    238239
    239 The MCS-51 emulator centres around a \texttt{Status} record, describing the current state of the microprocessor.
    240 This record contains fields corresponding to the microprocessor's program counter, special function registers, and so on.
     240The emulator centres around a \texttt{Status} record, describing the microprocessor's state.
     241This record contains fields corresponding to the microprocessor's program counter, registers, and so on.
    241242At the machine code level, code memory is implemented as a compact trie of bytes, addressed by the program counter.
    242243Machine code programs are loaded into \texttt{Status} using the \texttt{load\_code\_memory} function.
     
    264265If we change how we expand conditional jumps to labels, for instance, then the costing needs to change, hence \texttt{execute\_1\_pseudo\_instruction}'s parametricity in the costing.
    265266
    266 The costing returns \emph{pairs} of natural numbers because, in the case of expanding conditional jumps to labels, the expansion of the `true branch' and `false branch' may differ in the number of clock ticks needed for execution.
     267The costing returns \emph{pairs} of natural numbers because, in the case of expanding conditional jumps to labels, the expansion of the `true branch' and `false branch' may differ in execution time.
    267268This timing information is used inside \texttt{execute\_1\_pseudo\_instruction} to update the clock of the \texttt{PseudoStatus}.
    268269During the proof of correctness of the assembler we relate the clocks of \texttt{Status}es and \texttt{PseudoStatus}es for the policy induced by the cost model and optimisations.
Note: See TracChangeset for help on using the changeset viewer.