Changeset 2339 for Papers/cppasm2012
 Timestamp:
 Sep 26, 2012, 12:24:53 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Papers/cppasm2012/cpp2012asm.tex
r2329 r2339 159 159 definition execute_1: $\forall$cm. Status cm $\rightarrow$ Status cm := $\ldots$ 160 160 \end{lstlisting} 161 Here \texttt{Status} is parameterised by \texttt{cm}, a code memory represented as a trie. 161 162 %The function \texttt{execute} allows one to execute an arbitrary, but fixed (due to Matita's normalisation requirement) number of steps of a program. 162 163 The function \texttt{execute\_1} closely matches the operation of the MCS51 hardware, as described by a Siemen's manufacturer's data sheet (specifically, this one~\cite{siemens:2011}). … … 166 167 inductive preinstruction (A: Type[0]): Type[0] := 167 168  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 A169  DEC: $\llbracket$acc_a; registr; direct; indirect$\rrbracket$ $\rightarrow$ preinstruction A 169 170  JB: $\llbracket$bit_addr$\rrbracket$ $\rightarrow$ A $\rightarrow$ preinstruction A 170 171  ... … … 181 182 Once decoded, execution proceeds by a case analysis on the decoded instruction, following the operation of the hardware. 182 183 For example, the \texttt{DEC} instruction (`decrement') is implemented as follows: 183 184 184 \begin{lstlisting} 185 185  DEC addr $\Rightarrow$ … … 221 221 \begin{lstlisting} 222 222 definition 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$ 225 \end{lstlisting} 226 The type of \texttt{execute\_1\_pseudo\_instruction} is interesting. 227 Note here that our representation of code memory \texttt{cm} is no longer a bitvector trie of bytes, but a list of pseudoinstructions. 228 Further, 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. 227 229 We call this function a \emph{costing}, and note that the costing is induced by the particular strategy we use to expand pseudoinstructions. 228 230 If 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. 231 This costing function expects a proof, at its second argument, stating that the program counter falls within the bounds of the pseudoprogram. 232 A similar invariant holds of the pseudoprogram counter passed to the \texttt{execute\_1\_pseudo\_instruction} function. 229 233 230 234 The 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. … … 232 236 233 237 Execution proceeds by first fetching from pseudocode memory using the program countertreated as an index into the pseudoinstruction list. 238 This index is always guaranteed to be within the bounds of the pseudoinstruction list due to the dependent type placed on the function. 234 239 No decoding is required. 235 240 We then proceed by case analysis over the pseudoinstruction, reusing the code for object code for all instructions present in the MCS51's instruction set. … … 327 332 \begin{lstlisting} 328 333 definition 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). 342 349 \end{lstlisting} 343 350 In plain words, the type of \texttt{assembly} states the following.
Note: See TracChangeset
for help on using the changeset viewer.