# Changeset 515 for Deliverables/D4.1

Ignore:
Timestamp:
Feb 15, 2011, 11:49:19 AM (9 years ago)
Message:

finished tidying the introduction

File:
1 edited

### Legend:

Unmodified
 r514 To express even be able to express these properties, and to be able to reason about them, we are forced to adopt a cost model that assigns a cost to single, or blocks, of instructions. Ideally, we would like to have a compositional cost model that assigns the same cost to all occurrences of one instruction. However, compiler optimizations are inherently non-compositional: each occurrence of a high level instruction is usually compiled in a different way according to the context it finds itself in. However, compiler optimisations are inherently non-compositional: each occurrence of a high level instruction is usually compiled in a different way according to the context it finds itself in. Therefore both the cost model and intensional specifications are affected by the compilation process. Here, a user can certify that all deadlines' are met whilst wringing as many clock cycles from the processor---using a cost model that does not over-estimate---as possible. Other applications of our approach are in the domain of compiler verification itself. For instance, an extensional specification of an optimization is useless since it grants preservation of the semantics without stating that the cost (in space or time) of the optimized code should be lower. Another example is completeness and correctness of the compilation process in presence of space constraints: the compiler could refuse a source program for an embedded system when the size of the compiled code exceeds the available ROM size. Moreover, preservation of the semantics must be required only for those programs that do not exhausts their stack/heap space. Hence the statement of completeness of the compiler must take in account the realistic cost model. In the methodology proposed in CerCo we assume to be able to compute on the object code exact and realistic costs for sequential blocks of instructions. With modern processors, it is possible~\cite{??,??,??}, but difficult, to compute exact costs or to reasonably approximate them, since the execution of the program itself has an influence on the speed of processing. This is due mainly to caching effects and memory effects in the processor, used, for instance, to perform branch prediction. For this reason, at the current stage of CerCo we decided to focus on 8-bits microprocessors that are still widely used in embedded systems and whose cost model is easily predictable. In particular, we have fully formalized an executable formal semantics of the Family of 8 bits Freescale Microprocessors~\cite{oliboni} and a similar one for the MCS-51 microprocessors. The latter is the one described in this paper. The main focus of the formalization has been on capturing the intensional behaviour of the processor. The main problems we have faced, however, are mainly due to the extreme unorthogonality of the memory model and instruction sets of the MCS-51 microprocessors. To cope with this unorthogonality and to have executability, we have exploited the dependent type system of the interactive theorem prover Matita. %Compiler verification, as of late, is a hot topic' in computer science research. %This rapidly growing field is motivated by one simple question: `to what extent can you trust your compiler?' %Existing verification efforts have broadly focussed on \emph{semantic correctness}, that is, creating a compiler that is guaranteed to preserve the semantics of a program during the compilation process. %However, there is another important facet of correctness that has not garnered much attention, that is, correctness with respect to some intensional properties of the program to be compiled. Further, we see our approach as being relevant to the field of compiler verification (and construction) itself. For instance, an optimisation specified only extensionally is only half specified; though the optimisation may preserve the denotational semantics of a program, there is no guarantee that any intensional properties of the program, such as space or time usage, will be improved. Another potential application is toward completeness and correctness of the compilation process in the presence of space constraints. Here, a compiler could potentially reject a source program targetting an embedded system when the size of the compiled code exceeds the available ROM size. Moreover, preservation of a program's semantics may only be required for those programs that do not exhaust the stack or heap. Hence the statement of completeness of the compiler must take in to account a realistic cost model. In the methodology proposed in CerCo we assume we are able to compute on the object code exact and realistic costs for sequential blocks of instructions. With modern processors, though possible~\cite{??,??,??}, it is difficult to compute exact costs or to reasonably approximate them. This is because the execution of a program itself has an influence on the speed of processing. For instance, caching and memory effects in the processor are used in advanced features such as branch prediction. For this reason CerCo decided to focus on 8-bit microprocessors. These are still widely used in embedded systems, and have the advantage of an easily predictable cost model due to the relative sparcity of features that they possess. In particular, we have fully formalised an executable formal semantics of a family of 8 bit Freescale Microprocessors~\cite{oliboni}, and provided a similar executable formal semantics for the MCS-51 microprocessor. The latter work is what we describe in this paper. The main focus of the formalisation has been on capturing the intensional behaviour of the processor. However, the design of the MCS-51 itself has caused problems in our formalisation. For example, the MCS-51 has a highly unorthogonal instruction set. To cope with this unorthogonality, and to produce an executable specification, we have exploited the dependent type system of Matita, an interactive proof assistant. \subsection{The 8051/8052} The MCS-51 is an eight bit microprocessor introduced by Intel in the late 1970s. Commonly called the 8051, in the three decades since its introduction the processor has become a highly popular target for embedded systems engineers. Further, the processor and its immediate successor, the 8052, is still manufactured by a host of semiconductor suppliers---many of them European---including Atmel, Siemens Semiconductor, NXP (formerly Phillips Semiconductor), Texas Instruments, and Maxim (formerly Dallas Semiconductor). Further, the processor, its immediate successor the 8052, and many derivatives are still manufactured \emph{en masse} by a host of semiconductor suppliers. The 8051 is a well documented processor, and has the additional support of numerous open source and commercial tools, such as compilers for high-level languages and emulators. For instance, the open source Small Device C Compiler (SDCC) recognises a dialect of C, and other compilers targeting the 8051 for BASIC, Forth and Modula-2 are also extant. An open source emulator for the processor, MCU8051 IDE, is also available. An open source emulator for the processor, MCU-8051 IDE, is also available. Both MCU-8051 IDE and SDCC were used profitably in the implementation of our formalisation. \begin{figure}[t]