Changeset 3520 for Papers


Ignore:
Timestamp:
Nov 20, 2014, 12:42:03 PM (4 years ago)
Author:
mulligan
Message:

abstract added

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/jar-assembler-2014/boender-jar-2014.tex

    r3519 r3520  
    2121\newcommand{\todo}[1]{\ensuremath{\texttt{[#1]}}}
    2222
     23\makeatletter
     24\def\blfootnote{\xdef\@thefnmark{}\@footnotetext}
     25\makeatother
     26
    2327\bibliographystyle{alpha}
    2428
     
    2832
    2933\author{Jaap Boender \and Dominic P. Mulligan \and Claudio Sacerdoti Coen}
    30 \title{On the proof of correctness of a verified optimising assembler
    31 \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}}
    32 \date{\today}
     34\title{On the proof of correctness of a verified optimising assembler}
    3335
    3436\begin{document}
     
    3739
    3840\begin{abstract}
     41A typical microprocessor's instruction set provides several forms of conditional and unconditional jumps, procedure calls, and data movement instructions.
     42Unconditional jump and call instructions vary depending on the \emph{span} of the branch---the distance between the location of the instruction and the branch target---with short jump and call instructions taking less space in code memory to encode than their long jump and call counterparts.
     43
     44Assembly languages are a thin veneer over machine code, with a few light abstractions provided for the benefit of the programmer.
     45Two such abstractions provided in assembly languages are uniform `jump' and `call' pseudoinstructions that branch to a labelled point in program source rather than a concrete machine address.
     46These pseudoinstructions remove the burden of selecting between long and short jump instructions, and computing concrete machine addresses, from the programmer.
     47
     48Pseudoinstructions must be `assembled away' by the assembler, and a jump pseudoinstruction can always be replaced by a long jump machine code instruction with no semantic change.
     49Yet, such a na\"ive replacement is inefficient and wasteful in terms of code memory usage---a prime concern when targetting embedded devices---as some long jumps could have been replaced with short jumps, reducing the size of the program in code memory.
     50Therefore any assembler should replace as many long jumps with short jumps as possible, optimising for program size.
     51
     52We present a formalisation and proof of correctness of an optimising assembler targetting a space-constrained embedded microcontroller: the 8-bit Intel MCS-51 series.
     53All proofs are checked by the Matita theorem prover, and the work forms a major component of the Certified Complexity (`CerCo') project, aiming to produce a verified concrete complexity-preserving compiler for a subset of the C programming language.
     54
     55Our optimisations complicate the proof of correctness of the assembler proper and therefore we employ the use of `policies', separating out decisions of how a pseudoinstruction should be expanded from the expansion process itself, simplifying our proofs.
     56Our proof strategy also tracks `good' addresses, and only programs that use good addresses have their semantics preserved under assembly.
     57This tracking offers increased flexibility over the traditional approach---where addresses are kept abstract and immutable---as we may experiment with some manipulations of machine addresses.
    3958\end{abstract}
    4059
     
    4261
    4362\tableofcontents
     63
     64\blfootnote{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}
    4465
    4566\newpage
     
    193214% DPM and CSC
    194215
     216\begin{lstlisting}
     217definition BitVector := $\lambda$n: nat. Vector bool n.
     218\end{lstlisting}
     219
     220\begin{lstlisting}
     221definition Nibble := BitVector 4.
     222definition Byte7 := BitVector 7.
     223definition Byte := BitVector 8.
     224definition Word := BitVector 16.
     225definition Word11 := BitVector 11.
     226\end{lstlisting}
     227
     228\begin{lstlisting}
     229inductive BitVectorTrie (A: Type[0]): nat $\rightarrow$ Type[0] :=
     230  Leaf: A -> BitVectorTrie A O
     231| Node: $\forall$n: nat. BitVectorTrie A n $\rightarrow$ BitVectorTrie A n $\rightarrow$ BitVectorTrie A (S n)
     232| Stub: $\forall$n: nat. BitVectorTrie A n.
     233\end{lstlisting}
     234
    195235% Trie data structure and use of dependent types
    196236% Operational semantics of MCS-51
Note: See TracChangeset for help on using the changeset viewer.