source: Papers/cpp-policy-2012/conclusion.tex @ 2396

\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 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.

This algorithm is part of a greater whole, the CerCo project, which aims to
completely formalise and verify a concrete cost preserving compiler for a large
subset of the C programming language. More information on the formalisation of
the assembler, of which the present work is a part, can be found in a companion
publication~\cite{DC2012}.

\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, who add 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 bespoke 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.
  
\subsection{Formal development}

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}.