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

Last change on this file since 2093 was 2093, checked in by boender, 7 years ago
  • added reference to CompCertTSO
File size: 2.4 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 find to make such a solution practical for implementing
11in an existent compiler; this would be especially useful for embedded systems,
12where it is important to have a small solution as possible.
13
14This algorithm is part of a greater whole, the CerCo project, which aims at
15the complete formalisation and verification of a compiler. More information
16on the formalisation of the assembler, of which the present work is a part,
17can be found in a companion publication~\cite{DC2012}.
18
19\subsection{Related work}
20
21As far as we are aware, this is the first formal discussion of the branch
22displacement optimisation algorithm.
23
24The CompCert project is another project aimed at formally verifying a compiler.
25Their backend~\cite{Leroy2009} generates assembly code for (amongst others) the
26PowerPC and x86 (32-bit) architectures. At the assembly code stage, there is
27no distinction between the span-dependent jump instructions, so a branch
28displacement optimisation algorithm is not needed.
29
30An offshoot of the CompCert project is the CompCertTSO project, who add thread
31concurrency and synchronisation to the CompCert compiler~\cite{TSO2011}. This
32compiler also generate assembly code and therefore does not include a branch
33displacement algorithm.
34 
35There is also Piton~\cite{Moore1996}, which not only includes the
36formal verification of a compiler, but also of the machine architecture
37targeted by that compiler. However, this architecture does not have different
38jump sizes (branching is simulated by assigning values to the program counter),
39so the branch displacement problem does not occur.
40 
41\subsection{Formal development}
42
43All Matita files related to this development can be found on the CerCo
44website, \url{http://cerco.cs.unibo.it}. The specific part that contains the
45branch displacement algorithm is in the {\tt ASM} subdirectory, in the files
46{\tt PolicyFront.ma}, {\tt PolicyStep.ma} and {\tt Policy.ma}.
Note: See TracBrowser for help on using the repository browser.