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

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/CPP2011/cpp2011.tex
r927 r947 22 22 \section{Introduction} 23 23 \label{sect.introduction} 24 25 \begin{enumerate} 26 \item Assembler are considered simple pieces of code, but this is not the 27 case and they can be quite hard to formalize. 28 \item We are interested in an assembler for the legacy MCS family. 29 \item What does it do: 30 \begin{enumerate} 31 \item translates from human readabale to machine readable 32 \item expand labels 33 \item expand pseudo instructions by optimizing the expansion 34 \end{enumerate} 35 \item Problems due to the expansion/optimization: 36 \begin{itemize} 37 \item operations that fetch from the code memory do not make sense at 38 pseudo level 39 \item operations that combine the PC with constant shifts do not make sense 40 at pseudo level 41 \item more generally, memory addresses, wherever they are (memory, registers) 42 can only be copied and compared with other memory addresses 43 $\Rightarrow$ need to trace memory addresses UNDECIDABLE PROBLEM 44 \item consequence: full preservation of the semantics becomes IMPOSSIBLE 45 \end{itemize} 46 \item We are also interested in intensional properties 47 \begin{itemize} 48 \item the semantics is sensible to the timing (e.g. I/O, interrupts) 49 \item to show that the semantics is preserved, one needs to assign a 50 precise cost model to the pseudo instructions 51 \item the cost model is induced by the compilation itself 52 $\Rightarrow$ ``recursive'' statement 53 \end{itemize} 54 \item Finally, the optimizing expansion itself: certified compilers are 55 usually proved to be correct, but we want more: completeness and optimality 56 of the expansion. 57 \begin{itemize} 58 \item the optimization starts with a non solution 59 and incrementally refines it to a solution. At each step it uses functions 60 that are used to implement the expansion and that needs to be correct. 61 The solution can fail to exist. The proof becomes a mess 62 \item idea: split the policy from the implementation; prove the 63 implementation to be correct w.r.t. any correct policy; provide a correct 64 policy (when it exists) and show that it is also complete and optimal. 65 Show that the assembler fails iff a correct policy does not exist 66 (completeness). 67 \end{itemize} 68 \item Additional issues: 69 \begin{itemize} 70 \item use of dependent types to throw away wrong programs that would made 71 the statement for completeness complex. E.g. misuse of addressing modes, 72 jumps to non existent labels, etc. 73 \item try to go for small reflection; avoid inductive predicates that require 74 tactics (inversion, etc.) that do not work well with dependent types; small 75 reflection usually does 76 \item use coercions to simulate Russell; mix together the proof styles 77 a la Russell (for situations with heavy dependent types) and the standard 78 one 79 \end{itemize} 80 \end{itemize} 81 82 \end{enumerate} 24 83 25 84 This paper discusses the proof of correctness of an assembler for the Intel MCS51 8bit family of microprocessors.
Note: See TracChangeset
for help on using the changeset viewer.