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

Last change on this file since 2096 was 2096, checked in by mulligan, 9 years ago

Changes to the English for Jaap, and some tidying up and making consistent with the other CPP submission.

File size: 2.5 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.
14This algorithm is part of a greater whole, the CerCo project, which aims to
15complete formalise and verify a concrete cost preserving compiler for a large
16subset of the C programming language. More information
17on the formalisation of the assembler, of which the present work is a part,
18can be found in a companion publication~\cite{DC2012}.
20\subsection{Related work}
22As far as we are aware, this is the first formal discussion of the branch
23displacement optimisation algorithm.
25The CompCert project is another verified compiler project.
26Their backend~\cite{Leroy2009} generates assembly code for (amongst others) subsets of the
27PowerPC and x86 (32-bit) architectures. At the assembly code stage, there is
28no distinction between the span-dependent jump instructions, so a branch
29displacement optimisation algorithm is not needed.
31An offshoot of the CompCert project is the CompCertTSO project, who add thread
32concurrency and synchronisation to the CompCert compiler~\cite{TSO2011}. This
33compiler also generates assembly code and therefore does not include a branch
34displacement algorithm.
36Finally, there is also the Piton stack~\cite{Moore1996}, which not only includes the
37formal verification of a compiler, but also of the machine architecture
38targeted by that compiler, a bespoke microprocessor called the FM9001.
39However, this architecture does not have different
40jump sizes (branching is simulated by assigning values to the program counter),
41so the branch displacement problem is irrelevant.
43\subsection{Formal development}
45All Matita files related to this development can be found on the CerCo
46website, \url{}. The specific part that contains the
47branch displacement algorithm is in the {\tt ASM} subdirectory, in the files
48{\tt}, {\tt} and {\tt}.
Note: See TracBrowser for help on using the repository browser.