Changeset 2367


Ignore:
Timestamp:
Sep 28, 2012, 2:27:37 AM (7 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

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

    r2366 r2367  
    481481\end{lstlisting}
    482482We read \texttt{fetch\_assembly} as follows.
    483 Given an instruction, \texttt{i}, we first assemble the instruction to obtain \texttt{assembled}, checking that the assembled instruction was stored in code memory correctly.
    484 Fetching from code memory, we obtain a tuple consisting of the instruction, new program counter, and the number of ticks this instruction will take to execute.
    485 We finally check that the fetched instruction is the same instruction that we began with, and the number of ticks this instruction will take to execute is the same as the result returned by a lookup function, \texttt{ticks\_of\_instruction}, devoted to tracking this information.
    486 Or, in plainer words, assembling and then immediately fetching again gets you back to where you started.
     483Any time the encoding \texttt{assembled} of an instruction \texttt{i}
     484is found in code memory starting at position \texttt{pc} (the hypothesis
     485\texttt{encoding\_check} \ldots), when we fetch at address \texttt{pc}
     486we retrieve the instruction \texttt{i}, the updated program counter
     487is \texttt{pc} plus the length of the encoding, and the cost of the
     488fetched instruction is the one predicted for \texttt{i}.
     489Or, in plainer words, assembling, storing and then immediately fetching
     490gets you back to where you started.
    487491
    488492Lemma \texttt{fetch\_assembly\_pseudo} is obtained by composition of \texttt{expand\_pseudo\_instruction} and \texttt{assembly\_1\_pseudoinstruction}:
     493\XXX they do not exist any longer!
    489494\begin{lstlisting}
    490495lemma fetch_assembly_pseudo:
Note: See TracChangeset for help on using the changeset viewer.