1 | \documentclass[twocolumn,draft]{svjour3} |
---|
2 | \usepackage{algpseudocode} |
---|
3 | %\usepackage{algorithmicx} |
---|
4 | \usepackage{alltt} |
---|
5 | \usepackage{amsfonts} |
---|
6 | \usepackage{amsmath} |
---|
7 | \usepackage[british]{babel} |
---|
8 | \usepackage{caption} |
---|
9 | \usepackage{hyperref} |
---|
10 | \usepackage[utf8]{inputenc} |
---|
11 | \usepackage{listings} |
---|
12 | \usepackage{subcaption} |
---|
13 | |
---|
14 | \renewcommand{\verb}{\lstinline} |
---|
15 | \def\lstlanguagefiles{lst-grafite.tex} |
---|
16 | \lstset{language=Grafite} |
---|
17 | |
---|
18 | \begin{document} |
---|
19 | |
---|
20 | \title{A verified optimising assembler |
---|
21 | \thanks{Research supported by the CerCo project, within the Future and Emerging Technologies (FET) programme of the Seventh Framework Programme for Research of the European Commission, under FET-Open grant number 243881}} |
---|
22 | \author{Jaap Boender \and Dominic P. Mulligan \and Claudio Sacerdoti Coen} |
---|
23 | \institute{Department of Computer Science, University of Middlesex \and Computer Laboratory, University of Cambridge \and Dipartimento di Informatica, University of Bologna} |
---|
24 | |
---|
25 | \maketitle |
---|
26 | |
---|
27 | \begin{abstract} |
---|
28 | Optimising assemblers face the `branch displacement problem', i.e. how best to choose between concrete machine code jump instructions---typically of differing instruction and offset sizes---when expanding pseudo-instructions. |
---|
29 | Ideally, a well-implemented optimising assembler would choose the set of jump expansions that minimises the size of the resulting machine code program, a task that is provably \textsc{np}-hard. |
---|
30 | |
---|
31 | As part of CerCo (`Certified Complexity')---an \textsc{eu}-funded project to develop a verified concrete complexity preserving compiler for a large subset of the C programming language---we have implemented and proved correct an assembler within an interactive theorem prover. |
---|
32 | Our assembler targets the instruction set of a typical micro-controller, the Intel \textsc{mcs}-51 series. |
---|
33 | As is common in embedded systems development, this micro-controller has a paucity of available code memory and therefore we face an additional pressure in reducing the size of any assembled machine code program. |
---|
34 | Out of necessity, then, our assembler implements an algorithm for solving the branch displacement problem, and we must prove that this algorithm is correct. |
---|
35 | |
---|
36 | We discuss wider problems associated with proving an optimising assembler correct, discuss possible solutions to those problems, and detail our chosen solutions and their proofs of correctness. |
---|
37 | |
---|
38 | \keywords{formal verification, interactive theorem proving, assembler, branch displacement optimisation} |
---|
39 | \end{abstract} |
---|
40 | |
---|
41 | \input{problem} |
---|
42 | \input{algorithm} |
---|
43 | \input{proof} |
---|
44 | \input{conclusion} |
---|
45 | |
---|
46 | \bibliography{biblio} |
---|
47 | \bibliographystyle{spbasic} |
---|
48 | |
---|
49 | \end{document} |
---|