Changeset 2419


Ignore:
Timestamp:
Oct 30, 2012, 11:52:42 AM (7 years ago)
Author:
mulligan
Message:

Some initial work.

Location:
Papers/cerco-assembler-2012
Files:
1 added
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/cerco-assembler-2012/cerco-assembler.tex

    r2401 r2419  
     1\documentclass[a4paper, 10pt]{article}
     2
     3\author{Jaap Boender and Dominic P. Mulligan and Claudio Sacerdoti Coen}
     4\title{On the correctness of an optimising assembler for the MCS-51 microprocessor}
     5\date{\today}
     6
     7\begin{document}
     8
     9\maketitle
     10
     11\begin{abstract}
     12\end{abstract}
     13
     14%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     15% Section
     16%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     17\section{Introduction}
     18\label{sect.introduction}
     19
     20This paper describes the formalisation and proof of correctness of an optimising assembler for the MCS-51 microprocessor.
     21The formalisation and proof of correctness have been carried out in the Matita proof assistant, a dependently-typed, tactic driven system similar to Coq.
     22The complete formalisation of the microprocessor and assembler forms a substantial and important component of the EU's CerCo (`Certified Complexity') project.
     23
     24The MCS-51 is an 8-bit microprocessor introduced by Intel in the late 1970s.
     25Despite its relative age, the microprocessor is still manufactured in quantity by numerous foundries and is a popular component in embedded devices, where simple, well-tested and inexpensive microprocessors find their niche.
     26Further, the processor has been used as the basis for numerous derivatives over the last three decades.
     27However, compared to its more modern brethren the MCS-51 has a paucity of features: most MCS-51 derivatives do not feature any instruction caching, pipelining of instructions, branch prediction or features typical of cutting-edge microprocessors.
     28
     29The MCS-51's simplicity means it is well suited for CerCo's ends.
     30CerCo aims to construct and prove correct a concrete cost preserving compiler for a large subset of the C programming language.
     31The main novelty of the CerCo compiler is its certified lifting of a precise cost model.
     32This cost model is presented to the programmer as a series of \emph{cost annotations} that decorate the C source.
     33
     34
     35%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     36% Section
     37%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     38\subsection{Overview of the paper}
     39\label{subsect.overview.paper}
     40
     41\end{document}
Note: See TracChangeset for help on using the changeset viewer.