Changeset 2379 for Papers


Ignore:
Timestamp:
Sep 28, 2012, 6:26:29 PM (7 years ago)
Author:
mulligan
Message:

Down to 16 pages again

File:
1 edited

Legend:

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

    r2378 r2379  
    137137In practice, we note how our approach facilitates more code reuse between the semantics of assembly code and object code.
    138138
    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}
     139The formalisation of the assembler and its correctness proof are given in Sect.~\ref{sect.the.proof}.
     140Sect.~\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}
    147148Matita is a proof assistant based on a variant of the Calculus of (Co)inductive Constructions~\cite{asperti:user:2007}.
    148149It features dependent types that we exploit in the formalisation.
     
    421422We now begin the proof of correctness of the assembler.
    422423Correctness 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.
     424This second property can be further decomposed into two main properties: correctness with respect to fetching and decoding and correctness with respect to execution.
    425425
    426426Informally, 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.
     
    469469\end{lstlisting}
    470470We 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 updated 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}.
     471Any 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}.
    472472Or, in plainer words, assembling, storing and then immediately fetching gets you back to where you started.
    473473
     
    570570                                                            \end{cases}
    571571\end{gather*}
    572 In order to prove the preservation of the semantics, we need to associate an object code status to each assembly pseudostatus.
     572To prove semantic preservation we must associate an object code status to each assembly pseudostatus.
    573573This 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)}.
    574574If all the operations accepted by the address update map are well-behaved, this is sufficient to show preservation of the semantics for those computation steps that are well-behaved, i.e. such that the map update does not fail.
     
    599599\end{lstlisting}
    600600The 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 among 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.
     601For 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.
    602602Moreover, \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$}.
    603603These three operations are sufficient to implement the backend of the CerCo compiler.
     
    608608   program_counter s < $2^{16}$ $\rightarrow$ option internal_pseudo_address_map
    609609\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.
     610We now state the (simplified) statement of correctness of our compiler, whose proofs combines correctness with respect to fetching and correctness with respect to execution.
     611It states that the well-behaved 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.
    617612\begin{lstlisting}
    618613theorem main_thm:
     
    628623     policy.
    629624\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.
     625The statement is standard for forward simulation, but restricted to \texttt{PseudoStatuses} \texttt{ps} whose tracking map is \texttt{M} and who are well-behaved according to \texttt{internal\_pseudo\_address\_map} \texttt{M}.
     626The \texttt{ticks\_of program policy} function returns the costing computed by assembling the \texttt{program} using the given \texttt{policy}.
     627An 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 well-behaved with respect to the tracking map returned by the previous step.
    638628
    639629% ---------------------------------------------------------------------------- %
     
    672662Not 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.
    673663It 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}
    677667% piton
    678668We are not the first to consider the correctness of an assembler for a non-trivial assembly language.
     
    685675Care 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 MCS-51's I/O facilities.
    686676This 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}
    690680Our source files are available at~\url{http://cerco.cs.unibo.it}.
    691681We assumed several properties of `library functions', e.g. modular arithmetic and datastructure manipulation.
Note: See TracChangeset for help on using the changeset viewer.