Jun 17, 2013, 1:08:27 PM (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
1 edited


  • src/ASM/CPP2012-policy/conclusion.tex

    r2099 r3362  
    1010heuristics could be found to make such a solution practical for implementing
    1111in an existing compiler; this would be especially useful for embedded systems,
    12 where it is important to have as small solution as possible.
     12where it is important to have as small a solution as possible.
    1414In itself the algorithm is already useful, as it results in a smaller solution
    1818without sacrificing speed or correctness.
    20 This algorithm is part of a greater whole, the CerCo project, which aims to
    21 completely formalise and verify a concrete cost preserving compiler for a large
    22 subset of the C programming language. More information on the formalisation of
    23 the assembler, of which the present work is a part, can be found in a companion
    24 publication~\cite{DC2012}.
     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
    2657\subsection{Related work}
Note: See TracChangeset for help on using the changeset viewer.