Changeset 2349


Ignore:
Timestamp:
Sep 26, 2012, 5:44:31 PM (7 years ago)
Author:
mulligan
Message:

Up to section 3.5.

File:
1 edited

Legend:

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

    r2348 r2349  
    172172In this way, Matita supports the `Russell' proof methodology developed by Sozeau in~\cite{sozeau:subset:2006}, with an implementation that is lighter and more tightly integrated with the system than that of Coq.
    173173
     174Throughout this paper we simplify the statements of lemmas and types of definitions in order to emphasise readability.
     175
    174176% ---------------------------------------------------------------------------- %
    175177% SECTION                                                                      %
     
    349351definition expand_pseudo_instruction:
    350352 $\forall$lookup_labels: Identifier $\rightarrow$ Word.
    351  $\forall$sigma: Word $\rightarrow$ Word.
    352  $\forall$policy: Word $\rightarrow$ bool.
     353 $\forall$policy.
    353354 $\forall$ppc: Word.
    354355 $\forall$lookup_datalabels: Identifier $\rightarrow$ Word.
     
    358359Here, the functions \texttt{lookup\_labels} and \texttt{lookup\_datalabels} are the functions that map labels and datalabels to program counters respectively, both of them used in the semantics of assembly.
    359360The input \texttt{pi} is the pseudoinstruction to be expanded and is found at address \texttt{ppc} in the assembly program.
    360 The policy is defined using the two functions \texttt{sigma} and \texttt{policy}, of which \texttt{sigma} is the most interesting.
    361 The function \texttt{sigma} maps pseudoprogram counters to program counters: the encoding of the expansion of the pseudoinstruction found at address \texttt{a} in the assembly code should be placed into code memory at address \texttt{sigma(a)}.
     361The function takes \texttt{policy} as an input.
     362In reality, this is a pair of functions, but for the purposes of this paper we simplify.
     363The \texttt{policy} maps pseudo-program counters to program counters: the encoding of the expansion of the pseudoinstruction found at address \texttt{a} in the assembly code should be placed into code memory at address \texttt{policy(a)}.
    362364Of course this is possible only if the policy is correct, which means that the encoding of consecutive assembly instructions must be consecutive in code memory.
    363365\begin{displaymath}
    364 \texttt{sigma}(\texttt{ppc} + 1) = \texttt{pc} + \texttt{current\_instruction\_size}
     366\texttt{policy}(\texttt{ppc} + 1) = \texttt{pc} + \texttt{current\_instruction\_size}
    365367\end{displaymath}
    366368Here, \texttt{current\_instruction\_size} is the size in bytes of the encoding of the expanded pseudoinstruction found at \texttt{ppc}.
     
    369371A companion submission to this one~\cite{boender:correctness:2012} certifies an algorithm that finds branch displacement policies for the assembler described in this paper.
    370372
    371 The \texttt{expand\_pseudo\_instruction} function uses the \texttt{sigma} map to determine the size of jump required when expanding pseudojumps, computing the jump size by examining the size of the differences between program counters.
    372 For instance, if at address \texttt{ppc} in the assembly program we found \texttt{Jmp l} such that \texttt{lookup\_labels l = a}, if the offset \texttt{d = sigma(a) - sigma(ppc + 1)} is such that \texttt{d} $< 128$ then \texttt{Jmp l} is normally translated to the best local solution, the short jump \texttt{SJMP d}.
     373The \texttt{expand\_pseudo\_instruction} function uses the \texttt{policy} map to determine the size of jump required when expanding pseudojumps, computing the jump size by examining the size of the differences between program counters.
     374For instance, if at address \texttt{ppc} in the assembly program we found \texttt{Jmp l} such that \texttt{lookup\_labels l = a}, if the offset \texttt{d = policy(a) - policy(ppc + 1)} is such that \texttt{d} $< 128$ then \texttt{Jmp l} is normally translated to the best local solution, the short jump \texttt{SJMP d}.
    373375A global best solution to the branch displacement problem, however, is not always made of locally best solutions.
    374376Therefore, in some circumstances, it is necessary to force the assembler to expand jumps into larger ones.
    375 This is achieved by the \texttt{policy} function: if \texttt{policy ppc = true} then a \texttt{Jmp l} at address \texttt{ppc} is always translated to a long jump.
     377This is achieved by another boolean-valued function such that if the function applied to \texttt{ppc} returns true then a \texttt{Jmp l} at address \texttt{ppc} is always translated to a long jump.
    376378An essentially identical mechanism exists for call instructions.
    377379
     
    404406              nth assembled_i n = nth assembled (policy ppc + k).
    405407\end{lstlisting}
    406 [dpm: update]
    407408In plain words, the type of \texttt{assembly} states the following.
    408 Suppose we are given a policy that is correct for the program we are assembling, and suppose the program to be assembled is fully addressable by a 16-bit word.
    409 Then if we fetch from the pseudo-program counter \texttt{ppc} we get a pseudoinstruction \texttt{pi} and a new pseudo-program counter \texttt{ppc}.
    410 Further, assembling the pseudoinstruction \texttt{pi} results in a list of bytes, \texttt{a}.
    411 Then, indexing into this list with any natural number \texttt{j} less than the length of \texttt{a} gives the same result as indexing into \texttt{assembled} with \texttt{sigma(ppc)} (the program counter pointing to the start of the expansion in \texttt{assembled}) plus \texttt{j}.
     409Suppose we are given a policy that is correct for the program we are assembling.
     410Then 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.
     411Under 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}.
     412Further, assembling the pseudoinstruction \texttt{pseudo\_instr} results in a list of bytes, \texttt{assembled\_i}.
     413Then, 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}.
    412414
    413415Essentially the lemma above states that the \texttt{assembly} function correctly expands pseudoinstructions, and that the expanded instruction reside consecutively in memory.
     
    435437Or, in plainer words, assembling and then immediately fetching again gets you back to where you started.
    436438
    437 Lemma \texttt{fetch\_assembly\_pseudo} (slightly simplified, here) is obtained by composition of \texttt{expand\_pseudo\_instruction} and \texttt{assembly\_1\_pseudoinstruction}:
     439Lemma \texttt{fetch\_assembly\_pseudo} is obtained by composition of \texttt{expand\_pseudo\_instruction} and \texttt{assembly\_1\_pseudoinstruction}:
    438440\begin{lstlisting}
    439441lemma fetch_assembly_pseudo:
     
    445447 let pi := $\pi_1$ (fetch_pseudo_instruction instr_list ppc) in
    446448 let pc := policy ppc in
    447  let instrs := expand_pseudo_instructio sigma policy ppc pi in
    448  let $\langle$l, a$\rangle$ := assembly_1_pseudoinstruction sigma policy ppc pi in
     449 let instrs := expand_pseudo_instructio policy ppc pi in
     450 let $\langle$l, a$\rangle$ := assembly_1_pseudoinstruction policy ppc pi in
    449451 let pc_plus_len := pc + l in
    450452  encoding_check code_memory pc pc_plus_len a $\rightarrow$
     
    456458
    457459Intuitively, Lemma \texttt{fetch\_assembly\_pseudo} can be read as follows.
    458 Suppose we expand the pseudoinstruction at \texttt{ppc} with the policy decision \texttt{sigma}, obtaining the list of machine code instructions \texttt{instrs}.
     460Suppose we expand the pseudoinstruction at \texttt{ppc} with the policy, obtaining the list of machine code instructions \texttt{instrs}.
    459461Suppose we also assemble the pseudoinstruction at \texttt{ppc} to obtain \texttt{a}, a list of bytes.
    460462Then, we check with \texttt{fetch\_many} that the number of machine instructions that were fetched matches the number of instruction that \texttt{expand\_pseudo\_instruction} expanded.
    461463
    462 The final lemma in this series is \texttt{fetch\_assembly\_pseudo2} that combines the Lemma \texttt{fetch\_assembly\_pseudo} with the correctness of the functions that load object code into the processor's memory.
    463 Again, we slightly simplify:
     464The final lemma in this series is \texttt{fetch\_assembly\_pseudo2} that combines the Lemma \texttt{fetch\_assembly\_pseudo} with the correctness of the functions that load object code into the processor's memory:
    464465\begin{lstlisting}
    465466lemma fetch_assembly_pseudo2:
     
    469470 policy is correct for program $\rightarrow$
    470471 $\forall$ppc. ppc < $\mid$snd program$\mid$ $\rightarrow$
    471   let $\langle$preamble, instr_list$\rangle$ := program in
    472   let $\langle$labels, costs$\rangle$ := create_label_cost_map instr_list in
     472  let $\langle$labels, costs$\rangle$ := create_label_cost_map program in
    473473  let $\langle$assembled, costs'$\rangle$ := $\pi_1$ (assembly program sigma policy) in
    474474  let cmem := load_code_memory assembled in
    475   let $\langle$pi, newppc$\rangle$ := fetch_pseudo_instruction instr_list ppc in
     475  let $\langle$pi, newppc$\rangle$ := fetch_pseudo_instruction program ppc in
    476476  let instructions := expand_pseudo_instruction policy ppc pi in
    477477    fetch_many cmem (policy newppc) (policy ppc) instructions.
     
    481481
    482482We read \texttt{fetch\_assembly\_pseudo2} as follows.
     483Suppose we are given an assembly program which can be addressed by a 16-bit word and a policy that is correct for this program.
    483484Suppose we are able to successfully assemble an assembly program using \texttt{assembly} and produce a code memory, \texttt{cmem}.
    484 Then, fetching a pseudoinstruction from the pseudo-code memory at address \texttt{ppc} corresponds to fetching a sequence of instructions from the real code memory using \texttt{sigma} to expand pseudoinstructions.
    485 The fetched sequence corresponds to the expansion, according to \texttt{sigma}, of the pseudoinstruction.
     485Then, fetching a pseudoinstruction from the pseudo-code memory at address \texttt{ppc} corresponds to fetching a sequence of instructions from the real code memory using \texttt{policy} to expand pseudoinstructions.
     486The fetched sequence corresponds to the expansion, according to the policy, of the pseudoinstruction.
    486487
    487488At first, the lemma appears to immediately imply the correctness of the assembler.
Note: See TracChangeset for help on using the changeset viewer.