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

Last change on this file since 3362 was 3362, checked in by boender, 6 years ago
  • added some bits as per Claudio's mail
  • rewrote some small things
  • general reread, spell check, grammar check
  • 16 pages again now
File size: 4.7 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 a solution as possible.
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---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.
20The certification of an assembler that relies on the branch displacement
21algorithm described in this paper was presented in~\cite{lastyear}.
22The assembler computes the $\sigma$ map as described in this paper and
23then works in two passes. In the first pass it builds a map
24from instruction labels to addresses in the assembly code. In the
25second pass it iterates over the code, translating every pseudo jump
26at address src to a label l associated to the assembly instruction at
27address dst to a jump of the size dictated by $(\sigma\ src)$ to
28$(\sigma\ dst)$. In case of conditional jumps, the translated jump may be
29implemented with a series of instructions.
31The proof of correctness abstracts over the algorithm used and only relies on
32{\tt sigma\_policy\_specification} (page~\ref{sigmapolspec}). It is a variation
33of a standard 1-to-many forward simulation proof~\cite{compcert:2011}. The
34relation R between states just maps every code address ppc stored in
35registers or memory to $(\sigma\ ppc)$. To identify the code addresses,
36an additional data structure is always kept together with the source
37state and is updated by the semantics. The semantics is preserved
38only for those programs whose source code operations
39$(f\ ppc1\ \ldots\ ppcn)$ applied to code addresses $ppc1 \ldots ppcn$ are such
40that $(f\ (\sigma\ ppc1)\ ...\ (\sigma\ ppc) = f\ ppc\ ppcn))$. For example,
41an injective $\sigma$ preserves a binary equality test f for code addresses,
42but not pointer subtraction.
44The main lemma (fetching simulation), which relies on\\
45{\tt sigma\_policy\_specification} and is established by structural induction
46over the source code, says that fetching an assembly instruction at
47position ppc is equal to fetching the translation of the instruction at
48position $(\sigma\ ppc)$, and that the new incremented program counter is at
49the beginning of the next instruction (compactness). The only exception is
50when the instruction fetched is placed at the end of code memory and is
51followed only by dead code. Execution simulation is trivial because of the
52restriction over well behaved programs w.r.t. sigma. The condition
53$\sigma\ 0 = 0$ is necessary because the hardware model prescribes that the
54first instruction to be executed will be at address 0. For the details
57\subsection{Related work}
59As far as we are aware, this is the first formal discussion of the branch
60displacement optimisation algorithm.
62The CompCert project is another verified compiler project.
63Their backend~\cite{Leroy2009} generates assembly code for (amongst others) subsets of the
64PowerPC and x86 (32-bit) architectures. At the assembly code stage, there is
65no distinction between the span-dependent jump instructions, so a branch
66displacement optimisation algorithm is not needed.
68An offshoot of the CompCert project is the CompCertTSO project, who add thread
69concurrency and synchronisation to the CompCert compiler~\cite{TSO2011}. This
70compiler also generates assembly code and therefore does not include a branch
71displacement algorithm.
73Finally, there is also the Piton stack~\cite{Moore1996}, which not only includes the
74formal verification of a compiler, but also of the machine architecture
75targeted by that compiler, a bespoke microprocessor called the FM9001.
76However, this architecture does not have different
77jump sizes (branching is simulated by assigning values to the program counter),
78so the branch displacement problem is irrelevant.
80\subsection{Formal development}
82All Matita files related to this development can be found on the CerCo
83website, \url{}. The specific part that contains the
84branch displacement algorithm is in the {\tt ASM} subdirectory, in the files
85{\tt}, {\tt} and {\tt}.
Note: See TracBrowser for help on using the repository browser.