# Changeset 1203 for Deliverables

Ignore:
Timestamp:
Sep 10, 2011, 12:09:42 PM (8 years ago)
Message:

Location:
Deliverables/D4.1/ITP-Paper
Files:
2 edited

### Legend:

Unmodified
 r1202 Formal methods aim to increase our confidence in the design and implementation of software. Ideally, all software should come equipped with a formal specification and a proof of correctness for the corresponding implementation. The majority of programs are written in high level languages and then compiled into low level ones. Specifications are therefore also given at a high level and correctness can be proved by reasoning on the program's source code. Most programs are written in high level languages and then compiled into low level ones. Specifications are also given at a high level and correctness can be proved by reasoning on the program's source code. The code that is actually run is not the high level source code that we reason on, but low level code generated by the compiler. \paragraph*{Overview of paper}\quad In Section~\ref{sect.design.issues.formalisation} we discuss design issues in the development of the formalisation. In Section~\ref{sect.correctness.pseudoinstruction.expansion} we briefly discuss some difficulties present in the ongoing proof of correctness for the assembly process. In Section~\ref{sect.validation} we discuss validation of the emulator to ensure that what we formalised was an accurate model of an MCS-51 series microprocessor. In Section~\ref{sect.related.work} we describe previous work, with an eye toward describing its relation with the work described herein. In Section~\ref{sect.conclusions} we conclude. In Section~\ref{sect.related.work} we describe previous, related work. Section~\ref{sect.conclusions} concludes. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% As a programming language, Matita corresponds to the functional fragment of O'Caml extended with dependent types. Matita also features a rich higher-order logic for reasoning about programs, including a universe hierarchy with a single impredicative universe, \texttt{Prop}, and potentially infinitely many predicative universes \texttt{Type[i]} for $0 \geq i$. Unlike O'Caml, all recursive functions admitted by the Matita typechecker must be structurally recursive and total. All recursive functions admitted by the Matita typechecker must be structurally recursive and total. We box Matita code to distinguish it from O'Caml code. During the assembly phase, where labels and pseudoinstructions are eliminated, a map is generated associating cost labels with memory locations. This map is later used in a separate analysis which computes the cost of a program by traversing through a program, fetching one instruction at a time, and computing the cost of blocks. When targetting more complex processors, this simple analysis will need to be replaced by a more sophisticated WCET analysis. These block costings are stored in another map, and will later be passed back to the prototype compiler. When targetting more complex processors, this simple analysis could be replaced by a sophisticated WCET analysis. Block costings are stored in another map, and will be passed back to the compiler. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % SECTION                                                                      % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \section{Correctness of pseudoinstruction expansion} \label{sect.correctness.pseudoinstruction.expansion} With the addition of pseudoinstructions and labels, an assembly language is induced on top of the machine language. Pseudoinstructions in an assembly program must be expanded into machine instructions prior to execution. As we are interested in constructing a verified compiler, this expansion process must be shown to be correct', avoiding any semantic changes to the assembly program. Demonstrating such correctness'is subtle due to jump pseudoinstructions. We would like to expand jump pseudoinstructions to the smallest possible jump machine instruction. Doing this is non-trivial, as it is easy to construct programs with configurations of jumps where larger jump instructions can only be shrunk' if and only if others are also shrunk. This is a well-known problem in the assembly programming community, but causes difficulties for the correctness proof of an assembler that purports to produce small executables. Another problem is computing the cost of pseudoinstructions, a necessary step for lifting our cost model to the C-source level in a cost-preserving manner. Conditional jumps can be expanded in complex ways, where the true' and false branches' of the jump instruction get expanded into pieces of machine code with differing costs. What, then, is the cost of a conditional jump pseudoinstruction? How we solve these problems, and a full description of the assembler's correctness proof, will be described in a following publication. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% We have also built a complete MCS-51 ecosystem: UART, I/O lines, and hardware timers, complete with an assembler. Work closely related to our own can be found in~\cite{fox:trustworthy:2010}. Here, the authors describe the formalisation, in HOL4, of the ARMv7 instruction set architecture. Fox \emph{et al} formalised, in HOL4, the ARMv7 instruction set architecture, along with various related tools, such as assemblers~~\cite{fox:trustworthy:2010}. The formalisation is executable both within (using rewriting) and outwith the theorem prover. They further point to an excellent list of references to related work in the literature. This formalisation also considers the machine code level, opposed to their formalisation, which only considering an abstract assembly language. Instruction decoding is explicitly modeled inside HOL4's logic. We go further in also providing an assembly language, complete with assembler, to translate instructions and pseudoinstruction into machine code. In further related work~\cite{myreen:extensible:2009}, a verified compiler for a Lisp-like language is presented, targetting this formalised microprocessor. Further, in~\cite{fox:trustworthy:2010} the authors validated their formalisation by using development boards and random testing. We currently rely on non-exhaustive testing against a third party emulator. We recognise the importance of this exhaustive testing, but currently leave it for future work. Executability is another key difference between our work and that of~\cite{fox:trustworthy:2010}. Our formalisation is executable: applying the emulation function to an input state eventually reduces to an output state. This is because Matita is based on a logic, CIC, which internalizes conversion. In~\cite{fox:trustworthy:2010} the authors provide an automation layer to derive single step theorems: if the processor is in a state that satisfies some preconditions, then after execution of an instruction it will reside in a state satisfying some postconditions. We will not need single step theorems of this form to prove properties of the assembly code. Both models---ours and that of~\cite{fox:trustworthy:2010}---are executable'. Our main difficulties resided in the non-uniformity of an old 8-bit architecture, in terms of the instruction set, addressing modes and memory models. Other related projects CompCert~\cite{leroy:formally:2009} and the CLI Stack. CompCert concerns the certification of a C compiler and includes a formalisation in Coq of a subset of PowerPC. The CLI Stack consists of the design and verification of a whole chain of artefacts including a 32-bit microprocessor, the Piton assembler and two compilers. The CLI Stack consists of the design and verification of a whole chain of artefacts including a 32-bit microprocessor (FM9001), the Piton assembler and two compilers. Like CerCo, the CLI Stack compilers gave the cost of high-level instructions in processor cycles. The CLI Stack high-level languages ($\mu$Gypsy and Nqthm Lisp) and FM9001 microprocessor were not commercial products, but bespoke designs for the purpose of verification (see~\cite{moore:grand:2005}). This work has been continued by Hunt and Swords, verifying the Centaur Technologies Via Nano and Isaiah micoprocessors in ACL2~\cite{hunt:verifying:2010}. The CompCert C compiler is extracted to O'Caml using Coq's code extraction facility. We aim to make use of a similar code extraction facility in Matita, but only if the extracted code exhibits the same degree of type safety, provided by polymorphic variants, and human readability that the O'Caml emulator posseses. This is because we aim to use the emulator as a library for non-certified software written directly in O'Caml. How we have used Matita's dependent types to handle the instruction set (Subsection~\ref{subsect.instruction.set.unorthogonality}) could enable code extraction to make use of polymorphic variants. Matita's dependent typesm, used to handle the instruction set (Subsection~\ref{subsect.instruction.set.unorthogonality}), could enable code extraction to make use of polymorphic variants. Using Coq's current code extraction algorithm we could write assembly programs that would generate runtime errors when emulated. We leave this for future work. We provide an assembly language, enhanched with labels and pseudoinstructions, and an assembler from this language to machine code. This assembly language is similar to those found in `industrial strength' compilers, such as SDCC. A proof of correctness for the assembly process is ongoing. We introduce cost labels in the machine language to relate the data flow of the assembly program to that of the C source language, in order to associate costs to the C program. For the O'Caml version, we provide a parser and pretty printer from code memory to Intel HEX. Hence we can perform testing on programs compiled using any free or commercial compiler. Our main difficulty in formalising the MCS-51 was the unorthogonality of its memory model and instruction set. All instructions have been tested at least once, but we have not yet pushed testing further, for example with random testing or by using development boards. I/O in particular has not been tested yet, and it is currently unclear how to provide exhaustive testing in the presence of I/O. Finally, we are aware of having over-specified the processor in several places, by fixing a behaviour hopefully consistent with the real machine, where manufacturer data sheets are ambiguous or under-specified. Finally, we are aware of having over-specified the processor in several places, by fixing a behaviour hopefully consistent with the real machine, where manufacturer data sheets are ambiguous or under-specified.\footnote{Submitted paper 16 pages by permission of program committee.} \bibliography{itp-2011}