Changeset 3216
 Timestamp:
 Apr 29, 2013, 11:15:46 PM (6 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.4/Report/report.tex
r3214 r3216 309 309 \subsection{Main goals} 310 310 311 TODO: need an example for this312 313 311 Informally, our main intensional result links the time difference in a source 314 312 code execution to the time difference in the object code, expressing the time … … 342 340 guarantees on; they must start at a cost label and end at the return 343 341 of the enclosing function of the cost label\footnote{We expect that 344 this would generalise to subtraces between cost labels in the same345 f unction, but could not justify the extra complexity that would be346 required to show this.}. A typical example of such a subtrace is 347 the execution of an entire function from the cost label at the start348 of the function until it returns. We call such any such subtrace 349 \emph{measurable} if it (and the prefix of the trace from the start to 350 the subtrace) can also beexecuted within the available stack space.342 this would generalise to more general subtraces by subtracting costs 343 for unwanted measurable suffixes of a measurable subtrace.}. A 344 typical example of such a subtrace is the execution of an entire 345 function from the cost label at the start of the function until it 346 returns. We call such any such subtrace \emph{measurable} if it (and 347 the prefix of the trace from the start to the subtrace) can also be 348 executed within the available stack space. 351 349 352 350 Now we can give the main intensional statement for the compiler. … … 357 355 function calls and returns. 358 356 357 358 359 359 More formally, the definition of this statement in \matita{} is 360 360 \begin{lstlisting}[language=matita] 361 361 definition simulates := 362 362 $\lambda$p: compiler_output. 363 let initial_status := initialise_status $ \dots$ (cm (c_labelled_object_code $\dots$ p)) in363 let initial_status := initialise_status $...$ (cm (c_labelled_object_code $...$ p)) in 364 364 $\forall$m1,m2. 365 measurable Clight_pcs (c_labelled_clight $ \dots$ p) m1 m2366 (lookup_stack_cost (c_stack_cost $\dots$ p)) (c_max_stack $\dots$ p) $\rightarrow$365 measurable Clight_pcs (c_labelled_clight $...$ p) m1 m2 366 (stack_sizes (c_stack_cost $...$ p)) (c_max_stack $...$ p) $\rightarrow$ 367 367 $\forall$c1,c2. 368 clock_after Clight_pcs (c_labelled_clight $ \dots$ p) m1 (c_clight_cost_map $\dots$ p) = OK $\dots$ c1 $\rightarrow$369 clock_after Clight_pcs (c_labelled_clight $ \dots$ p) (m1+m2) (c_clight_cost_map $\dots$ p) = OK $\dots$ c2 $\rightarrow$368 clock_after Clight_pcs (c_labelled_clight $...$ p) m1 (c_clight_cost_map $...$ p) = OK $...$ c1 $\rightarrow$ 369 clock_after Clight_pcs (c_labelled_clight $...$ p) (m1+m2) (c_clight_cost_map $...$ p) = OK $...$ c2 $\rightarrow$ 370 370 $\exists$n1,n2. 371 observables Clight_pcs (c_labelled_clight $ \dots$ p) m1 m2 =372 observables (OC_preclassified_system (c_labelled_object_code $\dots$ p))373 (c_labelled_object_code $\dots$ p) n1 n2371 observables Clight_pcs (c_labelled_clight $...$ p) m1 m2 = 372 observables (OC_preclassified_system (c_labelled_object_code $...$ p)) 373 (c_labelled_object_code $...$ p) n1 n2 374 374 $\wedge$ 375 c2  c1 = clock $\dots$ (execute n2 ? initial_status)  clock $\dots$ (execute n1 ? initial_status). 375 clock ?? (execute (n1+n2) ? initial_status) = 376 clock ?? (execute n1 ? initial_status) + (c2c1). 376 377 \end{lstlisting} 377 378 where the \lstinline'measurable', \lstinline'clock_after' and 378 \lstinline'observables' definitions can be applied tomultiple379 \lstinline'observables' definitions are generic definitions for multiple 379 380 languages; in this case the \lstinline'Clight_pcs' record applies them 380 381 to \textsf{Clight} programs. … … 387 388 $\forall$input_program,output. 388 389 compile input_program = return output $\rightarrow$ 389 not_wrong … (exec_inf …clight_fullexec input_program) $\rightarrow$390 not_wrong $...$ (exec_inf $...$ clight_fullexec input_program) $\rightarrow$ 390 391 sim_with_labels 391 (exec_inf …clight_fullexec input_program)392 (exec_inf … clight_fullexec (c_labelled_clight …output))392 (exec_inf $...$ clight_fullexec input_program) 393 (exec_inf $...$ clight_fullexec (c_labelled_clight $...$ output)) 393 394 \end{lstlisting} 394 395 That is, any successful compilation produces a labelled program that … … 396 397 `undefined behaviour'. 397 398 398 Note that this provides full functional correctness, including399 Note that this statement provides full functional correctness, including 399 400 preservation of (non)termination. The intensional result above does 400 401 not do this directly  it does not guarantee the same result or same 401 402 termination. There are two mitigating factors, however: first, to 402 prove the intensional property you need local simulation results that403 prove the intensional property you need local simulation results  these 403 404 can be pieced together to form full behavioural equivalence, only time 404 405 constraints have prevented us from doing so. Second, if we wish to … … 412 413 413 414 The essential parts of the intensional proof were outlined during work 414 on a toy 415 compiler~\cite{d2.1,springerlink:10.1007/9783642324697_3}. These 416 are 415 on a toy compiler in Task 416 2.1~\cite{d2.1,springerlink:10.1007/9783642324697_3}. These are 417 417 \begin{enumerate} 418 418 \item functional correctness, in particular preserving the trace of … … 441 441 442 442 Jointly, we generalised the structured traces to apply to any of the 443 intermediate languages w ithsome idea of program counter. This means443 intermediate languages which have some idea of program counter. This means 444 444 that they are introduced part way through the compiler, see 445 445 Figure~\ref{fig:compiler}. Proving that a structured trace can be … … 451 451 language and so the structural properties are ensured by the 452 452 semantics. 453 \item Many of the backend languages from \textsf{RTL} share a common453 \item Many of the backend languages from \textsf{RTL} onwards share a common 454 454 core set of definitions, and using structured traces throughout 455 455 increases this uniformity. … … 497 497 with the transformations in \textsf{Clight} that produce the source 498 498 program with cost labels, then show that measurable traces can be 499 lifted to \textsf{RTLabs}, and finally that we can construct the499 lifted to \textsf{RTLabs}, and finally show that we can construct the 500 500 properties listed above ready for the backend proofs. 501 501 … … 505 505 As explained on page~\pageref{page:switchintro}, the costs of complex 506 506 C \lstinline[language=C]'switch' statements cannot be represented with 507 the simple labelling. Our first pass replaces these statements with 508 simpler C code, allowing our second pass to perform the cost 509 labelling. We show that the behaviour of programs is unchanged by 510 these passes. 507 the simple labelling used in the formalised compiler. Our first pass 508 replaces these statements with simpler C code, allowing our second 509 pass to perform the cost labelling. We show that the behaviour of 510 programs is unchanged by these passes using forward 511 simulations\footnote{All of our languages are deterministic, which can 512 be seen directly from their executable definitions. Thus we know that 513 forward simulations are sufficient because the target cannot have any 514 other behaviour.}. 511 515 512 516 \subsection{Switch removal} 513 517 514 The intermediate languages of the frontend have no jump tables. 515 Hence, we have to compile the \lstinline[language=C]'switch' 516 constructs away before going from \textsf{Clight} to \textsf{Cminor}. 518 We compile away \lstinline[language=C]'switch' statements into more 519 basic \textsf{Clight} code. 517 520 Note that this transformation does not necessarily deteriorate the 518 521 efficiency of the generated code. For instance, compilers such as GCC … … 535 538 may contain \lstinline[language=C]'break' statements, which have the 536 539 effect of exiting the switch statement. In the absence of break, the 537 execution falls through each case sequentially. In our currentimplementation,540 execution falls through each case sequentially. In our implementation, 538 541 we produce an equivalent sequence of ``ifthen'' chained by gotos: 539 542 \begin{lstlisting}[language=C] … … 545 548 if(fresh == v2) { 546 549 lbl_case2: 547 $\llbracket$stmt2 ;$\rrbracket$550 $\llbracket$stmt2$\rrbracket$; 548 551 goto lbl_case2; 549 552 }; … … 554 557 The proof had to tackle the following points: 555 558 \begin{itemize} 556 \item the source and target memories are not the same ( cf.fresh variable),559 \item the source and target memories are not the same (due to the fresh variable), 557 560 \item the flow of control is changed in a nonlocal way (e.g. \textbf{goto} 558 561 instead of \textbf{break}). … … 584 587 steps for the added cost labels. The extra instructions do not change 585 588 the memory or local environments, although we have to keep track of 586 the extra instructions in continuations. 589 the extra instructions that appear in continuations, for example 590 during the execution of a \lstinline[language=C]'while' loop. 587 591 588 592 We do not attempt to capture any cost properties of the labelling in 589 the simulation proof, allowing the proof to be oblivious to the choice 593 the simulation proof\footnote{We describe how the cost properties are 594 established in Section~\ref{sec:costchecks}.}, allowing the proof to be oblivious to the choice 590 595 of cost labels. Hence we do not have to reason about the threading of 591 596 name generation through the labelling function, greatly reducing the 592 amount of effort required. We describe how the cost properties are 593 established in Section~\ref{sec:costchecks}. 597 amount of effort required. 594 598 595 599 %TODO: both give onestepsimbymany forward sim results; switch … … 611 615 \item transformation to \textsf{RTLabs} control flow graph 612 616 \end{enumerate} 613 \todo{I keep mentioning forward sim results  I probably ought to say 614 something about determinancy} We have taken a common approach to 617 We have taken a common approach to 615 618 each pass: first we build (or axiomatise) forward simulation results 616 that are similar to normal compiler proofs, but slightly more619 that are similar to normal compiler proofs, but which are slightly more 617 620 finegrained so that we can see that the call structure and relative 618 621 placement of cost labels is preserved. … … 623 626 this result we can find a measurable subtrace of the execution of the 624 627 \textsf{RTLabs} code, suitable for the construction of a structured 625 trace (see Section~\ref{sec:structuredtrace} . This is essentially an628 trace (see Section~\ref{sec:structuredtrace}). This is essentially an 626 629 extra layer on top of the simulation proofs that provides us with the 627 extrainformation required for our intensional correctness proof.630 additional information required for our intensional correctness proof. 628 631 629 632 \subsection{Generic measurable subtrace lifting proof} … … 632 635 semantics for the source and target language, a classification of 633 636 states (the same form of classification is used when defining 634 structured traces), a simulation relation which loosely respects the 635 classification and cost labelling \todo{this isn't very helpful} and 636 four simulation results: 637 structured traces), a simulation relation which respects the 638 classification and cost labelling and 639 four simulation results. The simulations are split by the starting state's 640 classification and whether it is a cost label, which will allow us to 641 observe that the call structure is preserved. They are: 637 642 \begin{enumerate} 638 643 \item a step from a `normal' state (which is not classified as a call … … 689 694 \label{prog:terminationproof} 690 695 \begin{lstlisting}[language=matita] 691 let rec will_return_aux C (depth:nat)692 (trace:list (cs_state …C × trace)) on trace : bool :=693 match trace with694 [ nil $\Rightarrow$ false695  cons h tl $\Rightarrow$696 let $\langle$s,tr$\rangle$ := h in697 match cs_classify C s with698 [ cl_call $\Rightarrow$ will_return_aux C (S depth) tl699  cl_return $\Rightarrow$700 match depth with701 [ O $\Rightarrow$ match tl with [ nil $\Rightarrow$ true  _ $\Rightarrow$ false ]702  S d $\Rightarrow$ will_return_aux C d tl703 ]704  _ $\Rightarrow$ will_return_aux C depth tl705 ]706 ].696 let rec will_return_aux C (depth:nat) 697 (trace:list (cs_state $...$ C × trace)) on trace : bool := 698 match trace with 699 [ nil $\Rightarrow$ false 700  cons h tl $\Rightarrow$ 701 let $\langle$s,tr$\rangle$ := h in 702 match cs_classify C s with 703 [ cl_call $\Rightarrow$ will_return_aux C (S depth) tl 704  cl_return $\Rightarrow$ 705 match depth with 706 [ O $\Rightarrow$ match tl with [ nil $\Rightarrow$ true  _ $\Rightarrow$ false ] 707  S d $\Rightarrow$ will_return_aux C d tl 708 ] 709  _ $\Rightarrow$ will_return_aux C depth tl 710 ] 711 ]. 707 712 \end{lstlisting} 708 713 The \lstinline'depth' is the number of return states we need to see … … 728 733 \end{lstlisting} 729 734 The stack space requirement that is embedded in \lstinline'measurable' 730 is a consequence of the preservation of observables. 735 is a consequence of the preservation of observables, because it is 736 determined by the functions called and returned from, which are observable. 731 737 732 738 TODO: how to deal with untidy edges wrt to sim rel; anything to 733 739 say about obs? 734 740 735 TODO: say something about termination measures;cost labels are741 TODO: cost labels are 736 742 statements/exprs in these languages; split call/return gives simpler 737 743 simulations … … 739 745 \subsection{Simulation results for each pass} 740 746 741 \paragraph{Cast simplification.} 742 743 The parser used in Cerco introduces a lot of explicit type casts. 747 We now consider the simulation results for the passes, each of which 748 is used to instantiate the 749 \lstinline[language=matita]'measured_subtrace_preserved' theorem to 750 construct the measurable subtrace for the next language. 751 752 \subsubsection{Cast simplification} 753 754 The parser used in \cerco{} introduces a lot of explicit type casts. 744 755 If left as they are, these constructs can greatly hamper the 745 756 quality of the generated code  especially as the architecture 746 we consider is an $8$ 757 we consider is an $8$bit one. In \textsf{Clight}, casts are 747 758 expressions. Hence, most of the work of this transformation 748 759 proceeds on expressions. The tranformation proceeds by recursively … … 754 765 \begin{lstlisting}[language=matita] 755 766 let rec simplify_expr (e:expr) (target_sz:intsize) (target_sg:signedness) 756 : Σresult:bool×expr.757 ∀ge,en,m. simplify_inv ge en m e (\snd result) target_sz target_sg (\fst result) ≝$\ldots$758 759 and simplify_inside (e:expr) : Σresult:expr. conservation e result ≝$\ldots$767 : $\Sigma$result:bool$\times$expr. 768 $\forall$ge,en,m. simplify_inv ge en m e (\snd result) target_sz target_sg (\fst result) := $\ldots$ 769 770 and simplify_inside (e:expr) : $\Sigma$result:expr. conservation e result := $\ldots$ 760 771 \end{lstlisting} 761 772 … … 781 792 inductive simplify_inv 782 793 (ge : genv) (en : env) (m : mem) 783 (e1 : expr) (e2 : expr) (target_sz : intsize) (target_sg : signedness) : bool → Prop ≝784  Inv_eq : ∀result_flag. $\ldots$794 (e1 : expr) (e2 : expr) (target_sz : intsize) (target_sg : signedness) : bool $\rightarrow$ Prop := 795  Inv_eq : $\forall$result_flag. $\ldots$ 785 796 simplify_inv ge en m e1 e2 target_sz target_sg result_flag 786  Inv_coerce_ok : ∀src_sz,src_sg. 787 (typeof e1) = (Tint src_sz src_sg) → (typeof e2) = (Tint target_sz target_sg) → 788 (smaller_integer_val src_sz target_sz src_sg (exec_expr ge en m e1) (exec_expr ge en m e2)) → 797  Inv_coerce_ok : $\forall$src_sz,src_sg. 798 typeof e1 = Tint src_sz src_sg $\rightarrow$ 799 typeof e2 = Tint target_sz target_sg $\rightarrow$ 800 smaller_integer_val src_sz target_sz src_sg (exec_expr ge en m e1) (exec_expr ge en m e2) $\rightarrow$ 789 801 simplify_inv ge en m e1 e2 target_sz target_sg true. 790 802 \end{lstlisting} 791 803 792 The \textsf{conservation} invariant simply states the conservation804 The \textsf{conservation} invariant for \textsf{simplify\_inside} simply states the conservation 793 805 of the semantics, as in the \textsf{Inv\_eq} constructor of the previous 794 806 invariant. 795 807 796 808 \begin{lstlisting}[language=matita] 797 definition conservation ≝ λe,result. ∀ge,en,m.809 definition conservation := $\lambda$e,result. $\forall$ge,en,m. 798 810 res_sim ? (exec_expr ge en m e) (exec_expr ge en m result) 799 ∧res_sim ? (exec_lvalue ge en m e) (exec_lvalue ge en m result)800 ∧typeof e = typeof result.811 $\wedge$ res_sim ? (exec_lvalue ge en m e) (exec_lvalue ge en m result) 812 $\wedge$ typeof e = typeof result. 801 813 \end{lstlisting} 802 814 … … 805 817 inconsistently typed programs, a canonical case being a particular 806 818 integer constant of a certain size typed with another size. This 807 prompted the need to introduce numerous type checks, complexifying 808 both the implementation and the proof. 819 prompted the need to introduce numerous type checks, making 820 both the implementation and the proof more complex, even though more 821 comprehensive checks are made in the next stage. 809 822 \todo{Make this a particular case of the more general statement on baking more invariants in the Clight language} 810 823 811 \paragraph{Clight to Cminor.} 812 813 This pass is the last one operating on the Clight intermediate language. 814 Its input is a full \textsf{Clight} program, and its output is a \textsf{Cminor} 815 program. Note that we do not use an equivalent of the C\#minor language: we 816 translate directly to Cminor. This presents the advantage of not requiring the 817 special loop constructs, nor the explicit block structure. Another salient 818 point of our approach is that a significant part of the properties needed for 819 the simulation proof were directly encoded in dependently typed translation 820 functions. This concerns more precisely freshness conditions and welltypedness 821 conditions. The main effects of the transformation from \textsf{Clight} to 824 \subsection{Clight to Cminor} 825 826 This pass is the last one operating on the \textsf{Clight} language. 827 Its input is a full \textsf{Clight} program, and its output is a 828 \textsf{Cminor} program. Note that we do not use an equivalent of 829 Compcert's \textsf{C\#minor} language: we translate directly to a 830 variant of \textsf{Cminor}. This presents the advantage of not 831 requiring the special loop constructs, nor the explicit block 832 structure. Another salient point of our approach is that a significant 833 number of the properties needed for the simulation proof were directly 834 encoded in dependently typed translation functions. In particular, 835 freshness conditions and welltypedness conditions are included. The 836 main effects of the transformation from \textsf{Clight} to 822 837 \textsf{Cminor} are listed below. 823 838 … … 827 842 local variables is moved out of the modelled memory and stored in a 828 843 dedicated environment. 829 \item In Clight, each local variable has a dedicated memory block, whereas844 \item In \textsf{Clight}, each local variable has a dedicated memory block, whereas 830 845 stackallocated locals are bundled together on a functionbyfunction basis. 831 846 \item Loops are converted to jumps. … … 843 858 manipulations (as in the later version of Compcert's memory model). We proved 844 859 roughly 80 \% of the required lemmas. Some difficulties encountered were notably 845 due to some too relaxed conditions on pointer validity (problemfixed during development).846 Some more conditions had to be added to take care of possible overflows when converting847 from \textbf{Z} block bounds to $16$ bit pointer offsets (in pra tice, these overflows860 due to some overly relaxed conditions on pointer validity (fixed during development). 861 Some more side conditions had to be added to take care of possible overflows when converting 862 from \textbf{Z} block bounds to $16$ bit pointer offsets (in practice, these overflows 848 863 only occur in edge cases that are easily ruled out  but this fact is not visible 849 864 in memory injections). Concretely, some of the lemmas on the preservation of simulation of 850 loads after writes were axiomatised, forlack of time.865 loads after writes were axiomatised, due to a lack of time. 851 866 852 867 \subparagraph{Simulation proof.} 853 868 854 The correct ion proof for this transformation was not terminated. We proved the869 The correctness proof for this transformation was not completed. We proved the 855 870 simulation result for expressions and for some subset of the critical statement cases. 856 871 Notably lacking are the function entry and exit, where the memory injection is 857 properly set up. As can be guessed, a significant amount of work has to be performed872 properly set up. As would be expected, a significant amount of work has to be performed 858 873 to show the conservation of all invariants at each simulation step. 859 874 … … 864 879 865 880 Ideally, we would provide proofs that the cost labelling pass always 866 produce dprograms that are soundly and precisely labelled and that881 produces programs that are soundly and precisely labelled and that 867 882 each subsequent pass preserves these properties. This would match our 868 883 use of dependent types to eliminate impossible sources of errors … … 895 910 checking this is more difficult. 896 911 897 The implementation works through the set of nodes in the graph,912 The implementation progresses through the set of nodes in the graph, 898 913 following successors until a cost label is found or a labelfree cycle 899 914 is discovered (in which case the property does not hold and we stop). … … 909 924 was then used to prove the implementation sound and complete. 910 925 911 While we have not attempted to pro ofthat the cost labelled properties926 While we have not attempted to prove that the cost labelled properties 912 927 are established and preserved earlier in the compiler, we expect that 913 the effort for the \textsf{Cminor} to \textsf{RTLabs} would be similar914 to the work outlined above, because it involves the change from 915 requiring a cost label at particular positions to requiring cost 916 labels to break loops in the CFG. As there are another three passes 917 t o consider (including the labelling itself), we believe that using918 th e check above is much simpler overall.928 the effort for the \textsf{Cminor} to \textsf{RTLabs} stage alone 929 would be similar to the work outlined above, because it involves the 930 change from requiring a cost label at particular positions to 931 requiring cost labels to break loops in the CFG. As there are another 932 three passes to consider (including the labelling itself), we believe 933 that using the check above is much simpler overall. 919 934 920 935 % TODO? Found some Clight to Cminor bugs quite quickly … … 923 938 \label{sec:structuredtrace} 924 939 925 \emph{Structured traces} enrich the execution trace of a program by926 nesting function calls in a mixedstep style and embedding the cost 940 The \emph{structured traces} introduced in Section~\ref{sec:fegoals} enrich the execution trace of a program by 941 nesting function calls in a mixedstep style and embedding the cost labelling 927 942 properties of the program. It was originally designed to support the 928 943 proof of correctness for the timing analysis of the object code in the … … 948 963 }. 949 964 \end{lstlisting} 950 which gives a type of states, an execution relation, some notion of 951 program counters with decidable equality, the classification of states 965 which gives a type of states, an execution relation\footnote{All of 966 our semantics are executable, but using a relation was simpler in 967 the abstraction.}, some notion of 968 program counters with decidable equality, the classification of states, 952 969 and functions to extract the observable intensional information (cost 953 970 labels and the identity of functions that are called). The … … 961 978 The structured traces are defined using three mutually inductive 962 979 types. The core data structure is \lstinline'trace_any_label', which 963 captures some straightline execution until the next cost label or 964 function return. Each function call is embedded as a single step, 965 with its own trace nested inside and the before and after states 966 linked by \lstinline'as_after_return', and states classified as a 967 `jump' (in particular branches) must be followed by a cost label. 980 captures some straightline execution until the next cost label or the 981 return from the enclosing function. Any function calls are embedded as 982 a single step, with its own trace nested inside and the before and 983 after states linked by \lstinline'as_after_return'; and states 984 classified as a `jump' (in particular branches) must be followed by a 985 cost label. 968 986 969 987 The second type, \lstinline'trace_label_label', is a … … 981 999 982 1000 The construction of the structured trace replaces syntactic cost 983 labelling properties which place requirements on where labels appear1001 labelling properties, which place requirements on where labels appear 984 1002 in the program, with semantics properties that constrain the execution 985 1003 traces of the program. The construction begins by defining versions 986 of the sound and precise labelling properties on the program text that 987 appears in states rather than programs, and showing that these are 988 preserved by steps of the \textsf{RTLabs} semantics. 1004 of the sound and precise labelling properties on states and global 1005 environments (for the code that appears in each of them) rather than 1006 whole programs, and showing that these are preserved by steps of the 1007 \textsf{RTLabs} semantics. 989 1008 990 1009 Then we show that each cost labelling property the structured traces 991 definition requires is satisfied. These are broken up by the1010 definition requires is locally satisfied. These are broken up by the 992 1011 classification of states. Similarly, we prove a stepbystep stack 993 1012 preservation result, which states that the \textsf{RTLabs} semantics … … 1011 1030 label. 1012 1031 1013 \subsubsection{ Whole programstructured traces}1032 \subsubsection{Complete execution structured traces} 1014 1033 1015 1034 The development of the construction above started relatively early, 1016 before the measurable subtraces preservation proofs. To be confident 1017 that the traces were wellformed, we also developed a whole program 1018 form that embeds the traces above. This includes nonterminating 1019 programs, where an infinite number of the terminating structured 1020 traces are embedded. This construction confirmed that our definition 1021 of structured traces was consistent, although we later found that we 1022 did not require them for the compiler correctness results. 1035 before the measurable subtrace preservation proofs. To be confident 1036 that the traces were wellformed at that time, we also developed a 1037 complete execution form that embeds the traces above. This includes 1038 nonterminating program executions, where an infinite number of the terminating 1039 structured traces are embedded. This construction confirmed that our 1040 definition of structured traces was consistent, although we later 1041 found that we did not require the whole execution version for the 1042 compiler correctness results. 1023 1043 1024 1044 To construct these we need to know whether each function call will … … 1032 1052 concentrating on the novel intensional parts of the proof, we have 1033 1053 shown that it is possible to construct certifying compilers that 1034 correctly report execution time and stack space costs. 1054 correctly report execution time and stack space costs. The layering 1055 of intensional correctness proofs on top of normal simulation results 1056 provides a useful separation of concerns, and could permit the reuse 1057 of existing results. 1058 1059 1035 1060 1036 1061 TODO: appendix on code layout?
Note: See TracChangeset
for help on using the changeset viewer.