Changeset 2357 for Papers


Ignore:
Timestamp:
Sep 27, 2012, 2:46:30 PM (7 years ago)
Author:
mulligan
Message:

Begun editing down to reclaim space. Fixed some embarrassing typos (e.g. CICS for CISC).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/cpp-asm-2012/cpp-2012-asm.tex

    r2356 r2357  
    9090compiler (assembler) is to individually expand every pseudo-instruction in such a way
    9191that all global constraints are satisfied and that the compiled program size
    92 is minimal in size and faster in time. The problem is known to be particularly
    93 complex for most CICS architectures (for instance, see~\cite{hyde:branch:2006}).
     92is minimal in size and faster in time.
     93This problem is known to be complex for most CISC architectures (see~\cite{hyde:branch:2006}).
    9494
    9595To free the CerCo C compiler from having to consider complications relating to branch displacement, we have chosen to implement an optimising assembler, whose input language the compiler will target.
     
    111111
    112112Note that the temporal tightness of the simulation is a fundamental prerequisite
    113 of the correctness of the simulation because some functions of the MCS-51---notably timers and I/O---depend on the microprocessor's clock.
     113of the correctness of the simulation because some functions of the MCS-51---timers and I/O---depend on the microprocessor's clock.
    114114If the pseudo- and concrete clock differ the result of an I/O operation may not be preserved.
    115115
     
    146146with benefits on the size of the formalisation.
    147147
    148 The rest of this paper is a detailed description of our proof that is, in minimal part, still a work in progress.
    149 
    150 We provide the reader with a brief `roadmap' for the rest of the paper.
     148The rest of this paper is a detailed description of our proof that is marginally still a work in progress.
    151149In Section~\ref{sect.matita} we provide a brief overview of the Matita proof assistant for the unfamiliar reader.
    152150In Section~\ref{sect.the.proof} we discuss the design and implementation of the proof proper.
     
    668666Polymorphic variants nicely capture the absolutely unorthogonal instruction set of the MCS-51 where every opcode must accept its own subset of the 11 addressing mode of the processor.
    669667
    670 The second purpose is to single out the sources of incompleteness.
     668The second purpose is to single out sources of incompleteness.
    671669By abstracting our functions over the dependent type of correct policies, we were able to manifest the fact that the compiler never refuses to compile a program where a correct policy exists.
    672670This also allowed to simplify the initial proof by dropping lemmas establishing that one function fails if and only if some previous function does so.
    673671
    674 Finally, dependent types, together with Matita's liberal system of coercions, allow us to simulate almost entirely---in user space---the proof methodology `Russell' of Sozeau~\cite{sozeau:subset:2006}.
    675 However, not every proof has been carried out in this way: we only used this style to prove that a function satisfies a specification that only involves that function in a significant way.
    676 For example, it would be unnatural to see the proof that fetch and assembly commute as the specification of one of the two functions.
     672Finally, dependent types, together with Matita's liberal system of coercions, allow us to simulate almost entirely in user space the proof methodology `Russell' of Sozeau~\cite{sozeau:subset:2006}.
     673Not every proof has been carried out in this way: we only used this style to prove that a function satisfies a specification that only involves that function in a significant way.
     674It would not be natural to see the proof that fetch and assembly commute as the specification of one of the two functions.
    677675
    678676\subsection{Related work}
     
    681679% piton
    682680We are not the first to consider the correctness of an assembler for a non-trivial assembly language.
    683 Perhaps the most impressive piece of work in this domain is the Piton stack~\cite{moore:piton:1996}.
    684 This was a stack of verified components, written and verified in ACL2, ranging from a proprietary FM9001 microprocessor verified at the gate level, to assemblers and compilers for two high-level languages---a dialect of Lisp and $\mu$Gypsy~\cite{moore:grand:2005}.
     681The most impressive piece of work in this domain is the Piton stack~\cite{moore:piton:1996}, a stack of verified components, written and verified in ACL2, ranging from a proprietary FM9001 microprocessor verified at the gate level, to assemblers and compilers for two high-level languages---Lisp and $\mu$Gypsy~\cite{moore:grand:2005}.
    685682
    686683% jinja
Note: See TracChangeset for help on using the changeset viewer.