source: src/ASM/TACAS2013-policy/conclusion.tex @ 3415

\section{Conclusion}

In the previous sections we have discussed the branch displacement optimisation
problem, presented an optimised solution, and discussed the proof of
termination and correctness for this algorithm, as formalised in Matita.

The algorithm we have presented is fast and correct, but not optimal; a true
optimal solution would need techniques like constraint solvers. While outside
the scope of the present research, it would be interesting to see if enough
heuristics could be found to make such a solution practical for implementing
in an existing compiler; this would be especially useful for embedded systems,
where it is important to have as small a solution as possible.

In itself the algorithm is already useful, as it results in a smaller solution
than the simple `every branch instruction is long' used up until now---and with
only 64 Kb of memory, every byte counts. It also results in a smaller solution
than the greatest fixed point algorithm that {\tt gcc} uses. It does this
without sacrificing speed or correctness.

The certification of an assembler that relies on the branch displacement
algorithm described in this paper was presented in~\cite{lastyear}.
The assembler computes the $\sigma$ map as described in this paper and
then works in two passes. In the first pass it builds a map 
from instruction labels to addresses in the assembly code. In the 
second pass it iterates over the code, translating every pseudo jump
at address $src$ to a label l associated to the assembly instruction at
address $dst$ to a jump of the size dictated by $(\sigma\ src)$ to
$(\sigma\ dst)$. In case of conditional jumps, the translated jump may be 
implemented with a series of instructions.

The proof of correctness abstracts over the algorithm used and only relies on
{\tt sigma\_policy\_specification} (page~\ref{sigmapolspec}). It is a variation
of a standard 1-to-many forward simulation proof~\cite{Leroy2009}. The
relation R between states just maps every code address $ppc$ stored in 
registers or memory to $(\sigma\ ppc)$. To identify the code addresses,
an additional data structure is always kept together with the source
state and is updated by the semantics. The semantics is preserved
only for those programs whose source code operations
$(f\ ppc_1\ \ldots\ ppc_n)$ applied to code addresses $ppc_1 \ldots ppc_n$ are
such that $(f\ (\sigma\ ppc_1)\ ...\ (\sigma\ ppc_n) = f\ ppc_1\ ppc_n))$. For
example, an injective $\sigma$ preserves a binary equality test f for code
addresses, but not pointer subtraction.

The main lemma (fetching simulation), which relies on\\
{\tt sigma\_policy\_specification} and is established by structural induction
over the source code, says that fetching an assembly instruction at
position ppc is equal to fetching the translation of the instruction at
position $(\sigma\ ppc)$, and that the new incremented program counter is at
the beginning of the next instruction (compactness). The only exception is
when the instruction fetched is placed at the end of code memory and is
followed only by dead code. Execution simulation is trivial because of the
restriction over well behaved programs w.r.t. sigma. The condition
$\sigma\ 0 = 0$ is necessary because the hardware model prescribes that the
first instruction to be executed will be at address 0. For the details
see~\cite{lastyear}.

Instead of verifying the algorithm directly, another solution to the problem
would be to run an optimisation algorithm, and then verify the safety of the
result using a verified validator. Such a validator would be easier to verify
than the algorithm itself and it would also be efficient, requiring only a
linear pass over the source code to test the specification. However, it is
surely also interesting to formally prove that the assembler never rejects
programs that should be accepted, i.e. that the algorithm itself is correct.
This is the topic of the current paper.

\subsection{Related work}

As far as we are aware, this is the first formal discussion of the branch
displacement optimisation algorithm.

The CompCert project is another verified compiler project.
Their backend~\cite{Leroy2009} generates assembly code for (amongst others) subsets of the
PowerPC and x86 (32-bit) architectures. At the assembly code stage, there is
no distinction between the span-dependent jump instructions, so a branch
displacement optimisation algorithm is not needed.

%An offshoot of the CompCert project is the CompCertTSO project, which adds
%thread concurrency and synchronisation to the CompCert compiler~\cite{TSO2011}.
%This compiler also generates assembly code and therefore does not include a
%branch displacement algorithm.
 
%Finally, there is also the Piton stack~\cite{Moore1996}, which not only includes the
%formal verification of a compiler, but also of the machine architecture
%targeted by that compiler, a microprocessor called the FM9001.
%However, this architecture does not have different
%jump sizes (branching is simulated by assigning values to the program counter),
%so the branch displacement problem is irrelevant.