# Changeset 2357 for Papers/cpp-asm-2012/cpp-2012-asm.tex

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

Begun editing down to reclaim space. Fixed some embarrassing typos (e.g. CICS for CISC).

File:
1 edited

### Legend:

Unmodified
 r2356 compiler (assembler) is to individually expand every pseudo-instruction in such a way that all global constraints are satisfied and that the compiled program size is minimal in size and faster in time. The problem is known to be particularly complex for most CICS architectures (for instance, see~\cite{hyde:branch:2006}). is minimal in size and faster in time. This problem is known to be complex for most CISC architectures (see~\cite{hyde:branch:2006}). 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. Note that the temporal tightness of the simulation is a fundamental prerequisite of the correctness of the simulation because some functions of the MCS-51---notably timers and I/O---depend on the microprocessor's clock. of the correctness of the simulation because some functions of the MCS-51---timers and I/O---depend on the microprocessor's clock. If the pseudo- and concrete clock differ the result of an I/O operation may not be preserved. with benefits on the size of the formalisation. The rest of this paper is a detailed description of our proof that is, in minimal part, still a work in progress. We provide the reader with a brief roadmap' for the rest of the paper. The rest of this paper is a detailed description of our proof that is marginally still a work in progress. In Section~\ref{sect.matita} we provide a brief overview of the Matita proof assistant for the unfamiliar reader. In Section~\ref{sect.the.proof} we discuss the design and implementation of the proof proper. Polymorphic variants nicely capture the absolutely unorthogonal instruction set of the MCS-51 where every opcode must accept its own subset of the 11 addressing mode of the processor. The second purpose is to single out the sources of incompleteness. The second purpose is to single out sources of incompleteness. 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. 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. 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}. 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. For example, it would be unnatural to see the proof that fetch and assembly commute as the specification of one of the two functions. 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}. 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. It would not be natural to see the proof that fetch and assembly commute as the specification of one of the two functions. \subsection{Related work} % piton We are not the first to consider the correctness of an assembler for a non-trivial assembly language. Perhaps the most impressive piece of work in this domain is the Piton stack~\cite{moore:piton:1996}. 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 high-level languages---a dialect of Lisp and $\mu$Gypsy~\cite{moore:grand:2005}. 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 high-level languages---Lisp and $\mu$Gypsy~\cite{moore:grand:2005}. % jinja