# Changeset 2099

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

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

 r2098 year = {2012}, key = {GCC2012} } @misc{IntelDev, author = {Intel}, title = {{Intel 64 and IA-32 Architectures Developer's Manual}}, howpublished={\url{http://www.intel.com/content/www/us/en/processors/architectures-software-developer-manuals.html}}, volume=2, key = {IntelDev} }
• ## src/ASM/CPP2012-policy/conclusion.tex

 r2098 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. than the simple every branch instruction is long' used up until now---and with only 64 Kb of memory, every byte counts. 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 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, can be found in a companion publication~\cite{DC2012}. subset of the C programming language. More information on the formalisation of the assembler, of which the present work is a part, can be found in a companion publication~\cite{DC2012}. \subsection{Related work}
• ## src/ASM/CPP2012-policy/main.tex

 r2097 \input{conclusion} \clearpage \bibliography{biblio} \bibliographystyle{splncs03}
• ## src/ASM/CPP2012-policy/problem.tex

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

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