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

Last change on this file since 2227 was 2099, checked in by boender, 8 years ago
  • added reference to Intel dev manual
File size: 2.8 KB
RevLine 
[2064]1\section{Conclusion}
[2084]2
[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.
6
[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.
[2085]13
[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.
[2098]19
[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
24publication~\cite{DC2012}.
[2085]25
[2084]26\subsection{Related work}
27
28As far as we are aware, this is the first formal discussion of the branch
[2093]29displacement optimisation algorithm.
[2084]30
[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.
[2084]36
[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.
41 
[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.
[2085]48 
[2084]49\subsection{Formal development}
50
51All Matita files related to this development can be found on the CerCo
52website, \url{http://cerco.cs.unibo.it}. The specific part that contains the
53branch displacement algorithm is in the {\tt ASM} subdirectory, in the files
[2093]54{\tt PolicyFront.ma}, {\tt PolicyStep.ma} and {\tt Policy.ma}.
Note: See TracBrowser for help on using the repository browser.