# Changeset 2364 for Papers

Ignore:
Timestamp:
Sep 27, 2012, 5:46:59 PM (7 years ago)
Message:

Some minor changes to Claudio's additions and reinstatement of some sections and subsections.

File:
1 edited

### Legend:

Unmodified
 r2363 The rest of this paper is a detailed description of our proof that is marginally still a work in progress. \paragraph{Matita} % ---------------------------------------------------------------------------- % % SECTION                                                                      % % ---------------------------------------------------------------------------- % \section{Matita} \label{sect.matita} Matita is a proof assistant based on a variant of the Calculus of (Co)inductive Constructions~\cite{asperti:user:2007}. It features dependent types that we exploit in the formalisation. Conceptually the assembler works in two passes. The first pass expands every pseudoinstruction into a list of machine code instructions using the function \texttt{expand\_pseudo\_instruction}. The policy determines which expansion among the alternatives will be choosed for determines which expansion among the alternatives will be chosen for pseudo-jumps and pseudo-calls. Once the expansion is performed, the cost of the pseudoinstruction is defined as the cost of the expansion. still to be performed when expanding the instruction at \texttt{ppc}. To solve the issue, we define the policy \texttt{policy} as a maps from a valid pseudoaddress to the corresponding address in the assembled To solve the issue, we define the policy \texttt{policy} as a map from a valid pseudo-address to the corresponding address in the assembled program. Therefore, $\delta$ in the example above can be computed simply as \texttt{sigma(a) - sigma(ppc + 1)}. Moreover, the \texttt{expand\_pseudo\_instruction} emits a \texttt{SJMP} only after verifying for each \texttt{Jmp} that \texttt{policy(a) - policy(ppc + 1)}. Moreover, the \texttt{expand\_pseudo\_instruction} emits a \texttt{SJMP} only after verifying for each \texttt{Jmp} that $\delta < 128$. When this is not the case, the function emits an \texttt{AJMP} if possible, or an \texttt{LJMP} otherwise, therefore always the sum of the size of all the expansions of the pseudo-instructions that preceed the one at address \texttt{a}: the assembler just concatenates all expansions one after another. To grant this property, we impose a expansions sequentially. To grant this property, we impose a correctness criterion over policies. A policy is correct when for all valid pseudoaddresses \texttt{ppc} 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. It would not be natural to see the proof that fetch and assembly commute as the specification of one of the two functions. %\paragraph{Related work} \paragraph{Related work} % piton We are not the first to consider the correctness of an assembler for a non-trivial assembly language. 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 MCS-51's I/O facilities. This is only possible by inducing a cost model on the source code from the optimisation strategy and input program. %\paragraph{Resources} \paragraph{Resources} Our source files are available at~\url{http://cerco.cs.unibo.it}. We assumed several properties of `library functions', e.g. modular arithmetic and datastructure manipulation.