Changeset 515


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

finished tidying the introduction

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/ITP-Paper/itp-2011.tex

    r514 r515  
    104104To 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.
    105105Ideally, we would like to have a compositional cost model that assigns the same cost to all occurrences of one instruction.
    106 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.
     106However, 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.
    107107Therefore both the cost model and intensional specifications are affected by the compilation process.
    108108
     
    117117Here, 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.
    118118
    119 Other applications of our approach are in the domain of compiler verification
    120 itself. For instance, an extensional specification of an optimization is useless
    121 since it grants preservation of the semantics without stating that the cost
    122 (in space or time) of the optimized code should be lower. Another example is
    123 completeness and correctness of the compilation process in presence of
    124 space constraints: the compiler could refuse a source
    125 program for an embedded system when the size of the compiled code exceeds the
    126 available ROM size. Moreover, preservation of the semantics must be required
    127 only for those programs that do not exhausts their stack/heap space. Hence the
    128 statement of completeness of the compiler must take in account the realistic
    129 cost model.
    130 
    131 In the methodology proposed in CerCo we assume to be able to compute on the
    132 object code exact and realistic costs for sequential blocks of instructions.
    133 With modern processors, it is possible~\cite{??,??,??}, but difficult,
    134 to compute exact costs or to reasonably approximate them, since the execution
    135 of the program itself has an influence on the speed of processing. This is due
    136 mainly to caching effects and memory effects in the processor, used, for
    137 instance, to perform branch prediction. For this reason, at the current stage
    138 of CerCo we decided to focus on 8-bits microprocessors that are still widely
    139 used in embedded systems and whose cost model is easily predictable.
    140 
    141 In particular, we have fully formalized an executable formal semantics of
    142 the Family of 8 bits Freescale Microprocessors~\cite{oliboni} and a similar
    143 one for the MCS-51 microprocessors. The latter is the one described in this
    144 paper. The main focus of the formalization has been on capturing the
    145 intensional behaviour of the processor. The main problems we have faced,
    146 however, are mainly due to the extreme unorthogonality of the memory model
    147 and instruction sets of the MCS-51 microprocessors. To cope with this
    148 unorthogonality and to have executability, we have exploited the dependent
    149 type system of the interactive theorem prover Matita.
    150 
    151 %Compiler verification, as of late, is a `hot topic' in computer science research.
    152 %This rapidly growing field is motivated by one simple question: `to what extent can you trust your compiler?'
    153 %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.
    154 %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.
     119Further, we see our approach as being relevant to the field of compiler verification (and construction) itself.
     120For 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.
     121Another potential application is toward completeness and correctness of the compilation process in the presence of space constraints.
     122Here, a compiler could potentially reject a source program targetting an embedded system when the size of the compiled code exceeds the available ROM size.
     123Moreover, preservation of a program's semantics may only be required for those programs that do not exhaust the stack or heap.
     124Hence the statement of completeness of the compiler must take in to account a realistic cost model.
     125
     126In 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.
     127With modern processors, though possible~\cite{??,??,??}, it is difficult to compute exact costs or to reasonably approximate them.
     128This is because the execution of a program itself has an influence on the speed of processing.
     129For instance, caching and memory effects in the processor are used in advanced features such as branch prediction.
     130For this reason CerCo decided to focus on 8-bit microprocessors.
     131These 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.
     132
     133In 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.
     134The latter work is what we describe in this paper.
     135The main focus of the formalisation has been on capturing the intensional behaviour of the processor.
     136However, the design of the MCS-51 itself has caused problems in our formalisation.
     137For example, the MCS-51 has a highly unorthogonal instruction set.
     138To cope with this unorthogonality, and to produce an executable specification, we have exploited the dependent type system of Matita, an interactive proof assistant.
    155139
    156140\subsection{The 8051/8052}
     
    159143The MCS-51 is an eight bit microprocessor introduced by Intel in the late 1970s.
    160144Commonly called the 8051, in the three decades since its introduction the processor has become a highly popular target for embedded systems engineers.
    161 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).
     145Further, the processor, its immediate successor the 8052, and many derivatives are still manufactured \emph{en masse} by a host of semiconductor suppliers.
    162146
    163147The 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.
    164148For 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.
    165 An open source emulator for the processor, MCU8051 IDE, is also available.
     149An open source emulator for the processor, MCU-8051 IDE, is also available.
     150Both MCU-8051 IDE and SDCC were used profitably in the implementation of our formalisation.
    166151
    167152\begin{figure}[t]
Note: See TracChangeset for help on using the changeset viewer.