# Changeset 2358 for Papers

Ignore:
Timestamp:
Sep 27, 2012, 3:16:34 PM (9 years ago)
Message:

Down to 17 pages now.

File:
1 edited

### Legend:

Unmodified
 r2357 \begin{abstract} We present a proof of correctness, in Matita, for an optimising assembler for the MCS-51 microcontroller. This assembler constitutes a major component of the EU's CerCo project. The efficient expansion of pseudoinstructions---namely jumps---into MCS-51 machine instructions is complex. 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. To free CerCo's 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. 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 all feature in our assembly language. We simplify the proof by assuming that all our assembly programs are pre-linked (i.e. we do not formalise a linker---this is left for future work). Matita is a proof assistant based on a variant of the Calculus of (Co)inductive Constructions~\cite{asperti:user:2007}. In particular, it features dependent types that we exploit in the formalisation. The syntax of the statements and definitions in the paper should be self-explanatory, at least to those exposed to dependent type theory. It features dependent types that we exploit in the formalisation. The (simplified) syntax of the statements and definitions in the paper should be self-explanatory. Pairs are denoted with angular brackets, $\langle-, -\rangle$. instr = i $\wedge$ ticks = (ticks_of_instruction instr) $\wedge$ pc' = pc_plus_len. \end{lstlisting} In particular, we read \texttt{fetch\_assembly} as follows. We read \texttt{fetch\_assembly} as follows. Given an instruction, \texttt{i}, we first assemble the instruction to obtain \texttt{assembled}, checking that the assembled instruction was stored in code memory correctly. Fetching from code memory, we obtain a tuple consisting of the instruction, new program counter, and the number of ticks this instruction will take to execute. The fetched sequence corresponds to the expansion, according to the policy, of the pseudoinstruction. At first, the lemma appears to immediately imply the correctness of the assembler. However, this property is \emph{not} strong enough to establish that the semantics of an assembly program has been preserved by the assembly process since it does not establish the correspondence between the semantics of a pseudoinstruction and that of its expansion. At first, the lemma appears to immediately imply the correctness of the assembler, but this property is \emph{not} strong enough to establish that the semantics of an assembly program has been preserved by the assembly process since it does not establish the correspondence between the semantics of a pseudoinstruction and that of its expansion. In particular, the two semantics differ on instructions that \emph{could} directly manipulate program addresses. This approach, of using real addresses coupled with a weak, dynamic typing system sitting atop of memory, is similar to one taken by Tuch \emph{et al}~\cite{tuch:types:2007}, for reasoning about low-level C code. Our analogue of the semantic function above is then merely a wrapper around the function that implements the semantics of machine code, paired with a function that keeps track of addresses. This permits a large amount of code reuse, as the semantics of pseudo- and machine code are essentially shared. Our analogue of the semantic function above is merely a wrapper around the function that implements the semantics of machine code, paired with a function that keeps track of addresses. The semantics of pseudo- and machine code are then essentially shared. The only thing that changes at the assembly level is the presence of the new tracking function. \end{lstlisting} The statement is standard for forward simulation, but restricted to \texttt{PseudoStatuses} \texttt{ps} whose next instruction to be executed is well-behaved with respect to the \texttt{internal\_pseudo\_address\_map} \texttt{M}. Further, we explicitly require proof that our policy is correct, our program is well-labelled (i.e. no repeated labels, and so on) and the pseudo-program counter lies within the bounds of the program. Theorem \texttt{main\_thm} establishes the correctness of the assembly process and can simply be lifted to the forward simulation of an arbitrary number of well-behaved steps on the assembly program. We explicitly require proof that the policy is correct, the program is well-labelled (i.e. no repeated labels, etc.) and the pseudo-program counter is in the program's bounds. Theorem \texttt{main\_thm} establishes the correctness of the assembly process and can be lifted to the forward simulation of an arbitrary number of well-behaved steps on the assembly program. % ---------------------------------------------------------------------------- % We are proving the correctness of an assembler for MCS-51 assembly language. In particular, our assembly language features labels, arbitrary conditional and unconditional jumps to labels, global data and instructions for moving this data into the MCS-51's single 16-bit register. Our assembly language features labels, arbitrary conditional and unconditional jumps to labels, global data and instructions for moving this data into the MCS-51's single 16-bit register. Expanding these pseudoinstructions into machine code instructions is not trivial, and the proof that the assembly process is correct', in that the semantics of a subset of assembly programs are not changed is complex. The formalisation is a key component of the CerCo project, which aims to produce a verified concrete complexity preserving compiler for a large subset of the C programming language. The verified assembler, complete with the underlying formalisation of the semantics of MCS-51 machine code, will form the bedrock layer upon which the rest of the CerCo project will build its verified compiler platform. The formalisation is a component of CerCo which aims to produce a verified concrete complexity preserving compiler for a large subset of the C language. The verified assembler, complete with the underlying formalisation of the semantics of MCS-51 machine code, will form the bedrock layer upon which the rest of CerCo will build its verified compiler platform. It is interesting to compare our work to an industrial grade' assembler for the MCS-51: SDCC~\cite{sdcc:2011}. 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 constrain the size of bitvectors and tries that represent memory quantities and memory areas respectively. Dependent types are used to constrain the size of bitvectors and tries that represent memory quantities and memory areas respectively. They are also used to simulate polymorphic variants in Matita, in order to provide precise typings to various functions expecting only a subset of all possible addressing modes that the MCS-51 offers. 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. 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} \label{subsect.related.work} \paragraph{Related work} % piton We are not the first to consider the correctness of an assembler for a non-trivial assembly language. 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}. The most impressive piece of work in this domain is Piton~\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 This is only possible by inducing a cost model on the source code from the optimisation strategy and input program. This will be a \emph{leit motif} of CerCo. \subsection{Resources} \label{subsect.resources} All files relating to our formalisation effort can be found online at~\url{http://cerco.cs.unibo.it}. In particular, we have assumed several properties of library functions' related in particular to modular arithmetic and datastructure manipulation. Moreover, we have axiomatised various ancillary functions needed to complete the main theorems, as well as some routine' proof obligations of the theorems themselves, preferring instead to focus on the main meat of the theorems. We thus believe that the proof strategy is sound and that we will be able to close soon all axioms, up to possible minor bugs that should have local fixes that do not affect the global proof strategy. The development, including the definition of the executable semantics of the MCS-51, is spread across 29 files, totalling around 18,500 lines of Matita source. The bulk of the proof described herein is contained in a series of files, \texttt{AssemblyProof.ma}, \texttt{AssemblyProofSplit.ma} and \texttt{AssemblyProofSplitSplit.ma} consisting at the moment of approximately 4200 lines of Matita source. \paragraph{Resources} Our source files are available at~\url{http://cerco.cs.unibo.it}. We assumed several properties of library functions', e.g. modular arithmetic and datastructure manipulation. We axiomatised various small functions needed to complete the main theorems, as well as some routine' proof obligations of the theorems themselves, in focussing on the main meat of the theorems. We believe that the proof strategy is sound and that we will be able to close all axioms, up to minor bugs that should have local fixes that do not affect the global proof strategy. The development, including the definition of the executable semantics of the MCS-51, is spread across 29 files, with around 18,500 lines of Matita source. The bulk of the proof is contained in a series of files, \texttt{AssemblyProof.ma}, \texttt{AssemblyProofSplit.ma} and \texttt{AssemblyProofSplitSplit.ma} consisting of approximately 4500 lines of Matita source. Numerous other lines of proofs are spread all over the development because of dependent types and the Russell proof style, which does not allow one to separate the code from the proofs. The low ratio between the number of lines of code and the number of lines of proof is unusual. It is justified by the fact that the pseudo-assembly and the assembly language share most constructs and that large parts of the semantics are also shared. Therefore many lines of code are required to describe the complex semantics of the processor, but, for the shared cases, the proof of preservation of the semantics is essentially trivial. The low ratio between source lines and the number of lines of proof is unusual, but justified by the fact that the pseudo-assembly and the assembly language share most constructs and large swathes of the semantics are shared. Many lines of code are required to describe the complex semantics of the processor, but for the shared cases the proof of preservation of the semantics is essentially trivial. \bibliography{cpp-2012-asm.bib}