Changeset 2346
 Timestamp:
 Sep 26, 2012, 3:16:45 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Papers/cppasm2012/cpp2012asm.tex
r2345 r2346 111 111 112 112 Note that the temporal tightness of the simulation is a fundamental prerequisite 113 of the correctness of the simulation because some functions of the MCS51, 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. 113 of the correctness of the simulation because some functions of the MCS51notably timers and I/Odepend on the microprocessor's clock. 114 If the pseudo and concrete clock differ the result of an I/O operation may not be preserved. 117 115 118 116 Branch displacement algorithms must have a deep knowledge of the way … … 122 120 Nevertheless, the correctness of the whole assembler only depends on the 123 121 correctness of the branch displacement algorithm. 124 Therefore, in the rest of the paper, we abstract the assembler onthe122 Therefore, in the rest of the paper, we presuppose the 125 123 existence of a correct policy, to be computed by a branch displacement 126 124 algorithm if it exists. A policy is the decision over how 127 125 any particular jump should be expanded; it is correct when the global 128 126 constraints 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. 127 The assembler fails to assemble an assembly program if and only if a correct policy does not exist. 128 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. 130 129 131 130 The final complication in the proof of correctness of our optimising assembler 132 is due to the kind of semantics associated to pseudo 131 is due to the kind of semantics associated to pseudoassembly programs. 133 132 Should assembly programs be allowed to freely manipulate addresses? The 134 133 answer to the question deeply affects the proof of correctness. … … 145 144 malign programs. In practice, we note how the alternative approach allows 146 145 more 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. 146 with benefits on the size of the formalisation. 147 148 The rest of this paper is a detailed description of our proof that is, in minimal part, still a work in progress. 151 149 152 150 We provide the reader with a brief `roadmap' for the rest of the paper. … … 164 162 In particular, it features dependent types that we exploit in the formalisation. 165 163 The syntax of the statements and definitions in the paper should be selfexplanatory, 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.168 164 Pairs are denoted with angular brackets, $\langle, \rangle$. 169 165 … … 174 170 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$. 175 171 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. 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.172 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. 177 173 178 174 %  % … … 184 180 The aim of the section is to explain the main ideas and steps of the certified 185 181 proof of correctness for an optimizing assembler for the MCS8051. The 186 formali zation is available at~\url{http://cerco.cs.unibo.it}.182 formalisation is available at~\url{http://cerco.cs.unibo.it}. 187 183 188 184 In Section~\ref{subsect.machine.code.semantics} we sketch an operational … … 194 190 language and operational semantics. The latter is parametric in the cost model 195 191 that 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. 192 machine code on all `real' (i.e. non pseudo) instructions. 193 194 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. 201 195 202 196 The proof of correctness of the assembler consists in showing that the … … 239 233 We may execute a single step of a machine code program using the \texttt{execute\_1} function, which returns an updated \texttt{Status}: 240 234 \begin{lstlisting} 241 definition execute_1: $\forall$cm. Status cm $\rightarrow$ Status cm := $\ldots$235 definition execute_1: $\forall$cm. Status cm $\rightarrow$ Status cm 242 236 \end{lstlisting} 243 237 Here \texttt{Status} is parameterised by \texttt{cm}, a code memory represented as a trie. … … 267 261  DEC addr $\Rightarrow$ 268 262 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) 270 264 (bitvector_of_nat 8 1) false in 271 set_arg_8 $\ldots$s addr result265 set_arg_8 s addr result 272 266 \end{lstlisting} 273 267 … … 304 298 definition execute_1_pseudo_instruction: 305 299 $\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 307 301 \end{lstlisting} 308 302 The type of \texttt{execute\_1\_pseudo\_instruction} is interesting. … … 383 377 The input \texttt{pi} is the pseudoinstruction to be expanded and is found at address \texttt{ppc} in the assembly program. 384 378 The 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 379 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)}. 386 380 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. 387 381 \begin{displaymath} … … 431 425 In plain words, the type of \texttt{assembly} states the following. 432 426 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 16bit word. 433 Then if we fetch from the pseudo program counter \texttt{ppc} we get a pseudoinstruction \texttt{pi} and a new pseudoprogram counter \texttt{ppc}.427 Then if we fetch from the pseudoprogram counter \texttt{ppc} we get a pseudoinstruction \texttt{pi} and a new pseudoprogram counter \texttt{ppc}. 434 428 Further, assembling the pseudoinstruction \texttt{pi} results in a list of bytes, \texttt{a}. 435 429 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}. … … 502 496 \end{lstlisting} 503 497 504 Here we use $\pi_1 \ldots$ to project the existential witness from the Russelltyped function \texttt{assembly}.498 Here we use $\pi_1$ to project the existential witness from the Russelltyped function \texttt{assembly}. 505 499 506 500 We read \texttt{fetch\_assembly\_pseudo2} as follows. … … 620 614 [dpm change] 621 615 The statement is standard for forward simulation, but restricted to \texttt{PseudoStatuses} \texttt{ps} whose next instruction to be executed is wellbehaved 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 616 Further, we explicitly require proof that our policy is correct and the pseudoprogram counter lies within the bounds of the program. 623 617 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. 624 618 … … 663 657 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. 664 658 665 Finally, dependent types, together with Matita's liberal system of coercions, allow us to simulate almost entirelyin user spacethe proof methodology ` `Russell'' of Sozeau~\cite{sozeau:subset:2006}.659 Finally, dependent types, together with Matita's liberal system of coercions, allow us to simulate almost entirelyin user spacethe proof methodology `Russell' of Sozeau~\cite{sozeau:subset:2006}. 666 660 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. 667 661 For example, it would be unnatural to see the proof that fetch and assembly commute as the specification of one of the two functions. … … 690 684 691 685 All 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.686 In particular, we have assumed several properties of `library functions' related in particular to modular arithmetic and datastructure manipulation. 693 687 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. 694 688 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.
Note: See TracChangeset
for help on using the changeset viewer.