Changeset 2339 for Papers

Sep 26, 2012, 12:24:53 PM (7 years ago)

Got to page 8/9.

1 edited


  • Papers/cpp-asm-2012/cpp-2012-asm.tex

    r2329 r2339  
    159159definition execute_1: $\forall$cm. Status cm $\rightarrow$ Status cm := $\ldots$
     161Here \texttt{Status} is parameterised by \texttt{cm}, a code memory represented as a trie.
    161162%The function \texttt{execute} allows one to execute an arbitrary, but fixed (due to Matita's normalisation requirement) number of steps of a program.
    162163The function \texttt{execute\_1} closely matches the operation of the MCS-51 hardware, as described by a Siemen's manufacturer's data sheet (specifically, this one~\cite{siemens:2011}).
    166167inductive preinstruction (A: Type[0]): Type[0] :=
    167168 | ADD: $\llbracket$acc_a$\rrbracket$ → $\llbracket$registr; direct; indirect; data$\rrbracket$ $\rightarrow$ preinstruction A
    168  | INC: $\llbracket$ acc_a; registr; direct; indirect; dptr$\rrbracket$ $\rightarrow$ preinstruction A
     169 | DEC: $\llbracket$acc_a; registr; direct; indirect$\rrbracket$ $\rightarrow$ preinstruction A
    169170 | JB: $\llbracket$bit_addr$\rrbracket$ $\rightarrow$ A $\rightarrow$ preinstruction A
    170171 | ...
    181182Once decoded, execution proceeds by a case analysis on the decoded instruction, following the operation of the hardware.
    182183For example, the \texttt{DEC} instruction (`decrement') is implemented as follows:
    185185 | DEC addr $\Rightarrow$
    222222definition execute_1_pseudo_instruction:
    223  (Word $\rightarrow$ nat $\times$ nat) $\rightarrow$ $\forall$cm. PseudoStatus cm $\rightarrow$ PseudoStatus cm := $\ldots$
    224 \end{lstlisting}
    225 Notice, here, that the emulation function for assembly programs takes an additional argument over \texttt{execute\_1}.
    226 This is a function that maps program counters (at the assembly level) to pairs of natural numbers representing the number of clock ticks that the pseudoinstruction needs to execute, post expansion.
     223 $\forall$cm. ($\forall$ppc: Word. ppc < $\mid$snd cm$\mid$ $\rightarrow$ nat $\times$ nat) $\rightarrow$ $\forall$s:PseudoStatus cm.
     224  program_counter $\ldots$ s < $\mid$snd cm$\mid$ $\rightarrow$ PseudoStatus cm := $\ldots$
     226The type of \texttt{execute\_1\_pseudo\_instruction} is interesting.
     227Note here that our representation of code memory \texttt{cm} is no longer a bitvector trie of bytes, but a list of pseudoinstructions.
     228Further, we take in a function that maps program counters (at the assembly level) to pairs of natural numbers representing the number of clock ticks that the pseudoinstructions needs to execute, post expansion.
    227229We call this function a \emph{costing}, and note that the costing is induced by the particular strategy we use to expand pseudoinstructions.
    228230If we change how we expand conditional jumps to labels, for instance, then the costing needs to change, hence \texttt{execute\_1\_pseudo\_instruction}'s parametricity in the costing.
     231This costing function expects a proof, at its second argument, stating that the program counter falls within the bounds of the pseudoprogram.
     232A similar invariant holds of the pseudoprogram counter passed to the \texttt{execute\_1\_pseudo\_instruction} function.
    230234The costing returns \emph{pairs} of natural numbers because, in the case of expanding conditional jumps to labels, the expansion of the `true branch' and `false branch' may differ in execution time.
    233237Execution proceeds by first fetching from pseudo-code memory using the program counter---treated as an index into the pseudoinstruction list.
     238This index is always guaranteed to be within the bounds of the pseudoinstruction list due to the dependent type placed on the function.
    234239No decoding is required.
    235240We then proceed by case analysis over the pseudoinstruction, reusing the code for object code for all instructions present in the MCS-51's instruction set.
    328333definition assembly:
    329  $\forall$p: pseudo_assembly_program.
    330  $\forall$sigma: Word $\rightarrow$ Word.
    331  $\forall$policy: Word $\rightarrow$ bool.
    332   $\Sigma$res:list Byte $\times$ (BitVectorTrie costlabel 16).
    333    sigma_meets_specification p sigma policy $\rightarrow$
    334    let $\langle$preamble, instr_list$\rangle$ := p in
    335    |instr_list| < 2^16 $\rightarrow$
    336    let $\langle$assembled,costs$\rangle$ := res in
    337     $\forall$ppc. $\forall$ppc_ok:nat_of_bitvector $\ldots$ ppc < |instr_list|.
    338     let $\langle$pi,newppc$\rangle$ := fetch_pseudo_instruction instr_list ppc ppc_ok in
    339     let $\langle$l,a$\rangle$ := assembly_1_pseudoinstruction $\ldots$ sigma policy ppc $\ldots$ pi in
    340      $\forall$j:nat. j < |a|
    341       nth j a = nth (add $\ldots$ (sigma ppc) (bitvector_of_nat ? j))) assembled
     334  $\forall$program: pseudo_assembly_program.
     335  $\forall$policy.
     336    $\Sigma$assembled: list Byte $\times$ (BitVectorTrie costlabel 16).
     337      policy is correct for program $\rightarrow$
     338      $\mid$program$\mid$ < $2^{16}$ $\rightarrow$
     339      $\mid$fst assembled$\mid$ < $2^{16}$ $\wedge$
     340      policy ($\mid$program$\mid$) = $\mid$fst assembled$\mid$ $\vee$
     341      policy ($\mid$program$\mid$) = 0 $\wedge$ $\mid$fst assembled$\mid$ = $2^{16}$ $\wedge$
     342      $\forall$ppc: pseudo\_program\_counter such that ppc < $2^{16}$.
     343        let pseudo_instr := fetch from program at ppc in
     344        let assembled_i := assemble pseudo_instr in
     345          $\mid$assembled_i$\mid$ $\leq$ $2^{16}$ $\wedge$
     346            $\forall$n: nat such that n < $\mid$assembled_i$\mid$.
     347            $\exists$k: nat.
     348              nth assembled_i n = nth assembled (policy ppc + k).
    343350In plain words, the type of \texttt{assembly} states the following.
Note: See TracChangeset for help on using the changeset viewer.