# Changeset 3473 for Papers/sttt/conclusion.tex

Ignore:
Timestamp:
Sep 22, 2014, 11:25:51 AM (5 years ago)
Message:

inlined section into main document, title change

File:
1 edited

Unmodified
Added
Removed
• ## Papers/sttt/conclusion.tex

 r3470 \section{Conclusion} In the previous sections we have discussed the branch displacement optimisation problem, presented an optimised solution, and discussed the proof of termination and correctness for this algorithm, as formalised in Matita. The algorithm we have presented is fast and correct, but not optimal; a true optimal solution would need techniques like constraint solvers. While outside the scope of the present research, it would be interesting to see if enough heuristics could be found to make such a solution practical for implementing in an existing compiler; this would be especially useful for embedded systems, where it is important to have as small a solution as possible. In itself the algorithm is already useful, as it results in a smaller solution than the simple `every branch instruction is long' used up until now---and with only 64 Kb of memory, every byte counts. It also results in a smaller solution than the greatest fixed point algorithm that {\tt gcc} uses. It does this without sacrificing speed or correctness. The certification of an assembler that relies on the branch displacement algorithm described in this paper was presented in~\cite{lastyear}. The assembler computes the $\sigma$ map as described in this paper and then works in two passes. In the first pass it builds a map from instruction labels to addresses in the assembly code. In the second pass it iterates over the code, translating every pseudo jump at address $src$ to a label l associated to the assembly instruction at address $dst$ to a jump of the size dictated by $(\sigma\ src)$ to $(\sigma\ dst)$. In case of conditional jumps, the translated jump may be implemented with a series of instructions. The proof of correctness abstracts over the algorithm used and only relies on {\tt sigma\_policy\_specification} (page~\ref{sigmapolspec}). It is a variation of a standard 1-to-many forward simulation proof~\cite{Leroy2009}. The relation R between states just maps every code address $ppc$ stored in registers or memory to $(\sigma\ ppc)$. To identify the code addresses, an additional data structure is always kept together with the source state and is updated by the semantics. The semantics is preserved only for those programs whose source code operations $(f\ ppc_1\ \ldots\ ppc_n)$ applied to code addresses $ppc_1 \ldots ppc_n$ are such that $(f\ (\sigma\ ppc_1)\ ...\ (\sigma\ ppc_n) = f\ ppc_1\ ppc_n))$. For example, an injective $\sigma$ preserves a binary equality test f for code addresses, but not pointer subtraction. The main lemma (fetching simulation), which relies on\\ {\tt sigma\_policy\_specification} and is established by structural induction over the source code, says that fetching an assembly instruction at position ppc is equal to fetching the translation of the instruction at position $(\sigma\ ppc)$, and that the new incremented program counter is at the beginning of the next instruction (compactness). The only exception is when the instruction fetched is placed at the end of code memory and is followed only by dead code. Execution simulation is trivial because of the restriction over well behaved programs w.r.t. sigma. The condition $\sigma\ 0 = 0$ is necessary because the hardware model prescribes that the first instruction to be executed will be at address 0. For the details see~\cite{lastyear}. Instead of verifying the algorithm directly, another solution to the problem would be to run an optimisation algorithm, and then verify the safety of the result using a verified validator. Such a validator would be easier to verify than the algorithm itself and it would also be efficient, requiring only a linear pass over the source code to test the specification. However, it is surely also interesting to formally prove that the assembler never rejects programs that should be accepted, i.e. that the algorithm itself is correct. This is the topic of the current paper. \subsection{Related work} As far as we are aware, this is the first formal discussion of the branch displacement optimisation algorithm. The CompCert project is another verified compiler project. Their backend~\cite{Leroy2009} generates assembly code for (amongst others) subsets of the PowerPC and x86 (32-bit) architectures. At the assembly code stage, there is no distinction between the span-dependent jump instructions, so a branch displacement optimisation algorithm is not needed. %An offshoot of the CompCert project is the CompCertTSO project, which adds %thread concurrency and synchronisation to the CompCert compiler~\cite{TSO2011}. %This compiler also generates assembly code and therefore does not include a %branch displacement algorithm. %Finally, there is also the Piton stack~\cite{Moore1996}, which not only includes the %formal verification of a compiler, but also of the machine architecture %targeted by that compiler, a microprocessor called the FM9001. %However, this architecture does not have different %jump sizes (branching is simulated by assigning values to the program counter), %so the branch displacement problem is irrelevant.
Note: See TracChangeset for help on using the changeset viewer.