Changeset 509

Ignore:
Timestamp:
Feb 14, 2011, 3:27:57 PM (6 years ago)
Message:

Background.

File:
1 edited

Legend:

Unmodified
 r508 % SECTION                                                                      % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \section{Introduction} \section{Background} \label{sect.introduction} Compiler verification, as of late, is as of late a hot topic'. 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. Formal methods are aimed at increasing our confidence in our software and hardware artifacts. Ideally, in the future we would like all artifacts to be equipped with a formal specification and a proof of correctness of the implementation. Nowadays practically all programs are written in high level languages and then compiled into low level ones. Thus the specifications are also given at high level and correctness is proved reasoning automatically or interactively on the source code. The code that is actually run, however, is the object code generated by the compiler. A few simple questions then arise: What properties are preserved during compilation? What properties are affected by the compilation strategy? To what extent can you trust your compiler in preserving those properties? Compiler verification, as of late, is a hot topic' in computer science research. So far, it has been focused on the first and last question only. In particular, the attention has been put only on extensional properties, which are easily preserved during compilation: it is sufficient to completely preserve the denotational semantics of the input program. The situation is definitely more complex when we also take in account intesional properties of programs, like space, time or energy spent into computation and transmission of data. To express this properties and to reason on them we are forced to adopt a cost model that assigns a cost to single instructions or to blocks of instructions. Morally, 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 an high level instruction is usually compiled in a different way according to the surrounding instructions. Hence the cost model is affected by compilation and thus all intensional specifications are as well. In the EU Project CerCo (Certified Complexity) we will approach the problem by developing a compiler that induces the cost model on the source code by assigning to each block of high level instructions the cost associated to the obtained object code. The cost model will thus be inherently non compositional, but it can be extremely \emph{precise}, capturing the realistic cost. In particular, we already have a prototype where no approximation of the cost is provided at all. The natural applications of our approach are then in the domain of hard real time programs, where the user can certify the meeting of all dealines while fully exploiting the computational time, that would be wasted in case of over-estimation of the costs. 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. \subsection{The 8051/8052}