# Changeset 947 for src/ASM

Ignore:
Timestamp:
Jun 13, 2011, 2:14:11 PM (9 years ago)
Message:

...

File:
1 edited

### Legend:

Unmodified
 r927 \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.