Changeset 1022 for src/ASM/CPP2011


Ignore:
Timestamp:
Jun 21, 2011, 12:18:28 PM (8 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CPP2011/cpp-2011.tex

    r1021 r1022  
    289289%By composition, we then have that the whole assembly process is semantics preserving.
    290290
    291 %This is a tempting approach to the proof, but ultimately the wrong approach.
    292 %In particular, it is important that we track how the program counter indexing into the assembly program, and the machine's program counter evolve, so that we can relate them.
    293 %Expanding pseudoinstructions requires that the machine's program counter be incremented by $n$ steps, for $1 \leq n$, for every increment of the assembly program's program counter.
    294 %Keeping track of the correspondence between the two program counters quickly becomes unfeasible using a compositional approach, and hence the proof must be monolithic.
     291This is a tempting approach to the proof, but ultimately the wrong approach.
     292In particular, to expand a pseudo instruction we need to know the address
     293at which the expanded instructions will be located, for instance to determine
     294if a short jump is possible. That address is a function of the
     295\emph{object code} generated for the pseudo-instructions already visited.
     296Thus we need to assemble each pseduto instruction down to object code before
     297moving to the next one and this must be eventually reflected on the proof
     298of correctness. Therefore we will have lemmas for the \texttt{assembly1}
     299function and for the composition of \texttt{expand\_pseudo\_instruction} and
     300\texttt{assembly1}, but not for \texttt{expand\_pseudo\_instruction} alone.
    295301
    296302% ---------------------------------------------------------------------------- %
Note: See TracChangeset for help on using the changeset viewer.