# Changeset 1189 for Deliverables/D4.1/ITP-Paper/itp-2011.tex

Ignore:
Timestamp:
Sep 5, 2011, 5:23:28 PM (8 years ago)
Message:

implemented some language fixes as spotted by the referees

File:
1 edited

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

 r1184 These are easily' preserved during compilation. If we consider intensional properties of programs---space, time, and so forth---the situation is more complex. If we consider intentional properties of programs---space, time, and so forth---the situation is more complex. To express these properties, and reason about them, we must adopt a cost model that assigns a cost to single, or blocks, of instructions. A compositional cost model, assigning the same cost to all occurrences of one instruction, would be ideal. However, compiler optimisations are inherently non-compositional: each occurrence of a high level instruction may be compiled in a different way depending on its context. Therefore both the cost model and intensional specifications are affected by the compilation process. In the CerCo project (Certified Complexity')~\cite{cerco:2011} we approach the problem of reasoning about intensional properties of programs as follows. Therefore both the cost model and intentional specifications are affected by the compilation process. In the CerCo project (Certified Complexity')~\cite{cerco:2011} we approach the problem of reasoning about intentional properties of programs as follows. We are currently developing a compiler that induces a cost model on high level source code. Costs are assigned to each block of high level instructions by considering the costs of the corresponding blocks of compiled code. Our approach is also relevant to compiler verification and construction. \emph{An optimisation specified only extensionally is only half specified}; the optimisation may preserve the denotational semantics of a program, but there is no guarantee that intensional properties of the program improve. \emph{An optimisation specified only extensionally is only half specified}; the optimisation may preserve the denotational semantics of a program, but there is no guarantee that intentional properties of the program improve. Another potential application is toward completeness and correctness of the compilation process in the presence of space constraints. We have fully formalised an executable formal semantics of a family of 8-bit Freescale microprocessors~\cite{oliboni:matita:2008}, and provided a similar executable formal semantics for the MCS-51 microprocessor. The latter is what we describe in this paper. The focus of the formalisation has been on capturing the intensional behaviour of the processor; this is not novel. The focus of the formalisation has been on capturing the intentional behaviour of the processor; this is not novel. However, the design of the MCS-51 itself has caused problems in the formalisation. For example, the MCS-51 has a highly unorthogonal instruction set. \end{figure} The formalization of MCS-51 must deal with bytes (8-bits), words (16-bits), and also more exoteric quantities (7, 3 and 9-bits). The formalization of MCS-51 must deal with bytes (8-bits), words (16-bits), and also more esoteric quantities (7, 3 and 9-bits). To avoid difficult-to-trace size mismatch bugs, we represented all quantities using bitvectors, i.e. fixed length vectors of booleans. In the O'Caml emulator, we faked' bitvectors using phantom types~\cite{leijen:domain:1999} implemented with polymorphic variants~\cite{garrigue:programming:1998}, as in Figure~\ref{fig.ocaml.implementation.bitvectors}. The majority of it deals with proving correctness of implementations of microprocessors at the microcode or gate level, with many considering `cycle accurate' models. We are interested in providing a precise specification of the behaviour of the microprocessor in order to prove the correctness of a compiler which will target the processor. In particular, we are interested in intensional properties of the processor; precise timings of instruction execution in clock cycles. In particular, we are interested in intentional properties of the processor; precise timings of instruction execution in clock cycles. Moreover, in addition to formalising the interface of an MCS-51 processor, we have also built a complete MCS-51 ecosystem: UART, I/O lines, and hardware timers, complete with an assembler. 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. \bibliography{IEEEabrv,itp-2011} \bibliography{itp-2011} \end{document}
Note: See TracChangeset for help on using the changeset viewer.