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

Last change on this file since 2090 was 2085, checked in by boender, 8 years ago
  • rewrote introduction
  • changed 'medium' to 'absolute'
  • added a bit to conclusion (CompCert?, Piton, ...)
File size: 2.0 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 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.
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.
19\subsection{Related work}
21As far as we are aware, this is the first formal discussion of the branch
22displacement algorithm.
24The CompCert project is another project aimed at formally verifying a compiler.
25Their backend~\cite{Leroy2009} generates assembly for (amongst others) the
26PowerPC and x86 (32-bit) architectures, but does not include a branch
27displacement algorithm; at least for the x86 architecture, all jumps are
28encoded as long jumps.
30There is also Piton~\cite{Moore1996}, which not only includes the
31formal verification of a compiler, but also of the machine architecture
32targeted by that compiler. However, this architecture does not have different
33jump sizes (branching is simulated by assigning values to the program counter),
34so the branch displacement problem does not occur.
36\subsection{Formal development}
38All Matita files related to this development can be found on the CerCo
39website, \url{}. The specific part that contains the
40branch displacement algorithm is in the {\tt ASM} subdirectory, in the files
41whose name starts with {\tt Policy}.
Note: See TracBrowser for help on using the repository browser.