# Changeset 2098 for src/ASM

Ignore:
Timestamp:
Jun 15, 2012, 5:29:10 PM (8 years ago)
Message:
Location:
src/ASM/CPP2012-policy
Files:
4 edited

Unmodified
Removed

 r2096 \mathtt{absolute\_jump},\mathtt{long\_jump}\}$; a function that associates a pseudo-address with a memory address and a jump length. We do this to be able to more ease the comparison of jump lengths between iterations. In the algorithm, to ease the comparison of jump lengths between iterations. In the algorithm, we use the notation$sigma_1(x)$to denote the memory address corresponding to$x$, and$sigma_2(x)$to denote the jump length corresponding to$x$. • ## src/ASM/CPP2012-policy/biblio.bib  r2094 @misc{DC2012, title={On the correctness of an optimising assembler for the Intel MCS-51 microprocessor}, title={{On the correctness of an optimising assembler for the Intel MCS-51 microprocessor}}, author = {Dominic P. Mulligan and Claudio {Sacerdoti Coen}}, year = {2012}, • ## src/ASM/CPP2012-policy/conclusion.tex  r2096 where it is important to have as small 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. 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. This algorithm is part of a greater whole, the CerCo project, which aims to complete formalise and verify a concrete cost preserving compiler for a large 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, • ## src/ASM/CPP2012-policy/proof.tex  r2096 In this section, we present the correctness proof for the algorithm in more detail. The main correctness statement is as follows (slightly simplified, here): \clearpage \begin{lstlisting} \clearpage \begin{lstlisting} definition sigma_compact_unsafe := We need to use two different formulations, because the fact that$added\$ is 0 does not guarantee that no branch instructions have changed.  For instance, it is possible that we have replaced a short jump with a absolute jump, which it is possible that we have replaced a short jump with an absolute jump, which does not change the size of the branch instruction. If an iteration returns {\tt None}, we have the following invariant: \clearpage \begin{lstlisting} definition nec_plus_ultra :=
Note: See TracChangeset for help on using the changeset viewer.