Changeset 981 for src/ASM/CPP2011/cpp-2011.tex
- Timestamp:
- Jun 16, 2011, 2:39:23 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/CPP2011/cpp-2011.tex
r976 r981 363 363 \end{lstlisting} 364 364 Here, \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. 365 We assemble a single pseudoinstruction with \texttt{assembly\_1\_pseudoinstruction}, which internally calls \texttt{jump\_expansion} and \texttt{expand\_pseudo\_instruction}. 365 366 The function \texttt{fetch\_many} fetches multiple machine code instructions from code memory and performs some routine checks. 366 367 … … 438 439 We have proved the total correctness of an assembler for MCS-51 assembly language. 439 440 In 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. 440 441 \subsection{Use of dependent types and Russell} 442 \label{subsect.use.of.dependent.types.and.Russell} 443 441 Expanding 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. 442 443 Aside from their application in verified compiler projects such as CerCo, verified assemblers could also be applied to the verification of operating system kernels. 444 Of particular note is the verified seL4 kernel~\cite{klein:sel4:2009,klein:sel4:2010}. 445 This verification explicitly assumes the existence of, amongst other things, a trustworthy assembler. 446 447 \paragraph{Use of dependent types and Russell} 444 448 Our formalisation makes sparing use of dependent types. 445 449 In certain datastructures, such as tries and vectors, they are used to guarantee invariants. … … 449 453 However, there are certain cases where the use of dependent types is unavoidable. 450 454 For 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{}. 455 In cases such as these we make use of Matita's implementation of Russell~\cite{sozeau:subset:2006}. 456 In Matita, Russell may be implemented with two coercions and some notational sugaring. 452 457 453 458 \subsection{Related work} 454 459 \label{subsect.related.work} 460 461 % piton 462 We are not the first to consider the total correctness of an assembler for a non-trivial assembly language. 463 Perhaps the most impressive piece of work in this domain is the Piton stack~\cite{moore:piton:1996,moore:grand:2005}. 464 This 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? 466 467 % jinja 468 Klein and Nipkow consider a Java-like programming language, Jinja~\cite{klein:machine:2006,klein:machine:2010}. 469 They 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. 470 471 Finally, 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. 472 As previously mentioned, CompCert considers only extensional correctness of the compiler, and not intensional correctness, which CerCo focusses on. 473 However, CerCo also extends CompCert in other ways. 474 Namely, the CompCert verified compilation chain terminates at the PowerPC or ARM assembly level, and takes for granted the existence of a trustworthy assembler. 475 CerCo chooses to go further, by considering a verified compilation chain all the way down to the machine code level. 476 In essence, the work presented in this publication is one part of CerCo's extension over CompCert. 455 477 456 478 \bibliography{cpp-2011.bib}
Note: See TracChangeset
for help on using the changeset viewer.