Changeset 3158 for Deliverables
 Timestamp:
 Apr 17, 2013, 7:17:49 PM (8 years ago)
 Location:
 Deliverables/D3.4/Report
 Files:

 2 added
 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.4/Report/report.tex
r3142 r3158 448 448 \item transformation to \textsf{RTLabs} control flow graph 449 449 \end{enumerate} 450 451 TODO: layered approach  main part is the common measurable 452 preservation proof; finegrained version of normal simulation results 453 does rest. 450 \todo{I keep mentioning forward sim results  I probably ought to say 451 something about determinancy} We have taken a common approach to 452 each pass: first we build (or axiomatise) forward simulation results 453 that are similar to normal compiler proofs, but slightly more 454 finegrained so that we can see that the call structure and relative 455 placement of cost labels is preserved. 456 457 Then we instantiate a general result which shows that we can find a 458 \emph{measurable} subtrace in the target of the pass that corresponds 459 to the measurable subtract in the source. By repeated application of 460 this result we can find a measurable subtrace of the execution of the 461 \textsf{RTLabs} code, suitable for the construction of a structured 462 trace (see Section~\ref{sec:structuredtrace}. This is essentially an 463 extra layer on top of the simulation proofs that provides us with the 464 extra information required for our intensional correctness proof. 454 465 455 466 \subsection{Generic measurable subtrace lifting proof} 456 467 457 Sketch properties required; need to preserve prefix as well as meas 458 subtrace; how to deal with untidy edges wrt to sim rel; anything to 459 say about obs, stack? 468 Our generic proof is parametrised on a record containing smallstep 469 semantics for the source and target language, a classification of 470 states (the same form of classification is used when defining 471 structured traces), a simulation relation which loosely respects the 472 classification and cost labelling \todo{this isn't very helpful} and 473 four simulation results: 474 \begin{enumerate} 475 \item a step from a `normal' state (which is not classified as a call 476 or return) which is not a cost label is simulated by zero or more 477 `normal' steps; 478 \item a step from a `call' state followed by a cost label step is 479 simulated by a step from a `call' state, a corresponding label step, 480 then zero or more `normal' steps; 481 \item a step from a `call' state not followed by a cost label 482 similarly (note that this case cannot occur in a welllabelled 483 program, but we do not have enough information locally to exploit 484 this); and 485 \item a cost label step is simulated by a cost label step. 486 \end{enumerate} 487 Finally, we need to know that a successfully translated program will 488 have an initial state in the simulation relation with the original 489 program's initial state. 490 491 \begin{figure} 492 \begin{center} 493 \includegraphics[width=0.5\linewidth]{meassim.pdf} 494 \end{center} 495 \caption{Tiling of simulation for a measurable subtrace} 496 \label{fig:tiling} 497 \end{figure} 498 499 To find the measurable subtrace in the target program's execution we 500 walk along the original program's execution trace applying the 501 appropriate simulation result by induction on the number of steps. 502 While the number of steps taken varies, the overall structure is 503 preserved, as illustrated in Figure~\ref{fig:tiling}. By preserving 504 the structure we also maintain the same intensional observables. One 505 delicate point is that the cost label following a call must remain 506 directly afterwards\footnote{The prototype compiler allowed some 507 straightline code to appear before the cost label until a later 508 stage of the compiler, but we must move the requirement forward to 509 fit with the structured traces.} 510 % Damn it, I should have just moved the cost label forwards in RTLabs, 511 % like the prototype does in RTL to ERTL; the result would have been 512 % simpler. Or was there some reason not to do that? 513 (both in the program code and in the execution trace), even if we 514 introduce extra steps, for example to store parameters in memory in 515 \textsf{Cminor}. Thus we have a version of the call simulation 516 that deals with both in one result. 517 518 In addition to the subtrace we are interested in measuring we must 519 also prove that the earlier part of the trace is also preserved in 520 order to use the simulation from the initial state. It also 521 guarantees that we do not run out of stack space before the subtrace 522 we are interested in. The lemmas for this prefix and the measurable 523 subtrace are similar, following the pattern above. However, the 524 measurable subtrace also requires us to rebuild the termination 525 proof. This has a recursive form: 526 \begin{lstlisting}[language=matita] 527 let rec will_return_aux C (depth:nat) 528 (trace:list (cs_state … C × trace)) on trace : bool := 529 match trace with 530 [ nil $\Rightarrow$ false 531  cons h tl $\Rightarrow$ 532 let $\langle$s,tr$\rangle$ := h in 533 match cs_classify C s with 534 [ cl_call $\Rightarrow$ will_return_aux C (S depth) tl 535  cl_return $\Rightarrow$ 536 match depth with 537 [ O $\Rightarrow$ match tl with [ nil $\Rightarrow$ true  _ $\Rightarrow$ false ] 538  S d $\Rightarrow$ will_return_aux C d tl 539 ] 540  _ $\Rightarrow$ will_return_aux C depth tl 541 ] 542 ]. 543 \end{lstlisting} 544 The \lstinline'depth' is the number of return states we need to see 545 before we have returned to the original function (initially zero) and 546 \lstinline'trace' the measurable subtrace obtained from the running 547 the semantics for the correct number of steps. This definition 548 unfolds tail recursively for each step, and once the corresponding 549 simulation result has been applied a new one for the target can be 550 asserted by unfolding and applying the induction hypothesis on the 551 shorter trace. 552 553 This then gives us an overall result for any simulation fitting the 554 requirements above (contained in the \lstinline'meas_sim' record): 555 \begin{lstlisting}[language=matita] 556 theorem measured_subtrace_preserved : 557 $\forall$MS:meas_sim. 558 $\forall$p1,p2,m,n,stack_cost,max. 559 ms_compiled MS p1 p2 $\rightarrow$ 560 measurable (ms_C1 MS) p1 m n stack_cost max $\rightarrow$ 561 $\exists$m',n'. 562 measurable (ms_C2 MS) p2 m' n' stack_cost max $\wedge$ 563 observables (ms_C1 MS) p1 m n = observables (ms_C2 MS) p2 m' n'. 564 \end{lstlisting} 565 The stack space requirement that is embedded in \lstinline'measurable' 566 is a consequence of the preservation of observables. 567 568 TODO: how to deal with untidy edges wrt to sim rel; anything to 569 say about obs? 570 571 TODO: say something about termination measures; cost labels are 572 statements/exprs in these languages; split call/return gives simpler 573 simulations 460 574 461 575 \subsection{Simulation results for each pass} … … 472 586 473 587 \section{Existence of a structured trace} 474 \label{sec:structure trace}588 \label{sec:structuredtrace} 475 589 476 590 TODO: design, basic structure from termination proof, how cost
Note: See TracChangeset
for help on using the changeset viewer.