# Changeset 2369

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

English fixes and some rewording.

File:
1 edited

### Legend:

Unmodified
 r2368 \subsection{Correctness of the assembler with respect to fetching} \label{subsect.total.correctness.of.the.assembler} We now begin the proof of correctness of the assembler. Correctness consists of two properties: 1) the assembly process never fails when fed a correct policy; 2)~the object code returned simulates the source code when the latter is executed according to the cost model also returned by the assembler. Property 2) can be decomposed into two main properties: correctness with respect to fetching+decoding and correctness w.r.t. execution. 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 to prove correctness w.r.t. fetching. Section~\ref{subsect.total.correctness.for.well.behaved.assembly.programs} deals with correctness w.r.t. execution: the instructions \texttt{[J1, \ldots, Jn]} simulate the pseudoinstruction~\texttt{I}. We now begin the proof of correctness of the assembler. Correctness 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. The second property above can be further decomposed into two main properties: correctness with respect to fetching and decoding and correctness with respect to execution. Informally, 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. This section reviews the main steps to prove correctness with respect to fetching. Subsect.~\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}. The (slightly simplified) Russell type for the \texttt{assembly} function is: \end{lstlisting} In plain words, the type of \texttt{assembly} states the following. Given a correct policy for the program to be assembled, the assembler never fails and returns some object code and a costing function. 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 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)}. 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 allows to prove the inductive step of the proof, which is by induction over the assembly program. It is then simple to lift the property from lists of bytes (object code) to tries of bytes (i.e. code memories after loading). Given a correct policy for the program to be assembled, the assembler never fails and returns some object code and a costing function. 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 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)}. 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 allows us to prove the inductive step of the proof, which proceeds by induction over the assembly program. It is then straightforward to lift the property from lists of bytes (object code) to tries of bytes (i.e. code memories after loading). The \texttt{assembly\_ok} lemma does the lifting. We have established that every pseudoinstruction is compiled to a sequence of bytes that is found in memory at the expect place. This does not imply trivially that those bytes will be decoded in a correct way to recover the pseudoinstruction expansion. Indeed, we need first to prove a lemma that establish that the \texttt{fetch} function is the left inverse of the \texttt{assembly1} function: We have established that every pseudoinstruction is compiled to a sequence of bytes that is found in memory at the expect place. This does not trivially imply that those bytes will be decoded in a correct way to recover the pseudoinstruction expansion. Indeed, we first need to prove a lemma that establishes that the \texttt{fetch} function is the left inverse of the \texttt{assembly1} function: \begin{lstlisting} lemma fetch_assembly: \end{lstlisting} We read \texttt{fetch\_assembly} as follows. Any 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}. Or, in plainer words, assembling, storing and then immediately fetching gets you back to where you started. Remembering 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): Any 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}. Or, in plainer words, assembling, storing and then immediately fetching gets you back to where you started. Remembering 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): \begin{lstlisting} lemma fetch_assembly_pseudo: The function \texttt{fetch\_many} fetches multiple machine code instructions from code memory and performs some routine checks. Intuitively, 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. Combining \texttt{assembly\_ok} with the previos lemma and a proof of correctness of loading object code in memory, we finally get correctness of the assembler w.r.t. fetching: Intuitively, 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. Combining \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: \begin{lstlisting} lemma fetch_assembly_pseudo2: fetch_many cmem (policy newppc) (policy ppc) instructions. \end{lstlisting} Here we use $\pi_1$ to project the existential witness from the Russell-typed function \texttt{assembly}. We read \texttt{fetch\_assembly\_pseudo2} as follows. Suppose we are given an assembly program which can be addressed by a 16-bit word and a policy that is correct for this program. Suppose we are able to successfully assemble an assembly program using \texttt{assembly} and produce a code memory, \texttt{cmem}. Then, 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)]$. The correspondence is precise: the fetched instructions are exactly those obtained expanding the pseudoinstruction according to policy. In 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 w.r.t. execution). In general this is not the case when the instruction freely manipulates program addresses. Characterizing well behaved programs and proving correctness w.r.t. expansion is the topic of the next Section. Then, 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)]$. The correspondence is precise: the fetched instructions are exactly those obtained expanding the pseudoinstruction according to policy. In 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). In general this is not the case when instructions freely manipulate program addresses. Characterising well-behaved programs and proving correctness with respect to expansion is discussed next. % ---------------------------------------------------------------------------- %