Changeset 2369
 Timestamp:
 Sep 28, 2012, 3:13:49 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Papers/cppasm2012/cpp2012asm.tex
r2368 r2369 419 419 \subsection{Correctness of the assembler with respect to fetching} 420 420 \label{subsect.total.correctness.of.the.assembler} 421 We now begin the proof of correctness of the assembler. Correctness consists 422 of two properties: 1) the assembly process never fails when fed a correct 423 policy; 424 2)~the object code returned simulates the source code when the latter is 425 executed according to the cost model also returned by the assembler. 426 427 Property 2) can be decomposed into two main properties: correctness with 428 respect to fetching+decoding and correctness w.r.t. execution. 429 430 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 431 to prove correctness w.r.t. fetching. Section~\ref{subsect.total.correctness.for.well.behaved.assembly.programs} deals with correctness w.r.t. execution: 432 the instructions \texttt{[J1, \ldots, Jn]} simulate the pseudoinstruction~\texttt{I}. 421 We now begin the proof of correctness of the assembler. 422 Correctness consists of two properties: firstly that the assembly process never fails when fed a correct policy and secondly the object code returned simulates the source code when the latter is executed according to the cost model also returned by the assembler. 423 424 The second property above can be further decomposed into two main properties: correctness with respect to fetching and decoding and correctness with respect to execution. 425 426 Informally, correctness with respect to 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. 427 This section reviews the main steps to prove correctness with respect to fetching. 428 Subsect.~\ref{subsect.total.correctness.for.well.behaved.assembly.programs} deals with correctness with respect to execution: the instructions \texttt{[J1, \ldots, Jn]} simulate the pseudoinstruction~\texttt{I}. 433 429 434 430 The (slightly simplified) Russell type for the \texttt{assembly} function is: … … 447 443 \end{lstlisting} 448 444 In plain words, the type of \texttt{assembly} states the following. 449 Given a correct policy for the program to be assembled, the assembler never 450 fails and returns some object code and a costing function. 451 Under the condition that the policy is `correct' for the program and the program is fully addressable by a 16bit word, the object code is also fully addressable by a 16bit word. Moreover, the 452 result of assemblying the pseudoinstruction obtained fetching from the 453 assembly address \texttt{ppc} 454 is a list of bytes found in the generated object code starting from 455 the object code address \texttt{policy(ppc)}. 456 457 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 458 allows to prove the inductive step of the proof, which is by induction over 459 the assembly program. It is then simple to lift the property from lists 460 of bytes (object code) to tries of bytes (i.e. code memories after loading). 445 Given a correct policy for the program to be assembled, the assembler never fails and returns some object code and a costing function. 446 Under the condition that the policy is `correct' for the program and the program is fully addressable by a 16bit word, the object code is also fully addressable by a 16bit word. 447 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)}. 448 449 Essentially the type above states that the \texttt{assembly} function correctly expands pseudoinstructions, and that the expanded instruction reside consecutively in memory. 450 The fundamental hypothesis is correctness of the policy which allows us to prove the inductive step of the proof, which proceeds by induction over the assembly program. 451 It is then straightforward to lift the property from lists of bytes (object code) to tries of bytes (i.e. code memories after loading). 461 452 The \texttt{assembly\_ok} lemma does the lifting. 462 453 463 We have established that every pseudoinstruction is compiled to a sequence of 464 bytes that is found in memory at the expect place. This does not imply 465 trivially that those bytes will be decoded in a correct way to recover the 466 pseudoinstruction expansion. Indeed, we need first to prove a lemma that 467 establish that the \texttt{fetch} function is the left inverse of the 468 \texttt{assembly1} function: 454 We have established that every pseudoinstruction is compiled to a sequence of bytes that is found in memory at the expect place. 455 This does not trivially imply that those bytes will be decoded in a correct way to recover the pseudoinstruction expansion. 456 Indeed, we first need to prove a lemma that establishes that the \texttt{fetch} function is the left inverse of the \texttt{assembly1} function: 469 457 \begin{lstlisting} 470 458 lemma fetch_assembly: … … 481 469 \end{lstlisting} 482 470 We read \texttt{fetch\_assembly} as follows. 483 Any time the encoding \texttt{assembled} of an instruction \texttt{i} 484 is found in code memory starting at position \texttt{pc} (the hypothesis 485 \texttt{encoding\_check} \ldots), when we fetch at address \texttt{pc} 486 we retrieve the instruction \texttt{i}, the updated program counter 487 is \texttt{pc} plus the length of the encoding, and the cost of the 488 fetched instruction is the one predicted for \texttt{i}. 489 Or, in plainer words, assembling, storing and then immediately fetching 490 gets you back to where you started. 491 492 Remembering that \texttt{assembly\_1\_pseudo\_instruction} is the composition 493 of \texttt{assembly1} with \texttt{expand\_pseudo\_instruction}, we can 494 lift the previous result from instructions (already expanded) to 495 pseudoinstructions (to be expanded): 471 Any time the encoding \texttt{assembled} of an instruction \texttt{i} is found in code memory starting at position \texttt{pc} (the hypothesis \texttt{encoding\_check} \ldots), when we fetch at address \texttt{pc} we retrieve the instruction \texttt{i}, the updated program counter is \texttt{pc} plus the length of the encoding, and the cost of the fetched instruction is the one predicted for \texttt{i}. 472 Or, in plainer words, assembling, storing and then immediately fetching gets you back to where you started. 473 474 Remembering that \texttt{assembly\_1\_pseudo\_instruction} is the composition of \texttt{assembly1} with \texttt{expand\_pseudo\_instruction}, we can lift the previous result from instructions (already expanded) to pseudoinstructions (to be expanded): 496 475 \begin{lstlisting} 497 476 lemma fetch_assembly_pseudo: … … 511 490 The function \texttt{fetch\_many} fetches multiple machine code instructions from code memory and performs some routine checks. 512 491 513 Intuitively, Lemma \texttt{fetch\_assembly\_pseudo} says that 514 expanding a pseudoinstruction into $n$ instructions, encoding the instructions 515 and immediately fetching $n$ instructions back yield exactly the expansion. 516 517 Combining \texttt{assembly\_ok} with the previos lemma and a proof of 518 correctness of loading object code in memory, we finally get correctness 519 of the assembler w.r.t. fetching: 492 Intuitively, Lemma \texttt{fetch\_assembly\_pseudo} says that expanding a pseudoinstruction into $n$ instructions, encoding the instructions and immediately fetching $n$ instructions back yield exactly the expansion. 493 494 Combining \texttt{assembly\_ok} with the previous lemma and a proof of correctness of loading object code in memory, we finally get correctness of the assembler with respect to fetching: 520 495 \begin{lstlisting} 521 496 lemma fetch_assembly_pseudo2: … … 529 504 fetch_many cmem (policy newppc) (policy ppc) instructions. 530 505 \end{lstlisting} 531 532 506 Here we use $\pi_1$ to project the existential witness from the Russelltyped function \texttt{assembly}. 533 507 We read \texttt{fetch\_assembly\_pseudo2} as follows. 534 508 Suppose we are given an assembly program which can be addressed by a 16bit word and a policy that is correct for this program. 535 509 Suppose we are able to successfully assemble an assembly program using \texttt{assembly} and produce a code memory, \texttt{cmem}. 536 Then, fetching a pseudoinstruction from the pseudocode memory stored in 537 the interval $[ppc,newppc]$ corresponds to fetching a sequence of instructions from the real code memory, stored in the interval $[policy(ppc),policy(ppc+1)]$. 538 The correspondence is precise: the fetched instructions are exactly those 539 obtained expanding the pseudoinstruction according to policy. 540 541 In order to complete the proof of correctness of the assembler, we need 542 to prove that each pseudoinstruction is simulated by the execution of its 543 expansion (correctness w.r.t. execution). In general this is not the case 544 when the instruction freely manipulates program addresses. Characterizing 545 well behaved programs and proving correctness w.r.t. expansion is the topic 546 of the next Section. 510 Then, fetching a pseudoinstruction from the pseudocode memory stored in the interval $[ppc,newppc]$ corresponds to fetching a sequence of instructions from the real code memory, stored in the interval $[policy(ppc),policy(ppc+1)]$. 511 The correspondence is precise: the fetched instructions are exactly those obtained expanding the pseudoinstruction according to policy. 512 513 In order to complete the proof of correctness of the assembler, we need to prove that each pseudoinstruction is simulated by the execution of its expansion (correctness with respect to execution). 514 In general this is not the case when instructions freely manipulate program addresses. 515 Characterising wellbehaved programs and proving correctness with respect to expansion is discussed next. 547 516 548 517 %  %
Note: See TracChangeset
for help on using the changeset viewer.