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
Line 
1\section{Conclusion}
2
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.
6
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.
13
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.
18
19This algorithm is part of a greater whole, the CerCo project, which aims to
20completely formalise and verify a concrete cost preserving compiler for a large
21subset of the C programming language. More information
22on the formalisation of the assembler, of which the present work is a part,
23can be found in a companion publication~\cite{DC2012}.
24
25\subsection{Related work}
26
27As far as we are aware, this is the first formal discussion of the branch
28displacement optimisation algorithm.
29
30The CompCert project is another verified compiler project.
31Their backend~\cite{Leroy2009} generates assembly code for (amongst others) subsets of the
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.
35
36An offshoot of the CompCert project is the CompCertTSO project, who add thread
37concurrency and synchronisation to the CompCert compiler~\cite{TSO2011}. This
38compiler also generates assembly code and therefore does not include a branch
39displacement algorithm.
40 
41Finally, there is also the Piton stack~\cite{Moore1996}, which not only includes the
42formal verification of a compiler, but also of the machine architecture
43targeted by that compiler, a bespoke microprocessor called the FM9001.
44However, this architecture does not have different
45jump sizes (branching is simulated by assigning values to the program counter),
46so the branch displacement problem is irrelevant.
47 
48\subsection{Formal development}
49
50All Matita files related to this development can be found on the CerCo
51website, \url{http://cerco.cs.unibo.it}. The specific part that contains the
52branch displacement algorithm is in the {\tt ASM} subdirectory, in the files
53{\tt PolicyFront.ma}, {\tt PolicyStep.ma} and {\tt Policy.ma}.
Note: See TracBrowser for help on using the repository browser.