# Changeset 3362 for src/ASM/CPP2012-policy/conclusion.tex

Ignore:
Timestamp:
Jun 17, 2013, 1:08:27 PM (6 years ago)
Message:
• added some bits as per Claudio's mail
• rewrote some small things
• general reread, spell check, grammar check
• 16 pages again now
File:
1 edited

### Legend:

Unmodified
 r2099 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 solution as possible. 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 without sacrificing speed or correctness. This algorithm is part of a greater whole, the CerCo project, which aims to completely formalise and verify a concrete cost preserving compiler for a large subset of the C programming language. More information on the formalisation of the assembler, of which the present work is a part, can be found in a companion publication~\cite{DC2012}. 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{compcert:2011}. 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\ ppc1\ \ldots\ ppcn)$ applied to code addresses $ppc1 \ldots ppcn$ are such that $(f\ (\sigma\ ppc1)\ ...\ (\sigma\ ppc) = f\ ppc\ ppcn))$. 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}. \subsection{Related work}