# Changeset 2346 for Papers/cpp-asm-2012

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

Minor changes to Claudio's new text

File:
1 edited

### Legend:

Unmodified
 r2345 Note that the temporal tightness of the simulation is a fundamental prerequisite of the correctness of the simulation because some functions of the MCS-51, notably timers and I/O, depend on the microprocessor's clock. If the pseudo and concrete clock differs, the result of an I/O operation may not be preserved. of the correctness of the simulation because some functions of the MCS-51---notably timers and I/O---depend on the microprocessor's clock. If the pseudo- and concrete clock differ the result of an I/O operation may not be preserved. Branch displacement algorithms must have a deep knowledge of the way Nevertheless, the correctness of the whole assembler only depends on the correctness of the branch displacement algorithm. Therefore, in the rest of the paper, we abstract the assembler on the Therefore, in the rest of the paper, we presuppose the existence of a correct policy, to be computed by a branch displacement algorithm if it exists. A policy is the decision over how any particular jump should be expanded; it is correct when the global constraints are satisfied. 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. 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. The final complication in the proof of correctness of our optimising assembler is due to the kind of semantics associated to pseudo assembly programs. is due to the kind of semantics associated to pseudo-assembly programs. Should assembly programs be allowed to freely manipulate addresses? The answer to the question deeply affects the proof of correctness. malign programs. In practice, we note how the alternative approach allows more code reusal between the semantics of assembly code and object code, with benefits on the size of the formalization. The rest of this paper is a detailed description of our proof that is, in minimal part, still a work in progress. with benefits on the size of the formalisation. The rest of this paper is a detailed description of our proof that is, in minimal part, still a work in progress. We provide the reader with a brief roadmap' for the rest of the paper. In particular, it features dependent types that we exploit in the formalisation. The syntax of the statements and definitions in the paper should be self-explanatory, at least to those exposed to dependent type theory. 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. Those that are not inferred are left to the user as proof obligations. Pairs are denoted with angular brackets, $\langle-, -\rangle$. 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$. This 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. 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. 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. % ---------------------------------------------------------------------------- % The aim of the section is to explain the main ideas and steps of the certified proof of correctness for an optimizing assembler for the MCS-8051. The formalization is available at~\url{http://cerco.cs.unibo.it}. formalisation is available at~\url{http://cerco.cs.unibo.it}. In Section~\ref{subsect.machine.code.semantics} we sketch an operational language and operational semantics. The latter is parametric in the cost model that will be induced by the assembler. It fully reuses the semantics of the machine code on all real'' (i.e. non pseudo) instructions. 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. machine code on all real' (i.e. non pseudo) instructions. 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. The proof of correctness of the assembler consists in showing that the We may execute a single step of a machine code program using the \texttt{execute\_1} function, which returns an updated \texttt{Status}: \begin{lstlisting} definition execute_1: $\forall$cm. Status cm $\rightarrow$ Status cm := $\ldots$ definition execute_1: $\forall$cm. Status cm $\rightarrow$ Status cm \end{lstlisting} Here \texttt{Status} is parameterised by \texttt{cm}, a code memory represented as a trie. | DEC addr $\Rightarrow$ let s := add_ticks1 s in let $\langle$result, flags$\rangle$ := sub_8_with_carry (get_arg_8 $\ldots$ s true addr) let $\langle$result, flags$\rangle$ := sub_8_with_carry (get_arg_8 s true addr) (bitvector_of_nat 8 1) false in set_arg_8 $\ldots$ s addr result set_arg_8 s addr result \end{lstlisting} definition execute_1_pseudo_instruction: $\forall$cm. ($\forall$ppc: Word. ppc < $\mid$snd cm$\mid$ $\rightarrow$ nat $\times$ nat) $\rightarrow$ $\forall$s:PseudoStatus cm. program_counter $\ldots$ s < $\mid$snd cm$\mid$ $\rightarrow$ PseudoStatus cm := $\ldots$ program_counter s < $\mid$snd cm$\mid$ $\rightarrow$ PseudoStatus cm \end{lstlisting} The type of \texttt{execute\_1\_pseudo\_instruction} is interesting. The input \texttt{pi} is the pseudoinstruction to be expanded and is found at address \texttt{ppc} in the assembly program. The policy is defined using the two functions \texttt{sigma} and \texttt{policy}, of which \texttt{sigma} is the most interesting. 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)}. The 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)}. Of 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. \begin{displaymath} In plain words, the type of \texttt{assembly} states the following. Suppose 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. 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}. 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}. Further, assembling the pseudoinstruction \texttt{pi} results in a list of bytes, \texttt{a}. Then, 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}. \end{lstlisting} Here we use $\pi_1 \ldots$ to project the existential witness from the Russell-typed function \texttt{assembly}. Here we use $\pi_1$ to project the existential witness from the Russell-typed function \texttt{assembly}. We read \texttt{fetch\_assembly\_pseudo2} as follows. [dpm change] The 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}. Further, we explicitly require proof that our policy is correct and the pseudo program counter lies within the bounds of the program. Further, we explicitly require proof that our policy is correct and the pseudo-program counter lies within the bounds of the program. Theorem \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. This also allowed to simplify the initial proof by dropping lemmas establishing that one function fails if and only if some previous function does so. 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}. 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}. However, 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. For example, it would be unnatural to see the proof that fetch and assembly commute as the specification of one of the two functions. All files relating to our formalisation effort can be found online at~\url{http://cerco.cs.unibo.it}. In particular, we have assumed several properties of library functions'' related in particular to modular arithmetic and datastructure manipulation. In particular, we have assumed several properties of library functions' related in particular to modular arithmetic and datastructure manipulation. Moreover, 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. We 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.