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

Last change on this file since 2099 was 2099, checked in by boender, 8 years ago
  • added reference to Intel dev manual
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
[2099]15than the simple `every branch instruction is long' used up until now---and with
16only 64 Kb of memory, every byte counts. It also results in a smaller solution
17than the greatest fixed point algorithm that {\tt gcc} uses. It does this
18without sacrificing speed or correctness.
[2096]20This algorithm is part of a greater whole, the CerCo project, which aims to
[2098]21completely formalise and verify a concrete cost preserving compiler for a large
[2099]22subset of the C programming language. More information on the formalisation of
23the assembler, of which the present work is a part, can be found in a companion
[2084]26\subsection{Related work}
28As far as we are aware, this is the first formal discussion of the branch
[2093]29displacement optimisation algorithm.
[2096]31The CompCert project is another verified compiler project.
32Their backend~\cite{Leroy2009} generates assembly code for (amongst others) subsets of the
[2093]33PowerPC and x86 (32-bit) architectures. At the assembly code stage, there is
34no distinction between the span-dependent jump instructions, so a branch
35displacement optimisation algorithm is not needed.
[2093]37An offshoot of the CompCert project is the CompCertTSO project, who add thread
38concurrency and synchronisation to the CompCert compiler~\cite{TSO2011}. This
[2096]39compiler also generates assembly code and therefore does not include a branch
[2093]40displacement algorithm.
[2096]42Finally, there is also the Piton stack~\cite{Moore1996}, which not only includes the
[2085]43formal verification of a compiler, but also of the machine architecture
[2096]44targeted by that compiler, a bespoke microprocessor called the FM9001.
45However, this architecture does not have different
[2085]46jump sizes (branching is simulated by assigning values to the program counter),
[2096]47so the branch displacement problem is irrelevant.
[2084]49\subsection{Formal development}
51All Matita files related to this development can be found on the CerCo
52website, \url{}. The specific part that contains the
53branch displacement algorithm is in the {\tt ASM} subdirectory, in the files
[2093]54{\tt}, {\tt} and {\tt}.
Note: See TracBrowser for help on using the repository browser.