Index: /src/ASM/CPP2011/cpp-2011.tex
===================================================================
--- /src/ASM/CPP2011/cpp-2011.tex (revision 946)
+++ /src/ASM/CPP2011/cpp-2011.tex (revision 947)
@@ -22,4 +22,63 @@
\section{Introduction}
\label{sect.introduction}
+
+\begin{enumerate}
+ \item Assembler are considered simple pieces of code, but this is not the
+ case and they can be quite hard to formalize.
+ \item We are interested in an assembler for the legacy MCS family.
+ \item What does it do:
+ \begin{enumerate}
+ \item translates from human readabale to machine readable
+ \item expand labels
+ \item expand pseudo instructions by optimizing the expansion
+ \end{enumerate}
+ \item Problems due to the expansion/optimization:
+ \begin{itemize}
+ \item operations that fetch from the code memory do not make sense at
+ pseudo level
+ \item operations that combine the PC with constant shifts do not make sense
+ at pseudo level
+ \item more generally, memory addresses, wherever they are (memory, registers)
+ can only be copied and compared with other memory addresses
+ $\Rightarrow$ need to trace memory addresses UNDECIDABLE PROBLEM
+ \item consequence: full preservation of the semantics becomes IMPOSSIBLE
+ \end{itemize}
+ \item We are also interested in intensional properties
+ \begin{itemize}
+ \item the semantics is sensible to the timing (e.g. I/O, interrupts)
+ \item to show that the semantics is preserved, one needs to assign a
+ precise cost model to the pseudo instructions
+ \item the cost model is induced by the compilation itself
+ $\Rightarrow$ ``recursive'' statement
+ \end{itemize}
+ \item Finally, the optimizing expansion itself: certified compilers are
+ usually proved to be correct, but we want more: completeness and optimality
+ of the expansion.
+ \begin{itemize}
+ \item the optimization starts with a non solution
+ and incrementally refines it to a solution. At each step it uses functions
+ that are used to implement the expansion and that needs to be correct.
+ The solution can fail to exist. The proof becomes a mess
+ \item idea: split the policy from the implementation; prove the
+ implementation to be correct w.r.t. any correct policy; provide a correct
+ policy (when it exists) and show that it is also complete and optimal.
+ Show that the assembler fails iff a correct policy does not exist
+ (completeness).
+ \end{itemize}
+ \item Additional issues:
+ \begin{itemize}
+ \item use of dependent types to throw away wrong programs that would made
+ the statement for completeness complex. E.g. misuse of addressing modes,
+ jumps to non existent labels, etc.
+ \item try to go for small reflection; avoid inductive predicates that require
+ tactics (inversion, etc.) that do not work well with dependent types; small
+ reflection usually does
+ \item use coercions to simulate Russell; mix together the proof styles
+ a la Russell (for situations with heavy dependent types) and the standard
+ one
+ \end{itemize}
+\end{itemize}
+
+\end{enumerate}
This paper discusses the proof of correctness of an assembler for the Intel MCS-51 8-bit family of microprocessors.