Changeset 2099


Ignore:
Timestamp:
Jun 15, 2012, 5:56:30 PM (5 years ago)
Author:
boender
Message:
  • added reference to Intel dev manual
Location:
src/ASM/CPP2012-policy
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CPP2012-policy/biblio.bib

    r2098 r2099  
    6868        year = {2012},
    6969        key = {GCC2012}
     70}
     71
     72@misc{IntelDev,
     73        author = {Intel},
     74        title = {{Intel 64 and IA-32 Architectures Developer's Manual}},
     75        howpublished={\url{http://www.intel.com/content/www/us/en/processors/architectures-software-developer-manuals.html}},
     76        volume=2,
     77  key = {IntelDev}
    7078}
    7179
  • src/ASM/CPP2012-policy/conclusion.tex

    r2098 r2099  
    1313
    1414In 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.
     15than the simple `every branch instruction is long' used up until now---and with
     16only 64 Kb of memory, every byte counts. It also results in a smaller solution
     17than the greatest fixed point algorithm that {\tt gcc} uses. It does this
     18without sacrificing speed or correctness.
    1819
    1920This algorithm is part of a greater whole, the CerCo project, which aims to
    2021completely formalise and verify a concrete cost preserving compiler for a large
    21 subset of the C programming language. More information
    22 on the formalisation of the assembler, of which the present work is a part,
    23 can be found in a companion publication~\cite{DC2012}.
     22subset of the C programming language. More information on the formalisation of
     23the assembler, of which the present work is a part, can be found in a companion
     24publication~\cite{DC2012}.
    2425
    2526\subsection{Related work}
  • src/ASM/CPP2012-policy/main.tex

    r2097 r2099  
    4141\input{conclusion}
    4242
     43\clearpage
    4344\bibliography{biblio}
    4445\bibliographystyle{splncs03}
  • src/ASM/CPP2012-policy/problem.tex

    r2096 r2099  
    3434unconditional branch instruction, all with different ranges, instruction sizes
    3535and semantics (only six are valid in 64-bit mode, for example). Some examples
    36 are shown in Figure~\ref{f:x86jumps}.
     36are shown in Figure~\ref{f:x86jumps} (see also~\cite{IntelDev}).
    3737
    3838\begin{figure}[h]
  • src/ASM/CPP2012-policy/proof.tex

    r2098 r2099  
    128128\end{lstlisting}
    129129
    130 This is a temporary formulation of the main property
     130This is a temporary formulation of the main property\\
    131131({\tt sigma\_policy\_specification}); its main difference
    132132from the final version is that it uses {\tt instruction\_size\_jmplen} to
     
    236236
    237237If the iteration returns $\mathtt{Some}\ \sigma$, the invariants
    238 {\tt out\_of\_program\_none}, {\tt not\_jump\_default}, {\tt jump\_increase},
     238{\tt out\_of\_program\_none},\\
     239{\tt not\_jump\_default}, {\tt jump\_increase},
    239240and the two invariants that deal with $\sigma(0)$ and $\sigma(n)$ are
    240241retained without change.
Note: See TracChangeset for help on using the changeset viewer.