Jun 16, 2011, 2:39:23 PM (8 years ago)

added more, worked on conclusions and related work. need just to finish explanation of large lemmas

1 edited


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

    r976 r981  
    364364Here, \texttt{len} is the number of machine code instructions the pseudoinstruction at hand has been expanded into, \texttt{encoding\_check} is a recursive function that checks for any possible corruption of the code memory, resulting from expanding the pseudoinstruction.
     365We assemble a single pseudoinstruction with \texttt{assembly\_1\_pseudoinstruction}, which internally calls \texttt{jump\_expansion} and \texttt{expand\_pseudo\_instruction}.
    365366The function \texttt{fetch\_many} fetches multiple machine code instructions from code memory and performs some routine checks.
    438439We have proved the total correctness of an assembler for MCS-51 assembly language.
    439440In particular, our assembly language featured labels, arbitrary conditional and unconditional jumps to labels, global data and instructions for moving this data into the MCS-51's single 16-bit register.
    441 \subsection{Use of dependent types and Russell}
    442 \label{subsect.use.of.dependent.types.and.Russell}
     441Expanding these pseudoinstructions into machine code instructions is not trivial, and the proof that the assembly process is `correct', in that the semantics of an assembly program are not changed is complex.
     443Aside from their application in verified compiler projects such as CerCo, verified assemblers could also be applied to the verification of operating system kernels.
     444Of particular note is the verified seL4 kernel~\cite{klein:sel4:2009,klein:sel4:2010}.
     445This verification explicitly assumes the existence of, amongst other things, a trustworthy assembler.
     447\paragraph{Use of dependent types and Russell}
    444448Our formalisation makes sparing use of dependent types.
    445449In certain datastructures, such as tries and vectors, they are used to guarantee invariants.
    449453However, there are certain cases where the use of dependent types is unavoidable.
    450454For instance, when proving that the \texttt{build\_maps} function is correct, a function that collates the cost and data labels of an assembly program into map datastructures.
    451 In cases such as these we make use of Matita's implementation of Russell~\cite{}.
     455In cases such as these we make use of Matita's implementation of Russell~\cite{sozeau:subset:2006}.
     456In Matita, Russell may be implemented with two coercions and some notational sugaring.
    453458\subsection{Related work}
     461% piton
     462We are not the first to consider the total correctness of an assembler for a non-trivial assembly language.
     463Perhaps the most impressive piece of work in this domain is the Piton stack~\cite{moore:piton:1996,moore:grand:2005}.
     464This was a stack of verified components, written and verified in ACL2, ranging from a proprietary FM9001 microprocessor verified at the gate level, to assemblers and compilers for two high-level languages---a dialect of Lisp and $\mu$Gypsy~\cite{moore:grand:2005}.
     465%dpm more: weirich paper?
     467% jinja
     468Klein and Nipkow consider a Java-like programming language, Jinja~\cite{klein:machine:2006,klein:machine:2010}.
     469They provide a compiler, virtual machine and operational semantics for the programming language and virtual machine, and prove that their compiler is semantics and type preserving.
     471Finally, mention should be made of CompCert~\cite{compcert:2011,blazy:formal:2006,leroy:formal:2009,leroy:formally:2009}, another verified compiler project related to CerCo.
     472As previously mentioned, CompCert considers only extensional correctness of the compiler, and not intensional correctness, which CerCo focusses on.
     473However, CerCo also extends CompCert in other ways.
     474Namely, the CompCert verified compilation chain terminates at the PowerPC or ARM assembly level, and takes for granted the existence of a trustworthy assembler.
     475CerCo chooses to go further, by considering a verified compilation chain all the way down to the machine code level.
     476In essence, the work presented in this publication is one part of CerCo's extension over CompCert.
Note: See TracChangeset for help on using the changeset viewer.