Changeset 2379
 Timestamp:
 Sep 28, 2012, 6:26:29 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Papers/cppasm2012/cpp2012asm.tex
r2378 r2379 137 137 In practice, we note how our approach facilitates more code reuse between the semantics of assembly code and object code. 138 138 139 The formalization of the assembler and its correctness proof are given in Section~\ref{sect.the.proof}. Section~\ref{sect.matita} provides a brief introduction 140 to the syntax of Matita. Section~\ref{sect.conclusions} presents the conclusions and relations with previous work. 141 142 %  % 143 % SECTION % 144 %  % 145 \section{Matita} 146 \label{sect.matita} 139 The formalisation of the assembler and its correctness proof are given in Sect.~\ref{sect.the.proof}. 140 Sect.~\ref{sect.conclusions} presents the conclusions and relations with previous work. 141 142 %  % 143 % SECTION % 144 %  % 145 \paragraph{Matita} 146 %\section{Matita} 147 %\label{sect.matita} 147 148 Matita is a proof assistant based on a variant of the Calculus of (Co)inductive Constructions~\cite{asperti:user:2007}. 148 149 It features dependent types that we exploit in the formalisation. … … 421 422 We now begin the proof of correctness of the assembler. 422 423 Correctness consists of two properties: firstly that the assembly process never fails when fed a correct policy and secondly the object code returned simulates the source code when the latter is executed according to the cost model also returned by the assembler. 423 424 The second property above can be further decomposed into two main properties: correctness with respect to fetching and decoding and correctness with respect to execution. 424 This second property can be further decomposed into two main properties: correctness with respect to fetching and decoding and correctness with respect to execution. 425 425 426 426 Informally, correctness with respect to fetching is the following 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. … … 469 469 \end{lstlisting} 470 470 We read \texttt{fetch\_assembly} as follows. 471 Any time the encoding \texttt{assembled} of an instruction \texttt{i} is found in code memory starting at position \texttt{pc} (the hypothesis \texttt{encoding\_check} \ldots), when we fetch at address \texttt{pc} we retrieve the instruction \texttt{i}, the updatedprogram counter is \texttt{pc} plus the length of the encoding, and the cost of the fetched instruction is the one predicted for \texttt{i}.471 Any time the encoding \texttt{assembled} of an instruction \texttt{i} is found in code memory starting at position \texttt{pc} (the hypothesis \texttt{encoding\_check} \ldots), when we fetch at address \texttt{pc} retrieving the instruction \texttt{i}, the new program counter is \texttt{pc} plus the length of the encoding, and the cost of the fetched instruction is the one predicted for \texttt{i}. 472 472 Or, in plainer words, assembling, storing and then immediately fetching gets you back to where you started. 473 473 … … 570 570 \end{cases} 571 571 \end{gather*} 572 In order to prove the preservation of the semantics, we need toassociate an object code status to each assembly pseudostatus.572 To prove semantic preservation we must associate an object code status to each assembly pseudostatus. 573 573 This operation is driven by the current \texttt{AddrMap}: if at address \texttt{a} the assembly level memory holds \texttt{d}, then if \texttt{AddrMap(a) = Data} the object code memory will hold \texttt{d} (data is preserved), otherwise it will hold \texttt{policy(d)}. 574 574 If all the operations accepted by the address update map are wellbehaved, this is sufficient to show preservation of the semantics for those computation steps that are wellbehaved, i.e. such that the map update does not fail. … … 599 599 \end{lstlisting} 600 600 The function that implements the tracking map update, previously denoted by $\llbracket  \rrbracket$, is called \texttt{next\_internal\_pseudo\_address\_map} in the formalisation. 601 For the time being, we decided to accept as good behaviours the copy of addresses amongmemory cells and the accumulator (\texttt{MOV} pseudoinstruction) and the use of the \texttt{CJNE} conditional jump that compares two addresses and jumps to a given label if the two labels are equal.601 For the time being, we accept as good behaviours address copying amongst memory cells and the accumulator (\texttt{MOV} pseudoinstruction) and the use of the \texttt{CJNE} conditional jump that compares two addresses and jumps to a given label if the two labels are equal. 602 602 Moreover, \texttt{RET} to return from a function call is well behaved iff the lower and upper parts of the return address, fetched from the stack, are both marked as complementary parts of the same address (i.e. \texttt{h} is tracked as \texttt{$\langle$Upper,l$\rangle$} and \texttt{l} is tracked as \texttt{$\langle$Lower,h$\rangle$}. 603 603 These three operations are sufficient to implement the backend of the CerCo compiler. … … 608 608 program_counter s < $2^{16}$ $\rightarrow$ option internal_pseudo_address_map 609 609 \end{lstlisting} 610 611 We are now ready to state the (slightly simplified) statement of correctness of our compiler, whose 612 proofs combines correctness w.r.t. fetching and correctness w.r.t. execution. 613 It states that the well behaved execution of a single assembly pseudoinstruction 614 according to the cost model induced by compilation 615 is correctly simulated by the execution of (possibly) many machine code 616 instructions. 610 We now state the (simplified) statement of correctness of our compiler, whose proofs combines correctness with respect to fetching and correctness with respect to execution. 611 It states that the wellbehaved execution of a single assembly pseudoinstruction according to the cost model induced by compilation is correctly simulated by the execution of (possibly) many machine code instructions. 617 612 \begin{lstlisting} 618 613 theorem main_thm: … … 628 623 policy. 629 624 \end{lstlisting} 630 The statement is standard for forward simulation, but restricted to \texttt{PseudoStatuses} \texttt{ps} whose tracking map is \texttt{M} and who 631 are well behaved according to \texttt{internal\_pseudo\_address\_map} 632 \texttt{M}. The \texttt{ticks\_of program policy} function returns the 633 costing computed by assembling the \texttt{program} using the given 634 \texttt{policy}. An obvious corollary of \texttt{main\_thm} is the correct 635 simulation of $n$ well behaved steps by some number of steps $m$, where each 636 step must be well behaved w.r.t. the tracking map returned by the previous 637 step. 625 The statement is standard for forward simulation, but restricted to \texttt{PseudoStatuses} \texttt{ps} whose tracking map is \texttt{M} and who are wellbehaved according to \texttt{internal\_pseudo\_address\_map} \texttt{M}. 626 The \texttt{ticks\_of program policy} function returns the costing computed by assembling the \texttt{program} using the given \texttt{policy}. 627 An obvious corollary of \texttt{main\_thm} is the correct simulation of $n$ well behaved steps by some number of steps $m$, where each step must be wellbehaved with respect to the tracking map returned by the previous step. 638 628 639 629 %  % … … 672 662 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. 673 663 It would not be natural to see the proof that fetch and assembly commute as the specification of one of the two functions. 674 675 \subsection{Related work}676 \label{subsect.related.work}664 \paragraph{Related work} 665 %\subsection{Related work} 666 %\label{subsect.related.work} 677 667 % piton 678 668 We are not the first to consider the correctness of an assembler for a nontrivial assembly language. … … 685 675 Care 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 MCS51's I/O facilities. 686 676 This is only possible by inducing a cost model on the source code from the optimisation strategy and input program. 687 688 \subsection{Resources}689 \label{subsect.resources}677 \paragraph{Resources} 678 %\subsection{Resources} 679 %\label{subsect.resources} 690 680 Our source files are available at~\url{http://cerco.cs.unibo.it}. 691 681 We assumed several properties of `library functions', e.g. modular arithmetic and datastructure manipulation.
Note: See TracChangeset
for help on using the changeset viewer.