Changeset 947

Jun 13, 2011, 2:14:11 PM (8 years ago)


1 edited


  • src/ASM/CPP2011/cpp-2011.tex

    r927 r947  
     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}
    2584This paper discusses the proof of correctness of an assembler for the Intel MCS-51 8-bit family of microprocessors.
Note: See TracChangeset for help on using the changeset viewer.