 Timestamp:
 Jun 16, 2011, 11:24:27 AM (9 years ago)
 Location:
 src/ASM/CPP2011
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/CPP2011/cpp2011.tex
r973 r974 224 224 To a degree of approximation, the assembler on an assembly program, consisting of $n$ pseudoinstructions $\mathtt{P_i}$ for $1 \leq i \leq n$, works as in the following diagram: 225 225 \begin{displaymath} 226 [\mathtt{P_1}, \ldots \mathtt{P_n}] \xrightarrow{\ left(\mathtt{P_i} \xrightarrow{\mbox{\fontsize{7}{9}\selectfont$\mathtt{expand}$}} \mathtt{[I_1^i, \ldots I^q_i]} \xrightarrow{\mbox{\fontsize{7}{9}\selectfont$\mathtt{assembly1}^*$}} \mathtt{[0110]}\right)^{*}} \mathtt{[010101]}226 [\mathtt{P_1}, \ldots \mathtt{P_n}] \xrightarrow{\mathtt{flatten}\left(\mathtt{P_i} \xrightarrow{\mbox{\fontsize{7}{9}\selectfont$\mathtt{expand}$}} \mathtt{[I_1^i, \ldots I^q_i]} \xrightarrow{\mbox{\fontsize{7}{9}\selectfont$\mathtt{assembly1}^*$}} \mathtt{[0110]}\right)^{*}} \mathtt{[010101]} 227 227 \end{displaymath} 228 229 228 Here $\mathtt{I^i_j}$ for $1 \leq j \leq q$ are the $q$ machine code instructions obtained by expanding, with \texttt{expand\_pseudo\_instruction}, a single pseudoinstruction. 230 229 Each machine code instruction $\mathtt{I^i_j}$ is then assembled, using the \texttt{assembly1} function, into a list of bytes. 231 230 This process is iterated for each pseudoinstruction, before the lists are flattened into a single bit list representation of the original assembly program. 231 232 By inspecting the above diagram, it would appear that the best way to proceed with a proof that the assembly process does not change the semantics of an assembly program is via a decomposition of the problem into two subproblems. 233 Namely, we first expand any and all pseudoinstructions into lists of machine instructions, and provide a proof that this process does not change our program's semantics. 234 Finally, we assemble all machine code instructions into machine codelists of bytesand prove once more that this process does not have an adverse effect on a program's semantics. 235 By composition, we then have that the whole assembly process is semantics preserving. 236 237 This is a tempting approach to the proof, but ultimately the wrong approach. 238 In particular, it is important that we track how the program counter indexing into the assembly program, and the machine's program counter evolve, so that we can relate them. 239 Expanding pseudoinstructions requires that the machine's program counter be incremented by $n$ steps, for $1 \leq n$, for every increment of the assembly program's program counter. 240 Keeping track of the correspondence between the two program counters quickly becomes unfeasible using a compositional approach, and hence the proof must be monolithic. 232 241 233 242 %  % … … 256 265 This function fails if and only if an internal call to \texttt{assembly\_1\_pseudoinstruction} fails: 257 266 \begin{lstlisting} 258 definition sigma0: 259 pseudo_assembly_program$\rightarrow$ option (nat $\times$ (nat $\times$ (BitVectorTrie Word 16))) := $\ldots$267 definition sigma0: pseudo_assembly_program 268 $\rightarrow$ option (nat $\times$ (nat $\times$ (BitVectorTrie Word 16))) := $\ldots$ 260 269 \end{lstlisting} 261 270 We eventually lift this to functions from program counters to program counters: … … 273 282 definition sigma: pseudo_assembly_program $\rightarrow$ Word $\rightarrow$ Word := $\ldots$ 274 283 \end{lstlisting} 284 285 %  % 286 % SECTION % 287 %  % 288 \subsection{Total correctness of the assembler} 289 \label{subsect.total.correctness.of.the.assembler} 290 291 CSC: no options using policy 292 \begin{lstlisting} 293 lemma fetch_assembly_pseudo2: $\forall$program, assembled, costs, labels. 294 Some $\ldots$ $\langle$labels,costs$\rangle$ = build_maps program $\rightarrow$ 295 Some $\ldots$ $\langle$assembled,costs$\rangle$ = assembly program $\rightarrow$ $\forall$ppc. 296 let code_memory := load_code_memory assembled in 297 let preamble := $\pi_1$ program in 298 let data_labels := construct_datalabels preamble in 299 let lk_labels := 300 λx. sigma program (address_of_word_labels_code_mem ($\pi_2$ program) x) in 301 let lk_dlabels := λx. lookup ? ? x data_labels (zero ?) in 302 let expansion := jump_expansion ppc program in 303 let $\langle$pi,newppc$\rangle$ := fetch_pseudo_instruction ($\pi_2$ program) ppc in 304 let ppc' := sigma program ppc in 305 let newppc' := sigma program newppc in 306 let instructions' := 307 expand_pseudo_instruction lk_labels lk_dlabels ppc' expansion pi in 308 let fetched := fetch_many code_memory newppc' ppc' instructions in 309 $\exists$instructions. Some ? instructions = instructions' $\wedge$ fetched. 310 \end{lstlisting} 311 312 \begin{lstlisting} 313 definition expand_pseudo_instruction: 314 ∀lookup_labels, lookup_datalabels, pc, policy_decision. 315 pseudo_instruciton $\rightarrow$ option list instruction := $\ldots$ 316 \end{lstlisting} 317 318 \begin{lstlisting} 319 axiom assembly_ok: ∀program,assembled,costs,labels. 320 Some $\ldots$ $\langle$labels, costs$\rangle$ = build_maps program $\rightarrow$ 321 Some $\ldots$ $\langle$assembled, costs$\rangle$ = assembly program $\rightarrow$ 322 let code_memory := load_code_memory assembled in 323 let preamble := $\pi_1$ program in 324 let datalabels := construct_datalabels preamble in 325 let lk_labels := 326 $\lambda$x. sigma program (address_of_word_labels_code_mem ($\pi_2$ program) x) in 327 let lk_dlabels := $\lambda$x. lookup ? ? x datalabels (zero ?) in 328 ∀ppc,len,assembledi. 329 let $\langle$pi, newppc$\rangle$ := fetch_pseudo_instruction ($\pi_2$ program) ppc in 330 let assembly' := assembly_1_pseudoinstruction program ppc 331 (sigma program ppc) lk_labels lk_dlabels pi in 332 let newpc := (sigma program ppc) + len in 333 let echeck := 334 encoding_check code_memory (sigma program ppc) slen assembledi in 335 Some $\ldots$ $\langle$len, assembledi$\rangle$ = assembly' $\rightarrow$ 336 echeck $\wedge$ sigma program newppc = newpc. 337 \end{lstlisting} 338 339 \begin{lstlisting} 340 lemma fetch_assembly_pseudo: $\forall$program, ppc, lk_labels, lk_dlabels. 341 $\forall$pi, code_memory, len, assembled, instructions, pc. 342 let jexp := jump_expansion ppc program in 343 let exp := 344 expand_pseudo_instruction lookup_labels lookup_datalabels pc jexp pi 345 let ass := 346 assembly_1_pseudoinstruction program ppc pc lk_labels lk_dlabels pi in 347 Some ? instructions = exp $\rightarrow$ 348 Some $\ldots$ $\langle$len, assembled$\rangle$ = ass $\rightarrow$ 349 encoding_check code_memory pc (pc + len) assembled $\rightarrow$ 350 fetch_many code_memory (pc + len) pc instructions. 351 \end{lstlisting} 352 353 \begin{lstlisting} 354 theorem fetch_assembly: $\forall$pc, i, cmem, assembled. 355 assembled = assembly1 i $\rightarrow$ 356 let len := length ... assembled in 357 encoding_check cmem pc (pc + len) assembled $\rightarrow$ 358 let fetched := fetch code_memory (bitvector_of_nat $\ldots$ pc) in 359 let $\langle$instr_pc, ticks$\rangle$ := fetched in 360 let $\langle$instr,pc'$\rangle$ := instr_pc in 361 (eq_instruction instr i $\wedge$ 362 eqb ticks (ticks_of_instruction instr) $\wedge$ 363 eq_bv $\ldots$ pc' (pc + len)) = true. 364 \end{lstlisting} 365 275 366 An \texttt{internal\_pseudo\_address\_map} positions in the memory of a \texttt{PseudoStatus} with a physical memory address. 276 367 \begin{lstlisting} … … 298 389 This is done with the following function: 299 390 \begin{lstlisting} 300 definition next_internal_pseudo_address_map: 301 internal_pseudo_address_map $\rightarrow$ PseudoStatus $\rightarrow$ option internal_pseudo_address_map 302 \end{lstlisting} 303 Finally, we are able to state and prove our main theorem relating the execution of a single assembly instruction and the execution of (possibly) many machine code instructions: 304 \begin{lstlisting} 305 lemma main_thm: 391 definition next_internal_pseudo_address_map: internal_pseudo_address_map 392 $\rightarrow$ PseudoStatus $\rightarrow$ option internal_pseudo_address_map 393 \end{lstlisting} 394 Finally, we are able to state and prove our main theorem. 395 This relates the execution of a single assembly instruction and the execution of (possibly) many machine code instructions. 396 That is, the assembly process preserves the semantics of an assembly program, as it is translated into machine code: 397 \begin{lstlisting} 398 theorem main_thm: 306 399 ∀M,M',ps,s,s''. 307 400 next_internal_pseudo_address_map M ps = Some ... M' $\rightarrow$ … … 316 409 Suppose further that, after executing a single assembly instruction and converting the resulting \texttt{PseudoStatus} into a \texttt{Status}, we obtain $s''$, being careful to track the number of ticks executed. 317 410 Then, there exists some number $n$, so that executing $n$ machine code instructions in \texttt{Status} $s$ gives us \texttt{Status} $s''$. 318 319 %  % 320 % SECTION % 321 %  % 322 \subsection{Proof of correctness} 323 \label{subsect.proof.of.correctness} 324 325 CSC: no options using policy 326 \begin{lstlisting} 327 lemma fetch_assembly_pseudo2: 328 ∀program,assembled,costs,labels. 329 Some ... LANGLElabels,costsRANGLE = build_maps program → 330 Some ... LANGLEassembled,costsRANGLE = assembly program → 331 ∀ppc. 332 let code_memory ≝ load_code_memory assembled in 333 let preamble ≝ \fst program in 334 let data_labels ≝ construct_datalabels preamble in 335 let lookup_labels ≝ λx. sigma program (address_of_word_labels_code_mem (\snd program) x) in 336 let lookup_datalabels ≝ λx. lookup ? ? x data_labels (zero ?) in 337 let expansion ≝ jump_expansion ppc program in 338 let LANGLEpi,newppcRANGLE ≝ fetch_pseudo_instruction (\snd program) ppc in 339 ∃instructions. 340 Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (sigma program ppc) expansion pi ∧ 341 fetch_many code_memory (sigma program newppc) (sigma program ppc) instructions. 342 \end{lstlisting} 343 344 \begin{lstlisting} 345 definition expand_pseudo_instruction: 346 ∀lookup_labels.∀lookup_datalabels.∀pc.∀policy_decision. (sigma program ppc) expansion. pseudo_instruciton > list instruction. 347 \end{lstlisting} 348 349 \begin{lstlisting} 350 axiom assembly_ok: 351 ∀program,assembled,costs,labels. 352 Some ... LANGLElabels,costsRANGLE = build_maps program → 353 Some ... LANGLEassembled,costsRANGLE = assembly program → 354 let code_memory ≝ load_code_memory assembled in 355 let preamble ≝ \fst program in 356 let datalabels ≝ construct_datalabels preamble in 357 let lookup_labels ≝ λx. sigma program (address_of_word_labels_code_mem (\snd program) x) in 358 let lookup_datalabels ≝ λx. lookup ?? x datalabels (zero ?) in 359 ∀ppc,len,assembledi. 360 let LANGLEpi,newppcRANGLE ≝ fetch_pseudo_instruction (\snd program) ppc in 361 Some ... LANGLElen,assemblediRANGLE = assembly_1_pseudoinstruction program ppc (sigma program ppc) lookup_labels lookup_datalabels pi → 362 encoding_check code_memory (sigma program ppc) (bitvector_of_nat ... (nat_of_bitvector ... (sigma program ppc) + len)) assembledi ∧ 363 sigma program newppc = bitvector_of_nat ... (nat_of_bitvector ... (sigma program ppc) + len). 364 \end{lstlisting} 365 366 \begin{lstlisting} 367 lemma fetch_assembly_pseudo: 368 ∀program,ppc,lookup_labels,lookup_datalabels. 369 ∀pi,code_memory,len,assembled,instructions,pc. 370 let expansion ≝ jump_expansion ppc program in 371 Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (bitvector_of_nat ? pc) expansion pi → 372 Some ... LANGLElen,assembledRANGLE = assembly_1_pseudoinstruction program ppc (bitvector_of_nat ? pc) lookup_labels lookup_datalabels pi → 373 encoding_check code_memory (bitvector_of_nat ... pc) (bitvector_of_nat ... (pc + len)) assembled → 374 fetch_many code_memory (bitvector_of_nat ... (pc + len)) (bitvector_of_nat ... pc) instructions. 375 \end{lstlisting} 376 377 \begin{lstlisting} 378 theorem fetch_assembly: 379 ∀pc,i,code_memory,assembled. 380 assembled = assembly1 i → 381 let len ≝ length ... assembled in 382 encoding_check code_memory (bitvector_of_nat ... pc) (bitvector_of_nat ... (pc + len)) assembled → 383 let fetched ≝ fetch code_memory (bitvector_of_nat ... pc) in 384 let LANGLEinstr_pc, ticksRANGLE ≝ fetched in 385 let LANGLEinstr,pc'RANGLE ≝ instr_pc in 386 (eq_instruction instr i ∧ eqb ticks (ticks_of_instruction instr) ∧ eq_bv ... pc' (bitvector_of_nat ... (pc + len))) = true. 387 \end{lstlisting} 411 Theorem \texttt{main\_thm} establishes the correctness of the assembly process. 388 412 389 413 %  % 
src/ASM/CPP2011/lstgrafite.tex
r960 r974 2 2 mathescape=true, 3 3 texcl=false, 4 keywords={include}, 5 morekeywords={record, with, match, let, rec, corec, inductive, definition, axiom, 4 keywords={record, with, match, let, rec, corec, inductive, definition, axiom, 6 5 qed, intro, intros, symmetry, simplify, rewrite, apply, elim, assumption, 7 6 left, cut, cases, auto, right, coercion, split, lemma, theorem, skip, constructor, copy, from, letin, 8 7 by, done, we, conclude, assume, need, to, prove, unfold, return, and, check, 9 8 notation, interpretation, lapply, repeat, try, as, clear, in, change, whd, exists}, 9 morekeywords={[2]include}, 10 10 %emph={[1]Type, Prop, nat, real}, emphstyle={[1]\textit}, 11 11 literate= … … 142 142 {...}{{$\ldots$}}1 143 143 , 144 tabsize=1, 144 145 comment=[s]{(*}{*)}, 145 146 showstringspaces=true, … … 149 150 captionpos=b, 150 151 mathescape=true, 152 keywordstyle=\bfseries, 153 keywordstyle=[2]\bfseries, 154 keywordstyle=[3]\bfseries, 151 155 %backgroundcolor=\color{gray}, 152 156 frame=tblr,
Note: See TracChangeset
for help on using the changeset viewer.