Changeset 2345 for Papers

Sep 26, 2012, 2:57:50 PM (7 years ago)


1 edited


  • Papers/cpp-asm-2012/cpp-2012-asm.tex

    r2344 r2345  
     184The aim of the section is to explain the main ideas and steps of the certified
     185proof of correctness for an optimizing assembler for the MCS-8051. The
     186formalization is available at~\url{}.
     188In Section~\ref{subsect.machine.code.semantics} we sketch an operational
     189semantics (a realistic and efficient emulator) for the MCS-8051.
     190We also introduce a syntax for decoded instructions that will be reused for
     191the assembly language.
     193In Section~\ref{subsect.assembly.code.semantics} we describe the assembly code
     194language and operational semantics. The latter is parametric in the cost model
     195that will be induced by the assembler. It fully reuses the semantics of the
     196machine code on all ``real'' (i.e. non pseudo) instructions.
     198Branch displacement policies are introduced in
     199Section~\ref{subsect.the.assembler} where we
     200also describe the assembler as a function over policies as previously described.
     202The proof of correctness of the assembler consists in showing that the
     203object code given in output together with a cost model for the source program
     204simulates the source program executed using that cost model. The proof
     205can be divided into two main lemmas. The first is correctness with respect
     206to fetching, described in
     207Section~\ref{}. It roughly
     208states that one step of fetching at the assembly level that returns the
     209decoded instruction $I$ is simulated by
     210$n$ steps of fetching at object level that return instructions
     211$J_1,\ldots,J_n$, where $J_1,\ldots,J_n$ is, among the possible expansions
     212of $I$, the one picked by the policy.
     213The second lemma shows that $J_1,\ldots,J_n$ simulates $I$ but only if
     214the $I$ is well-behaved, i.e. it manipulates addresses in ways that are
     215anticipated in the correctness proof. To keep track of the well-behaved ways,
     216we couple the assembly status with a map that records where addresses are
     217currently stored in memory or in the registers. Then we introduce a dynamic
     218checking function that inspects the assembly status and the map to determine
     219if the operation is well behaved. A positive answer is the pre-condition of
     220the lemma. The second lemma is part of
     222where we also establish \emph{total correctness} of our assembler as a
     223composition of the two lemmas: programs that are well behaved when executed
     224under the cost model induced by the compiler are correctly simulated by the
     225compiled code.
    184227% ---------------------------------------------------------------------------- %
    185228% SECTION                                                                      %
Note: See TracChangeset for help on using the changeset viewer.