Changeset 1029
 Timestamp:
 Jun 21, 2011, 2:23:42 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/CPP2011/cpp2011.tex
r1028 r1029 224 224 For instance, to apply a coercion to force $\lambda x.M : A \to B$ to have type $\forall x:A.\Sigma y:B.P~x~y$, the system looks for a coercion from $M: B$ to $\Sigma y:B.P~x~y$ in a context augmented with $x:A$. 225 225 This is significant when the coercion opens a proof obligation, as the user will be presented with multiple, but simpler proof obligations in the correct context. 226 In this way, Matita supports the 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.226 In 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. 227 227 228 228 %  % … … 301 301 \begin{lstlisting} 302 302 inductive jump_length: Type[0] := 303  short_jump: jump_length 304  medium_jump: jump_length 305  long_jump: jump_length. 303 short_jump:jump_length medium_jump:jump_length long_jump:jump_length. 306 304 \end{lstlisting} 307 305 … … 384 382 lookup $\ldots$ id labels (zero $\ldots$) = sigma pseudo_program pol addr := $\ldots$ 385 383 \end{lstlisting} 386 The type of \texttt{build\_maps} owes to our use of Matita's Russell facility to provide a strong specification for the function in the type (c.f. the use of $\Sigma$types , through which Russell is implemented in Matita).384 The type of \texttt{build\_maps} owes to our use of Matita's Russell facility to provide a strong specification for the function in the type (c.f. the use of $\Sigma$types and coercions, through which Russell is simulated in Matita). 387 385 We express that for all labels that appear exactly once in any assembly program, the newly created map used in the implementation, and the stronger \texttt{sigma} function used in the specification, agree. 388 386 … … 415 413 The \texttt{fetch} function, as its name implies, fetches the instruction indexed by the program counter in the code memory, while \texttt{assembly1} maps a single instruction to its byte encoding: 416 414 \begin{lstlisting} 417 theorem fetch_assembly: $\forall$pc, i, cmem, assembled. 418 assembled = assembly1 i $\rightarrow$ 415 theorem fetch_assembly: $\forall$pc, i, cmem, assembled. assembled=assembly1 i $\rightarrow$ 419 416 let len := length $\ldots$ assembled in 420 417 encoding_check cmem pc (pc + len) assembled $\rightarrow$ 421 418 let fetched := fetch code_memory (bitvector_of_nat $\ldots$ pc) in 422 419 let $\langle$instr_pc, ticks$\rangle$ := fetched in 423 420 let $\langle$instr, pc'$\rangle$ := instr_pc in 424 (eq_instruction instr i $\wedge$ 425 eqb ticks (ticks_of_instruction instr) $\wedge$ 421 (eq_instruction instr i $\wedge$ eqb ticks (ticks_of_instruction instr) $\wedge$ 426 422 eq_bv $\ldots$ pc' (pc + len)) = true. 427 423 \end{lstlisting} … … 436 432 lemma fetch_assembly_pseudo: 437 433 ∀program.∀pol:policy program.∀ppc.∀code_memory. 438 let pi := fst (fetch_pseudo_instruction (sndprogram) ppc) in434 let pi := $\pi_1$ (fetch_pseudo_instruction ($\pi_2$ program) ppc) in 439 435 let instructions := expand_pseudo_instruction program pol ppc ... in 440 436 let $\langle$len,assembled$\rangle$ := assembly_1_pseudoinstruction program pol ppc ... in … … 447 443 448 444 Intuitively, Lemma \texttt{fetch\_assembly\_pseudo} can be read as follows. 449 Suppose our policy \texttt{jump\_expansion} dictates that the pseudoinstruction indexed by the pseudo program counter \texttt{ppc} in assembly program \texttt{program} gives us the policy decision \texttt{pol}. 450 Further, suppose we expand the pseudoinstruction at \texttt{ppc} with the policy decision \texttt{pol}, obtaining the list of machine code instructions \texttt{instructions}. 445 Suppose we expand the pseudoinstruction at \texttt{ppc} with the policy decision \texttt{pol}, obtaining the list of machine code instructions \texttt{instructions}. 451 446 Suppose we also assemble the pseudoinstruction at \texttt{ppc} to obtain \texttt{assembled}, a list of bytes. 452 447 Then, 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. 453 448 454 449 The final lemma in this series is \texttt{fetch\_assembly\_pseudo2} that combines the Lemma \texttt{fetch\_aasembly\_pseudo} with the correctness of the functions that load object code into the processor's memory. 455 At first, the lemmas appears to nearly establish the correctness of the assembler:456 450 \begin{lstlisting} 457 451 lemma fetch_assembly_pseudo2: 458 452 ∀program,pol,ppc. 459 453 let $\langle$labels,costs$\rangle$ := build_maps program pol in 460 let assembled := \fst(assembly program pol) in454 let assembled := $\pi_1$ (assembly program pol) in 461 455 let code_memory := load_code_memory assembled in 462 let data_labels := construct_datalabels ( \fstprogram) in456 let data_labels := construct_datalabels ($\pi_1$ program) in 463 457 let lookup_labels := 464 λx. sigma $\ldots$ pol (address_of_word_labels_code_mem ( \sndprogram) x) in458 λx. sigma $\ldots$ pol (address_of_word_labels_code_mem ($\pi_2$ program) x) in 465 459 let lookup_datalabels := λx. lookup ? ? x data_labels (zero ?) in 466 let $\langle$pi,newppc$\rangle$ := fetch_pseudo_instruction (\snd program) ppc in 467 let instructions ≝ expand_pseudo_instruction program pol ppc ... in 468 fetch_many code_memory (sigma program pol newppc) 469 (sigma program pol ppc) instructions. 460 let $\langle$pi,newppc$\rangle$ := fetch_pseudo_instruction ($\pi_2$ program) ppc in 461 let instrs ≝ expand_pseudo_instruction program pol ppc ... in 462 fetch_many code_memory (sigma $\ldots$ pol newppc) (sigma $\ldots$ pol ppc) instrs. 470 463 \end{lstlisting} 471 464 … … 475 468 The fetched sequence corresponds to the expansion, according to \texttt{pol}, of the pseudoinstruction. 476 469 470 At first, the lemmas appears to immediately imply the correctness of the assembler. 477 471 However, this property is \emph{not} strong enough to establish that the semantics of an assembly program has been preserved by the assembly process since it does not establish the correspondence between the semantics of a pseudoinstruction and that of its expansion. 478 472 In particular, the two semantics differ on instructions that \emph{could} directly manipulate program addresses. … … 513 507 \begin{lstlisting} 514 508 axiom low_internal_ram_of_pseudo_low_internal_ram: 515 internal_pseudo_address_map $\rightarrow$ BitVectorTrie Byte 7 $\rightarrow$BitVectorTrie Byte 7.509 internal_pseudo_address_map$\rightarrow$BitVectorTrie Byte 7$\rightarrow$BitVectorTrie Byte 7. 516 510 \end{lstlisting} 517 511 … … 526 520 The \texttt{next\_internal\_pseudo\_address\_map} function is responsible for run time monitoring of the behaviour of assembly programs, in order to detect well behaved ones. 527 521 It returns a map that traces memory addresses in internal RAM after execution of the next pseudoinstruction, failing when the instruction tampers with memory addresses in unanticipated (but potentially correct) ways. 528 It thus decides the membership of a correct but not complete subset of well behaved programs.522 It thus decides the membership of a strict subset of the set of well behaved programs. 529 523 \begin{lstlisting} 530 524 definition next_internal_pseudo_address_map: internal_pseudo_address_map … … 581 575 However, this comes at the expense of assembler completeness: the generated program may be too large to fit into code memory. 582 576 In this respect, there is a tradeoff between the completeness of the assembler and the efficiency of the assembled program. 583 The definition and proof of a ncomplete, optimal (in the sense that jump pseudoinstructions are expanded to the smallest possible opcode) and correct jump expansion policy is ongoing work.577 The definition and proof of a complete, optimal (in the sense that jump pseudoinstructions are expanded to the smallest possible opcode) and correct jump expansion policy is ongoing work. 584 578 585 579 Aside from their application in verified compiler projects such as CerCo and CompCert, verified assemblers such as ours could also be applied to the verification of operating system kernels.
Note: See TracChangeset
for help on using the changeset viewer.