Changeset 2098
 Timestamp:
 Jun 15, 2012, 5:29:10 PM (7 years ago)
 Location:
 src/ASM/CPP2012policy
 Files:

 4 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/CPP2012policy/algorithm.tex
r2096 r2098 170 170 \mathtt{absolute\_jump},\mathtt{long\_jump}\}$; a function that associates a 171 171 pseudoaddress with a memory address and a jump length. We do this to be able 172 to moreease the comparison of jump lengths between iterations. In the algorithm,172 to ease the comparison of jump lengths between iterations. In the algorithm, 173 173 we use the notation $sigma_1(x)$ to denote the memory address corresponding to 174 174 $x$, and $sigma_2(x)$ to denote the jump length corresponding to $x$. 
src/ASM/CPP2012policy/biblio.bib
r2094 r2098 104 104 105 105 @misc{DC2012, 106 title={ On the correctness of an optimising assembler for the Intel MCS51 microprocessor},106 title={{On the correctness of an optimising assembler for the Intel MCS51 microprocessor}}, 107 107 author = {Dominic P. Mulligan and Claudio {Sacerdoti Coen}}, 108 108 year = {2012}, 
src/ASM/CPP2012policy/conclusion.tex
r2096 r2098 12 12 where it is important to have as small solution as possible. 13 13 14 In itself the algorithm is already useful, as it results in a smaller solution 15 than the simple `every branch instruction is long' used up until now. It also 16 results in a smaller solution than the greatest fixed point algorithm that 17 {\tt gcc} uses. It does this without sacrificing speed or correctness. 18 14 19 This algorithm is part of a greater whole, the CerCo project, which aims to 15 complete formalise and verify a concrete cost preserving compiler for a large20 completely formalise and verify a concrete cost preserving compiler for a large 16 21 subset of the C programming language. More information 17 22 on the formalisation of the assembler, of which the present work is a part, 
src/ASM/CPP2012policy/proof.tex
r2096 r2098 3 3 In this section, we present the correctness proof for the algorithm in more 4 4 detail. The main correctness statement is as follows (slightly simplified, here): 5 6 \clearpage7 5 8 6 \begin{lstlisting} … … 114 112 115 113 \clearpage 116 117 114 \begin{lstlisting} 118 115 definition sigma_compact_unsafe := … … 200 197 We need to use two different formulations, because the fact that $added$ is 0 201 198 does not guarantee that no branch instructions have changed. For instance, 202 it is possible that we have replaced a short jump with a absolute jump, which199 it is possible that we have replaced a short jump with an absolute jump, which 203 200 does not change the size of the branch instruction. 204 201 … … 224 221 If an iteration returns {\tt None}, we have the following invariant: 225 222 223 \clearpage 226 224 \begin{lstlisting} 227 225 definition nec_plus_ultra :=
Note: See TracChangeset
for help on using the changeset viewer.