Changeset 2416 for Papers/cpp-asm-2012


Ignore:
Timestamp:
Oct 25, 2012, 12:30:01 PM (7 years ago)
Author:
mulligan
Message:

Some more minor changes

File:
1 edited

Legend:

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

    r2380 r2416  
    114114the rest of the assembler works in order to build globally correct solutions.
    115115Proving their correctness is quite a complex task (see, for instance,
    116 the compaion paper~\cite{boender:correctness:2012}).
     116the companion paper~\cite{boender:correctness:2012}).
    117117Nevertheless, the correctness of the whole assembler only depends on the
    118118correctness of the branch displacement algorithm.
     
    365365The cost returned by the assembler for a pseudoinstruction is set to be the
    366366cost of its expansion in clock cycles. For conditional jumps that are expanded
    367 as just shown, the costs of takin the true and false branches are different and
     367as just shown, the costs of taking the true and false branches are different and
    368368both need to be returned.
    369369
     
    396396\texttt{AJMP} if possible, or an \texttt{LJMP} otherwise, therefore always
    397397picking the locally best solution.
    398 In order to accomodate those optimal solutions that require local sub-optimal
    399 choices, the policy may also return a boolean used to force
     398In order to accommodate those optimal solutions that require local sub-optimal
     399choices, the policy may also return a Boolean used to force
    400400the translation of a \texttt{Jmp} into a \texttt{LJMP} even if
    401401$\delta < 128$. An essentially identical mechanism exists for call
     
    405405\texttt{a} by the policy and by the assembler must coincide. The latter is
    406406the sum of the size of all the expansions of the pseudo-instructions that
    407 preceed the one at address \texttt{a}: the assembler just concatenates all
     407precede the one at address \texttt{a}: the assembler just concatenates all
    408408expansions sequentially. To grant this property, we impose a
    409409correctness criterion over policies. A policy is correct when
     
    445445Given a correct policy for the program to be assembled, the assembler never fails and returns some object code and a costing function.
    446446Under the condition that the policy is `correct' for the program and the program is fully addressable by a 16-bit word, the object code is also fully addressable by a 16-bit word.
    447 Moreover, the result of assemblying the pseudoinstruction obtained fetching from the assembly address \texttt{ppc} is a list of bytes found in the generated object code starting from the object code address \texttt{policy(ppc)}.
     447Moreover, the result of assembling the pseudoinstruction obtained fetching from the assembly address \texttt{ppc} is a list of bytes found in the generated object code starting from the object code address \texttt{policy(ppc)}.
    448448
    449449Essentially the type above states that the \texttt{assembly} function correctly expands pseudoinstructions, and that the expanded instruction reside consecutively in memory.
     
    680680Our source files are available at~\url{http://cerco.cs.unibo.it}.
    681681We assumed several properties of `library functions', e.g. modular arithmetic and datastructure manipulation.
    682 We axiomatised various small functions needed to complete the main theorems, as well as some `routine' proof obligations of the theorems themselves, in focussing on the main meat of the theorems.
     682We axiomatised various small functions needed to complete the main theorems, as well as some `routine' proof obligations of the theorems themselves, in focusing on the main meat of the theorems.
    683683We believe that the proof strategy is sound and that all axioms can be closed, up to minor bugs that should have local fixes that do not affect the global proof strategy.
    684684
    685685The complete development is spread across 29 files with around 20,000 lines of Matita source.
    686 Relavent files are: \texttt{AssemblyProof.ma}, \texttt{AssemblyProofSplit.ma} and \texttt{AssemblyProofSplitSplit.ma}, consisting of approximately 4500 lines of Matita source.
     686Relevant files are: \texttt{AssemblyProof.ma}, \texttt{AssemblyProofSplit.ma} and \texttt{AssemblyProofSplitSplit.ma}, consisting of approximately 4500 lines of Matita source.
    687687Numerous other lines of proofs are spread all over the development because of dependent types and the Russell proof style, which does not allow one to separate the code from the proofs.
    688688The low ratio between source lines and the number of lines of proof is unusual, but justified by the fact that the pseudo-assembly and the assembly language share most constructs and large swathes of the semantics are shared.
Note: See TracChangeset for help on using the changeset viewer.