source: Papers/jar-assembler-2014/boender-jar-2014.tex @ 3521

Last change on this file since 3521 was 3521, checked in by boender, 7 years ago
  • some more additions
File size: 17.3 KB
Line 
1\documentclass[a4paper]{article}
2\usepackage{algpseudocode}
3\usepackage{alltt}
4\usepackage{amsfonts}
5\usepackage{amsmath}
6\usepackage[british]{babel}
7\usepackage{caption}
8\usepackage[colorlinks]{hyperref}
9\usepackage[utf8]{inputenc}
10\usepackage{listings}
11\usepackage{microtype}
12\usepackage{subcaption}
13
14\usepackage{kpfonts}
15\usepackage[T1]{fontenc}
16\usepackage[ttdefault=true]{AnonymousPro}
17
18\newcommand{\All}[1]{\forall{#1}.\;}
19\newcommand{\deffont}[1]{\textbf{#1}}
20\newcommand{\lam}[1]{\lambda{#1}.\;}
21\newcommand{\todo}[1]{\ensuremath{\texttt{[#1]}}}
22
23\makeatletter
24\def\blfootnote{\xdef\@thefnmark{}\@footnotetext}
25\makeatother
26
27\bibliographystyle{alpha}
28
29%\renewcommand{\verb}{\lstinline}
30\def\lstlanguagefiles{lst-grafite.tex}
31\lstset{language=Grafite}
32
33\author{Jaap Boender \and Dominic P. Mulligan \and Claudio Sacerdoti Coen}
34\title{On the proof of correctness of a verified optimising assembler}
35
36\begin{document}
37
38\maketitle
39
40\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.
58\end{abstract}
59
60\newpage
61
62\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}
65
66\newpage
67
68%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
69% Section                                 %
70%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
71\section{Introduction}
72\label{sect.introduction}
73
74% Everybody
75
76%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
77% Section                                 %
78%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
79\subsection{Matita}
80\label{subsect.matita}
81
82In this Subsection we provide an overview of Matita, the host system for all proofs reported in this paper.
83
84Matita is a theorem prover based on a variant of the Calculus of Coinductive Constructions~\cite{asperti:user:2007}.
85The system features a full spectrum of dependent types and (co)inductive families, a sophisticated system of uniform coercions, a tactic-driven proof construction engine~\cite{sacerdoti-coen:tinycals:2007}, and paramodulation based automation~\cite{asperti:higher-order:2007} all of which we exploit in the formalisation described herein.
86
87Matita's syntax is largely similar to the syntaxes of mainstream functional programming languages such as OCaml or Standard ML, and the type theory that Matita implements is very similar to that of Coq~\cite{coq:2004} and Agda~\cite{bove:brief:2009}.
88Nevertheless, we provide a brief explanation of the main syntactic and type-theoretic features of Matita that will be needed to follow the body of the paper:
89\begin{itemize}
90\item
91Non-recursive functions and definitions are introduced via the \texttt{definition} keyword whilst recursive functions are introduced with \texttt{let rec}.
92Mutually recursive functions are separated via the \texttt{and} keyword.
93Matita checks that all recursive functions are terminating before being admitted.
94\item
95Matita has an infinite hierarchy of type universes.
96A single impredicative universe of types, \texttt{Prop}, exists at the base of this hierarchy.
97An infinite series of predicative universes, \texttt{Type[0]} : \texttt{Type[1]} : \texttt{Type[2]}, and so on and so forth, sits atop \texttt{Prop}.
98Matita, unlike Coq or Agda, implements no form of typical ambiguity or universe polymorphism, with explicit concrete universe levels being preferred instead.
99\item
100Matita's type theory plays host to a rich and expressive higher-order logic.
101Constant \texttt{True} and \texttt{False} represent truth and falsity in \texttt{Prop} respectively.
102Two inductive families in \texttt{Prop} encode conjunction and disjunction---$\mathtt{P \wedge Q}$ and $\mathtt{P \vee Q}$ respectively.
103As is usual, implication and universal quantification are identified with the dependent function space ($\Pi$ types), whereas (constructive) existential quantification is encoded as a dependent sum (a $\Sigma$-type).
104We write $\All{x : \phi}\psi$ for the dependent function space, and abbreviate this as $\phi \rightarrow \psi$ when $x \not\in fv(\psi)$ as usual.
105\item
106Inductive and coinductive families are introduced via the \texttt{inductive} and \texttt{coinductive} keywords respectively, with named constructor declarations separated with a bar.
107Mutually inductive data family declarations are separated via \texttt{with}.
108In the following declaration
109\begin{lstlisting}
110inductive I ($P_1$ : $\tau_1$) $\ldots$ ($P_n$ : $\tau_n$) : $\phi_1 \rightarrow \ldots \rightarrow \phi_m \rightarrow \phi$ := $\ldots$
111\end{lstlisting}
112we call $P_i$ for $0 \leq i \leq n$ the \deffont{parameters} of \texttt{I} and $\phi_j$ for $0 \leq j \leq m$ the \deffont{indices} of \texttt{I}.
113Matita checks that constructors have strictly-positive types before admitting an inductive family.
114\item
115Records are introduced with the \texttt{record} keyword.
116A Matita record
117\begin{lstlisting}
118record R : Type[0] := { F1 : nat }.
119\end{lstlisting}
120may be thought of as syntactic sugar for a single-constructor inductive data type of the same name:
121\begin{lstlisting}
122inductive R : Type[0] :=
123  | mk_R : nat -> R.
124\end{lstlisting}
125The declaration of a record \texttt{R} causes a \deffont{constructor} function \texttt{mk\_R} to be entered into the global context as a side effect.
126\deffont{Projections}, one for each of the record's fields, are also registered in the global context, and in the example record above \texttt{F1} of type $R \rightarrow nat$ is registered as a field projection.
127A record field's type may depend on fields declared earlier in the record.
128
129Record fields may be marked as coercions.
130In the following example
131\begin{lstlisting}
132record S : Type[1] :=
133{
134  Carrier :> Type[0];
135  op : Carrier -> Carrier -> Carrier
136}
137\end{lstlisting}
138the field \texttt{Carrier} is declared to be a coercion with `\texttt{:>}' with the effect that the field projection \texttt{Carrier} may be omitted where it could be successfully inferred by Matita.
139Field coercions facilitate the informal but common mathematical practice of intentionally confusing a structure with its underlying carrier set.
140\item
141Terms may be freely omitted, allowing the user to write down partial types and terms.
142A question mark, \texttt{?}, denotes a single term that has been omitted by the user.
143Some omitted terms can be deduced by Matita's refinement system.
144Other, more complex goals arising from omitted terms may require user input to solve, in which case a proof obligation is opened for each term that cannot be deduced automatically.
145Three consecutive dots, \texttt{$\ldots$}, denote multiple terms or types that have been omitted.
146\item
147Pattern matching is carried out with a \texttt{match} expression.
148We may sometimes fully annotate a \texttt{match} expression with its return type.
149This is especially useful when working with indexed families of types or with invariants, expressed as types, on functions.
150In the following
151\begin{lstlisting}
152match t return $\lam{x}x = 0 \rightarrow bool$ with
153[ 0    $\Rightarrow$ $\lam{prf_1}P_1$
154| S m $\Rightarrow$ $\lam{prf_2}P_2$
155] (refl $\ldots$ t)
156\end{lstlisting}
157the \texttt{0} branch of the \texttt{match} expression returns a function from $0 = 0$ to \texttt{bool}, whereas the \texttt{S m} branch of the \texttt{match} expression returns a function from \texttt{S m = 0} to \texttt{bool}.
158In both cases the annotated return type $\lam{x}x = 0 \rightarrow bool$ has been specialised given new information about \texttt{t} revealed by the act of pattern matching.
159The entire term, with \texttt{match} expression applied to \texttt{refl $\ldots$ t}, has type \texttt{bool}.
160\item
161Matita features a liberal system of coercions (distinct from the previously mentioned record field coercions).
162It is possible to define a uniform coercion $\lam{x}\langle x, ?\rangle$ from every type $T$ to the dependent product $\Sigma{x : T}. P x$ (here $\langle \_,\_ \rangle$ is Matita's sugared syntax for pairs).
163The coercion opens a proof obligation that asks the user to prove that $P$ holds for $x$.
164When a coercion is to be applied to a complex term (for example, a $\lambda$-abstraction, a local definition, or a case analysis), the system automatically propagates the coercion to the sub-terms.
165For instance, to apply a coercion to force $\lam{x}M : A \rightarrow B$ to
166have type $\All{x : A}\Sigma{y : B}. P x y$, the system looks for a coercion from $M : B$ to $\Sigma{y : B}. P x y$ in a context augmented with $x : A$.
167This is significant when the coercion opens a proof obligation, as the user will be presented with multiple, but simpler proof obligations in the correct context.
168In this way, Matita supports the `Russell' proof methodology developed by Sozeau in~\cite{sozeau:subset:2007}, in a lightweight but tightly-integrated manner.
169\end{itemize}
170Throughout, for reasons of clarity, conciseness, and readability, we may choose to simplify or omit parts of Matita code.
171We will always ensure that these omissions do not mislead the reader.
172
173%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
174% Section                                 %
175%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
176\subsection{Map of paper}
177\label{subsect.map.of.paper}
178
179% Anybody
180
181%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
182% Section                                 %
183%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
184\section{The proof}
185\label{sect.the.proof}
186
187%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
188% Section                                 %
189%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
190\subsection{Structure of the assembler}
191\label{subsect.structure.of.the.assembler}
192
193% Everybody
194
195%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
196% Section                                 %
197%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
198\subsection{Encoding the instruction set}
199\label{subsect.encoding.the.instruction.set}
200
201% DPM and CSC
202
203% Polymorphic variants
204% Non-regularity of instruction set (CISC)
205% Use of dependent types in get_arg_XXX and set_arg_XXX
206% Assembly code features (what pseudo-instructions are present)
207
208%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
209% Section                                 %
210%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
211\subsection{Operational semantics}
212\label{subsect.operational.semantics}
213
214% DPM and CSC
215
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
235% Trie data structure and use of dependent types
236% Operational semantics of MCS-51
237% Operational semantics of assembly code
238
239%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
240% Section                                 %
241%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
242\subsection{Policies and the correctness proof}
243\label{subsect.policies.and.the.correctness.proof}
244
245% DPM and CSC
246
247%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
248% Section                                 %
249%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
250\subsection{Correctness of branch displacement}
251\label{subsect.correctness.of.branch.displacement}
252
253% JB and CSC
254One of the consequences of using the MCS-51 instruction set is that we have to take its specific branch instructions into account. The MCS-51 has three different types of branch instruction---which one should be used depends on the distance between the instruction and its target (the {\em span}). This applies to unconditional branches, conditional branches and procedure calls.
255
256The three different types of branch instructions are:
257\begin{itemize}
258  \item The {\em short} branch: a 2-byte instruction that can branch over a 1-byte displacement, i.e. XXX bytes forwards or YYY bytes backwards.
259  \item The {\em absolute} branch: a 2-byte instruction that can change the last 11 bits of the program counter. Thus, it can branch to any destination within the same 2048-byte segment.
260  \item The {\em long} branch: a 3-byte instruction that can branch to any destination in memory.
261\end{itemize}
262
263Not all combinations of instructions are provided. For example, there is no short call, nor is there a long conditional branch.
264
265Apart from their difference in size, the instructions also take different amounts of time to execute: 2 cycles for the short and absolute branch, 3 cycles for the long branch.
266
267The {\em branch optimisation problem}, a well-known problem in assembler design, is to find the smallest branch instructions for a given assembler program. This is complicated by the fact that branch instructions can influence each other: an instruction's span depends on the size of any branch instructions in between.
268
269The branch displacement problem has been found to be NP-complete for several
270similar architectures~\cite{Robertson1979,Szymanski1978}, therefore an optimal
271solution could be time-consuming to find. The standard
272solution~\cite{Szymanski1978,Dickson2008} is to use a fixed point algorithm.
273
274Two flavours of solution are possible: either a greatest fixed point algorithm
275(encoding all branches as long and then replacing them by shorter branches
276insofar possible), or a least fixed point algorithm (encoding all branches as
277short and then replacing them by longer branches as necessary). The advantage
278of a greatest fixed point algorithm is that it can be stopped after any
279iteration, as all the intermediate solutions are safe, if not necessarily
280optimal. This is not the case for a least fixed point algorithm, but this
281algorithm, if it terminates, will result in a smaller solution.
282
283In the particular case of the MCS-51 instruction set, matters are complicated
284by the existence of the absolute branch. Now, the encoding of a branch does not
285solely depend on its span, but also on their location within the program. This
286means that instead of being determined solely by the size of instructions
287within its span, the encoding of a branch is determined also by all of the
288branches that precede it.
289
290%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
291% Section                                 %
292%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
293\subsection{Fitting together}
294\label{subsect.fitting.together}
295
296% Everybody
297
298%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
299% Section                                 %
300%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
301\section{Conclusion}
302\label{sect.conclusion}
303
304% Everbody
305
306%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
307% Section                                 %
308%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
309\subsection{Related work}
310\label{subsect.related.work}
311
312% Everybody
313
314%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
315% Section                                 %
316%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
317\subsection{Formalisation}
318\label{subsect.formalisation}
319
320% Everybody
321
322% Man-hours of effort
323% Lines of code, etc.
324% Pointer to web address for formalisation
325
326\newpage
327
328\bibliography{boender-jar-2014}
329
330\end{document}
Note: See TracBrowser for help on using the repository browser.