Changeset 2067 for src/ASM/CPP2012-asm
- Timestamp:
- Jun 13, 2012, 7:50:53 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/CPP2012-asm/cpp-2012-asm.tex
r2066 r2067 188 188 definition execute_1: $\forall$cm. Status cm $\rightarrow$ Status cm := $\ldots$ 189 189 \end{lstlisting} 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. 191 191 The function \texttt{execute\_1} closely matches the operation of the MCS-51 hardware, as described by a Siemen's manufacturer's data sheet. 192 192 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}. 246 246 Both \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). 247 The more general type will be crucial to share most of the semantics of the 248 two languages. 248 249 249 250 Emulation for pseudoinstructions is handled by \texttt{execute\_1\_pseudo\_instruction}: … … 258 259 259 260 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. 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. 261 The \texttt{ticks1} function we already seen used to increment the machine 262 clock is determined, for the assembly language, from the costing function. 263 It is instead fixed and precomputed for machine code. 262 264 263 265 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} 333 335 Here, \texttt{current\_instruction\_size} is the size in bytes of the encoding of the expanded pseudoinstruction found at \texttt{ppc}. 336 Note that the entanglement we hinted at is only partially solved in this 337 way: the assembler code can ignore the implementative details of the 338 algorithm that finds a policy; however, the algorithm that finds a policy 339 must know the exact behaviour of the assembly because it needs to predict 340 the way the assembly will expand and encode pseudoinstructions, once feeded 341 with a policy. The companion paper~\cite{jaap} certifies an algorithm that 342 finds branch displacement policies for the assembler described in this paper. 343 334 344 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. 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. 345 For instance, if at address $ppc$ in the assembly program we found 346 $Jmp~l$ such that \texttt{lookup\_labels~l} $= a$, if the 347 offset $ d = \sigma(a) - \sigma(ppc+1)$ is such that $d < 128$ then $Jmp~l$ is 348 normally translated to the best local solution, the short jump $SJMP~d$. 349 A global best solution to the branch displacement problem, however, is not 350 always made of locally best solutions. Therefore, in some circumstances, 351 it is necessary to force the assembler to expand jumps into larger ones. 352 This is achieved by the \texttt{policy} function: if \texttt{policy~ppc}$= true$ 353 then a $Jmp~l$ at address $ppc$ is always translated to a long jump. 354 The mechanism is essentially identical for calls. 336 355 337 356 % ---------------------------------------------------------------------------- %
Note: See TracChangeset
for help on using the changeset viewer.