source: Papers/jar-assembler-2015/old_paper.tex

Last change on this file was 3556, checked in by boender, 7 years ago
  • Renamed old paper to something more appropriate
  • Property svn:executable set to *
File size: 53.5 KB
25\title{On the proof of correctness of a verified optimising assembler
26\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}}
27\author{Jaap Boender \and Dominic P. Mulligan \and Claudio Sacerdoti Coen}
28%\institute{Department of Computer Science, University of Middlesex \and Computer Laboratory, University of Cambridge \and Dipartimento di Informatica, University of Bologna}
33Optimising assemblers face the `branch displacement' or `jump encoding' problem, that is: how best to choose between concrete machine code jump instructions---typically of differing instruction and offset sizes---when expanding pseudo-instructions.
34Ideally, on space constrained hardware, an optimising assembler would choose the set of pseudo-instruction expansions that minimises the size of the resulting machine code program, a task that is provably \textsc{np}-hard.
36As 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.
37Our assembler targets the instruction set of a typical micro-controller, the Intel \textsc{mcs-51} series.
38As is common with embedded systems development this micro-controller has a paucity of available code memory and therefore we face an additional pressure in reducing the size of any assembled machine code program.
39Out of necessity, then, our assembler implements an algorithm for solving the branch displacement problem, and we have proved that this algorithm is correct.
41However, 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.
42We 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.
43Our 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.
44Our strategy offers increased flexibility over the traditional approach to proving the correctness of assemblers, wherein addresses in assembly are kept opaque and immutable.
45In particular, our approach permits experimentation with the benign manipulation of addresses.
47We 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.
49%\keywords{Formal verification, interactive theorem proving, assembler, branch displacement optimisation, CerCo (`Certified Complexity'), MCS-51 microcontroller, Matita proof assistant}
54We consider the formalisation of an assembler for the Intel MCS-51 8-bit microprocessor in the Matita proof assistant~\cite{asperti:user:2007}.
55This formalisation forms a major component of the EU-funded 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.
56Though this document describes the formalisation of an assembler for a specific microprocessor, we believe that the techniques described are general, and should be of interest to anybody providing a proof of correctness for an optimising assembler.
58The \textsc{mcs-51}, commonly called the 8051, is an 8-bit Harvard architecture \textsc{cisc} instruction set microprocessor dating from the early 1980s.
59An extended variant, the \textsc{mcs-52}, or 8052, was subsequently released adding extra \textsc{ram} and \textsc{rom} above and beyond that offered by the original \textsc{mcs-51}, along with an additional timer.
60Originally manufactured and marketed by Intel, the microprocessor quickly gained and maintained its popularity, especially in embedded systems development, with dozens of semiconductor foundries subsequently releasing derivative copies many of which are still manufactured today.
62Admittedly, a typical \textsc{mcs-51} derivative lacks many features compared to its more modern brethren.
63In particular, most derivatives lack a cache, any pipelining features, branch speculation, out-of-order execution, or other advanced microarchitectural features we now take for granted on state-of-the-art microprocessors.
64As a direct result program execution is much more predictable: as part of the processor's specification provided by the manufacturer we can be sure that a \texttt{NOP} instruction will always take exactly one processor cycle to execute, whilst an \texttt{ADD} instruction always takes two processor cycles, and so on and so forth for all instructions in the processor's instruction set.
66Certainty surrounding execution times makes the \textsc{mcs-51} especially attractive for certain embedded development tasks.
67Moreover, this same certainty also makes the \textsc{mcs-51} especially attractive for CerCo's ends, wherein we aim to produce a verified concrete-complexity preserving compiler that lifts a cost model for a C program---induced on the program's machine code image under compilation---back through the compilation chain.
68This cost model will ultimately be made manifest as complexity assertions annotating the original C source code, and these annotations may then be used by the programmer---perhaps in conjunction with external reasoning tools---to derive accurate resource bounds for their program.
69As a result, knowing that a given block of machine code instructions will take a fixed number of cycles to execute, irrespective of the program context or processor state when executed, permits us to generate a cycle-accurate cost model on the original C source code and make several simplifying assumptions in the correctness proof of our compiler.
71Yet, such a goal introduces two complications.
72First, as the CerCo cost model is induced on machine code, the CerCo compilation chain must ultimately produce machine code, rather than assembly code as in other verified compiler projects such as CompCert~\cite{Leroy2009}.
73Ultimately, for the CerCo compilation chain to be fully verified, a verified assembler and a verified compiler must both be produced.
75Second, the presence of an assembler allows us to simplify the proof of correctness of the CerCo compiler proper.
76Rather than having the compiler choose particular jump, call or move machine code instructions, the compiler may produce idealised pseudoinstructions
78To do this, we must solve the `branch displacement' problem---deciding how best to expand pseudojumps to labels in assembly language to machine code jumps.
79This problem, also known as `jump encoding', is
80a well-known problem amongst assembler implementors~\cite{Hyde2006} and arises when pseudojumps can be expanded
81in different ways to real machine instructions, but the different expansions
82are 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
83correct (e.g. correctness is only up to global constraints over the compiled
84code). For instance, some jump instructions (short jumps) are very small
85and can be executed quickly, but they can only reach destinations within a
86certain distance from the current instruction. When the destinations are
87too far away, larger and slower long jumps must be used. The use of a long jump may
88augment the distance between another pseudojump and its target, forcing
89another long jump use, in a cascade. The job of the optimising
90compiler (assembler) is to individually expand every pseudo-instruction in such a way
91that all global constraints are satisfied and that the compiled program
92is minimal in size and faster in concrete time complexity.
93This problem is known to be computationally hard for most CISC architectures (\textsc{np}-hard, see~\cite{hyde:branch:2006}).
95To simplify the CerCo C compiler we have chosen to implement an optimising assembler whose input language the compiler will target.
96Labels, conditional jumps to labels, a program preamble containing global data and a \texttt{MOV} instruction for moving this global data into the MCS-51's one 16-bit register all feature in our assembly language.
97We further simplify by ignoring linking, assuming that all our assembly programs are pre-linked.
99The requirements of the CerCo project add yet more complications to our proof of correctness, as we must also address a cost model.
100CerCo imposes a cost model on C programs or, more specifically, on simple blocks of instructions.
101This cost model is induced by the compilation process itself, and its non-compositional nature allows us to assign different costs to identical C statements depending on how they are compiled.
102In short, we aim to obtain a very precise costing for a program by embracing the compilation process, not ignoring it.
103At the assembler level, this is reflected by our need to induce a cost
104model on the assembly code as a function of the assembly program and the
105strategy used to solve the branch displacement problem. In particular, our
106optimising assembler should also return a map that assigns a cost (in clock
107cycles) to every instruction in the source program. We expect the induced cost
108to be preserved by the assembler: we will prove that the compiled code
109tightly simulates the source code by taking exactly the predicted amount of
111Note that the temporal `tightness' of the simulation is a fundamental prerequisite
112of the correctness of the simulation, as some functions of the MCS-51---timers and \textsc{i/o}---depend on the microprocessor's clock.
113If the pseudo- and concrete clock differ the result of an \textsc{i/o} operation may not be preserved.
135% This problem is the subject of the present paper. After introducing the problem
136% in more detail, we will discuss the solutions used by other compilers, present
137% the algorithm we use in the CerCo assembler, and discuss its verification,
138% that is the proofs of termination and correctness using the Matita proof
139% assistant~\cite{Asperti2007}.
141% Formulating the final statement of correctness and finding the loop invariants
142% have been non-trivial tasks and are, indeed, the main contribution of this
143% paper. It has required considerable care and fine-tuning to formulate not
144% only the minimal statement required for the ulterior proof of correctness of
145% the assembler, but also the minimal set of invariants needed for the proof
146% of correctness of the algorithm.
148% The research presented in this paper has been executed within the CerCo project
149% which aims at formally verifying a C compiler with cost annotations. The
150% target architecture for this project is the MCS-51, whose instruction set
151% contains span-dependent instructions. Furthermore, its maximum addressable
152% memory size is very small (64 Kb), which makes it important to generate
153% 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.
155% All Matita files related to this development can be found on the CerCo
156% website, \url{}. The specific part that contains the
157% branch displacement algorithm is in the {\tt ASM} subdirectory, in the files
158% {\tt}, {\tt} and {\tt}.
160\section{The branch displacement optimisation problem}
162In most modern instruction sets that have them, the only span-dependent
163instructions are branch instructions. Taking the ubiquitous x86-64 instruction
164set as an example, we find that it contains eleven different forms of the
165unconditional branch instruction, all with different ranges, instruction sizes
166and semantics (only six are valid in 64-bit mode, for example). Some examples
167are shown in Figure~\ref{f:x86jumps} (see also~\cite{IntelDev}).
173Instruction & Size (bytes) & Displacement range \\
175Short jump & 2 & -128 to 127 bytes \\
176Relative near jump & 5 & $-2^{32}$ to $2^{32}-1$ bytes \\
177Absolute near jump & 6 & one segment (64-bit address) \\
178Far jump & 8 & entire memory (indirect jump) \\
182\caption{List of x86 branch instructions}
186The chosen target architecture of the CerCo project is the Intel MCS-51, which
187features three types of branch instructions (or jump instructions; the two terms
188are used interchangeably), as shown in Figure~\ref{f:mcs51jumps}.
194Instruction & Size    & Execution time & Displacement range \\
195            & (bytes) & (cycles) & \\
197SJMP (`short jump') & 2 & 2 & -128 to 127 bytes \\
198AJMP (`absolute jump') & 2 & 2 & one segment (11-bit address) \\
199LJMP (`long jump') & 3 & 3 & entire memory \\
203\caption{List of MCS-51 branch instructions}
207Conditional branch instructions are only available in short form, which
208means that a conditional branch outside the short address range has to be
209encoded using three branch instructions (for instructions whose logical
210negation is available, it can be done with two branch instructions, but for
211some instructions this is not the case). The call instruction is
212only available in absolute and long forms.
214Note that even though the MCS-51 architecture is much less advanced and much
215simpler than the x86-64 architecture, the basic types of branch instruction
216remain the same: a short jump with a limited range, an intra-segment jump and a
217jump that can reach the entire available memory.
219Generally, in code fed to the assembler as input, the only
220difference between branch instructions is semantics, not span. This
221means that a distinction is made between an unconditional branch and the
222several kinds of conditional branch, but not between their short, absolute or
223long variants.
225The algorithm used by the assembler to encode these branch instructions into
226the different machine instructions is known as the {\em branch displacement
227algorithm}. The optimisation problem consists of finding as small an encoding as
228possible, thus minimising program length and execution time.
230Similar problems, e.g. the branch displacement optimisation problem for other
231architectures, are known to be NP-complete~\cite{Robertson1979,Szymanski1978},
232which could make finding an optimal solution very time-consuming.
234The canonical solution, as shown by Szymanski~\cite{Szymanski1978} or more
235recently by Dickson~\cite{Dickson2008} for the x86 instruction set, is to use a
236fixed point algorithm that starts with the shortest possible encoding (all
237branch instruction encoded as short jumps, which is likely not a correct
238solution) and then iterates over the source to re-encode those branch
239instructions whose target is outside their range.
241\subsection*{Adding absolute jumps}
243In both papers mentioned above, the encoding of a jump is only dependent on the
244distance between the jump and its target: below a certain value a short jump
245can be used; above this value the jump must be encoded as a long jump.
247Here, termination of the smallest fixed point algorithm is easy to prove. All
248branch instructions start out encoded as short jumps, which means that the
249distance between any branch instruction and its target is as short as possible
250(all the intervening jumps are short).
251If, in this situation, there is a branch instruction $b$ whose span is not
252within the range for a short jump, we can be sure that we can never reach a
253situation where the span of $j$ is so small that it can be encoded as a short
254jump. This argument continues to hold throughout the subsequent iterations of
255the algorithm: short jumps can change into long jumps, but not \emph{vice versa},
256as spans only increase. Hence, the algorithm either terminates early when a fixed
257point is reached or when all short jumps have been changed into long jumps.
259Also, we can be certain that we have reached an optimal solution: a short jump
260is only changed into a long jump if it is absolutely necessary.
262However, neither of these claims (termination nor optimality) hold when we add
263the absolute jump. With absolute jumps, the encoding of a branch
264instruction no longer depends only on the distance between the branch
265instruction and its target. An absolute jump is possible when instruction and
266target are in the same segment (for the MCS-51, this means that the first 5
267bytes of their addresses have to be equal). It is therefore entirely possible
268for two branch instructions with the same span to be encoded in different ways
269(absolute if the branch instruction and its target are in the same segment,
270long if this is not the case).
276    jmp X
277    \ldots
278L\(\sb{0}\): \ldots
279% Start of new segment if
280% jmp X is encoded as short
281    \ldots
282    jmp L\(\sb{0}\)
284\caption{Example of a program where a long jump becomes absolute}
291L\(\sb{0}\): jmp X
292X:  \ldots
293    \ldots
294L\(\sb{1}\): \ldots
295% Start of new segment if
296% jmp X is encoded as short
297    \ldots
298    jmp L\(\sb{1}\)
299    \ldots
300    jmp L\(\sb{1}\)
301    \ldots
302    jmp L\(\sb{1}\) 
303    \ldots
305\caption{Example of a program where the fixed-point algorithm is not optimal}
310This invalidates our earlier termination argument: a branch instruction, once encoded
311as a long jump, can be re-encoded during a later iteration as an absolute jump.
312Consider the program shown in Figure~\ref{f:term_example}. At the start of the
313first iteration, both the branch to {\tt X} and the branch to $\mathtt{L}_{0}$
314are encoded as small jumps. Let us assume that in this case, the placement of
315$\mathtt{L}_{0}$ and the branch to it are such that $\mathtt{L}_{0}$ is just
316outside the segment that contains this branch. Let us also assume that the
317distance between $\mathtt{L}_{0}$ and the branch to it is too large for the
318branch instruction to be encoded as a short jump.
320All this means that in the second iteration, the branch to $\mathtt{L}_{0}$ will
321be encoded as a long jump. If we assume that the branch to {\tt X} is encoded as
322a long jump as well, the size of the branch instruction will increase and
323$\mathtt{L}_{0}$ will be `propelled' into the same segment as its branch
324instruction, because every subsequent instruction will move one byte forward.
325Hence, in the third iteration, the branch to $\mathtt{L}_{0}$ can be encoded as
326an absolute jump. At first glance, there is nothing that prevents us from
327constructing a configuration where two branch instructions interact in such a
328way as to iterate indefinitely between long and absolute encodings.
330This situation mirrors the explanation by Szymanski~\cite{Szymanski1978} of why
331the branch displacement optimisation problem is NP-complete. In this explanation,
332a condition for NP-completeness is the fact that programs be allowed to contain
333{\em pathological} jumps. These are branch instructions that can normally not be
334encoded as a short(er) jump, but gain this property when some other branch
335instructions are encoded as a long(er) jump. This is exactly what happens in
336Figure~\ref{f:term_example}. By encoding the first branch instruction as a long
337jump, another branch instruction switches from long to absolute (which is
340In addition, our previous optimality argument no longer holds. Consider the
341program shown in Figure~\ref{f:opt_example}. Suppose that the distance between
342$\mathtt{L}_{0}$ and $\mathtt{L}_{1}$ is such that if {\tt jmp X} is encoded
343as a short jump, there is a segment border just after $\mathtt{L}_{1}$. Let
344us also assume that all three branches to $\mathtt{L}_{1}$ are in the same
345segment, but far enough away from $\mathtt{L}_{1}$ that they cannot be encoded
346as short jumps.
348Then, if {\tt jmp X} were to be encoded as a short jump, which is clearly
349possible, all of the branches to $\mathtt{L}_{1}$ would have to be encoded as
350long jumps. However, if {\tt jmp X} were to be encoded as a long jump, and
351therefore increase in size, $\mathtt{L}_{1}$ would be `propelled' across the
352segment border, so that the three branches to $\mathtt{L}_{1}$ could be encoded
353as absolute jumps. Depending on the relative sizes of long and absolute jumps,
354this solution might actually be smaller than the one reached by the smallest
355fixed point algorithm.
357\section{Our algorithm}
359\subsection{Design decisions}
361Given the NP-completeness of the problem, finding optimal solutions
362(using, for example, a constraint solver) can potentially be very costly.
364The SDCC compiler~\cite{SDCC2011}, which has a backend targeting the MCS-51
365instruction set, simply encodes every branch instruction as a long jump
366without taking the distance into account. While certainly correct (the long
367jump can reach any destination in memory) and a very fast solution to compute,
368it results in a less than optimal solution in terms of output size and
369execution time.
371On the other hand, the {\tt gcc} compiler suite, while compiling
372C on the x86 architecture, uses a greatest fix point algorithm. In other words,
373it starts with all branch instructions encoded as the largest jumps
374available, and then tries to reduce the size of branch instructions as much as
377Such an algorithm has the advantage that any intermediate result it returns
378is correct: the solution where every branch instruction is encoded as a large
379jump is always possible, and the algorithm only reduces those branch
380instructions whose destination address is in range for a shorter jump.
381The algorithm can thus be stopped after a determined number of steps without
382sacrificing correctness.
384The result, however, is not necessarily optimal. Even if the algorithm is run
385until it terminates naturally, the fixed point reached is the {\em greatest}
386fixed point, not the least fixed point. Furthermore, {\tt gcc} (at least for
387the x86 architecture) only uses short and long jumps. This makes the algorithm
388more efficient, as shown in the previous section, but also results in a less
389optimal solution.
391In the CerCo assembler, we opted at first for a least fixed point algorithm,
392taking absolute jumps into account.
394Here, we ran into a problem with proving termination, as explained in the
395previous section: if we only take short and long jumps into account, the jump
396encoding can only switch from short to long, but never in the other direction.
397When we add absolute jumps, however, it is theoretically possible for a branch
398instruction to switch from absolute to long and back, as previously explained.
399Proving termination then becomes difficult, because there is nothing that
400precludes a branch instruction from oscillating back and forth between absolute
401and long jumps indefinitely.
403To keep the algorithm in the same complexity class and more easily
404prove termination, we decided to explicitly enforce the `branch instructions
405must always grow longer' requirement: if a branch instruction is encoded as a
406long jump in one iteration, it will also be encoded as a long jump in all the
407following iterations. Therefore the encoding of any branch instruction
408can change at most two times: once from short to absolute (or long), and once
409from absolute to long.
411There is one complicating factor. Suppose that a branch instruction is encoded
412in step $n$ as an absolute jump, but in step $n+1$ it is determined that
413(because of changes elsewhere) it can now be encoded as a short jump. Due to
414the requirement that the branch instructions must always grow longer,
415the branch encoding will be encoded as an absolute jump in step
416$n+1$ as well.
418This is not necessarily correct. A branch instruction that can be
419encoded as a short jump cannot always also be encoded as an absolute jump, as a
420short jump can bridge segments, whereas an absolute jump cannot. Therefore,
421in this situation we have decided to encode the branch instruction as a long
422jump, which is always correct.
424The resulting algorithm, therefore, will not return the least fixed point, as
425it might have too many long jumps. However, it is still better than the
426algorithms from SDCC and {\tt gcc}, since even in the worst case, it will still
427return a smaller or equal solution.
429Experimenting with our algorithm on the test suite of C programs included with
430gcc 2.3.3 has shown that on average, about 25 percent of jumps are encoded as short or absolute jumps by the algorithm. As not all instructions are jumps, this does not make for a large reduction in size, but it can make for a reduction in execution time: if jumps
431are executed multiple times, for example in loops, the fact that short jumps take less cycles to execute than long jumps can have great effect.
433As for complexity, there are at most $2n$ iterations, where $n$ is the number of
434branch instructions. Practical tests within the CerCo project on small to
435medium pieces of code have shown that in almost all cases, a fixed point is
436reached in 3 passes. Only in one case did the algorithm need 4. This is not surprising: after all, the difference between short/absolute and
437long jumps is only one byte (three for conditional jumps). For a change from
438short/absolute to long to have an effect on other jumps is therefore relatively
439uncommon, which explains why a fixed point is reached so quickly.
441\subsection{The algorithm in detail}
443The branch displacement algorithm forms part of the translation from
444pseudocode to assembler. More specifically, it is used by the function that
445translates pseudo-addresses (natural numbers indicating the position of the
446instruction in the program) to actual addresses in memory. Note that in pseudocode, all instructions are of size 1.
448Our original intention was to have two different functions, one function
449$\mathtt{policy}: \mathbb{N} \rightarrow \{\mathtt{short\_jump},
450\mathtt{absolute\_jump}, \mathtt{long\_jump}\}$ to associate jumps to their
451intended encoding, and a function $\sigma: \mathbb{N} \rightarrow
452\mathtt{Word}$ to associate pseudo-addresses to machine addresses. $\sigma$
453would use $\mathtt{policy}$ to determine the size of jump instructions. This turned out to be suboptimal from the algorithmic point of view and
454impossible to prove correct.
456From the algorithmic point of view, in order to create the $\mathtt{policy}$
457function, we must necessarily have a translation from pseudo-addresses
458to machine addresses (i.e. a $\sigma$ function): in order to judge the distance
459between a jump and its destination, we must know their memory locations.
460Conversely, in order to create the $\sigma$ function, we need to have the
461$\mathtt{policy}$ function, otherwise we do not know the sizes of the jump
462instructions in the program.
464Much the same problem appears when we try to prove the algorithm correct: the
465correctness of $\mathtt{policy}$ depends on the correctness of $\sigma$, and
466the correctness of $\sigma$ depends on the correctness of $\mathtt{policy}$.
468We solved this problem by integrating the $\mathtt{policy}$ and $\sigma$
469algorithms. We now have a function
470$\sigma: \mathbb{N} \rightarrow \mathtt{Word} \times \mathtt{bool}$ which
471associates a pseudo-address to a machine address. The boolean denotes a forced
472long jump; as noted in the previous section, if during the fixed point
473computation an absolute jump changes to be potentially re-encoded as a short
474jump, the result is actually a long jump. It might therefore be the case that
475jumps are encoded as long jumps without this actually being necessary, and this
476information needs to be passed to the code generating function.
478The assembler function encodes the jumps by checking the distance between
479source and destination according to $\sigma$, so it could select an absolute
480jump in a situation where there should be a long jump. The boolean is there
481to prevent this from happening by indicating the locations where a long jump
482should be encoded, even if a shorter jump is possible. This has no effect on
483correctness, since a long jump is applicable in any situation.
489  \State $\langle added, pc, sigma \rangle \gets acc$
490  \If {$instr$ is a backward jump to $j$}
491    \State $length \gets \mathrm{jump\_size}(pc,sigma_1(labels(j)))$
492    \Comment compute jump distance
493  \ElsIf {$instr$ is a forward jump to $j$}
494    \State $length \gets \mathrm{jump\_size}(pc,old\_sigma_1(labels(j))+added)$
495  \EndIf
496  \State $old\_length \gets \mathrm{old\_sigma_1}(ppc)$
497  \State $new\_length \gets \mathrm{max}(old\_length, length)$
498  \Comment length must never decrease
499  \State $old\_size \gets \mathrm{old\_sigma_2}(ppc)$
500  \State $new\_size \gets \mathrm{instruction\_size}(instr,new\_length)$
501  \Comment compute size in bytes
502  \State $new\_added \gets added+(new\_size-old\_size)$
503  \Comment keep track of total added bytes
504  \State $new\_sigma \gets old\_sigma$
505  \State $new\_sigma_1(ppc+1) \gets pc+new\_size$
506  \State $new\_sigma_2(ppc) \gets new\_length$
507  \Comment update $\sigma$ \\
508  \Return $\langle new\_added, pc+new\_size, new\_sigma \rangle$
511\caption{The heart of the algorithm}
515The algorithm, shown in Figure~\ref{f:jump_expansion_step}, works by folding the
516function {\sc f} over the entire program, thus gradually constructing $sigma$.
517This constitutes one step in the fixed point calculation; successive steps
518repeat the fold until a fixed point is reached. We have abstracted away the case where an instruction is not a jump, since the size of these instructions is constant.
520Parameters of the function {\sc f} are:
522  \item a function $labels$ that associates a label to its pseudo-address;
523  \item $old\_sigma$, the $\sigma$ function returned by the previous
524    iteration of the fixed point calculation;
525  \item $instr$, the instruction currently under consideration;
526  \item $ppc$, the pseudo-address of $instr$;
527  \item $acc$, the fold accumulator, which contains $added$ (the number of
528  bytes added to the program size with respect to the previous iteration), $pc$
529  (the highest memory address reached so far), and of course $sigma$, the
530    $\sigma$ function under construction.
532The first two are parameters that remain the same through one iteration, the
533final three are standard parameters for a fold function (including $ppc$,
534which is simply the number of instructions of the program already processed).
536The $\sigma$ functions used by {\sc f} are not of the same type as the final
537$\sigma$ function: they are of type
538$\sigma: \mathbb{N} \rightarrow \mathbb{N} \times \{\mathtt{short\_jump},
539\mathtt{absolute\_jump},\mathtt{long\_jump}\}$; a function that associates a
540pseudo-address with a memory address and a jump length. We do this to
541ease the comparison of jump lengths between iterations. In the algorithm,
542we use the notation $sigma_1(x)$ to denote the memory address corresponding to
543$x$, and $sigma_2(x)$ for the jump length corresponding to $x$.
545Note that the $\sigma$ function used for label lookup varies depending on
546whether the label is behind our current position or ahead of it. For
547backward branches, where the label is behind our current position, we can use
548$sigma$ for lookup, since its memory address is already known. However, for
549forward branches, the memory address of the address of the label is not yet
550known, so we must use $old\_sigma$.
552We cannot use $old\_sigma$ without change: it might be the case that we have
553already increased the size of some branch instructions before, making the
554program longer and moving every instruction forward. We must compensate for this
555by adding the size increase of the program to the label's memory address
556according to $old\_sigma$, so that branch instruction spans do not get
559%Note also that we add the pc to $sigma$ at location $ppc+1$, whereas we add the
560%jump length at location $ppc$. We do this so that $sigma(ppc)$ will always
561%return a pair with the start address of the instruction at $ppc$ and the
562%length of its branch instruction (if any); the end address of the program can
563%be found at $sigma(n+1)$, where $n$ is the number of instructions in the
566\section{The proof}
568In this section, we present the correctness proof for the algorithm in more
569detail. The main correctness statement is shown, slightly simplified, in~Figure~\ref{statement}.
574\mathtt{sigma}&\omit\rlap{$\mathtt{\_policy\_specification} \equiv
575\lambda program.\lambda sigma.$} \notag\\
576  & \omit\rlap{$sigma\ 0 = 0\ \wedge$} \notag\\
577  & \mathbf{let}\ & & \omit\rlap{$instr\_list \equiv code\ program\ \mathbf{in}$} \notag\\
578  &&& \omit\rlap{$\forall ppc.ppc < |instr\_list| \rightarrow$} \notag\\
579  &&& \mathbf{let}\ && pc \equiv sigma\ ppc\ \mathbf{in} \notag\\
580  &&& \mathbf{let}\ && instruction \equiv \mathtt{fetch\_pseudo\_instruction}\ instr\_list\ ppc\ \mathbf{in} \notag\\
581  &&& \mathbf{let}\ && next\_pc \equiv sigma\ (ppc+1)\ \mathbf{in}\notag\\
582  &&&&& next\_pc = pc + \mathtt{instruction\_size}\ sigma\ ppc\ instruction\ \wedge\notag\\
583  &&&&& (pc + \mathtt{instruction\_size}\ sigma\ ppc\ instruction < 2^{16}\ \vee\notag\\
584  &&&&& (\forall ppc'.ppc' < |instr\_list| \rightarrow ppc < ppc' \rightarrow \notag\\
585  &&&&& \mathbf{let}\ instruction' \equiv \mathtt{fetch\_pseudo\_instruction}\ instr\_list\ ppc'\ \mathbf{in} \notag\\
586  &&&&&\ \mathtt{instruction\_size}\ sigma\ ppc'\ instruction' = 0)\ \wedge \notag\\
587  &&&&& pc + \mathtt{instruction\_size}\ sigma\ ppc\ instruction = 2^{16})
589\caption{Main correctness statement\label{statement}}
593Informally, this means that when fetching a pseudo-instruction at $ppc$, the
594translation by $\sigma$ of $ppc+1$ is the same as $\sigma(ppc)$ plus the size
595of the instruction at $ppc$.  That is, an instruction is placed consecutively
596after the previous one, and there are no overlaps. The rest of the statement deals with memory size: either the next instruction fits within memory ($next\_pc < 2^{16}$) or it ends exactly at the limit memory,
597in which case it must be the last translated instruction in the program (enforced by specfiying that the size of all subsequent instructions is 0: there may be comments or cost annotations that are not translated).
599Finally, we enforce that the program starts at address 0, i.e. $\sigma(0) = 0$. It may seem strange that we do not explicitly include a safety property stating that every jump instruction is of the right type with respect to its target (akin to the lemma from Figure~\ref{sigmasafe}), but this is not necessary. The distance is recalculated according to the instruction addresses from $\sigma$, which implicitly expresses safety.
601Since our computation is a least fixed point computation, we must prove
602termination in order to prove correctness: if the algorithm is halted after
603a number of steps without reaching a fixed point, the solution is not
604guaranteed to be correct. More specifically, branch instructions might be
605encoded which do not coincide with the span between their location and their
608Proof of termination rests on the fact that the encoding of branch
609instructions can only grow larger, which means that we must reach a fixed point
610after at most $2n$ iterations, with $n$ the number of branch instructions in
611the program. This worst case is reached if at every iteration, we change the
612encoding of exactly one branch instruction; since the encoding of any branch
613instruction can change first from short to absolute, and then to long, there
614can be at most $2n$ changes.
616%The proof has been carried out using the ``Russell'' style from~\cite{Sozeau2006}.
617%We have proven some invariants of the {\sc f} function from the previous
618%section; these invariants are then used to prove properties that hold for every
619%iteration of the fixed point computation; and finally, we can prove some
620%properties of the fixed point.
622\subsection{Fold invariants}
624In this section, we present the invariants that hold during the fold of {\sc f}
625over the program. These will be used later on to prove the properties of the
626iteration. During the fixed point computation, the $\sigma$ function is
627implemented as a trie for ease of access; computing $\sigma(x)$ is achieved by
628looking up the value of $x$ in the trie. Actually, during the fold, the value
629we pass along is a pair $\mathbb{N} \times \mathtt{ppc\_pc\_map}$. The first
630component is the number of bytes added to the program so far with respect to
631the previous iteration, and the second component, {\tt ppc\_pc\_map}, is the
632actual $\sigma$ trie (which we'll call $strie$ to avoid confusion).
636\mathtt{out} & \mathtt{\_of\_program\_none} \equiv \lambda prefix.\lambda strie. \notag\\
637& \forall i.i < 2^{16} \rightarrow (i > |prefix| \leftrightarrow
638 \mathtt{lookup\_opt}\ i\ (\mathtt{snd}\ strie) = \mathtt{None})
641The first invariant states that any pseudo-address not yet examined is not
642present in the lookup trie.
646\mathtt{not} & \mathtt{\_jump\_default} \equiv \lambda prefix.\lambda strie.\forall i.i < |prefix| \rightarrow\notag\\
647& \neg\mathtt{is\_jump}\ (\mathtt{nth}\ i\ prefix) \rightarrow \mathtt{lookup}\ i\ (\mathtt{snd}\ strie) = \mathtt{short\_jump}
650This invariant states that when we try to look up the jump length of a
651pseudo-address where there is no branch instruction, we will get the default
652value, a short jump.
656\mathtt{jump} & \mathtt{\_increase} \equiv \lambda pc.\lambda op.\lambda p.\forall i.i < |prefix| \rightarrow \notag\\ 
657& \mathbf{let}\  oj \equiv \mathtt{lookup}\ i\ (\mathtt{snd}\ op)\ \mathbf{in} \notag\\
658& \mathbf{let}\ j \equiv \mathtt{lookup}\ i\ (\mathtt{snd}\ p)\ \mathbf{in}\ \mathtt{jmpleq}\ oj\ j
661This invariant states that between iterations (with $op$ being the previous
662iteration, and $p$ the current one), jump lengths either remain equal or
663increase. It is needed for proving termination.
668\mathtt{sigma} & \omit\rlap{$\mathtt{\_compact\_unsafe} \equiv \lambda prefix.\lambda strie.\forall n.n < |prefix| \rightarrow$}\notag\\
669& \mathbf{match}\ && \omit\rlap{$\mathtt{lookup\_opt}\ n\ (\mathtt{snd}\ strie)\ \mathbf{with}$}\notag\\
670&&& \omit\rlap{$\mathtt{None} \Rightarrow \mathrm{False}$} \notag\\
671&&& \omit\rlap{$\mathtt{Some}\ \langle pc, j \rangle \Rightarrow$} \notag\\
672&&& \mathbf{match}\ && \mathtt{lookup\_opt}\ (n+1)\ (\mathtt{snd}\ strie)\ \mathbf{with}\notag\\
673&&&&& \mathtt{None} \Rightarrow \mathrm{False} \notag\\
674&&&&& \mathtt{Some}\ \langle pc_1, j_1 \rangle \Rightarrow
675    pc_1 = pc + \notag\\
676&&&&& \ \ \mathtt{instruction\_size\_jmplen}\ j\ (\mathtt{nth}\ n\ prefix)
678\caption{Temporary safety property}
682We now proceed with the safety lemmas. The lemma in
683Figure~\ref{sigmacompactunsafe} is a temporary formulation of the main
684property {\tt sigma\_policy\_specification}. Its main difference from the
685final version is that it uses {\tt instruction\_size\_jmplen} to compute the
686instruction size. This function uses $j$ to compute the span of branch
687instructions  (i.e. it uses the $\sigma$ under construction), instead
688of looking at the distance between source and destination. This is because
689$\sigma$ is still under construction; we will prove below that after the
690final iteration, {\tt sigma\_compact\_unsafe} is equivalent to the main
691property in Figure~\ref{sigmasafe} which holds at the end of the computation.
696\mathtt{sigma} & \omit\rlap{$\mathtt{\_safe} \equiv \lambda prefix.\lambda labels.\lambda old\_strie.\lambda strie.\forall i.i < |prefix| \rightarrow$} \notag\\
697& \omit\rlap{$\forall dest\_label.\mathtt{is\_jump\_to\ (\mathtt{nth}\ i\ prefix})\ dest\_label \rightarrow$} \notag\\
698& \mathbf{let} && \omit\rlap{$\ paddr \equiv \mathtt{lookup}\ labels\ dest\_label\ \mathbf{in}$} \notag\\
699& \mathbf{let} && \omit\rlap{$\ \langle j, src, dest \rangle \equiv \mathbf{if} \ paddr\ \leq\ i\ \mathbf{then}$}\notag\\
700&&&&& \mathbf{let}\ \langle \_, j \rangle \equiv \mathtt{lookup}\ i\ (\mathtt{snd}\ strie)\ \mathbf{in} \notag\\
701&&&&& \mathbf{let}\ \langle pc\_plus\_jl, \_ \rangle \equiv \mathtt{lookup}\ (i+1)\ (\mathtt{snd}\ strie)\ \mathbf{in}\notag\\
702&&&&& \mathbf{let}\ \langle addr, \_ \rangle \equiv \mathtt{lookup}\ paddr\ (\mathtt{snd}\ strie)\ \mathbf{in}\notag\\
703&&&&& \langle j, pc\_plus\_jl, addr \rangle\notag\\
704&&&\mathbf{else} \notag\\
705&&&&&\mathbf{let}\ \langle \_, j \rangle \equiv \mathtt{lookup}\ i\ (\mathtt{snd}\ strie)\ \mathbf{in} \notag\\
706&&&&&\mathbf{let}\ \langle pc\_plus\_jl, \_ \rangle \equiv \mathtt{lookup}\ (i+1)\ (\mathtt{snd}\ old\_strie)\ \mathbf{in}\notag\\
707&&&&&\mathbf{let}\ \langle addr, \_ \rangle \equiv \mathtt{lookup}\ paddr\ (\mathtt{snd}\ old\_strie)\ \mathbf{in}\notag\\
708&&&&&\langle j, pc\_plus\_jl, addr \rangle \mathbf{in}\ \notag\\
709&&&\mathbf{match} && \ j\ \mathbf{with} \notag\\
710&&&&&\mathrm{short\_jump} \Rightarrow \mathtt{short\_jump\_valid}\ src\ dest\notag\\
711&&&&&\mathrm{absolute\_jump} \Rightarrow \mathtt{absolute\_jump\_valid}\ src\ dest\notag\\
712&&&&&\mathrm{long\_jump} \Rightarrow \mathrm{True}
714\caption{Safety property}
718We compute the distance using the memory address of the instruction
719plus its size. This follows the behaviour of the MCS-51 microprocessor, which
720increases the program counter directly after fetching, and only then executes
721the branch instruction (by changing the program counter again).
723There are also some simple, properties to make sure that our policy
724remains consistent, and to keep track of whether the fixed point has been
725reached. We do not include them here in detail. Two of these properties give the values of $\sigma$ for the start and end of the program; $\sigma(0) = 0$ and $\sigma(n)$, where $n$ is the number of instructions up until now, is equal to the maximum memory address so far. There are also two properties that deal with what happens when the previous
726iteration does not change with respect to the current one. $added$ is a
727variable that keeps track of the number of bytes we have added to the program
728size by changing the encoding of branch instructions. If $added$ is 0, the program
729has not changed and vice versa.
733%& \mathtt{lookup}\ 0\ (\mathtt{snd}\ strie) = 0 \notag\\
734%& \mathtt{lookup}\ |prefix|\ (\mathtt{snd}\ strie) = \mathtt{fst}\ strie
740%& added = 0\ \rightarrow\ \mathtt{policy\_pc\_equal}\ prefix\ old\_strie\ strie \notag\\
741%& \mathtt{policy\_jump\_equal}\ prefix\ old\_strie\ strie\ \rightarrow\ added = 0
744We need to use two different formulations, because the fact that $added$ is 0
745does not guarantee that no branch instructions have changed.  For instance,
746it is possible that we have replaced a short jump with an absolute jump, which
747does not change the size of the branch instruction. Therefore {\tt policy\_pc\_equal} states that $old\_sigma_1(x) = sigma_1(x)$, whereas {\tt policy\_jump\_equal} states that $old\_sigma_2(x) = sigma_2(x)$. This formulation is sufficient to prove termination and compactness. 
749Proving these invariants is simple, usually by induction on the prefix length.
751\subsection{Iteration invariants}
753These are invariants that hold after the completion of an iteration. The main
754difference between these invariants and the fold invariants is that after the
755completion of the fold, we check whether the program size does not supersede
75664 Kb, the maximum memory size the MCS-51 can address. The type of an iteration therefore becomes an option type: {\tt None} in case
757the program becomes larger than 64 Kb, or $\mathtt{Some}\ \sigma$
758otherwise. We also no longer pass along the number of bytes added to the
759program size, but a boolean that indicates whether we have changed something
760during the iteration or not.
762If the iteration returns {\tt None}, which means that it has become too large for memory, there is an invariant that states that the previous iteration cannot
763have every branch instruction encoded as a long jump. This is needed later in the proof of termination. If the iteration returns $\mathtt{Some}\ \sigma$, the fold invariants are retained without change.
765Instead of using {\tt sigma\_compact\_unsafe}, we can now use the proper
770\mathtt{sigma} & \omit\rlap{$\mathtt{\_compact} \equiv \lambda program.\lambda sigma.$} \notag\\
771& \omit\rlap{$\forall n.n < |program|\ \rightarrow$} \notag\\
772& \mathbf{match}\ && \omit\rlap{$\mathtt{lookup\_opt}\ n\ (\mathtt{snd}\ sigma)\ \mathbf{with}$}\notag\\
773&&& \omit\rlap{$\mathrm{None}\ \Rightarrow\ \mathrm{False}$}\notag\\
774&&& \omit\rlap{$\mathrm{Some}\ \langle pc, j \rangle \Rightarrow$}\notag\\
775&&& \mathbf{match}\ && \mathtt{lookup\_opt}\ (n+1)\ (\mathtt{snd}\ sigma)\ \mathbf{with}\notag\\
776&&&&& \mathrm{None}\ \Rightarrow\ \mathrm{False}\notag\\
777&&&&& \mathrm{Some} \langle pc1, j1 \rangle \Rightarrow\notag\\
778&&&&& \ \ pc1 = pc + \mathtt{instruction\_size}\ n\ (\mathtt{nth}\ n\ program)
781This is almost the same invariant as ${\tt sigma\_compact\_unsafe}$, but differs in that it
782computes the sizes of branch instructions by looking at the distance between
783position and destination using $\sigma$. In actual use, the invariant is qualified: $\sigma$ is compact if there have
784been no changes (i.e. the boolean passed along is {\tt true}). This is to
785reflect the fact that we are doing a least fixed point computation: the result
786is only correct when we have reached the fixed point.
788There is another, trivial, invariant in case the iteration returns
789$\mathtt{Some}\ \sigma$: it must hold that $\mathtt{fst}\ sigma < 2^{16}$.
790We need this invariant to make sure that addresses do not overflow.
792The proof of {\tt nec\_plus\_ultra} goes as follows: if we return {\tt None},
793then the program size must be greater than 64 Kb. However, since the
794previous iteration did not return {\tt None} (because otherwise we would
795terminate immediately), the program size in the previous iteration must have
796been smaller than 64 Kb.
798Suppose that all the branch instructions in the previous iteration are
799encoded as long jumps. This means that all branch instructions in this
800iteration are long jumps as well, and therefore that both iterations are equal
801in the encoding of their branch instructions. Per the invariant, this means that
802$added = 0$, and therefore that all addresses in both iterations are equal.
803But if all addresses are equal, the program sizes must be equal too, which
804means that the program size in the current iteration must be smaller than
80564 Kb. This contradicts the earlier hypothesis, hence not all branch
806instructions in the previous iteration are encoded as long jumps.
808The proof of {\tt sigma\_compact} follows from {\tt sigma\_compact\_unsafe} and
809the fact that we have reached a fixed point, i.e. the previous iteration and
810the current iteration are the same. This means that the results of
811{\tt instruction\_size\_jmplen} and {\tt instruction\_size} are the same.
813\subsection{Final properties}
815These are the invariants that hold after $2n$ iterations, where $n$ is the
816program size (we use the program size for convenience; we could also use the
817number of branch instructions, but this is more complex). Here, we only
818need {\tt out\_of\_program\_none}, {\tt sigma\_compact} and the fact that
819$\sigma(0) = 0$.
821Termination can now be proved using the fact that there is a $k \leq 2n$, with
822$n$ the length of the program, such that iteration $k$ is equal to iteration
823$k+1$. There are two possibilities: either there is a $k < 2n$ such that this
824property holds, or every iteration up to $2n$ is different. In the latter case,
825since the only changes between the iterations can be from shorter jumps to
826longer jumps, in iteration $2n$ every branch instruction must be encoded as
827a long jump. In this case, iteration $2n$ is equal to iteration $2n+1$ and the
828fixed point is reached.
832In the previous sections we have discussed the branch displacement optimisation
833problem, presented an optimised solution, and discussed the proof of
834termination and correctness for this algorithm, as formalised in Matita.
836The algorithm we have presented is fast and correct, but not optimal; a true
837optimal solution would need techniques like constraint solvers. While outside
838the scope of the present research, it would be interesting to see if enough
839heuristics could be found to make such a solution practical for implementing
840in an existing compiler; this would be especially useful for embedded systems,
841where it is important to have as small a solution as possible.
843In itself the algorithm is already useful, as it results in a smaller solution
844than the simple `every branch instruction is long' used up until now---and with
845only 64 Kb of memory, every byte counts. It also results in a smaller solution
846than the greatest fixed point algorithm that {\tt gcc} uses. It does this
847without sacrificing speed or correctness.
849The certification of an assembler that relies on the branch displacement
850algorithm described in this paper was presented in~\cite{lastyear}.
851The assembler computes the $\sigma$ map as described in this paper and
852then works in two passes. In the first pass it builds a map
853from instruction labels to addresses in the assembly code. In the
854second pass it iterates over the code, translating every pseudo jump
855at address $src$ to a label l associated to the assembly instruction at
856address $dst$ to a jump of the size dictated by $(\sigma\ src)$ to
857$(\sigma\ dst)$. In case of conditional jumps, the translated jump may be
858implemented with a series of instructions.
860The proof of correctness abstracts over the algorithm used and only relies on
861{\tt sigma\_policy\_specification} (page~\ref{sigmapolspec}). It is a variation
862of a standard 1-to-many forward simulation proof~\cite{Leroy2009}. The
863relation R between states just maps every code address $ppc$ stored in
864registers or memory to $(\sigma\ ppc)$. To identify the code addresses,
865an additional data structure is always kept together with the source
866state and is updated by the semantics. The semantics is preserved
867only for those programs whose source code operations
868$(f\ ppc_1\ \ldots\ ppc_n)$ applied to code addresses $ppc_1 \ldots ppc_n$ are
869such that $(f\ (\sigma\ ppc_1)\ ...\ (\sigma\ ppc_n) = f\ ppc_1\ ppc_n))$. For
870example, an injective $\sigma$ preserves a binary equality test f for code
871addresses, but not pointer subtraction.
873The main lemma (fetching simulation), which relies on\\
874{\tt sigma\_policy\_specification} and is established by structural induction
875over the source code, says that fetching an assembly instruction at
876position ppc is equal to fetching the translation of the instruction at
877position $(\sigma\ ppc)$, and that the new incremented program counter is at
878the beginning of the next instruction (compactness). The only exception is
879when the instruction fetched is placed at the end of code memory and is
880followed only by dead code. Execution simulation is trivial because of the
881restriction over well behaved programs w.r.t. sigma. The condition
882$\sigma\ 0 = 0$ is necessary because the hardware model prescribes that the
883first instruction to be executed will be at address 0. For the details
886Instead of verifying the algorithm directly, another solution to the problem
887would be to run an optimisation algorithm, and then verify the safety of the
888result using a verified validator. Such a validator would be easier to verify
889than the algorithm itself and it would also be efficient, requiring only a
890linear pass over the source code to test the specification. However, it is
891surely also interesting to formally prove that the assembler never rejects
892programs that should be accepted, i.e. that the algorithm itself is correct.
893This is the topic of the current paper.
895\subsection{Related work}
897As far as we are aware, this is the first formal discussion of the branch
898displacement optimisation algorithm.
900The CompCert project is another verified compiler project.
901Their backend~\cite{Leroy2009} generates assembly code for (amongst others) subsets of the
902PowerPC and x86 (32-bit) architectures. At the assembly code stage, there is
903no distinction between the span-dependent jump instructions, so a branch
904displacement optimisation algorithm is not needed.
906%An offshoot of the CompCert project is the CompCertTSO project, which adds
907%thread concurrency and synchronisation to the CompCert compiler~\cite{TSO2011}.
908%This compiler also generates assembly code and therefore does not include a
909%branch displacement algorithm.
911%Finally, there is also the Piton stack~\cite{Moore1996}, which not only includes the
912%formal verification of a compiler, but also of the machine architecture
913%targeted by that compiler, a microprocessor called the FM9001.
914%However, this architecture does not have different
915%jump sizes (branching is simulated by assigning values to the program counter),
916%so the branch displacement problem is irrelevant.
Note: See TracBrowser for help on using the repository browser.