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

Last change on this file since 2593 was 2099, checked in by boender, 9 years ago
  • added reference to Intel dev manual
File size: 2.8 KB
3In the previous sections we have discussed the branch displacement optimisation
4problem, presented an optimised solution, and discussed the proof of
5termination and correctness for this algorithm, as formalised in Matita.
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
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.
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---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.
20This algorithm is part of a greater whole, the CerCo project, which aims to
21completely formalise and verify a concrete cost preserving compiler for a large
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
26\subsection{Related work}
28As far as we are aware, this is the first formal discussion of the branch
29displacement optimisation algorithm.
31The CompCert project is another verified compiler project.
32Their backend~\cite{Leroy2009} generates assembly code for (amongst others) subsets of the
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.
37An offshoot of the CompCert project is the CompCertTSO project, who add thread
38concurrency and synchronisation to the CompCert compiler~\cite{TSO2011}. This
39compiler also generates assembly code and therefore does not include a branch
40displacement algorithm.
42Finally, there is also the Piton stack~\cite{Moore1996}, which not only includes the
43formal verification of a compiler, but also of the machine architecture
44targeted by that compiler, a bespoke microprocessor called the FM9001.
45However, this architecture does not have different
46jump sizes (branching is simulated by assigning values to the program counter),
47so the branch displacement problem is irrelevant.
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
54{\tt}, {\tt} and {\tt}.
Note: See TracBrowser for help on using the repository browser.