# Changeset 2360 for Papers

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

Back to 17 pages after Claudio's additions.

File:
1 edited

### Legend:

Unmodified
 r2359 The 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. 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. In particular, the MCS-51 features a relatively minuscule series of memory spaces by modern standards. 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. 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 However, 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. As a result our C compiler, to be able to successfully compile realistic programs for embedded devices, ought to produce tight' machine code. 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 arises when pseudojumps can be expanded in different ways to real machine instructions, but the different expansions are not equivalent (e.g. do not have the same size or speed) and not always are not equivalent (e.g. differ in size or speed) and not always correct (e.g. correctness is only up to global constraints over the compiled code). For instance, some jump instructions (short jumps) are very small too far away, larger and slower long jumps must be used. The use of a long jump may augment the distance between another pseudojump and its target, forcing another long jump use, in a cascading effect. The job of the optimising another long jump use, in a cascade. The job of the optimising compiler (assembler) is to individually expand every pseudo-instruction in such a way that all global constraints are satisfied and that the compiled program size is minimal in size and faster in time. This problem is known to be complex for most CISC architectures (see~\cite{hyde:branch:2006}). that all global constraints are satisfied and that the compiled program is minimal in size and faster in concrete time complexity. This problem is known to be computationally hard for most CISC architectures (see~\cite{hyde:branch:2006}). To 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. The rest of this paper is a detailed description of our proof that is marginally still a work in progress. In Section~\ref{sect.matita} we provide a brief overview of the Matita proof assistant for the unfamiliar reader. In Subsection~\ref{subsect.matita} we provide a brief overview of the Matita proof assistant for the unfamiliar reader. In Section~\ref{sect.the.proof} we discuss the design and implementation of the proof proper. In Section~\ref{sect.conclusions} we conclude. % SECTION                                                                      % % ---------------------------------------------------------------------------- % \section{Matita} \label{sect.matita} \subsection{Matita} \label{subsect.matita} Matita is a proof assistant based on a variant of the Calculus of (Co)inductive Constructions~\cite{asperti:user:2007}. This 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. In 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. Throughout this paper we simplify the statements of lemmas and types of definitions in order to emphasise readability. % ---------------------------------------------------------------------------- %