Changeset 1189


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

implemented some language fixes as spotted by the referees

File:
1 edited

Legend:

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

    r1184 r1189  
    111111These are `easily' preserved during compilation.
    112112
    113 If we consider intensional properties of programs---space, time, and so forth---the situation is more complex.
     113If we consider intentional properties of programs---space, time, and so forth---the situation is more complex.
    114114To express these properties, and reason about them, we must adopt a cost model that assigns a cost to single, or blocks, of instructions.
    115115A compositional cost model, assigning the same cost to all occurrences of one instruction, would be ideal.
    116116However, compiler optimisations are inherently non-compositional: each occurrence of a high level instruction may be compiled in a different way depending on its context.
    117 Therefore both the cost model and intensional specifications are affected by the compilation process.
    118 
    119 In the CerCo project (`Certified Complexity')~\cite{cerco:2011} we approach the problem of reasoning about intensional properties of programs as follows.
     117Therefore both the cost model and intentional specifications are affected by the compilation process.
     118
     119In the CerCo project (`Certified Complexity')~\cite{cerco:2011} we approach the problem of reasoning about intentional properties of programs as follows.
    120120We are currently developing a compiler that induces a cost model on high level source code.
    121121Costs are assigned to each block of high level instructions by considering the costs of the corresponding blocks of compiled code.
     
    129129
    130130Our approach is also relevant to compiler verification and construction.
    131 \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.
     131\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.
    132132
    133133Another potential application is toward completeness and correctness of the compilation process in the presence of space constraints.
     
    157157We 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.
    158158The latter is what we describe in this paper.
    159 The focus of the formalisation has been on capturing the intensional behaviour of the processor; this is not novel.
     159The focus of the formalisation has been on capturing the intentional behaviour of the processor; this is not novel.
    160160However, the design of the MCS-51 itself has caused problems in the formalisation.
    161161For example, the MCS-51 has a highly unorthogonal instruction set.
     
    360360\end{figure}
    361361
    362 The formalization of MCS-51 must deal with bytes (8-bits), words (16-bits), and also more exoteric quantities (7, 3 and 9-bits).
     362The formalization of MCS-51 must deal with bytes (8-bits), words (16-bits), and also more esoteric quantities (7, 3 and 9-bits).
    363363To avoid difficult-to-trace size mismatch bugs, we represented all quantities using bitvectors, i.e. fixed length vectors of booleans.
    364364In 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}.
     
    757757The majority of it deals with proving correctness of implementations of microprocessors at the microcode or gate level, with many considering `cycle accurate' models.
    758758We 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.
    759 In particular, we are interested in intensional properties of the processor; precise timings of instruction execution in clock cycles.
     759In particular, we are interested in intentional properties of the processor; precise timings of instruction execution in clock cycles.
    760760Moreover, 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.
    761761
     
    846846Finally, 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.
    847847
    848 \bibliography{IEEEabrv,itp-2011}
     848\bibliography{itp-2011}
    849849
    850850\end{document}
Note: See TracChangeset for help on using the changeset viewer.