Changeset 2067

Jun 13, 2012, 7:50:53 PM (5 years ago)


1 edited


  • src/ASM/CPP2012-asm/cpp-2012-asm.tex

    r2066 r2067  
    188188definition execute_1: $\forall$cm. Status cm $\rightarrow$ Status cm := $\ldots$
    190 The function \texttt{execute} allows one to execute an arbitrary, but fixed (due to Matita's normalisation requirement) number of steps of a program.
     190%The function \texttt{execute} allows one to execute an arbitrary, but fixed (due to Matita's normalisation requirement) number of steps of a program.
    191191The function \texttt{execute\_1} closely matches the operation of the MCS-51 hardware, as described by a Siemen's manufacturer's data sheet.
    192192We first fetch, using the program counter, from code memory the first byte of the instruction to be executed, decoding the resulting opcode, fetching more bytes as is necessary.
    245245Execution of pseudoinstructions is a function from \texttt{PseudoStatus} to \texttt{PseudoStatus}.
    246246Both \texttt{Status} and \texttt{PseudoStatus} are instances of a more general type parameterised over the representation of code memory.
    247 This allows us to share some code that is common to both records (for instance, `setter' and `getter' functions).
     247The more general type will be crucial to share most of the semantics of the
     248two languages.
    249250Emulation for pseudoinstructions is handled by \texttt{execute\_1\_pseudo\_instruction}:
    259260The costing returns \emph{pairs} of natural numbers because, in the case of expanding conditional jumps to labels, the expansion of the `true branch' and `false branch' may differ in execution time.
    260 This timing information is used inside \texttt{execute\_1\_pseudo\_instruction} to update the clock of the \texttt{PseudoStatus}.
    261 During the proof of correctness of the assembler we relate the clocks of \texttt{Status}es and \texttt{PseudoStatus}es for the policy induced by the cost model and optimisations.
     261The \texttt{ticks1} function we already seen used to increment the machine
     262clock is determined, for the assembly language, from the costing function.
     263It is instead fixed and precomputed for machine code.
    263265Execution proceeds by first fetching from pseudo-code memory using the program counter---treated as an index into the pseudoinstruction list.
    333335Here, \texttt{current\_instruction\_size} is the size in bytes of the encoding of the expanded pseudoinstruction found at \texttt{ppc}.
     336Note that the entanglement we hinted at is only partially solved in this
     337way: the assembler code can ignore the implementative details of the
     338algorithm that finds a policy; however, the algorithm that finds a policy
     339must know the exact behaviour of the assembly because it needs to predict
     340the way the assembly will expand and encode pseudoinstructions, once feeded
     341with a policy. The companion paper~\cite{jaap} certifies an algorithm that
     342finds branch displacement policies for the assembler described in this paper.
    334344The \texttt{expand\_pseudo\_instruction} function uses the \texttt{sigma} map to determine the size of jump required when expanding pseudojumps, computing the jump size by examining the size of the differences between program counters.
    335 In some circumstances the decision as to what machine code jump a particular pseudojump should be expanded into is ambiguous, and requires the use of the \texttt{policy} function to force a decision.
     345For instance, if at address $ppc$ in the assembly program we found
     346$Jmp~l$ such that \texttt{lookup\_labels~l} $= a$, if the
     347offset $ d = \sigma(a) - \sigma(ppc+1)$ is such that $d < 128$ then $Jmp~l$ is
     348normally translated to the best local solution, the short jump $SJMP~d$.
     349A global best solution to the branch displacement problem, however, is not
     350always made of locally best solutions. Therefore, in some circumstances,
     351it is necessary to force the assembler to expand jumps into larger ones.
     352This is achieved by the \texttt{policy} function: if \texttt{policy~ppc}$= true$
     353then a $Jmp~l$ at address $ppc$ is always translated to a long jump.
     354The mechanism is essentially identical for calls.
    337356% ---------------------------------------------------------------------------- %
Note: See TracChangeset for help on using the changeset viewer.