Changeset 2364 for Papers/cpp-asm-2012


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

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

File:
1 edited

Legend:

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

    r2363 r2364  
    138138
    139139The rest of this paper is a detailed description of our proof that is marginally still a work in progress.
    140 \paragraph{Matita}
     140
     141% ---------------------------------------------------------------------------- %
     142% SECTION                                                                      %
     143% ---------------------------------------------------------------------------- %
     144\section{Matita}
     145\label{sect.matita}
    141146Matita is a proof assistant based on a variant of the Calculus of (Co)inductive Constructions~\cite{asperti:user:2007}.
    142147It features dependent types that we exploit in the formalisation.
     
    324329Conceptually the assembler works in two passes.
    325330The first pass expands every pseudoinstruction into a list of machine code instructions using the function \texttt{expand\_pseudo\_instruction}. The policy
    326 determines which expansion among the alternatives will be choosed for
     331determines which expansion among the alternatives will be chosen for
    327332pseudo-jumps and pseudo-calls. Once the expansion is performed, the cost
    328333of the pseudoinstruction is defined as the cost of the expansion.
     
    376381still to be performed when expanding the instruction at \texttt{ppc}.
    377382
    378 To solve the issue, we define the policy \texttt{policy} as a maps
    379 from a valid pseudoaddress to the corresponding address in the assembled
     383To solve the issue, we define the policy \texttt{policy} as a map
     384from a valid pseudo-address to the corresponding address in the assembled
    380385program.
    381386Therefore, $\delta$ in the example above can be computed simply as
    382 \texttt{sigma(a) - sigma(ppc + 1)}. Moreover, the \texttt{expand\_pseudo\_instruction} emits a \texttt{SJMP} only after verifying for each \texttt{Jmp} that
     387\texttt{policy(a) - policy(ppc + 1)}. Moreover, the \texttt{expand\_pseudo\_instruction} emits a \texttt{SJMP} only after verifying for each \texttt{Jmp} that
    383388$\delta < 128$. When this is not the case, the function emits an
    384389\texttt{AJMP} if possible, or an \texttt{LJMP} otherwise, therefore always
     
    394399the sum of the size of all the expansions of the pseudo-instructions that
    395400preceed the one at address \texttt{a}: the assembler just concatenates all
    396 expansions one after another. To grant this property, we impose a
     401expansions sequentially. To grant this property, we impose a
    397402correctness criterion over policies. A policy is correct when for all
    398403valid pseudoaddresses \texttt{ppc}
     
    654659Not 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.
    655660It would not be natural to see the proof that fetch and assembly commute as the specification of one of the two functions.
    656 %\paragraph{Related work}
    657 
     661\paragraph{Related work}
    658662% piton
    659663We are not the first to consider the correctness of an assembler for a non-trivial assembly language.
     
    666670Care 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.
    667671This is only possible by inducing a cost model on the source code from the optimisation strategy and input program.
    668 %\paragraph{Resources}
    669 
     672\paragraph{Resources}
    670673Our source files are available at~\url{http://cerco.cs.unibo.it}.
    671674We assumed several properties of `library functions', e.g. modular arithmetic and datastructure manipulation.
Note: See TracChangeset for help on using the changeset viewer.