source: src/ASM/CPP2012-policy/conclusion.tex @ 2098

Last change on this file since 2098 was 2098, checked in by boender, 8 years ago
  • updates & changes
File size: 2.8 KB
[2096]3In the previous sections we have discussed the branch displacement optimisation
[2084]4problem, presented an optimised solution, and discussed the proof of
5termination and correctness for this algorithm, as formalised in Matita.
[2085]7The algorithm we have presented is fast and correct, but not optimal; a true
8optimal solution would need techniques like constraint solvers. While outside
9the scope of the present research, it would be interesting to see if enough
[2096]10heuristics could be found to make such a solution practical for implementing
11in an existing compiler; this would be especially useful for embedded systems,
12where it is important to have as small solution as possible.
[2098]14In itself the algorithm is already useful, as it results in a smaller solution
15than the simple `every branch instruction is long' used up until now. It also
16results in a smaller solution than the greatest fixed point algorithm that
17{\tt gcc} uses. It does this without sacrificing speed or correctness.
[2096]19This algorithm is part of a greater whole, the CerCo project, which aims to
[2098]20completely formalise and verify a concrete cost preserving compiler for a large
[2096]21subset of the C programming language. More information
[2085]22on the formalisation of the assembler, of which the present work is a part,
[2091]23can be found in a companion publication~\cite{DC2012}.
[2084]25\subsection{Related work}
27As far as we are aware, this is the first formal discussion of the branch
[2093]28displacement optimisation algorithm.
[2096]30The CompCert project is another verified compiler project.
31Their backend~\cite{Leroy2009} generates assembly code for (amongst others) subsets of the
[2093]32PowerPC and x86 (32-bit) architectures. At the assembly code stage, there is
33no distinction between the span-dependent jump instructions, so a branch
34displacement optimisation algorithm is not needed.
[2093]36An offshoot of the CompCert project is the CompCertTSO project, who add thread
37concurrency and synchronisation to the CompCert compiler~\cite{TSO2011}. This
[2096]38compiler also generates assembly code and therefore does not include a branch
[2093]39displacement algorithm.
[2096]41Finally, there is also the Piton stack~\cite{Moore1996}, which not only includes the
[2085]42formal verification of a compiler, but also of the machine architecture
[2096]43targeted by that compiler, a bespoke microprocessor called the FM9001.
44However, this architecture does not have different
[2085]45jump sizes (branching is simulated by assigning values to the program counter),
[2096]46so the branch displacement problem is irrelevant.
[2084]48\subsection{Formal development}
50All Matita files related to this development can be found on the CerCo
51website, \url{}. The specific part that contains the
52branch displacement algorithm is in the {\tt ASM} subdirectory, in the files
[2093]53{\tt}, {\tt} and {\tt}.
Note: See TracBrowser for help on using the repository browser.