Changeset 2067 for src/ASM/CPP2012-asm

Timestamp:

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

Author:

sacerdot

Message:

...

File:

• src/ASM/CPP2012-asm/cpp-2012-asm.tex (modified) (4 diffs)

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

@@ -188 +188 @@
 definition execute_1: $\forall$cm. Status cm $\rightarrow$ Status cm := $\ldots$
 \end{lstlisting}
-The function \texttt{execute} allows one to execute an arbitrary, but fixed (due to Matita's normalisation requirement) number of steps of a program.
+%The function \texttt{execute} allows one to execute an arbitrary, but fixed (due to Matita's normalisation requirement) number of steps of a program.
 The function \texttt{execute\_1} closely matches the operation of the MCS-51 hardware, as described by a Siemen's manufacturer's data sheet.
 We 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.
@@ -245 +245 @@
 Execution of pseudoinstructions is a function from \texttt{PseudoStatus} to \texttt{PseudoStatus}.
 Both \texttt{Status} and \texttt{PseudoStatus} are instances of a more general type parameterised over the representation of code memory.
-This allows us to share some code that is common to both records (for instance, `setter' and `getter' functions).
+The more general type will be crucial to share most of the semantics of the
+two languages.
 
 Emulation for pseudoinstructions is handled by \texttt{execute\_1\_pseudo\_instruction}:
@@ -258 +259 @@
 
 The 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.
-This timing information is used inside \texttt{execute\_1\_pseudo\_instruction} to update the clock of the \texttt{PseudoStatus}.
-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.
+The \texttt{ticks1} function we already seen used to increment the machine
+clock is determined, for the assembly language, from the costing function.
+It is instead fixed and precomputed for machine code.
 
 Execution proceeds by first fetching from pseudo-code memory using the program counter---treated as an index into the pseudoinstruction list.
@@ -332 +334 @@
 \end{displaymath}
 Here, \texttt{current\_instruction\_size} is the size in bytes of the encoding of the expanded pseudoinstruction found at \texttt{ppc}.
+Note that the entanglement we hinted at is only partially solved in this
+way: the assembler code can ignore the implementative details of the
+algorithm that finds a policy; however, the algorithm that finds a policy
+must know the exact behaviour of the assembly because it needs to predict
+the way the assembly will expand and encode pseudoinstructions, once feeded
+with a policy. The companion paper~\cite{jaap} certifies an algorithm that
+finds branch displacement policies for the assembler described in this paper.
+
 The \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.
-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.
+For instance, if at address $ppc$ in the assembly program we found
+$Jmp~l$ such that \texttt{lookup\_labels~l} $= a$, if the
+offset $ d = \sigma(a) - \sigma(ppc+1)$ is such that $d < 128$ then $Jmp~l$ is
+normally translated to the best local solution, the short jump $SJMP~d$.
+A global best solution to the branch displacement problem, however, is not
+always made of locally best solutions. Therefore, in some circumstances,
+it is necessary to force the assembler to expand jumps into larger ones.
+This is achieved by the \texttt{policy} function: if \texttt{policy~ppc}$= true$
+then a $Jmp~l$ at address $ppc$ is always translated to a long jump.
+The mechanism is essentially identical for calls.
 
 % ---------------------------------------------------------------------------- %