Changeset 2362


Ignore:
Timestamp:
Sep 27, 2012, 5:34:35 PM (7 years ago)
Author:
mulligan
Message:

16 pages at last due to all sorts of fiddling. Any more additions will cause an overflow to 17 pages. Require Jaap's ArXiv? reference now.

Location:
Papers/cpp-asm-2012
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • Papers/cpp-asm-2012/cpp-2012-asm.bib

    r2095 r2362  
    3434@article
    3535{ klein:sel4:2010,
    36   author = {Gerwin Klein and June Andronick and Kevin Elphinstone and Gernot Heiser and David Cock and Philip Derrin and Dhammika Elkaduwe and Kai Engelhardt and Rafal Kolanski and Michael Norrish and Thomas Sewell, Harvey Tuch and Simon Winwood},
     36  author = {Gerwin Klein and June Andronick and Kevin Elphinstone and Gernot Heiser and David Cock and Philip Derrin and Dhammika Elkaduwe and Kai Engelhardt and Rafal Kolanski and Michael Norrish and Thomas Sewell and Harvey Tuch and Simon Winwood},
    3737  title = {{seL4}: Formal verification of an operating system kernel},
    3838  journal = {Communications of the {ACM}},
     
    8080  author = {Robert Atkey},
    8181  title = {{CoqJVM}: An executable specification of the {Java Virtual Machine} using dependent types},
    82   booktitle = {Types for Proofs and Programs},
     82  booktitle = {Types},
    8383  pages = {18--32},
    8484  year = {2007}
     
    9898  author = {Jaap Boender and Claudio {Sacerdoti Coen}},
    9999  title = {On the correctness of a branch displacement algorithm},
    100   booktitle = {Certified Proofs and Programs {(CPP)}},
     100  booktitle = {{CPP}},
    101101  year =  {2012},
    102102  note = {Submitted}
     
    116116  author = {Jaroslav \v{S}ev\v{c}\'ik and Viktor Vafeiadis and  Francesco {Zappa Nardelli} and Suresh Jagannathan and Peter Sewell},
    117117  title = {Relaxed-Memory Concurrency and Verified Compilation},
    118   booktitle = {Principles of Programming Languages {(POPL)}},
     118  booktitle = {{POPL}},
    119119  year = {2011}
    120120}
     
    124124  author = {Harvey Tuch and Gerwin Klein and Michael Norrish},
    125125  title = {Types, Bytes, and Separation Logic},
    126   booktitle = {Principles of Programming Languages {(POPL)}},
     126  booktitle = {{POPL}},
    127127  pages = {97--108},
    128128  year =  {2007}
     
    132132@inproceedings
    133133{ klein:sel4:2009,
    134   author = {Gerwin Klein and June Andronick and Kevin Elphinstone and Gernot Heiser and David Cock and Philip Derrin and Dhammika Elkaduwe and Kai Engelhardt and Rafal Kolanski and Michael Norrish and Thomas Sewell, Harvey Tuch and Simon Winwood},
     134  author = {Gerwin Klein and June Andronick and Kevin Elphinstone and Gernot Heiser and David Cock and Philip Derrin and Dhammika Elkaduwe and Kai Engelhardt and Rafal Kolanski and Michael Norrish and Thomas Sewell and Harvey Tuch and Simon Winwood},
    135135  title = {{seL4}: Formal verification of an operating system kernel},
    136   booktitle = {{ACM} Symposium on Operating Systems Principles {(SOSP)}},
     136  booktitle = {{SOSP}},
    137137  year = {2009}
    138138}
     
    160160  author = {Matthieu Sozeau},
    161161  title = {Subset Coercions in {Coq}},
    162   booktitle = {Types for proofs and programs},
     162  booktitle = {Types},
    163163  pages = {237--252},
    164164  year = {2006}
  • Papers/cpp-asm-2012/cpp-2012-asm.tex

    r2361 r2362  
    158158\label{sect.the.proof}
    159159
    160 The aim of the section is to explain the main ideas and steps of the certified
    161 proof of correctness for an optimizing assembler for the MCS-51.
    162 
    163 In Section~\ref{subsect.machine.code.semantics} we sketch an operational semantics (a realistic and efficient emulator) for the MCS-51.
     160Our aim here is to explain the main ideas and steps of the certified proof of correctness for an optimising assembler for the MCS-51.
     161
     162In Subsect.~\ref{subsect.machine.code.semantics} we sketch an operational semantics (a realistic and efficient emulator) for the MCS-51.
    164163We also introduce a syntax for decoded instructions that will be reused for the assembly language.
    165164
    166 In Section~\ref{subsect.assembly.code.semantics} we describe the assembly language and its operational semantics.
     165In Subsect.~\ref{subsect.assembly.code.semantics} we describe the assembly language and its operational semantics.
    167166The latter is parametric in the cost model that will be induced by the assembler, reusing the semantics of the machine code on all `real' instructions.
    168167
    169 Branch displacement policies are introduced in Section~\ref{subsect.the.assembler} where we also describe the assembler as a function over policies as previously described.
     168Branch displacement policies are introduced in Subsect.~\ref{subsect.the.assembler} where we also describe the assembler as a function over policies as previously described.
    170169
    171170To prove our assembler correct we show that the object code given in output, together with a cost model for the source program, simulates the source program executed using that cost model.
    172171The proof can be divided into two main lemmas.
    173 The first is correctness with respect to fetching, described in Section~\ref{subsect.total.correctness.of.the.assembler}.
     172The first is correctness with respect to fetching, described in Subsect.~\ref{subsect.total.correctness.of.the.assembler}.
    174173Roughly it states that a step of fetching at the assembly level, returning the decoded instruction $I$, is simulated by $n$ steps of fetching at the object level that returns instructions $J_1,\ldots,J_n$, where $J_1,\ldots,J_n$ is, amongst the possible expansions of $I$, the one picked by the policy.
    175174The second lemma states that $J_1,\ldots,J_n$ simulates $I$ but only if $I$ is well-behaved, i.e. manipulates addresses in `good' ways.
    176175To keep track of well-behaved address manipulations we record where addresses are currently stored (in memory or an accumulator).
    177176We introduce a dynamic checking function that inspects this map to determine if the operation is well-behaved, with an affirmative answer being the pre-condition of the lemma.
    178 The second lemma is detailed in Section~\ref{subsect.total.correctness.for.well.behaved.assembly.programs} where we also establish correctness of our assembler as a composition of the two lemmas: programs that are well-behaved when executed under the cost model induced by the compiler are correctly simulated by the compiled code.
     177The second lemma is detailed in Subsect.~\ref{subsect.total.correctness.for.well.behaved.assembly.programs} where we also establish correctness of our assembler as a composition of the two lemmas: programs that are well-behaved when executed under the cost model induced by the compiler are correctly simulated by the compiled code.
    179178
    180179% ---------------------------------------------------------------------------- %
     
    235234
    236235The parameterised type $A$ of \texttt{preinstruction} represents the addressing mode allowed for conditional jumps; in the \texttt{RealInstruction} constructor
    237 we constraint it to be a relative offset. A different instantiation will be
    238 used in the next Section for assembly programs.
     236we constraint it to be a relative offset.
     237A different instantiation will be used in the next section for assembly programs.
    239238
    240239Once decoded, execution proceeds by a case analysis on the decoded instruction, following the operation of the hardware.
     
    296295The costing is a function that maps valid program counters to pairs of natural numbers representing the number of clock ticks used by the pseudoinstructions stored at those program counters. For conditional jumps the two numbers differ
    297296to represent different costs for the `true branch' and the `false branch'.
    298 In the next Section we will see how the optimizing
    299 assembler induces the only costing that is preserved by compilation.
    300 Obviously the induced costing is determined by the branch displacement policy
    301 that decides how to expand every pseudojump to a label into concrete
    302 instructions.
     297In the next section we will see how the optimising
     298assembler induces the only costing (induced by the branch displacement policy deciding how to expand pseudojumps) that is preserved by compilation.
    303299
    304300Execution proceeds by first fetching from pseudo-code memory using the program counter---treated as an index into the pseudoinstruction list.
     
    313309The only limitation introduced by this approach is that the size of
    314310assembly programs is bounded by $2^16$.
    315 This will be further discussed in Subsection~\ref{subsect.total.correctness.for.well.behaved.assembly.programs}.
     311This will be further discussed in Subsect.~\ref{subsect.total.correctness.for.well.behaved.assembly.programs}.
    316312
    317313% ---------------------------------------------------------------------------- %
     
    399395
    400396The aim of this section is to prove the following informal statement: when we fetch an assembly pseudoinstruction \texttt{I} at address \texttt{ppc}, then we can fetch the expanded pseudoinstruction(s) \texttt{[J1, \ldots, Jn] = fetch\_pseudo\_instruction \ldots\ I\ ppc} from \texttt{policy ppc} in the code memory obtained by loading the assembled object code.
    401 This constitutes the first major step in the proof of correctness of the assembler, the next one being the simulation of \texttt{I} by \texttt{[J1, \ldots, Jn]} (see Subsection~\ref{subsect.total.correctness.for.well.behaved.assembly.programs}).
     397This constitutes the first major step in the proof of correctness of the assembler, the next one being the simulation of \texttt{I} by \texttt{[J1, \ldots, Jn]} (see Subsect.~\ref{subsect.total.correctness.for.well.behaved.assembly.programs}).
    402398
    403399The \texttt{assembly} function is given a Russell type (slightly simplified here):
     
    491487
    492488Here we use $\pi_1$ to project the existential witness from the Russell-typed function \texttt{assembly}.
    493 
    494489We read \texttt{fetch\_assembly\_pseudo2} as follows.
    495490Suppose we are given an assembly program which can be addressed by a 16-bit word and a policy that is correct for this program.
     
    523518In this paper we take a different approach, tracing memory locations (and accumulators) that contain memory addresses.
    524519We prove that only those assembly programs that use addresses in `safe' ways have their semantics preserved by the assembly process---a sort of dynamic type system sitting atop memory.
    525 In principle this approach allows us to introduce some permitted \emph{benign} manipulations of addresses that the traditional approach, using opaque addresses, cannot handle, therefore expanding the set of input programs that can be assembled correctly.
     520In principle this approach allows us to introduce some permitted \emph{benign} manipulations of addresses that the traditional approach cannot handle, therefore expanding the set of input programs that can be assembled correctly.
    526521This approach seems similar to one taken by Tuch \emph{et al}~\cite{tuch:types:2007} for reasoning about low-level C code.
    527522
     
    539534    $\times$ (option address_entry).
    540535\end{lstlisting}
    541 Here, \texttt{upper\_lower} is a type isomorphic to the booleans denoting whether a byte value is the upper or lower byte of some 16-bit address.
    542 
     536Here, \texttt{upper\_lower} is a type isomorphic to the booleans.
    543537The implementation of \texttt{internal\_pseudo\_address\_map} is complicated by some peculiarities of the MCS-51's instruction set.
    544538Note here that all addresses are 16 bit words, but are stored (and manipulated) as 8 bit bytes.
     
    621615The verified assembler, complete with the underlying formalisation of the semantics of MCS-51 machine code, will form the bedrock layer upon which the rest of CerCo will build its verified compiler platform.
    622616
    623 It is interesting to compare our work to an `industrial grade' assembler for the MCS-51: SDCC~\cite{sdcc:2011}.
    624 SDCC is the only open source C compiler that targets the MCS-51 instruction set.
     617We may compare our work to an `industrial grade' assembler for the MCS-51: SDCC~\cite{sdcc:2011}, the only open source C compiler that targets the MCS-51 instruction set.
    625618It appears that all pseudojumps in SDCC assembly are expanded to \texttt{LJMP} instructions, the worst possible jump expansion policy from an efficiency point of view.
    626 Note that this policy is the only possible policy \emph{in theory} that can preserve the semantics of an assembly program during the assembly process.
    627 However, this comes at the expense of assembler completeness: the generated program may be too large to fit into code memory.
    628 In this respect, there is a trade-off between the completeness of the assembler and the efficiency of the assembled program.
    629 The definition and proof of a terminating, correct jump expansion policy is described in a companion publication to this one~\cite{boender:correctness:2012}.
    630 
    631 Aside from their application in verified compiler projects such as CerCo, CompCert~\cite{leroy:formally:2009} and CompCertTSO~\cite{sevcik:relaxed-memory:2011}, verified assemblers such as ours could also be applied to the verification of operating system kernels.
    632 Of particular note is the verified seL4 kernel~\cite{klein:sel4:2009}.
    633 This verification explicitly assumes the existence of, amongst other things, a trustworthy assembler and compiler.
    634 
    635 CompCert, CompCertTSO and the seL4 formalisation assume the existence of `trustworthy' assemblers.
    636 For instance, the CompCert C compiler's default backend stops at the PowerPC assembly language.
    637 The observation that an optimising assembler cannot preserve the semantics of every assembly program may have consequences for these projects (though in the case of CompCertTSO, targetting a multiprocessor, what exactly constitutes the subset of `good programs' may not be entirely clear).
    638 If CompCert chooses to assume the existence of an optimising assembler, then care should be made to ensure that any assembly program produced by the CompCert compiler falls into the subset of programs that can have their semantics preserved by an optimising assembler.
     619Note that this policy is the only possible policy \emph{in theory} that can preserve the semantics of an assembly program during the assembly process, coming at the expense of assembler completeness as the generated program may be too large for code memory, there being a trade-off between the completeness of the assembler and the efficiency of the assembled program.
     620The definition and proof of a terminating, correct jump expansion policy is described elsewhere~\cite{boender:correctness:2012}.
     621
     622Verified assemblers could also be applied to the verification of operating system kernels and other formalised compilers.
     623For instance the verified seL4 kernel~\cite{klein:sel4:2009}, CompCert~\cite{leroy:formally:2009} and CompCertTSO~\cite{sevcik:relaxed-memory:2011} all explicitly assume the existence of trustworthy assemblers.
     624The fact that an optimising assembler cannot preserve the semantics of all assembly programs may have consequences for these projects.
    639625
    640626Our formalisation exploits dependent types in different ways and for multiple purposes.
     
    656642We are not the first to consider the correctness of an assembler for a non-trivial assembly language.
    657643The most impressive piece of work in this domain is Piton~\cite{moore:piton:1996}, 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---Lisp and $\mu$Gypsy~\cite{moore:grand:2005}.
    658 
    659644% jinja
    660 Klein and Nipkow consider a Java-like programming language, Jinja~\cite{klein:machine:2006}.
    661 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.
    662 
    663 Though other verified assemblers exist in the literature what sets our work apart from that above is our attempt to optimise the generated machine code.
    664 This complicates any formalisation effort as an attempt at the best possible selection of machine instructions must be made---especially important on devices with limited code memory.
     645Klein and Nipkow also provide a compiler, virtual machine and operational semantics for the Jinja~\cite{klein:machine:2006} language and prove that their compiler is semantics and type preserving.
     646
     647Though other verified assemblers exist what sets our work apart from that above is our attempt to optimise the generated machine code.
     648This complicates a formalisation as an attempt at the best possible selection of machine instructions must be made---especially important on devices with limited code memory.
    665649Care must be taken to ensure that the time properties of an assembly program are not modified by assembly lest we affect the semantics of any program employing the MCS-51's I/O facilities.
    666650This is only possible by inducing a cost model on the source code from the optimisation strategy and input program.
     
    672656We believe that the proof strategy is sound and that all axioms can be closed, up to minor bugs that should have local fixes that do not affect the global proof strategy.
    673657
    674 The development, including the definition of the executable semantics of the MCS-51, is spread across 29 files, with around 18,500 lines of Matita source.
    675 The bulk of the proof is contained in a series of files, \texttt{AssemblyProof.ma}, \texttt{AssemblyProofSplit.ma} and \texttt{AssemblyProofSplitSplit.ma} consisting of approximately 4500 lines of Matita source.
     658The complete development is spread across 29 files with around 20,000 lines of Matita source.
     659Relavent files are: \texttt{AssemblyProof.ma}, \texttt{AssemblyProofSplit.ma} and \texttt{AssemblyProofSplitSplit.ma}, consisting of approximately 4500 lines of Matita source.
    676660Numerous other lines of proofs are spread all over the development because of dependent types and the Russell proof style, which does not allow one to separate the code from the proofs.
    677661The low ratio between source lines and the number of lines of proof is unusual, but justified by the fact that the pseudo-assembly and the assembly language share most constructs and large swathes of the semantics are shared.
    678 Many lines of code are required to describe the complex semantics of the processor, but for the shared cases the proof of preservation of the semantics is essentially trivial.
    679662
    680663\bibliography{cpp-2012-asm.bib}
Note: See TracChangeset for help on using the changeset viewer.