# Changeset 2366 for Papers

Ignore:
Timestamp:
Sep 28, 2012, 2:19:06 AM (7 years ago)
Message:

...

File:
1 edited

### Legend:

Unmodified
 r2365 At the assembler level, this is reflected by our need to induce a cost model on the assembly code as a function of the assembly program and the strategy used to solve the branch displacement problem. In particular, the optimising compiler should also return a map that assigns a cost (in clock strategy used to solve the branch displacement problem. In particular, our optimising assembler should also return a map that assigns a cost (in clock cycles) to every instruction in the source program. We expect the induced cost to be preserved by the compiler: we will prove that the compiled code to be preserved by the assembler: we will prove that the compiled code tightly simulates the source code by taking exactly the predicted amount of time. In practice, we note how our approach facilitates more code reuse between the semantics of assembly code and object code. The rest of this paper is a detailed description of our proof that is marginally still a work in progress. The formalization of the assembler and its correctness proof are given in Section~\ref{sect.the.proof}. Section~\ref{sect.matita} provides a brief introduction to the syntax of Matita. Section~\ref{sect.conclusions} presents the conclusions and relations with previous work. % ---------------------------------------------------------------------------- % % SECTION                                                                      % % ---------------------------------------------------------------------------- % \section{The proof} \section{Certification of an optimizing assembler} \label{sect.the.proof} memory of the processor, represented as a compact trie of bytes addressed by the program counter. The \texttt{Status} of the emulator is described as The \texttt{Status} of the emulator is a record that contains the microprocessor's program counter, registers, stack pointer, clock, special function registers, code memory, and so on. pointer, clock, special function registers, data memory, and so on. The value of the code memory is a parameter of the record since it is not changed during execution. The parameterised type $A$ of \texttt{preinstruction} represents the addressing mode allowed for conditional jumps; in the \texttt{RealInstruction} constructor we constraint it to be a relative offset. A different instantiation will be used in the next section for assembly programs. A different instantiation (labels) will be used in the next section for assembly programs. Once decoded, execution proceeds by a case analysis on the decoded instruction, following the operation of the hardware. We do not perform any kind of symbolic execution, wherein data is the disjoint union of bytes and addresses, with addresses kept opaque and immutable. Labels are immediately translated to concrete addresses, and registers and memory locations only ever contain bytes, never labels. Labels are immediately translated before execution to concrete addresses, and registers and memory locations only ever contain bytes, never labels. As a consequence, we allow the programmer to mangle, change and generally adjust addresses as they want, under the proviso that the translation process may not be able to preserve the semantics of programs that do this. This will be further discussed in Subsect.~\ref{subsect.total.correctness.for.well.behaved.assembly.programs}. The only limitation introduced by this approach is that the size of assembly programs is bounded by $2^{16}$. This will be further discussed in Subsect.~\ref{subsect.total.correctness.for.well.behaved.assembly.programs}. % ---------------------------------------------------------------------------- % \subsection{The assembler} \label{subsect.the.assembler} The assembler takes in input an assembly program to expand and a branch displacement policy for it. It returns both the assembled program (a list of bytes to be loaded in code memory for execution) and the costing of the source program. The assembler takes in input an assembly program made of pseudoinstructions and a branch displacement policy for it. It returns both the object code (a list of bytes to be loaded in code memory for execution) and the costing for the source. Conceptually the assembler works in two passes. Naturally, if \texttt{label} is close enough', a conditional jump pseudoinstruction is mapped directly to a conditional jump machine instruction; the above translation only applies if \texttt{label} is not sufficiently local. The cost returned by the assembler for a pseudoinstruction is set to be the cost of its expansion in clock cycles. For conditional jumps that are expanded as just shown, the costs of takin the true and false branches are different and both need to be returned. %In order to implement branch displacement it is impossible to really make the \texttt{expand\_pseudo\_instruction} function completely independent of the encoding function. %This is due to branch displacement requiring the distance in bytes of the target of the jump. preceed the one at address \texttt{a}: the assembler just concatenates all expansions sequentially. To grant this property, we impose a correctness criterion over policies. A policy is correct when for all valid pseudoaddresses \texttt{ppc} $${\texttt{policy(ppc+1) = policy(ppc) + instruction\_size(ppc)}}$$ correctness criterion over policies. A policy is correct when \texttt{policy(0) = 0} and for all valid pseudoaddresses \texttt{ppc} $${\texttt{policy(ppc+1) = policy(ppc) + instruction\_size(ppc)} \leq 2^{16}}$$ Here \texttt{instruction\_size(ppc)} is the size in bytes of the expansion of the pseudoinstruction found at \texttt{pcc}, i.e. the length of \subsection{Correctness of the assembler with respect to fetching} \label{subsect.total.correctness.of.the.assembler} Using our policies, we now work toward proving the correctness of the assembler. Correctness means that the assembly process never fails when provided with a correct policy and that the process does not change the semantics of a certain class of well-behaved assembly programs. The aim of this section is to prove the following informal 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 constitutes the first major step in the proof of correctness of the assembler, the next one being the simulation of \texttt{I} by \texttt{[J1, \ldots, Jn]} (see Subsect.~\ref{subsect.total.correctness.for.well.behaved.assembly.programs}). The \texttt{assembly} function is given a Russell type (slightly simplified here): 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}. The (slightly simplified) Russell type for the \texttt{assembly} function is: \begin{lstlisting} definition assembly: $\forall$program: pseudo_assembly_program. $\forall$policy. $\Sigma$assembled: list Byte $\times$ (BitVectorTrie costlabel 16). policy is correct for program $\rightarrow$ $\mid$program$\mid$ < $2^{16}$ $\rightarrow$ $\mid$fst assembled$\mid$ < $2^{16}$ $\wedge$ (policy ($\mid$program$\mid$) = $\mid$fst assembled$\mid$ $\vee$ (policy ($\mid$program$\mid$) = 0 $\wedge$ $\mid$fst assembled$\mid$ = $2^{16}$)) $\wedge$ $\forall$ppc: pseudo_program_counter. ppc < $2^{16}$ $\rightarrow$ let pseudo_instr := fetch from program at ppc in let assembled_i := assemble pseudo_instr in $\mid$assembled_i$\mid$ $\leq$ $2^{16}$ $\wedge$ $\forall$n: nat. n < $\mid$assembled_i$\mid$ $\rightarrow$ $\exists$k: nat. nth assembled_i n = nth assembled (policy ppc + k). $\forall$program: pseudo_assembly_program.  $\forall$policy. $\Sigma$assembled: list Byte $\times$ (BitVectorTrie nat 16). $\mid$program$\mid$ $\leq$ $2^{16}$ $\rightarrow$ policy is correct for program $\rightarrow$ policy ($\mid$program$\mid$) = $\mid$fst assembled$\mid$ $\leq$ $2^{16}$ $\wedge$ $\forall$ppc: pseudo_program_counter. ppc < $2^{16}$ $\rightarrow$ let pseudo_instr := fetch from program at ppc in let assembled_i := assemble pseudo_instr in $\mid$assembled_i$\mid$ $\leq$ $2^{16}$ $\wedge$ $\forall$n: nat. n < $\mid$assembled_i$\mid$ $\rightarrow$ $\exists$k: nat. nth assembled_i n = nth assembled (policy ppc + k). \end{lstlisting} In plain words, the type of \texttt{assembly} states the following. Suppose we are given a policy that is correct for the program we are assembling. Then we return a list of assembled bytes, complete with a map from program counters to cost labels, such that the following properties hold for the list of bytes. Under the condition that the policy is correct' for the program and the program is fully addressable by a 16-bit word, the assembled list is also fully addressable by a 16-bit word, the policy maps the last program counter that can address the program to the last instruction of the assemble pseudoinstruction or overflows, and if we fetch from the pseudo-program counter \texttt{ppc} we get a pseudoinstruction \texttt{pi} and a new pseudo-program counter \texttt{ppc}. Further, assembling the pseudoinstruction \texttt{pseudo\_instr} results in a list of bytes, \texttt{assembled\_i}. Then, indexing into this list with any natural number \texttt{n} less than the length of \texttt{assembled\_i} gives the same result as indexing into \texttt{assembled} with \texttt{policy ppc} (the program counter pointing to the start of the expansion in \texttt{assembled}) plus \texttt{k}. Essentially the lemma above states that the \texttt{assembly} function correctly expands pseudoinstructions, and that the expanded instruction reside consecutively in memory. This result is lifted from lists of bytes into a result on tries of bytes (i.e. code memories), using an additional lemma: \texttt{assembly\_ok}. Lemma \texttt{fetch\_assembly} establishes that the \texttt{fetch} and \texttt{assembly1} functions interact correctly. The \texttt{fetch} function, as its name implies, fetches the instruction indexed by the program counter in the code memory, while \texttt{assembly1} maps a single instruction to its byte encoding: 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). 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: \begin{lstlisting} lemma fetch_assembly: