Changeset 999


Ignore:
Timestamp:
Jun 20, 2011, 5:07:29 PM (8 years ago)
Author:
mulligan
Message:

conclusions

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CPP2011/cpp-2011.tex

    r997 r999  
    5555We prove, under the assumption of the existence of a correct policy, that the assembly process never fails and preserves the semantics of a subset of assembly programs.
    5656Correct policies fail to exist only in a limited number of pathological circumstances.
    57 Quite surprisingly, it is impossible for an optimising assembler to preserve the semantics of every assembly program.
     57Our assembler is complete with respect to the choice of policy.
     58
     59Surprisingly, we observe that it is impossible for an optimising assembler to preserve the semantics of every assembly program.
    5860\end{abstract}
    5961
     
    155157To understand why this problem is not trivial, consider the following snippet of assembly code:
    156158\begin{displaymath}
    157 \text{dpm: finish me}
     159\begin{array}{r@{\qquad}r@{\quad}l@{\;\;}l@{\qquad}l}
     160\text{1:} & \mathtt{0x000}  & \texttt{LJMP} & \texttt{0x100}  & \text{\texttt{;; Jump forward 256.}} \\
     161\text{2:} & \mathtt{...}    & \mathtt{...}  &                 &                                               \\
     162\text{3:} & \mathtt{0x0FA}  & \texttt{LJMP} & \texttt{0x100}  & \text{\texttt{;; Jump forward 256.}} \\
     163\text{4:} & \mathtt{...}    & \mathtt{...}  &                 &                                               \\
     164\text{5:} & \mathtt{0x100}  & \texttt{LJMP} & \texttt{0x100}  & \text{\texttt{;; Jump forward 256.}} \\
     165\text{6:} & \mathtt{...}    & \mathtt{...}  &                 &                                               \\
     166\text{7:} & \mathtt{0x1F9}  & \texttt{LJMP} & \texttt{-0x300} & \text{\texttt{;; Arbitrary instruction.}} \\
     167\end{array}
    158168\end{displaymath}
    159 
    160 As our example shows, given an occurence $l$ of an \texttt{LJMP} instruction, it may be possible to shrink $l$ to an occurence of an \texttt{SJMP} providing we can shrink any \texttt{LJMP}s that exist between $l$ and its target location.
    161 However, shrinking these \texttt{LJMP}s may in turn depend on shrinking $l$ to an \texttt{SJMP}, as it is perfectly possible to jump backwards.
    162 In short, unless we can somehow break this loop of circularity, and similar knotty configurations of jumps, we are stuck with a suboptimal solution to the expanding jumps problem.
     169We observe that $100_{16} = 256_{10}$, and lies \emph{just} outside the range expressible in an 8-bit byte (0--255).
     170
     171As our example shows, given an occurence $l$ of an \texttt{LJMP} instruction, it may be possible to shrink $l$ to an occurence of an \texttt{SJMP}---consuming fewer bytes of code memory---provided we can shrink any \texttt{LJMP}s that exist between $l$ and its target location.
     172In particular, if we can somehow shrink the \texttt{LJMP} occurring at line 5, the \texttt{LJMP}s occurring at lines 1 and 3 above may both be replaced by \texttt{SJMP}s, provided that \emph{both} jumps at 1 and 3 are replaced at the same time.
     173Thinking more, it is easy to imagine knotty, circular configurations of jumps developing, each jump occurrence only being shrinkable if every other is.
     174Finding a solution to this `shrinking jumps' problem then involves us finding a method to break any vicious circularities that develop.
    163175
    164176How we went about resolving this problem affected the shape of our proof of correctness for the whole assembler in a rather profound way.
     
    222234The counterpart of the \texttt{Status} record is \texttt{PseudoStatus}.
    223235Instead of code memory being implemented as tries of bytes, code memory is here implemented as lists of pseudoinstructions, and program counters are merely indices into this list.
     236In actual fact, both \texttt{Status} and \texttt{PseudoStatus} are both specialisations of the same \texttt{PreStatus} record, parametric in the representation of code memory.
     237This allows us to share some code that is common to both records (for instance, `setter' and `getter' functions).
     238A further benefit of this sharing is that those instructions that are completely ambivalent about the particular representation of code memory can be factored out into their own type.
     239
    224240Our analogue of \texttt{execute\_1} is \texttt{execute\_1\_pseudo\_instruction}:
    225241\begin{lstlisting}
     
    234250The costing returns \emph{pairs} of natural numbers because, in the case of expanding conditional jumps to labels, the expansion of the `true branch' and `false branch' may differ in the number of clock ticks needed for execution.
    235251This timing information is used inside \texttt{execute\_1\_pseudo\_instruction} to update the clock of the \texttt{PseudoStatus}.
    236 During the proof of correctness of the assembler we relate the clocks of \texttt{Status}es and \texttt{PseudoStatus}es.
     252During the proof of correctness of the assembler we relate the clocks of \texttt{Status}es and \texttt{PseudoStatus}es for the policy induced by the cost model and optimisations.
    237253
    238254The assembler, mapping programs consisting of lists of pseudoinstructions to lists of bytes, operates in a mostly straightforward manner.
    239 To a degree of approximation, the assembler on an assembly program, consisting of $n$ pseudoinstructions $\mathtt{P_i}$ for $1 \leq i \leq n$, works as in the following diagram:
     255To a degree of approximation, the assembler on an assembly program, consisting of $n$ pseudoinstructions $\mathtt{P_i}$ for $1 \leq i \leq n$, works as in the following diagram (we use $-^{*}$ to denote a combined map and flatten operation):
    240256\begin{displaymath}
    241 [\mathtt{P_1}, \ldots \mathtt{P_n}] \xrightarrow{\mathtt{flatten}\left(\mathtt{P_i} \xrightarrow{\mbox{\fontsize{7}{9}\selectfont$\mathtt{expand}$}} \mathtt{[I_1^i, \ldots I^q_i]} \xrightarrow{\mbox{\fontsize{7}{9}\selectfont$\mathtt{assembly1}^*$}} \mathtt{[0110]}\right)^{*}} \mathtt{[010101]}
     257[\mathtt{P_1}, \ldots \mathtt{P_n}] \xrightarrow{\left(\mathtt{P_i} \xrightarrow{\mbox{\fontsize{7}{9}\selectfont$\mathtt{expand\_pseudo\_instruction}$}} \mathtt{[I_1^i, \ldots I^q_i]} \xrightarrow{\mbox{\fontsize{7}{9}\selectfont$\mathtt{~~~~~~~~assembly1^{*}~~~~~~~~}$}} \mathtt{[0110]}\right)^{*}} \mathtt{[010101]}
    242258\end{displaymath}
    243259Here $\mathtt{I^i_j}$ for $1 \leq j \leq q$ are the $q$ machine code instructions obtained by expanding, with \texttt{expand\_pseudo\_instruction}, a single pseudoinstruction.
     
    250266By composition, we then have that the whole assembly process is semantics preserving.
    251267
    252 This is a tempting approach to the proof, but ultimately the wrong approach.
    253 In particular, it is important that we track how the program counter indexing into the assembly program, and the machine's program counter evolve, so that we can relate them.
    254 Expanding pseudoinstructions requires that the machine's program counter be incremented by $n$ steps, for $1 \leq n$, for every increment of the assembly program's program counter.
    255 Keeping track of the correspondence between the two program counters quickly becomes unfeasible using a compositional approach, and hence the proof must be monolithic.
     268%This is a tempting approach to the proof, but ultimately the wrong approach.
     269%In particular, it is important that we track how the program counter indexing into the assembly program, and the machine's program counter evolve, so that we can relate them.
     270%Expanding pseudoinstructions requires that the machine's program counter be incremented by $n$ steps, for $1 \leq n$, for every increment of the assembly program's program counter.
     271%Keeping track of the correspondence between the two program counters quickly becomes unfeasible using a compositional approach, and hence the proof must be monolithic.
    256272
    257273% ---------------------------------------------------------------------------- %
     
    469485We have proved the total correctness of an assembler for MCS-51 assembly language.
    470486In 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.
    471 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.
     487Expanding these pseudoinstructions into machine code instructions is not trivial, and the proof that the assembly process is `correct', in that the semantics of a subset of assembly programs are not changed is complex.
     488Further, we have observed the `shocking' fact that any optimising assembler cannot preserve the semantics of all assembly programs.
    472489
    473490The formalisation is a key component of the CerCo project, which aims to produce a verified concrete complexity preserving compiler for a large subset of the C programming language.
    474491The verified assembler, complete with the underlying formalisation of the semantics of MCS-51 machine code (described fully in~\cite{mulligan:executable:2011}), will form the bedrock layer upon which the rest of the CerCo project will build its verified compiler platform.
    475 
    476 Aside from their application in verified compiler projects such as CerCo, verified assemblers such as ours could also be applied to the verification of operating system kernels.
     492However, further work is needed.
     493In particular, as it stands, the code produced by the prototype CerCo C compiler does not fall into the `semantics preserving' subset of assembly programs for our assembler.
     494This is because the MCS-51 features a small stack space, and a larger stack is customarily manually emulated in external RAM.
     495As a result, the majority of programs feature slices of memory addresses and program counters being moved in-and-out of external RAM via the registers, simulating the stack mechanism.
     496At the moment, this movement is not tracked by \texttt{internal\_pseudo\_address\_map}, which only tracks the movement of memory addresses in low internal RAM.
     497We leave extending this tracking of memory addresses throughout the whole of the MCS-51's address spaces as future work.
     498
     499Aside from their application in verified compiler projects such as CerCo and CompCert, verified assemblers such as ours could also be applied to the verification of operating system kernels.
    477500Of particular note is the verified seL4 kernel~\cite{klein:sel4:2009,klein:sel4:2010}.
    478501This verification explicitly assumes the existence of, amongst other things, a trustworthy assembler and compiler.
    479502
    480 \paragraph{Use of dependent types and Russell}
    481 Our formalisation makes sparing use of dependent types.
    482 In certain datastructures, such as tries and vectors, they are used to guarantee invariants.
    483 However, we have currently shyed away from making extensive use of dependent types and inductive predicates in the proof of correctness for the assembler itself.
    484 This is because complex dependent types and inductive predicates tend not to co\"operate particularly well with tactics such as inversion.
    485 
    486 However, there are certain cases where the use of dependent types is unavoidable.
    487 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.
    488 In cases such as these we make use of Matita's implementation of Russell~\cite{sozeau:subset:2006}.
    489 In Matita, Russell may be implemented with two coercions and some notational sugaring.
     503We note here that both CompCert and the seL4 formalisation assume the existence of `trustworthy' assemblers.
     504Our observation that an optimising assembler cannot preserve the semantics of every assembly program may have important consequences for these projects.
     505In particular, 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 C compiler falls into the class of assembly programs that have a hope of having their semantics preserved by an optimising assembler.
     506
     507In certain places in our formalisation (e.g. in proving \texttt{build\_maps} is correct) we made use of Matita's implementation of Russell~\cite{sozeau:subset:2006}.
     508In Matita, Russell may be implemented using two coercions and some notational sugaring.
     509% more
    490510
    491511\subsection{Related work}
     
    496516Perhaps the most impressive piece of work in this domain is the Piton stack~\cite{moore:piton:1996,moore:grand:2005}.
    497517This 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}.
    498 %dpm more: weirich paper?
    499518
    500519% jinja
     
    502521They 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.
    503522
    504 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.
     523We believe many other verified assemblers exist in the literature.
     524However, what sets our work apart from that above is our attempt to optimise the machine code generated by our assembler.
     525This complicates any formalisation effort, as the best possible selection of machine instructions must be made, especially important on a device such as the MCS-51 with a miniscule code memory.
     526Further, care must be taken to ensure that the time properties of an assembly program are not modified by the assembly process lest we affect the semantics of any program employing the MCS-51's I/O facilities.
     527
     528Finally, mention of CerCo will invariably invite comparisons with CompCert~\cite{compcert:2011,leroy:formal:2009}, another verified compiler project closely related to CerCo.
    505529As previously mentioned, CompCert considers only extensional correctness of the compiler, and not intensional correctness, which CerCo focusses on.
    506530However, CerCo also extends CompCert in other ways.
     
    509533In essence, the work presented in this publication is one part of CerCo's extension over CompCert.
    510534
     535\subsection{Source code}
     536\label{subsect.source.code}
     537
     538All files relating to our formalisation effort can be found online at~\url{http://cerco.cs.unibo.it}.
     539
    511540\bibliography{cpp-2011.bib}
    512541
Note: See TracChangeset for help on using the changeset viewer.