# Changeset 1033 for src/ASM/CPP2011/cpp-2011.tex

Ignore:
Timestamp:
Jun 21, 2011, 3:08:25 PM (9 years ago)
Message:

ispelled & submitted

File:
1 edited

### Legend:

Unmodified
 r1032 \begin{abstract} We consider the formalisation of an assembler for Intel MCS-51 assembly language in the Matita proof assistant. This formalisation forms a major component of the EU-funded CerCo project, concering the construction and formalisation of a concrete complexity preserving compiler for a large subset of the C programming language. This formalisation forms a major component of the EU-funded CerCo project, concerning the construction and formalisation of a concrete complexity preserving compiler for a large subset of the C programming language. The efficient expansion of pseudoinstructions---particularly jumps---into MCS-51 machine instructions is complex. We consider the formalisation of an assembler for the Intel MCS-51 8-bit microprocessor in the Matita proof assistant~\cite{asperti:user:2007}. 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. This formalisation forms a major component of the EU-funded CerCo project~\cite{cerco:2011}, concerning the construction and formalisation of a concrete complexity preserving compiler for a large subset of the C programming language. The MCS-51 dates from the early 1980s and is commonly called the 8051/8052. For the MCS-51, if a manufacturer states that a particular opcode takes three clock cycles to execute, then that opcode \emph{always} takes three clock cycles to execute. This predicability of timing information is especially attractive to the CerCo consortium. This predictability of timing information is especially attractive to the CerCo consortium. 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. Consequently, the size of each opcode is different, and to squeeze as much code as possible into the MCS-51's limited code memory, the smallest possible opcode that will suffice should be selected. The prototype CerCo C compiler does not attempt to select the smallest jump opcode in this manner, as this was thought to unneccessarily complicate the compilation chain, making the eventual translation and formalisation of the compiler into Matita much harder. The prototype CerCo C compiler does not attempt to select the smallest jump opcode in this manner, as this was thought to unnecessarily complicate the compilation chain, making the eventual translation and formalisation of the compiler into Matita much harder. Instead, the compiler targets a bespoke assembly language, similar to `real world' assembly languages, complete with pseudoinstructions including \texttt{Jmp} and \texttt{Call} instructions. Labels, conditional jumps to labels, a program preamble containing global data and a \texttt{MOV} instruction for moving this global data into the MCS-51's one 16-bit register also feature. Depending on the particular MCS-51 derivative at hand, an \texttt{SJMP} could in theory take a different number of clock cycles to execute than an \texttt{LJMP}. These issues must also be dealt with in order to prove that the translation pass preserves the concrete complexity of assembly code, and that the semantics of a program using the MCS-51's I/O facilities does not change. We address this problem by parameterizing the semantics over a cost model. We address this problem by parameterising the semantics over a cost model. We prove the preservation of concrete complexity only for the program-dependent cost model induced by the optimisation. We observe that $100_{16} = 256_{10}$, and lies \emph{just} outside the range expressible in an 8-bit byte (0--255). As our example shows, given an occurence $l$ of an \texttt{LJMP} instruction, it may be possible to shrink $l$ to an occurence of an \texttt{SJMP}---consuming fewer bytes of code memory---provided we can shrink any \texttt{LJMP}s that exist between $l$ and its target location. As our example shows, given an occurrence $l$ of an \texttt{LJMP} instruction, it may be possible to shrink $l$ to an occurrence of an \texttt{SJMP}---consuming fewer bytes of code memory---provided we can shrink any \texttt{LJMP}s that exist between $l$ and its target location. In particular, if we wish to shrink the \texttt{LJMP} occurring at line 1, then we must shrink the \texttt{LJMP} occurring at line 3. However, to shrink the \texttt{LJMP} occurring at line 3 we must also shrink the \texttt{LJMP} occurring at line 5, and \emph{vice versa}. How we went about resolving this problem affected the shape of our proof of correctness for the whole assembler in a rather profound way. We first attempted to synthesize a solution bottom up: starting with no solution, we gradually refine a solution using the same functions that implement the jump expansion process. We first attempted to synthesise a solution bottom up: starting with no solution, we gradually refine a solution using the same functions that implement the jump expansion process. Using this technique, solutions can fail to exist, and the proof of correctness for the assembler quickly descends into a diabolical quagmire. Then, we check with \texttt{fetch\_many} that the number of machine instructions that were fetched matches the number of instruction that \texttt{expand\_pseudo\_instruction} expanded. The final lemma in this series is \texttt{fetch\_assembly\_pseudo2} that combines the Lemma \texttt{fetch\_aasembly\_pseudo} with the correctness of the functions that load object code into the processor's memory. The final lemma in this series is \texttt{fetch\_assembly\_pseudo2} that combines the Lemma \texttt{fetch\_assembly\_pseudo} with the correctness of the functions that load object code into the processor's memory. \begin{lstlisting} lemma fetch_assembly_pseudo2: However, this comes at the expense of assembler completeness: the generated program may be too large to fit into code memory. In this respect, there is a trade-off between the completeness of the assembler and the efficiency of the assembled program. The definition and proof of a complete, optimal (in the sense that object code size is minimized) and correct jump expansion policy is ongoing work. The definition and proof of a complete, optimal (in the sense that object code size is minimised) and correct jump expansion policy is ongoing work. Aside from their application in verified compiler projects such as CerCo and CompCert, verified assemblers such as ours could also be applied to the verification of operating system kernels. If CompCert chooses to assume the existence of an optimising assembler, then care should be made to ensure that any assembly program produced by the CompCert compiler falls into the subset of programs that have a hope of having their semantics preserved by an optimising assembler. Our formalization exploits dependent types in different ways and for multiple purposes. The first purpose is to reduce potential errors in the formalization Our formalisation exploits dependent types in different ways and for multiple purposes. The first purpose is to reduce potential errors in the formalisation of the microprocessor. In particular, dependent types are used to constraint the size of bit-vectors and proof has been done 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 innatural to see the proof that 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.