 Timestamp:
 Sep 27, 2012, 2:46:30 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Papers/cppasm2012/cpp2012asm.tex
r2356 r2357 90 90 compiler (assembler) is to individually expand every pseudoinstruction in such a way 91 91 that all global constraints are satisfied and that the compiled program size 92 is minimal in size and faster in time. The problem is known to be particularly93 complex for most CICS architectures (for instance,see~\cite{hyde:branch:2006}).92 is minimal in size and faster in time. 93 This problem is known to be complex for most CISC architectures (see~\cite{hyde:branch:2006}). 94 94 95 95 To 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. … … 111 111 112 112 Note that the temporal tightness of the simulation is a fundamental prerequisite 113 of the correctness of the simulation because some functions of the MCS51 notablytimers and I/Odepend on the microprocessor's clock.113 of the correctness of the simulation because some functions of the MCS51timers and I/Odepend on the microprocessor's clock. 114 114 If the pseudo and concrete clock differ the result of an I/O operation may not be preserved. 115 115 … … 146 146 with benefits on the size of the formalisation. 147 147 148 The rest of this paper is a detailed description of our proof that is, in minimal part, still a work in progress. 149 150 We provide the reader with a brief `roadmap' for the rest of the paper. 148 The rest of this paper is a detailed description of our proof that is marginally still a work in progress. 151 149 In Section~\ref{sect.matita} we provide a brief overview of the Matita proof assistant for the unfamiliar reader. 152 150 In Section~\ref{sect.the.proof} we discuss the design and implementation of the proof proper. … … 668 666 Polymorphic variants nicely capture the absolutely unorthogonal instruction set of the MCS51 where every opcode must accept its own subset of the 11 addressing mode of the processor. 669 667 670 The second purpose is to single out thesources of incompleteness.668 The second purpose is to single out sources of incompleteness. 671 669 By abstracting our functions over the dependent type of correct policies, we were able to manifest the fact that the compiler never refuses to compile a program where a correct policy exists. 672 670 This also allowed to simplify the initial proof by dropping lemmas establishing that one function fails if and only if some previous function does so. 673 671 674 Finally, dependent types, together with Matita's liberal system of coercions, allow us to simulate almost entirely in user spacethe proof methodology `Russell' of Sozeau~\cite{sozeau:subset:2006}.675 However, not every proof has been carried out in this way: we only used this style to prove that a function satisfies a specification that only involves that function in a significant way.676 For example, it would be unnatural to see the proof that fetch and assembly commute as the specification of one of the two functions.672 Finally, dependent types, together with Matita's liberal system of coercions, allow us to simulate almost entirely in user space the proof methodology `Russell' of Sozeau~\cite{sozeau:subset:2006}. 673 Not every proof has been carried out in this way: we only used this style to prove that a function satisfies a specification that only involves that function in a significant way. 674 It would not be natural to see the proof that fetch and assembly commute as the specification of one of the two functions. 677 675 678 676 \subsection{Related work} … … 681 679 % piton 682 680 We are not the first to consider the correctness of an assembler for a nontrivial assembly language. 683 Perhaps the most impressive piece of work in this domain is the Piton stack~\cite{moore:piton:1996}. 684 This was a stack of verified components, written and verified in ACL2, ranging from a proprietary FM9001 microprocessor verified at the gate level, to assemblers and compilers for two highlevel languagesa dialect of Lisp and $\mu$Gypsy~\cite{moore:grand:2005}. 681 The most impressive piece of work in this domain is the Piton stack~\cite{moore:piton:1996}, a stack of verified components, written and verified in ACL2, ranging from a proprietary FM9001 microprocessor verified at the gate level, to assemblers and compilers for two highlevel languagesLisp and $\mu$Gypsy~\cite{moore:grand:2005}. 685 682 686 683 % jinja
Note: See TracChangeset
for help on using the changeset viewer.