Changeset 2360


Ignore:
Timestamp:
Sep 27, 2012, 3:28:44 PM (7 years ago)
Author:
mulligan
Message:

Back to 17 pages after Claudio's additions.

File:
1 edited

Legend:

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

    r2359 r2360  
    7373
    7474The MCS-51 has a relative paucity of features compared to its more modern brethren, with the lack of any caching or pipelining features meaning that timing of execution is predictable, making the MCS-51 very attractive for CerCo's ends.
    75 Yet---as with many things---what one hand giveth, the other taketh away, and the MCS-51's paucity of features---though an advantage in many respects---also quickly becomes a hindrance.
    76 In particular, the MCS-51 features a relatively minuscule series of memory spaces by modern standards.
    77 As a result our C compiler, to have any sort of hope of successfully compiling realistic programs for embedded devices, ought to produce `tight' machine code.
    78 
    79 In order to do this, we must solve the `branch displacement' problem---deciding how best to expand pseudojumps to labels in assembly language to machine code jumps. The branch displacement problem happears when pseudojumps can be expanded
     75However, the MCS-51's paucity of features---though an advantage in many respects---also quickly becomes a hindrance, as the MCS-51 features a relatively minuscule series of memory spaces by modern standards.
     76As a result our C compiler, to be able to successfully compile realistic programs for embedded devices, ought to produce `tight' machine code.
     77
     78To do this, we must solve the `branch displacement' problem---deciding how best to expand pseudojumps to labels in assembly language to machine code jumps.
     79The branch displacement problem arises when pseudojumps can be expanded
    8080in different ways to real machine instructions, but the different expansions
    81 are not equivalent (e.g. do not have the same size or speed) and not always
     81are not equivalent (e.g. differ in size or speed) and not always
    8282correct (e.g. correctness is only up to global constraints over the compiled
    8383code). For instance, some jump instructions (short jumps) are very small
     
    8686too far away, larger and slower long jumps must be used. The use of a long jump may
    8787augment the distance between another pseudojump and its target, forcing
    88 another long jump use, in a cascading effect. The job of the optimising
     88another long jump use, in a cascade. The job of the optimising
    8989compiler (assembler) is to individually expand every pseudo-instruction in such a way
    90 that all global constraints are satisfied and that the compiled program size
    91 is minimal in size and faster in time.
    92 This problem is known to be complex for most CISC architectures (see~\cite{hyde:branch:2006}).
     90that all global constraints are satisfied and that the compiled program
     91is minimal in size and faster in concrete time complexity.
     92This problem is known to be computationally hard for most CISC architectures (see~\cite{hyde:branch:2006}).
    9393
    9494To free CerCo's 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.
     
    146146
    147147The rest of this paper is a detailed description of our proof that is marginally still a work in progress.
    148 In Section~\ref{sect.matita} we provide a brief overview of the Matita proof assistant for the unfamiliar reader.
     148In Subsection~\ref{subsect.matita} we provide a brief overview of the Matita proof assistant for the unfamiliar reader.
    149149In Section~\ref{sect.the.proof} we discuss the design and implementation of the proof proper.
    150150In Section~\ref{sect.conclusions} we conclude.
     
    153153% SECTION                                                                      %
    154154% ---------------------------------------------------------------------------- %
    155 \section{Matita}
    156 \label{sect.matita}
     155\subsection{Matita}
     156\label{subsect.matita}
    157157
    158158Matita is a proof assistant based on a variant of the Calculus of (Co)inductive Constructions~\cite{asperti:user:2007}.
     
    168168This is significant when the coercion opens a proof obligation, as the user will be presented with multiple, but simpler proof obligations in the correct context.
    169169In this way, Matita supports the `Russell' proof methodology developed by Sozeau in~\cite{sozeau:subset:2006}, with an implementation that is lighter and more tightly integrated with the system than that of Coq.
    170 
    171 Throughout this paper we simplify the statements of lemmas and types of definitions in order to emphasise readability.
    172170
    173171% ---------------------------------------------------------------------------- %
Note: See TracChangeset for help on using the changeset viewer.