Changeset 2369 for Papers/cpp-asm-2012


Ignore:
Timestamp:
Sep 28, 2012, 3:13:49 PM (7 years ago)
Author:
mulligan
Message:

English fixes and some rewording.

File:
1 edited

Legend:

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

    r2368 r2369  
    419419\subsection{Correctness of the assembler with respect to fetching}
    420420\label{subsect.total.correctness.of.the.assembler}
    421 We now begin the proof of correctness of the assembler. Correctness consists
    422 of two properties: 1) the assembly process never fails when fed a correct
    423 policy;
    424 2)~the object code returned simulates the source code when the latter is
    425 executed according to the cost model also returned by the assembler.
    426 
    427 Property 2) can be decomposed into two main properties: correctness with
    428 respect to fetching+decoding and correctness w.r.t. execution.
    429 
    430 Informally, correctness w.r.t. fetching is the following statement: when we fetch an assembly pseudoinstruction \texttt{I} at address \texttt{ppc}, then we can fetch the expanded pseudoinstruction(s) \texttt{[J1, \ldots, Jn] = fetch\_pseudo\_instruction \ldots\ I\ ppc} from \texttt{policy ppc} in the code memory obtained by loading the assembled object code. This Section reviews the main steps
    431 to prove correctness w.r.t. fetching. Section~\ref{subsect.total.correctness.for.well.behaved.assembly.programs} deals with correctness w.r.t. execution:
    432 the instructions \texttt{[J1, \ldots, Jn]} simulate the pseudoinstruction~\texttt{I}.
     421We now begin the proof of correctness of the assembler.
     422Correctness consists of two properties: firstly that the assembly process never fails when fed a correct policy and secondly the object code returned simulates the source code when the latter is executed according to the cost model also returned by the assembler.
     423
     424The second property above can be further decomposed into two main properties: correctness with respect to fetching and decoding and correctness with respect to execution.
     425
     426Informally, correctness with respect to fetching is the following statement: when we fetch an assembly pseudoinstruction \texttt{I} at address \texttt{ppc}, then we can fetch the expanded pseudoinstruction(s) \texttt{[J1, \ldots, Jn] = fetch\_pseudo\_instruction \ldots\ I\ ppc} from \texttt{policy ppc} in the code memory obtained by loading the assembled object code.
     427This section reviews the main steps to prove correctness with respect to fetching.
     428Subsect.~\ref{subsect.total.correctness.for.well.behaved.assembly.programs} deals with correctness with respect to execution: the instructions \texttt{[J1, \ldots, Jn]} simulate the pseudoinstruction~\texttt{I}.
    433429
    434430The (slightly simplified) Russell type for the \texttt{assembly} function is:
     
    447443\end{lstlisting}
    448444In plain words, the type of \texttt{assembly} states the following.
    449 Given a correct policy for the program to be assembled, the assembler never
    450 fails and returns some object code and a costing function.
    451 Under the condition that the policy is `correct' for the program and the program is fully addressable by a 16-bit word, the object code is also fully addressable by a 16-bit word. Moreover, the
    452 result of assemblying the pseudoinstruction obtained fetching from the
    453 assembly address \texttt{ppc}
    454 is a list of bytes found in the generated object code starting from
    455 the object code address \texttt{policy(ppc)}.
    456 
    457 Essentially the type above states that the \texttt{assembly} function correctly expands pseudoinstructions, and that the expanded instruction reside consecutively in memory. The fundamental hypothesis is correctness of the policy which
    458 allows to prove the inductive step of the proof, which is by induction over
    459 the assembly program. It is then simple to lift the property from lists
    460 of bytes (object code) to tries of bytes (i.e. code memories after loading).
     445Given a correct policy for the program to be assembled, the assembler never fails and returns some object code and a costing function.
     446Under the condition that the policy is `correct' for the program and the program is fully addressable by a 16-bit word, the object code is also fully addressable by a 16-bit word.
     447Moreover, the result of assemblying the pseudoinstruction obtained fetching from the assembly address \texttt{ppc} is a list of bytes found in the generated object code starting from the object code address \texttt{policy(ppc)}.
     448
     449Essentially the type above states that the \texttt{assembly} function correctly expands pseudoinstructions, and that the expanded instruction reside consecutively in memory.
     450The fundamental hypothesis is correctness of the policy which allows us to prove the inductive step of the proof, which proceeds by induction over the assembly program.
     451It is then straightforward to lift the property from lists of bytes (object code) to tries of bytes (i.e. code memories after loading).
    461452The \texttt{assembly\_ok} lemma does the lifting.
    462453
    463 We have established that every pseudoinstruction is compiled to a sequence of
    464 bytes that is found in memory at the expect place. This does not imply
    465 trivially that those bytes will be decoded in a correct way to recover the
    466 pseudoinstruction expansion. Indeed, we need first to prove a lemma that
    467 establish that the \texttt{fetch} function is the left inverse of the
    468 \texttt{assembly1} function:
     454We have established that every pseudoinstruction is compiled to a sequence of bytes that is found in memory at the expect place.
     455This does not trivially imply that those bytes will be decoded in a correct way to recover the pseudoinstruction expansion.
     456Indeed, we first need to prove a lemma that establishes that the \texttt{fetch} function is the left inverse of the \texttt{assembly1} function:
    469457\begin{lstlisting}
    470458lemma fetch_assembly:
     
    481469\end{lstlisting}
    482470We read \texttt{fetch\_assembly} as follows.
    483 Any time the encoding \texttt{assembled} of an instruction \texttt{i}
    484 is found in code memory starting at position \texttt{pc} (the hypothesis
    485 \texttt{encoding\_check} \ldots), when we fetch at address \texttt{pc}
    486 we retrieve the instruction \texttt{i}, the updated program counter
    487 is \texttt{pc} plus the length of the encoding, and the cost of the
    488 fetched instruction is the one predicted for \texttt{i}.
    489 Or, in plainer words, assembling, storing and then immediately fetching
    490 gets you back to where you started.
    491 
    492 Remembering that \texttt{assembly\_1\_pseudo\_instruction} is the composition
    493 of \texttt{assembly1} with \texttt{expand\_pseudo\_instruction}, we can
    494 lift the previous result from instructions (already expanded) to
    495 pseudoinstructions (to be expanded):
     471Any time the encoding \texttt{assembled} of an instruction \texttt{i} is found in code memory starting at position \texttt{pc} (the hypothesis \texttt{encoding\_check} \ldots), when we fetch at address \texttt{pc} we retrieve the instruction \texttt{i}, the updated program counter is \texttt{pc} plus the length of the encoding, and the cost of the fetched instruction is the one predicted for \texttt{i}.
     472Or, in plainer words, assembling, storing and then immediately fetching gets you back to where you started.
     473
     474Remembering that \texttt{assembly\_1\_pseudo\_instruction} is the composition of \texttt{assembly1} with \texttt{expand\_pseudo\_instruction}, we can lift the previous result from instructions (already expanded) to pseudoinstructions (to be expanded):
    496475\begin{lstlisting}
    497476lemma fetch_assembly_pseudo:
     
    511490The function \texttt{fetch\_many} fetches multiple machine code instructions from code memory and performs some routine checks.
    512491
    513 Intuitively, Lemma \texttt{fetch\_assembly\_pseudo} says that
    514 expanding a pseudoinstruction into $n$ instructions, encoding the instructions
    515 and immediately fetching $n$ instructions back yield exactly the expansion.
    516 
    517 Combining \texttt{assembly\_ok} with the previos lemma and a proof of
    518 correctness of loading object code in memory, we finally get correctness
    519 of the assembler w.r.t. fetching:
     492Intuitively, Lemma \texttt{fetch\_assembly\_pseudo} says that expanding a pseudoinstruction into $n$ instructions, encoding the instructions and immediately fetching $n$ instructions back yield exactly the expansion.
     493
     494Combining \texttt{assembly\_ok} with the previous lemma and a proof of correctness of loading object code in memory, we finally get correctness of the assembler with respect to fetching:
    520495\begin{lstlisting}
    521496lemma fetch_assembly_pseudo2:
     
    529504    fetch_many cmem (policy newppc) (policy ppc) instructions.
    530505\end{lstlisting}
    531 
    532506Here we use $\pi_1$ to project the existential witness from the Russell-typed function \texttt{assembly}.
    533507We read \texttt{fetch\_assembly\_pseudo2} as follows.
    534508Suppose we are given an assembly program which can be addressed by a 16-bit word and a policy that is correct for this program.
    535509Suppose we are able to successfully assemble an assembly program using \texttt{assembly} and produce a code memory, \texttt{cmem}.
    536 Then, fetching a pseudoinstruction from the pseudo-code memory stored in
    537 the interval $[ppc,newppc]$ corresponds to fetching a sequence of instructions from the real code memory, stored in the interval $[policy(ppc),policy(ppc+1)]$.
    538 The correspondence is precise: the fetched instructions are exactly those
    539 obtained expanding the pseudoinstruction according to policy.
    540 
    541 In order to complete the proof of correctness of the assembler, we need
    542 to prove that each pseudoinstruction is simulated by the execution of its
    543 expansion (correctness w.r.t. execution). In general this is not the case
    544 when the instruction freely manipulates program addresses. Characterizing
    545 well behaved programs and proving correctness w.r.t. expansion is the topic
    546 of the next Section.
     510Then, fetching a pseudoinstruction from the pseudo-code memory stored in the interval $[ppc,newppc]$ corresponds to fetching a sequence of instructions from the real code memory, stored in the interval $[policy(ppc),policy(ppc+1)]$.
     511The correspondence is precise: the fetched instructions are exactly those obtained expanding the pseudoinstruction according to policy.
     512
     513In order to complete the proof of correctness of the assembler, we need to prove that each pseudoinstruction is simulated by the execution of its expansion (correctness with respect to execution).
     514In general this is not the case when instructions freely manipulate program addresses.
     515Characterising well-behaved programs and proving correctness with respect to expansion is discussed next.
    547516
    548517% ---------------------------------------------------------------------------- %
Note: See TracChangeset for help on using the changeset viewer.