Changeset 1026


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

final version? under 16 pages

Location:
src/ASM/CPP2011
Files:
2 edited

Legend:

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

    r1020 r1026  
    33  author = {Andrea Asperti and Claudio {Sacerdoti Coen} and Enrico Tassi and Stefano Zacchiroli},
    44  title = {User interaction with the {Matita} proof assistant},
    5   journal = {Journal of Automated Reasoning},
     5  journal = {Automated Reasoning},
    66  pages = {109--139},
    77  volume = {39},
     
    2525  author = {Gerwin Klein and Tobias Nipkow},
    2626  title = {A machine-checked model for a {Java-like} language, virtual machine and compiler},
    27   journal = {Transactions on Programming Languages and Systems},
     27  journal = {{TOPLAS}},
    2828  volume = {28},
    2929  number = {4},
     
    3636  author = {Gerwin Klein and June Andronick and Kevin Elphinstone and Gernot Heiser and David Cock and Philip Derrin and Dhammika Elkaduwe and Kai Engelhardt and Rafal Kolanski and Michael Norrish and Thomas Sewell, Harvey Tuch and Simon Winwood},
    3737  title = {{seL4}: Formal verification of an operating system kernel},
    38   journal = {Communications of the {ACM}},
     38  journal = {{CACM}},
    3939  issue = {6},
    4040  volume = {53},
     
    4747  author = {Xavier Leroy},
    4848  title = {Formal verification of a realistic compiler},
    49   journal = {Communications of the {Association of Computing Machinery}},
     49  journal = {{CACM}},
    5050  volume = {52},
    5151  number = {7},
     
    5858  author = {Xavier Leroy},
    5959  title = {A formally verified compiler back-end},
    60   journal = {Journal of Automated Reasoning},
     60  journal = {Automated Reasoning},
    6161  volume = {43},
    6262  number = {4},
     
    8080  author = {Robert Atkey},
    8181  title = {{CoqJVM}: An executable specification of the {Java Virtual Machine} using dependent types},
    82   booktitle = {Conference of the {TYPES} Project},
     82  booktitle = {{TYPES}},
    8383  pages = {18--32},
    8484  year = {2007}
     
    8989  author = {Sandrine Blazy and Zaynah Dargaye and Xavier Leroy},
    9090  title = {Formal Verification of a {C} Compiler Front-End},
    91   booktitle = {International Symposium on Formal Methods},
     91  booktitle = {{FM}},
    9292  pages = {460--475},
    9393  year = {2006}
     
    9898  author = {Anthony Fox and Magnus O. Myreen},
    9999  title = {A Trustworthy Monadic Formalization of the {ARMv7} Instruction Set Architecture},
    100   booktitle = {$\mathrm{1^{st}}$ International Conference on Interactive Theorem Proving},
     100  booktitle = {{ITP}},
    101101  pages = {243--258},
    102102  year = {2010}
     
    107107  author = {Gerwin Klein and June Andronick and Kevin Elphinstone and Gernot Heiser and David Cock and Philip Derrin and Dhammika Elkaduwe and Kai Engelhardt and Rafal Kolanski and Michael Norrish and Thomas Sewell, Harvey Tuch and Simon Winwood},
    108108  title = {{seL4}: Formal verification of an operating system kernel},
    109   booktitle = {Proceedings of the $22^\mathrm{nd}$ {ACM} Symposium on Operating Systems Principles},
     109  booktitle = {{SOSP}},
    110110  year = {2009}
    111111}
     
    115115  author = {Dominic P. Mulligan and Claudio {Sacerdoti Coen}},
    116116  title = {An executable formal semantics of the {MCS-51} microprocessor in {Matita}},
    117   booktitle = {Formal Methods in Computer Aided Design},
     117  booktitle = {{FMCAD}},
    118118  year = {2011},
    119119  note = {Submitted}
     
    124124  author = {Susmit Sarkar and Peter Sewell and Francesco Zappa Nardelli and Scott Owens and Tom Ridge and Thomas Braibant and Magnus O. Myreen and Jade Alglave},
    125125  title = {The semantics of {x86-CC} multiprocessor machine code},
    126   booktitle = {$\mathrm{36^{th}}$ Annual Symposium on Principles of Programming Languages},
     126  booktitle = {{POPL}},
    127127  pages = {379--391},
    128128  year = {2009}
     
    133133  author = {Matthieu Sozeau},
    134134  title = {Subset Coercions in {Coq}},
    135   booktitle = {Types for Proofs and Programs},
     135  booktitle = {{TYPES}},
    136136  pages = {237--252},
    137137  year = {2006}
     
    142142  author = {Jun Yan and Wei Zhang},
    143143  title = {{WCET} Analysis for Multi-Core Processors with Shared {L2} Instruction Caches},
    144   booktitle = {$\mathrm{14^{th}}$ {IEEE} Symposium on Real-time and Embedded Technology and Applications},
     144  booktitle = {{RTAS}},
    145145  pages = {80--89},
    146146  year = {2008}
     
    218218
    219219}
    220 
    221 @inproceedings{russell,
    222   author    = {Matthieu Sozeau},
    223   title     = {Subset Coercions in {C}oq},
    224   booktitle = {Types for Proofs and Programs},
    225   series    = {LNCS},
    226   year      = {2006},
    227   pages     = {237-252},
    228   VOLUME = {4502/2007},
    229   PUBLISHER = {Springer-Verlag},
    230   doi = {10.1007/978-3-540-74464-1\_16},
    231 }
  • 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.