Changeset 1026 for src/ASM/CPP2011
- Timestamp:
- Jun 21, 2011, 12:47:27 PM (10 years ago)
- Location:
- src/ASM/CPP2011
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/CPP2011/cpp-2011.bib
r1020 r1026 3 3 author = {Andrea Asperti and Claudio {Sacerdoti Coen} and Enrico Tassi and Stefano Zacchiroli}, 4 4 title = {User interaction with the {Matita} proof assistant}, 5 journal = { Journal ofAutomated Reasoning},5 journal = {Automated Reasoning}, 6 6 pages = {109--139}, 7 7 volume = {39}, … … 25 25 author = {Gerwin Klein and Tobias Nipkow}, 26 26 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}}, 28 28 volume = {28}, 29 29 number = {4}, … … 36 36 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}, 37 37 title = {{seL4}: Formal verification of an operating system kernel}, 38 journal = { Communications of the {ACM}},38 journal = {{CACM}}, 39 39 issue = {6}, 40 40 volume = {53}, … … 47 47 author = {Xavier Leroy}, 48 48 title = {Formal verification of a realistic compiler}, 49 journal = { Communications of the {Association of Computing Machinery}},49 journal = {{CACM}}, 50 50 volume = {52}, 51 51 number = {7}, … … 58 58 author = {Xavier Leroy}, 59 59 title = {A formally verified compiler back-end}, 60 journal = { Journal ofAutomated Reasoning},60 journal = {Automated Reasoning}, 61 61 volume = {43}, 62 62 number = {4}, … … 80 80 author = {Robert Atkey}, 81 81 title = {{CoqJVM}: An executable specification of the {Java Virtual Machine} using dependent types}, 82 booktitle = { Conference of the {TYPES} Project},82 booktitle = {{TYPES}}, 83 83 pages = {18--32}, 84 84 year = {2007} … … 89 89 author = {Sandrine Blazy and Zaynah Dargaye and Xavier Leroy}, 90 90 title = {Formal Verification of a {C} Compiler Front-End}, 91 booktitle = { International Symposium on Formal Methods},91 booktitle = {{FM}}, 92 92 pages = {460--475}, 93 93 year = {2006} … … 98 98 author = {Anthony Fox and Magnus O. Myreen}, 99 99 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}}, 101 101 pages = {243--258}, 102 102 year = {2010} … … 107 107 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}, 108 108 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}}, 110 110 year = {2009} 111 111 } … … 115 115 author = {Dominic P. Mulligan and Claudio {Sacerdoti Coen}}, 116 116 title = {An executable formal semantics of the {MCS-51} microprocessor in {Matita}}, 117 booktitle = { Formal Methods in Computer Aided Design},117 booktitle = {{FMCAD}}, 118 118 year = {2011}, 119 119 note = {Submitted} … … 124 124 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}, 125 125 title = {The semantics of {x86-CC} multiprocessor machine code}, 126 booktitle = { $\mathrm{36^{th}}$ Annual Symposium on Principles of Programming Languages},126 booktitle = {{POPL}}, 127 127 pages = {379--391}, 128 128 year = {2009} … … 133 133 author = {Matthieu Sozeau}, 134 134 title = {Subset Coercions in {Coq}}, 135 booktitle = { Types for Proofs and Programs},135 booktitle = {{TYPES}}, 136 136 pages = {237--252}, 137 137 year = {2006} … … 142 142 author = {Jun Yan and Wei Zhang}, 143 143 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}}, 145 145 pages = {80--89}, 146 146 year = {2008} … … 218 218 219 219 } 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 69 69 This 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. 70 70 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.}71 The MCS-51 dates from the early 1980s and is commonly called the 8051/8052. 72 72 Despite the microprocessor's age, derivatives are still widely manufactured by a number of semiconductor foundries. 73 73 As a result the processor is widely used, especially in embedded systems development, where well-tested, cheap, predictable microprocessors find their niche. … … 80 80 81 81 This 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.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{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. 83 83 84 84 As 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. … … 118 118 119 119 Second, 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}.120 However, 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}. 121 121 That 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. 122 122 However 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. … … 128 128 This 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. 129 129 In 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. 130 This, however, complicates the proof of correctness for the compiler proper. 131 In 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. 131 132 This also applies for the translation from assembly language to machine code. 132 133 … … 145 146 \end{array} 146 147 \end{displaymath}}} 147 In the translation, if \texttt{JZ} fails, we fall through to the \texttt{SJMP} which jumps over the \texttt{LJMP}.148 Here, if \texttt{JZ} fails, we fall through to the \texttt{SJMP} which jumps over the \texttt{LJMP}. 148 149 Naturally, 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.150 We address the calculation of whether a label is indeed `close enough' for the simpler translation to be used below. 150 151 151 152 Crucially, the above translation demonstrates the difficulty in predicting how many clock cycles a pseudoinstruction will take to execute. … … 237 238 We merely describe enough here to understand the rest of the proof. 238 239 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 functionregisters, and so on.240 The emulator centres around a \texttt{Status} record, describing the microprocessor's state. 241 This record contains fields corresponding to the microprocessor's program counter, registers, and so on. 241 242 At the machine code level, code memory is implemented as a compact trie of bytes, addressed by the program counter. 242 243 Machine code programs are loaded into \texttt{Status} using the \texttt{load\_code\_memory} function. … … 264 265 If 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. 265 266 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.267 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 execution time. 267 268 This timing information is used inside \texttt{execute\_1\_pseudo\_instruction} to update the clock of the \texttt{PseudoStatus}. 268 269 During 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.