Index: Papers/sttt/biblio.bib
===================================================================
 Papers/sttt/biblio.bib (revision 3476)
+++ Papers/sttt/biblio.bib (revision 3477)
@@ 1,2 +1,257 @@
+@article
+{ asperti:user:2007,
+ author = {Andrea Asperti and Claudio {Sacerdoti Coen} and Enrico Tassi and Stefano Zacchiroli},
+ title = {User interaction with the {Matita} proof assistant},
+ journal = {Automated Reasoning},
+ pages = {109139},
+ volume = {39},
+ issue = {2},
+ year = {2007}
+}
+
+@article
+{ bate:wcet:2011,
+ author = {Iain Bate and Usman Khan},
+ title = {{WCET} analysis of modern processors using multicriteria optimisation},
+ journal = {Empirical Software Engineering},
+ pages = {528},
+ volume = {16},
+ issue = {1},
+ year = {2011}
+}
+
+@article
+{ klein:machine:2006,
+ author = {Gerwin Klein and Tobias Nipkow},
+ title = {A machinechecked model for a {Javalike} language, virtual machine and compiler},
+ journal = {{ACM} Transactions on Programming Languages and Systems},
+ volume = {28},
+ number = {4},
+ pages = {619695},
+ year = {2006}
+}
+
+@article
+{ klein:sel4:2010,
+ author = {Gerwin Klein and June Andronick and Kevin Elphinstone and Gernot Heiser and David Cock and Philip Derrin and Dhammika Elkaduwe and Kai Engelhardt and Rafal Kolanski and Michael Norrish and Thomas Sewell and Harvey Tuch and Simon Winwood},
+ title = {{seL4}: Formal verification of an operating system kernel},
+ journal = {Communications of the {ACM}},
+ issue = {6},
+ volume = {53},
+ pages = {107115},
+ year = {2010}
+}
+
+@article
+{ leroy:formal:2009,
+ author = {Xavier Leroy},
+ title = {Formal verification of a realistic compiler},
+ journal = {Communications of the {ACM}},
+ volume = {52},
+ number = {7},
+ pages = {107115},
+ year = {2009}
+}
+
+@article
+{ leroy:formally:2009,
+ author = {Xavier Leroy},
+ title = {A formally verified compiler backend},
+ journal = {Automated Reasoning},
+ volume = {43},
+ number = {4},
+ pages = {363446},
+ year = {2009}
+}
+
+@book
+{ moore:piton:1996,
+ author = {J Strother Moore},
+ title = {Piton: A mechanically verified assembly language},
+ series = {Automated Reasoning Series},
+ volume = {3},
+ isbn = {9780792339205},
+ publisher = {Springer},
+ year = {1996}
+}
+
+@inproceedings
+{ atkey:coqjvm:2007,
+ author = {Robert Atkey},
+ title = {{CoqJVM}: An executable specification of the {Java Virtual Machine} using dependent types},
+ booktitle = {Types},
+ pages = {1832},
+ year = {2007}
+}
+
+@inproceedings
+{ blazy:formal:2006,
+ author = {Sandrine Blazy and Zaynah Dargaye and Xavier Leroy},
+ title = {Formal Verification of a {C} Compiler FrontEnd},
+ booktitle = {{FM}},
+ pages = {460475},
+ year = {2006}
+}
+
+@inproceedings
+{ fox:trustworthy:2010,
+ author = {Anthony Fox and Magnus O. Myreen},
+ title = {A Trustworthy Monadic Formalization of the {ARMv7} Instruction Set Architecture},
+ booktitle = {{ITP}},
+ pages = {243258},
+ year = {2010}
+}
+
+@inproceedings
+{ sevcik:relaxedmemory:2011,
+ author = {Jaroslav \v{S}ev\v{c}\'ik and Viktor Vafeiadis and Francesco {Zappa Nardelli} and Suresh Jagannathan and Peter Sewell},
+ title = {RelaxedMemory Concurrency and Verified Compilation},
+ booktitle = {{POPL}},
+ year = {2011}
+}
+
+@inproceedings
+{ tuch:types:2007,
+ author = {Harvey Tuch and Gerwin Klein and Michael Norrish},
+ title = {Types, Bytes, and Separation Logic},
+ booktitle = {{POPL}},
+ pages = {97108},
+ year = {2007}
+}
+
+
+@inproceedings
+{ klein:sel4:2009,
+ author = {Gerwin Klein and June Andronick and Kevin Elphinstone and Gernot Heiser and David Cock and Philip Derrin and Dhammika Elkaduwe and Kai Engelhardt and Rafal Kolanski and Michael Norrish and Thomas Sewell and Harvey Tuch and Simon Winwood},
+ title = {{seL4}: Formal verification of an operating system kernel},
+ booktitle = {{SOSP}},
+ year = {2009}
+}
+
+@inproceedings
+{ mulligan:executable:2011,
+ author = {Dominic P. Mulligan and Claudio {Sacerdoti Coen}},
+ title = {An executable formal semantics of the {MCS51} microprocessor in {Matita}},
+ booktitle = {{FMCAD}},
+ year = {2011},
+ note = {Submitted}
+}
+
+@inproceedings
+{ sarkar:semantics:2009,
+ author = {Susmit Sarkar and Peter Sewell and Francesco Zappa Nardelli and Scott Owens and Tom Ridge and Thomas Braibant and Magnus O. Myreen and Jade Alglave},
+ title = {The semantics of {x86CC} multiprocessor machine code},
+ booktitle = {{POPL}},
+ pages = {379391},
+ year = {2009}
+}
+
+@inproceedings
+{ sozeau:subset:2006,
+ author = {Matthieu Sozeau},
+ title = {Subset Coercions in {Coq}},
+ booktitle = {Types},
+ pages = {237252},
+ year = {2006}
+}
+
+@inproceedings
+{ yan:wcet:2008,
+ author = {Jun Yan and Wei Zhang},
+ title = {{WCET} Analysis for MultiCore Processors with Shared {L2} Instruction Caches},
+ booktitle = {{RTAS}},
+ pages = {8089},
+ year = {2008}
+}
+
+@misc
+{ boender:correctness:2012,
+ author = {Jaap Boender and Claudio {Sacerdoti Coen}},
+ title = {On the correctness of a branch displacement algorithm},
+ howpublished = {\url{http://arxiv.org/abs/1209.5920}},
+ year = {2012}
+}
+
+@misc
+{ cerco:2011,
+ title = {The {CerCo} {FETOpen} project},
+ howpublished = {\url{http://cerco.cs.unibo.it/}},
+ year = {2011},
+ key = {CerCo:2011}
+}
+
+@misc
+{ cercoreportcode:2011,
+ title = {{CerCo Deliverable D2.2}: prototype costpreserving {C} compiler},
+ howpublished = {\url{http://cerco.cs.unibo.it/rawattachment/wiki/WikiStart/D2_2.pdf} and \url{http://cerco.cs.unibo.it/rawattachment/wiki/WikiStart/D2_2_Code.tar.gz}},
+ year = {2011},
+ key = {CerCo2.2ReportCode:2011}
+}
+
+@misc
+{ compcert:2011,
+ title = {The {CompCert} project},
+ howpublished = {\url{http://compcert.inria.fr/}},
+ year = {2011},
+ key = {CompCert:2011}
+}
+
+@misc
+{ hyde:branch:2006,
+ title = {Branch displacement optimisation},
+ howpublished = {\url{http://groups.google.com/group/alt.lang.asm/msg/d31192d442accad3}},
+ year = {2006},
+ key = {Hyde:Branch:2006}
+}
+
+@misc
+{ moore:grand:2005,
+ author = {J Strother Moore},
+ title = {A Grand Challenge Proposal for Formal Methods},
+ year = {2005}
+}
+
+@misc
+{ sdcc:2011,
+ title = {Small Device {C} Compiler 3.0.0},
+ howpublished = {\url{http://sdcc.sourceforge.net/}},
+ year = {2011},
+ key = {sdcc:2010}
+}
+
+@misc
+{ sel4:2011,
+ title = {The {l4.verified} project},
+ howpublished = {\url{http://ertos.nicta.com.au/research/l4.verified/}},
+ year = {2011}
+}
+
+@misc
+{ siemens:2011,
+ title = {{Siemens Semiconductor Group} 8051 derivative instruction set},
+ howpublished = {\url{http://www.win.tue.nl/~aeb/comp/8051/instructionset.pdf}},
+ year = {2011},
+ key = {siemens:2011}
+}
+
+@techreport
+{ amadio:certifying:2010,
+ author = {Roberto M. Amadio and Nicolas Ayache and Yann R\'{e}gisGianas and Ronan Saillard},
+ title = {Cerifying cost annotations in compilers},
+ institution = {Universit\'{e} Paris Diderot {(Paris 7)}, Laboratoire {PPS}},
+ year = {2010}
+}
+
+@techreport
+{ klein:machine:2010,
+ author = {Gerwin Klein and Tobias Nipkow},
+ title = {A machinechecked model for a {Javalike} language, virtual machine and compiler},
+ institution = {National {ICT} Australia},
+ number = {0400001T.1},
+ year = {2010}
+
+}
+
+
@article{Szymanski1978,
author = {Szymanski, Thomas G.},
Index: Papers/sttt/main.tex
===================================================================
 Papers/sttt/main.tex (revision 3476)
+++ Papers/sttt/main.tex (revision 3477)
@@ 1,3 +1,4 @@
\documentclass[twocolumn,draft]{svjour3}
+%\documentclass[twocolumn,draft]{svjour3}
+\documentclass[a4paper]{article}
\usepackage{algpseudocode}
%\usepackage{algorithmicx}
@@ 7,7 +8,8 @@
\usepackage[british]{babel}
\usepackage{caption}
\usepackage{hyperref}
+\usepackage[colorlinks]{hyperref}
\usepackage[utf8]{inputenc}
\usepackage{listings}
+\usepackage{microtype}
\usepackage{subcaption}
@@ 21,62 +23,122 @@
\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}}
\author{Jaap Boender \and Dominic P. Mulligan \and Claudio Sacerdoti Coen}
\institute{Department of Computer Science, University of Middlesex \and Computer Laboratory, University of Cambridge \and Dipartimento di Informatica, University of Bologna}
+%\institute{Department of Computer Science, University of Middlesex \and Computer Laboratory, University of Cambridge \and Dipartimento di Informatica, University of Bologna}
\maketitle
\begin{abstract}
Optimising assemblers face the `branch displacement' or `jump encoding' problem, i.e. how best to choose between concrete machine code jump instructions  typically of differing instruction and offset sizes  when expanding pseudoinstructions.
Ideally, an 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.

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 optimising assembler within the Matita interactive theorem prover.
Our assembler targets the instruction set of a typical microcontroller, the Intel \textsc{mcs}51 series.
As is common in embedded systems development, this microcontroller has a paucity of available code memory and therefore we face an additional pressure in reducing the size of any assembled machine code program.
Out of necessity, then, our assembler implements an algorithm for solving the branch displacement problem, and we must prove that this algorithm is correct.

However, the efficient expansion of pseudoinstructions, namely jumps, into machine instructions is complex.
We therefore isolate the decision making over how jumps should be expanded from the expansion process itself as much as possible using `policies', making the proof of correctness for the assembler more straightforward.
+Optimising assemblers face the `branch displacement' or `jump encoding' problem, that is: how best to choose between concrete machine code jump instructionstypically of differing instruction and offset sizeswhen expanding pseudoinstructions.
+Ideally, on space constrained hardware, an optimising assembler would choose the set of pseudoinstruction expansions that minimises the size of the resulting machine code program, a task that is provably \textsc{np}hard.
+
+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 optimising assembler within the Matita interactive theorem prover.
+Our assembler targets the instruction set of a typical microcontroller, the Intel \textsc{mcs51} series.
+As is common with embedded systems development this microcontroller has a paucity of available code memory and therefore we face an additional pressure in reducing the size of any assembled machine code program.
+Out of necessity, then, our assembler implements an algorithm for solving the branch displacement problem, and we have proved that this algorithm is correct.
+
+However, this efficient expansion of jump pseudoinstructions into machine code equivalents is complex, and therefore could unneccessarily complicate the proof of correctness for the rest of the assembler.
+We therefore isolate the decision making over how jumps should be expanded from the expansion process itself as much as possible using `policies', making the rest of the proof of correctness more straightforward.
Our proof strategy contains a tracking facility for `good addresses' and only programs that use good addresses have their semantics preserved under assembly, as we observe that it is impossible for an assembler to preserve the semantics of every assembly program.
Our strategy offers increased flexibility over the traditional approach to proving the correctness of assemblers, wherein addresses in assembly are kept opaque and immutable.
In particular, we may experiment with allowing the benign manipulation of addresses.
+In particular, our approach permits experimentation with the benign manipulation of addresses.
We discuss wider issues associated with a proof of correctness for an assembler, detail our algorithm solving the `branch displacement' problem, and discuss our proof of correctness, employing `policies', for the assembler.
\keywords{Formal verification, interactive theorem proving, assembler, branch displacement optimisation, CerCo (`Certified Complexity'), MCS51 microcontroller, Matita proof assistant}
+%\keywords{Formal verification, interactive theorem proving, assembler, branch displacement optimisation, CerCo (`Certified Complexity'), MCS51 microcontroller, Matita proof assistant}
\end{abstract}
\section{Introduction}
The problem of branch displacement optimisation, also known as jump encoding, is
a wellknown problem in assembler design~\cite{Hyde2006}. Its origin lies in the
fact that in many architecture sets, the encoding (and therefore size) of some
instructions depends on the distance to their operand (the instruction 'span').
The branch displacement optimisation problem consists of encoding these
spandependent instructions in such a way that the resulting program is as
small as possible.

This problem is the subject of the present paper. After introducing the problem
in more detail, we will discuss the solutions used by other compilers, present
the algorithm we use in the CerCo assembler, and discuss its verification,
that is the proofs of termination and correctness using the Matita proof
assistant~\cite{Asperti2007}.

Formulating the final statement of correctness and finding the loop invariants
have been nontrivial tasks and are, indeed, the main contribution of this
paper. It has required considerable care and finetuning to formulate not
only the minimal statement required for the ulterior proof of correctness of
the assembler, but also the minimal set of invariants needed for the proof
of correctness of the algorithm.

The research presented in this paper has been executed within the CerCo project
which aims at formally verifying a C compiler with cost annotations. The
target architecture for this project is the MCS51, whose instruction set
contains spandependent instructions. Furthermore, its maximum addressable
memory size is very small (64 Kb), which makes it important to generate
programs that are as small as possible. With this optimisation, however, comes increased complexity and hence increased possibility for error. We must make sure that the branch instructions are encoded correctly, otherwise the assembled program will behave unpredictably.

All Matita files related to this development can be found on the CerCo
website, \url{http://cerco.cs.unibo.it}. The specific part that contains the
branch displacement algorithm is in the {\tt ASM} subdirectory, in the files
{\tt PolicyFront.ma}, {\tt PolicyStep.ma} and {\tt Policy.ma}.
+We consider the formalisation of an assembler for the Intel MCS51 8bit microprocessor in the Matita proof assistant~\cite{asperti:user:2007}.
+This formalisation forms a major component of the EUfunded CerCo (`Certified Complexity') project~\cite{cerco:2011}, concerning the construction and formalisation of a concrete complexity preserving compiler for a large subset of the C programming language.
+
+The \textsc{mcs51}, commonly called the 8051, is an 8bit Harvard architecture \textsc{cisc} instruction set microcontroller dating from the early 1980s, and was originally manufactured by Intel.
+An extended variant, the \textsc{mcs52} or 8052, was subsequently released adding extra \textsc{ram} and \textsc{rom} above and beyond that offered by the original \textsc{mcs51}, and an extra timer.
+Derivatives are still widely manufactured by a number of semiconductor foundries, with the processor being used especially in embedded systems.
+
+The MCS51 has a relative paucity of features compared to its more modern brethren, with a lack of any caching or pipelining features meaning that timing of execution is predictable, making the MCS51 very attractive for CerCo's ends.
+However, the MCS51's paucity of featuresthough an advantage in many respectsalso quickly becomes a hindrance, as the MCS51 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' problemdeciding how best to expand pseudojumps to labels in assembly language to machine code jumps.
+This problem, also known as `jump encoding', is
+a wellknown problem amongst assembler implementors~\cite{Hyde2006} and arises when pseudojumps can be expanded
+in different ways to real machine instructions, but the different expansions
+are not equivalent (e.g. jumps that differ in the distance that they `span', or instructions that differ in the number of clock cycles needed to completely execute them) and are 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
+and can be executed quickly, but they can only reach destinations within a
+certain distance from the current instruction. When the destinations are
+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 cascade. The job of the optimising
+compiler (assembler) is to individually expand every pseudoinstruction in such a way
+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 (\textsc{np}hard, see~\cite{hyde:branch:2006}).
+
+To simplify the CerCo C compiler we have chosen to implement an optimising assembler whose input language the compiler will target.
+Labels, conditional jumps to labels, a program preamble containing global data and a \texttt{MOV} instruction for moving this global data into the MCS51's one 16bit register all feature in our assembly language.
+We further simplify by ignoring linking, assuming that all our assembly programs are prelinked.
+
+The requirements of the CerCo project add yet more complications to our proof of correctness, as we must also address a cost model.
+CerCo imposes a cost model on C programs or, more specifically, on simple blocks of instructions.
+This cost model is induced by the compilation process itself, and its noncompositional nature allows us to assign different costs to identical C statements depending on how they are compiled.
+In short, we aim to obtain a very precise costing for a program by embracing the compilation process, not ignoring it.
+At the assembler level, this is reflected by our need to induce a cost
+model on the assembly code as a function of the assembly program and the
+strategy used to solve the branch displacement problem. In particular, our
+optimising assembler should also return a map that assigns a cost (in clock
+cycles) to every instruction in the source program. We expect the induced cost
+to be preserved by the assembler: we will prove that the compiled code
+tightly simulates the source code by taking exactly the predicted amount of
+time.
+Note that the temporal `tightness' of the simulation is a fundamental prerequisite
+of the correctness of the simulation, as some functions of the MCS51timers and \textsc{i/o}depend on the microprocessor's clock.
+If the pseudo and concrete clock differ the result of an \textsc{i/o} operation may not be preserved.
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+% This problem is the subject of the present paper. After introducing the problem
+% in more detail, we will discuss the solutions used by other compilers, present
+% the algorithm we use in the CerCo assembler, and discuss its verification,
+% that is the proofs of termination and correctness using the Matita proof
+% assistant~\cite{Asperti2007}.
+
+% Formulating the final statement of correctness and finding the loop invariants
+% have been nontrivial tasks and are, indeed, the main contribution of this
+% paper. It has required considerable care and finetuning to formulate not
+% only the minimal statement required for the ulterior proof of correctness of
+% the assembler, but also the minimal set of invariants needed for the proof
+% of correctness of the algorithm.
+
+% The research presented in this paper has been executed within the CerCo project
+% which aims at formally verifying a C compiler with cost annotations. The
+% target architecture for this project is the MCS51, whose instruction set
+% contains spandependent instructions. Furthermore, its maximum addressable
+% memory size is very small (64 Kb), which makes it important to generate
+% programs that are as small as possible. With this optimisation, however, comes increased complexity and hence increased possibility for error. We must make sure that the branch instructions are encoded correctly, otherwise the assembled program will behave unpredictably.
+
+% All Matita files related to this development can be found on the CerCo
+% website, \url{http://cerco.cs.unibo.it}. The specific part that contains the
+% branch displacement algorithm is in the {\tt ASM} subdirectory, in the files
+% {\tt PolicyFront.ma}, {\tt PolicyStep.ma} and {\tt Policy.ma}.
\section{The branch displacement optimisation problem}
@@ 839,7 +901,7 @@

+\bibliographystyle{alpha}
\bibliography{biblio}
\bibliographystyle{spbasic}
+%\bibliographystyle{spbasic}
\end{document}