Changeset 2098


Ignore:
Timestamp:
Jun 15, 2012, 5:29:10 PM (5 years ago)
Author:
boender
Message:
  • updates & changes
Location:
src/ASM/CPP2012-policy
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CPP2012-policy/algorithm.tex

    r2096 r2098  
    170170\mathtt{absolute\_jump},\mathtt{long\_jump}\}$; a function that associates a
    171171pseudo-address with a memory address and a jump length. We do this to be able
    172 to more ease the comparison of jump lengths between iterations. In the algorithm,
     172to ease the comparison of jump lengths between iterations. In the algorithm,
    173173we use the notation $sigma_1(x)$ to denote the memory address corresponding to
    174174$x$, and $sigma_2(x)$ to denote the jump length corresponding to $x$.
  • src/ASM/CPP2012-policy/biblio.bib

    r2094 r2098  
    104104
    105105@misc{DC2012,
    106         title={On the correctness of an optimising assembler for the Intel MCS-51 microprocessor},
     106        title={{On the correctness of an optimising assembler for the Intel MCS-51 microprocessor}},
    107107        author = {Dominic P. Mulligan and Claudio {Sacerdoti Coen}},
    108108        year = {2012},
  • src/ASM/CPP2012-policy/conclusion.tex

    r2096 r2098  
    1212where it is important to have as small solution as possible.
    1313
     14In itself the algorithm is already useful, as it results in a smaller solution
     15than the simple `every branch instruction is long' used up until now. It also
     16results in a smaller solution than the greatest fixed point algorithm that
     17{\tt gcc} uses. It does this without sacrificing speed or correctness.
     18
    1419This 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 large
     20completely formalise and verify a concrete cost preserving compiler for a large
    1621subset of the C programming language. More information
    1722on the formalisation of the assembler, of which the present work is a part,
  • src/ASM/CPP2012-policy/proof.tex

    r2096 r2098  
    33In this section, we present the correctness proof for the algorithm in more
    44detail.  The main correctness statement is as follows (slightly simplified, here):
    5 
    6 \clearpage
    75
    86\begin{lstlisting}
     
    114112
    115113\clearpage
    116 
    117114\begin{lstlisting}
    118115definition sigma_compact_unsafe :=
     
    200197We need to use two different formulations, because the fact that $added$ is 0
    201198does 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, which
     199it is possible that we have replaced a short jump with an absolute jump, which
    203200does not change the size of the branch instruction.
    204201
     
    224221If an iteration returns {\tt None}, we have the following invariant:
    225222
     223\clearpage
    226224\begin{lstlisting}
    227225definition nec_plus_ultra :=
Note: See TracChangeset for help on using the changeset viewer.