Changeset 2346


Ignore:
Timestamp:
Sep 26, 2012, 3:16:45 PM (7 years ago)
Author:
mulligan
Message:

Minor changes to Claudio's new text

File:
1 edited

Legend:

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

    r2345 r2346  
    111111
    112112Note that the temporal tightness of the simulation is a fundamental prerequisite
    113 of the correctness of the simulation because some functions of the MCS-51,
    114 notably timers and I/O, depend on the microprocessor's clock. If the
    115 pseudo and concrete clock differs, the result of an I/O operation may not be
    116 preserved.
     113of the correctness of the simulation because some functions of the MCS-51---notably timers and I/O---depend on the microprocessor's clock.
     114If the pseudo- and concrete clock differ the result of an I/O operation may not be preserved.
    117115
    118116Branch displacement algorithms must have a deep knowledge of the way
     
    122120Nevertheless, the correctness of the whole assembler only depends on the
    123121correctness of the branch displacement algorithm.
    124 Therefore, in the rest of the paper, we abstract the assembler on the
     122Therefore, in the rest of the paper, we presuppose the
    125123existence of a correct policy, to be computed by a branch displacement
    126124algorithm if it exists. A policy is the decision over how
    127125any particular jump should be expanded; it is correct when the global
    128126constraints are satisfied.
    129 The assembler fails to assemble an assembly program if and only if a correct policy does not exist. This is stated in an elegant way in the dependent type of the assembler: the assembly function is total over a program, a policy and the proof that the policy is correct for that program.
     127The assembler fails to assemble an assembly program if and only if a correct policy does not exist.
     128This is stated in an elegant way in the dependent type of the assembler: the assembly function is total over a program, a policy and the proof that the policy is correct for that program.
    130129
    131130The final complication in the proof of correctness of our optimising assembler
    132 is due to the kind of semantics associated to pseudo assembly programs.
     131is due to the kind of semantics associated to pseudo-assembly programs.
    133132Should assembly programs be allowed to freely manipulate addresses? The
    134133answer to the question deeply affects the proof of correctness.
     
    145144malign programs. In practice, we note how the alternative approach allows
    146145more code reusal between the semantics of assembly code and object code,
    147 with benefits on the size of the formalization.
    148 
    149 The rest of this paper is a detailed description of our proof that is, in
    150 minimal part, still a work in progress.
     146with benefits on the size of the formalisation.
     147
     148The rest of this paper is a detailed description of our proof that is, in minimal part, still a work in progress.
    151149
    152150We provide the reader with a brief `roadmap' for the rest of the paper.
     
    164162In particular, it features dependent types that we exploit in the formalisation.
    165163The syntax of the statements and definitions in the paper should be self-explanatory, at least to those exposed to dependent type theory.
    166 We only remark that the use of `$\mathtt{?}$' or `$\mathtt{\ldots}$' for omitting single terms or sequences of terms to be inferred automatically by the system, respectively.
    167 Those that are not inferred are left to the user as proof obligations.
    168164Pairs are denoted with angular brackets, $\langle-, -\rangle$.
    169165
     
    174170 For instance, to apply a coercion to force $\lambda x.M : A \to B$ to have type $\forall x:A.\Sigma y:B.P~x~y$, the system looks for a coercion from $M: B$ to $\Sigma y:B.P~x~y$ in a context augmented with $x:A$.
    175171This is significant when the coercion opens a proof obligation, as the user will be presented with multiple, but simpler proof obligations in the correct context.
    176 In this way, Matita supports the ``Russell'' proof methodology developed by Sozeau in~\cite{sozeau:subset:2006}, with an implementation that is lighter and more tightly integrated with the system than that of Coq.
     172In this way, Matita supports the `Russell' proof methodology developed by Sozeau in~\cite{sozeau:subset:2006}, with an implementation that is lighter and more tightly integrated with the system than that of Coq.
    177173
    178174% ---------------------------------------------------------------------------- %
     
    184180The aim of the section is to explain the main ideas and steps of the certified
    185181proof of correctness for an optimizing assembler for the MCS-8051. The
    186 formalization is available at~\url{http://cerco.cs.unibo.it}.
     182formalisation is available at~\url{http://cerco.cs.unibo.it}.
    187183
    188184In Section~\ref{subsect.machine.code.semantics} we sketch an operational
     
    194190language and operational semantics. The latter is parametric in the cost model
    195191that will be induced by the assembler. It fully reuses the semantics of the
    196 machine code on all ``real'' (i.e. non pseudo) instructions.
    197 
    198 Branch displacement policies are introduced in
    199 Section~\ref{subsect.the.assembler} where we
    200 also describe the assembler as a function over policies as previously described.
     192machine code on all `real' (i.e. non pseudo) instructions.
     193
     194Branch displacement policies are introduced in Section~\ref{subsect.the.assembler} where we also describe the assembler as a function over policies as previously described.
    201195
    202196The proof of correctness of the assembler consists in showing that the
     
    239233We may execute a single step of a machine code program using the \texttt{execute\_1} function, which returns an updated \texttt{Status}:
    240234\begin{lstlisting}
    241 definition execute_1: $\forall$cm. Status cm $\rightarrow$ Status cm := $\ldots$
     235definition execute_1: $\forall$cm. Status cm $\rightarrow$ Status cm
    242236\end{lstlisting}
    243237Here \texttt{Status} is parameterised by \texttt{cm}, a code memory represented as a trie.
     
    267261 | DEC addr $\Rightarrow$
    268262  let s := add_ticks1 s in
    269   let $\langle$result, flags$\rangle$ := sub_8_with_carry (get_arg_8 $\ldots$ s true addr)
     263  let $\langle$result, flags$\rangle$ := sub_8_with_carry (get_arg_8 s true addr)
    270264   (bitvector_of_nat 8 1) false in
    271      set_arg_8 $\ldots$ s addr result
     265     set_arg_8 s addr result
    272266\end{lstlisting}
    273267
     
    304298definition execute_1_pseudo_instruction:
    305299 $\forall$cm. ($\forall$ppc: Word. ppc < $\mid$snd cm$\mid$ $\rightarrow$ nat $\times$ nat) $\rightarrow$ $\forall$s:PseudoStatus cm.
    306   program_counter $\ldots$ s < $\mid$snd cm$\mid$ $\rightarrow$ PseudoStatus cm := $\ldots$
     300  program_counter s < $\mid$snd cm$\mid$ $\rightarrow$ PseudoStatus cm
    307301\end{lstlisting}
    308302The type of \texttt{execute\_1\_pseudo\_instruction} is interesting.
     
    383377The input \texttt{pi} is the pseudoinstruction to be expanded and is found at address \texttt{ppc} in the assembly program.
    384378The policy is defined using the two functions \texttt{sigma} and \texttt{policy}, of which \texttt{sigma} is the most interesting.
    385 The function \texttt{sigma} maps pseudo program counters to program counters: the encoding of the expansion of the pseudoinstruction found at address \texttt{a} in the assembly code should be placed into code memory at address \texttt{sigma(a)}.
     379The function \texttt{sigma} maps pseudoprogram counters to program counters: the encoding of the expansion of the pseudoinstruction found at address \texttt{a} in the assembly code should be placed into code memory at address \texttt{sigma(a)}.
    386380Of course this is possible only if the policy is correct, which means that the encoding of consecutive assembly instructions must be consecutive in code memory.
    387381\begin{displaymath}
     
    431425In plain words, the type of \texttt{assembly} states the following.
    432426Suppose we are given a policy that is correct for the program we are assembling, and suppose the program to be assembled is fully addressable by a 16-bit word.
    433 Then if we fetch from the pseudo program counter \texttt{ppc} we get a pseudoinstruction \texttt{pi} and a new pseudo program counter \texttt{ppc}.
     427Then if we fetch from the pseudo-program counter \texttt{ppc} we get a pseudoinstruction \texttt{pi} and a new pseudo-program counter \texttt{ppc}.
    434428Further, assembling the pseudoinstruction \texttt{pi} results in a list of bytes, \texttt{a}.
    435429Then, indexing into this list with any natural number \texttt{j} less than the length of \texttt{a} gives the same result as indexing into \texttt{assembled} with \texttt{sigma(ppc)} (the program counter pointing to the start of the expansion in \texttt{assembled}) plus \texttt{j}.
     
    502496\end{lstlisting}
    503497
    504 Here we use $\pi_1 \ldots$ to project the existential witness from the Russell-typed function \texttt{assembly}.
     498Here we use $\pi_1$ to project the existential witness from the Russell-typed function \texttt{assembly}.
    505499
    506500We read \texttt{fetch\_assembly\_pseudo2} as follows.
     
    620614[dpm change]
    621615The statement is standard for forward simulation, but restricted to \texttt{PseudoStatuses} \texttt{ps} whose next instruction to be executed is well-behaved with respect to the \texttt{internal\_pseudo\_address\_map} \texttt{M}.
    622 Further, we explicitly require proof that our policy is correct and the pseudo program counter lies within the bounds of the program.
     616Further, we explicitly require proof that our policy is correct and the pseudo-program counter lies within the bounds of the program.
    623617Theorem \texttt{main\_thm} establishes the total correctness of the assembly process and can simply be lifted to the forward simulation of an arbitrary number of well behaved steps on the assembly program.
    624618
     
    663657This also allowed to simplify the initial proof by dropping lemmas establishing that one function fails if and only if some previous function does so.
    664658
    665 Finally, dependent types, together with Matita's liberal system of coercions, allow us to simulate almost entirely---in user space---the proof methodology ``Russell'' of Sozeau~\cite{sozeau:subset:2006}.
     659Finally, dependent types, together with Matita's liberal system of coercions, allow us to simulate almost entirely---in user space---the proof methodology `Russell' of Sozeau~\cite{sozeau:subset:2006}.
    666660However, not every proof has been carried out in this way: we only used this style to prove that a function satisfies a specification that only involves that function in a significant way.
    667661For example, it would be unnatural to see the proof that fetch and assembly commute as the specification of one of the two functions.
     
    690684
    691685All files relating to our formalisation effort can be found online at~\url{http://cerco.cs.unibo.it}.
    692 In particular, we have assumed several properties of ``library functions'' related in particular to modular arithmetic and datastructure manipulation.
     686In particular, we have assumed several properties of `library functions' related in particular to modular arithmetic and datastructure manipulation.
    693687Moreover, we have axiomatised various ancillary functions needed to complete the main theorems, as well as some `routine' proof obligations of the theorems themselves, preferring instead to focus on the main meat of the theorems.
    694688We thus believe that the proof strategy is sound and that we will be able to close soon all axioms, up to possible minor bugs that should have local fixes that do not affect the global proof strategy.
Note: See TracChangeset for help on using the changeset viewer.