Changeset 3471
 Timestamp:
 Sep 11, 2014, 12:01:40 PM (6 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Papers/sttt/main.tex
r3470 r3471 18 18 \begin{document} 19 19 20 \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 FETOpen grant number 243881}} 21 \author{Jaap Boender \and Dominic Mulligan \and Claudio Sacerdoti Coen} 20 \title{On the correctness of a branch displacement algorithm 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 FETOpen grant number 243881}} 22 \author{Jaap Boender \and Dominic P. Mulligan \and Claudio Sacerdoti Coen} 22 23 23 24 \maketitle 24 25 25 26 \begin{abstract} 26 The branch displacement problem is a wellknown problem in assembler design. 27 It revolves around the feature, present in several processor families, of 28 having different instructions, of different sizes, for jumps of different 29 displacements. The problem, which is provably NPhard, is then to select the 30 instructions such that one ends up with the smallest possible program. 27 Optimising assemblers face the `branch displacement problem', i.e. how best to choose between concrete machine code jump instructionstypically of differing instruction and offset sizeswhen expanding pseudoinstructions. 28 Ideally, a wellimplemented 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. 31 29 32 During our research with the CerCo project on formally verifying a C compiler, 33 we have implemented and proven correct an algorithm for this problem. In this 34 paper, we discuss the problem, possible solutions, our specific solutions and 35 the proofs. 30 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 languagewe have implemented and proved correct an assembler within an interactive theorem prover. 31 Our assembler targets the instruction set of a typical microcontroller, the \textsc{mcs}51. 32 As is common in embedded systems, this microcontroller has a paucity of available code memory and therefore we face additional pressure in reducing the size of any assembled machine code program. 33 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. 34 35 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. 36 36 37 37 \keywords{formal verification, interactive theorem proving, assembler, branch displacement optimisation}
Note: See TracChangeset
for help on using the changeset viewer.