Changeset 3471

Timestamp:

Sep 11, 2014, 12:01:40 PM (6 years ago)

Author:

mulligan

Message:

reworked the abstract

File:

• Papers/sttt/main.tex (modified) (1 diff)

Papers/sttt/main.tex

@@ -18 +18 @@
 \begin{document}
 
-\title{On the correctness of a branch displacement algorithm\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}}
-\author{Jaap Boender \and Dominic Mulligan \and Claudio Sacerdoti Coen}
+\title{On the correctness of a branch displacement algorithm
+\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}}
+\author{Jaap Boender \and Dominic P. Mulligan \and Claudio Sacerdoti Coen}
 
 \maketitle
 
 \begin{abstract}
-The branch displacement problem is a well-known problem in assembler design.
-It revolves around the feature, present in several processor families, of
-having different instructions, of different sizes, for jumps of different
-displacements. The problem, which is provably NP-hard, is then to select the
-instructions such that one ends up with the smallest possible program. 
+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.
+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.
 
-During our research with the CerCo project on formally verifying a C compiler,
-we have implemented and proven correct an algorithm for this problem. In this
-paper, we discuss the problem, possible solutions, our specific solutions and
-the proofs.
+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.
+Our assembler targets the instruction set of a typical micro-controller, the \textsc{mcs}-51.
+As is common in embedded systems, this micro-controller has a paucity of available code memory and therefore we face additional pressure in reducing the size of any assembled machine code program.
+Out of necessity, then, our assembler must implement an algorithm for solving the branch displacement problem, and we must prove that this algorithm is correct.
+
+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.
 
 \keywords{formal verification, interactive theorem proving, assembler, branch displacement optimisation}