Changeset 1201


Ignore:
Timestamp:
Sep 9, 2011, 11:27:45 AM (8 years ago)
Author:
mulligan
Message:

more changes to reduce length

File:
1 edited

Legend:

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

    r1200 r1201  
    9797Specifications are therefore also given at a high level and correctness can be proved by reasoning on the program's source code.
    9898The code that is actually run is not the high level source code that we reason on, but low level code generated by the compiler.
    99 A few questions now arise:
    100 \begin{itemize*}
    101 \item
    102 What properties are preserved during compilation?
    103 \item
     99
     100Questions now arise:  What properties are preserved during compilation?
    104101What properties are affected by the compilation strategy?
    105 \item
    106102To what extent can you trust your compiler in preserving those properties?
    107 \end{itemize*}
    108103These and other questions motivate a current `hot topic' in computer science research: \emph{compiler verification} (e.g.~\cite{chlipala:verified:2010,leroy:formal:2009}, and so on).
    109104So far, the field has only been focused on the first and last questions.
     
    267262Memory may be addressed in numerous ways: immediate, direct, indirect, external direct and code indirect.
    268263As the latter two addressing modes hint, there are some restrictions enforced by the 8051, and its derivatives, on which addressing modes may be used with specific types of memory.
    269 For instance, the extra 128 bytes of IRAM of the 8052 cannot be addressed using indirect addressing; rather, external (in)direct addressing must be used. Moreover, some memory segments are addressed using 8-bit pointers while others require 16-bits.
     264For instance, the extra 128 bytes of IRAM of the 8052 cannot be addressed using indirect addressing; rather, external (in)direct addressing must be used.
     265Some memory segments are also addressed using 8-bit pointers while others require 16-bits.
    270266
    271267The 8051 possesses an 8-bit Arithmetic and Logic Unit (ALU), with a variety of instructions for performing arithmetic and logical operations on bits and integers.
     
    658654We leave the computation of the delay time to the environment.
    659655
    660 We use only the P1 and P3 lines despite the MCS-51 having~4 output lines, P0--P3.
    661 This is because P0 and P2 become inoperable if XRAM is present (we assume it is).
     656We use only the P1 and P3 lines.
     657This is because the other lines become inoperable if XRAM is present (we assume it is).
    662658
    663659The UART port can work in several modes, depending on the how the SFRs are set.
     
    740736We 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.
    741737In particular, we are interested in intentional properties of the processor; precise timings of instruction execution in clock cycles.
    742 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.
     738We have also built a complete MCS-51 ecosystem: UART, I/O lines, and hardware timers, complete with an assembler.
    743739
    744740Work closely related to our own can be found in~\cite{fox:trustworthy:2010}.
     
    762758In contrast, the various ARM instruction sets and memory models are relatively uniform.
    763759
    764 Two close projects to CerCo are CompCert~\cite{leroy:formally:2009} and the CLI Stack.
     760Other related projects CompCert~\cite{leroy:formally:2009} and the CLI Stack.
    765761CompCert concerns the certification of a C compiler and includes a formalisation in Coq of a subset of PowerPC.
    766 The CLI Stack consists of the design and verification of a whole chain of artifacts including a 32-bit microprocessor, the Piton assembler and two compilers for high-level languages.
     762The CLI Stack consists of the design and verification of a whole chain of artefacts including a 32-bit microprocessor, the Piton assembler and two compilers.
    767763Like CerCo, the CLI Stack compilers gave the cost of high-level instructions in processor cycles.
    768 However, unlike CerCo, both the CLI Stack high-level languages ($\mu$Gypsy and Nqthm Lisp) and FM9001 microprocessor were not commercial products, but designs created for the purpose of verification (see~\cite{moore:grand:2005}).
     764The CLI Stack high-level languages ($\mu$Gypsy and Nqthm Lisp) and FM9001 microprocessor were not commercial products, but bespoke designs for the purpose of verification (see~\cite{moore:grand:2005}).
    769765
    770766The CompCert C compiler is extracted to O'Caml using Coq's code extraction facility.
     
    781777Our formalisation is \emph{directly} executable, while the one in CompCert only provides a relation that describes execution.
    782778In CompCert I/O is only described as a synchronous external function call and there is no I/O at the processor level.
    783 Moreover an idealized abstract and uniform memory model is assumed, while we take into account the complicated overlapping memory model of the MCS-51 architecture.
     779CompCert assumes an idealized abstract and uniform memory model; we take into account the complicated overlapping memory model of the MCS-51 architecture.
    784780Finally, 82 instructions of the more than 200 offered by the processor are formalised in CompCert, and the assembly language is augmented with macro instructions that are turned into `real' instructions only during communication with the external assembler.
    785 Even from a technical level the two formalisations differ: we tried to exploit dependent types whilst CompCert largely sticks to a non-dependent fragment of Coq.
     781Even from a technical level the two formalisations differ: we use dependent types whilst CompCert largely sticks to non-dependent types.
    786782
    787783In~\cite{atkey:coqjvm:2007} an executable specification of the Java Virtual Machine, using dependent types, is presented.
     
    813809
    814810The formalisation is done at machine level and not at assembly level; we also formalise fetching and decoding.
    815 We separately provide an assembly language, enhanched with labels and pseudoinstructions, and an assembler from this language to machine code.
     811We provide an assembly language, enhanched with labels and pseudoinstructions, and an assembler from this language to machine code.
    816812This assembly language is similar to those found in `industrial strength' compilers, such as SDCC.
    817813We introduce cost labels in the machine language to relate the data flow of the assembly program to that of the C source language, in order to associate costs to the C program.
Note: See TracChangeset for help on using the changeset viewer.