Changeset 1761 for Deliverables/D1.2/CompilerProofOutline
 Timestamp:
 Feb 27, 2012, 11:31:21 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D1.2/CompilerProofOutline/outline.tex
r1760 r1761 778 778 the proof of correctness of cost prediction shows that the cost of executing 779 779 a labelled object code program is the same as the sum over all labels in the 780 program execution trace of the cost statically associated to the label on780 program execution trace of the cost statically associated to the label and 781 781 computed on the object code itself. 782 782 783 The previous statement is too weak to be proved that way. 784 785 T O D O ! ! ! 783 In presence of object level function calls, the previous statement is, however, 784 incorrect. The reason is twofold. First of all, a function call may diverge. 785 To the last labels that comes before the call, however, we also associate 786 the cost of the instructions that follow the call. Therefore, in the 787 sum over all labels, when we meet a label we prepay for the instructions 788 after function calls, assuming all calls to be terminating. This choice is 789 driven by considerations on the source code. Functions can be called also 790 inside expressions and it would be too disruptive to put labels inside 791 expressions to capture the cost of instructions that follow a call. Moreover, 792 adding a label after each call would produce a much higher number of proof 793 obligations in the certification of source programs using FramaC. The 794 proof obligations, moreover, would be guarded by termination of all functions 795 involved, that also generates lots of additional complex proof obligations 796 that have little to do with execution costs. With our approach, instead, we 797 put less burden on the user, at the price of proving a weaker statement: 798 the estimated and actual costs will be the same if and only if the high level 799 program is converging. For prefixes of diverging programs we can provide 800 a similar result where the equality is replaced by an inequality (loss of 801 precision). 802 803 Assuming totality of functions is however not sufficient yet at the object 804 level. Even if a function returns, there is no guarantee that it will transfer 805 control back to the calling point. For instance, the function could have 806 manipulated the return address from its stack frame. Moreover, an object level 807 program can forge any address and transfer control to it, with no guarantee 808 on the execution behaviour and labelling properties of the called program. 809 810 To solve the problem, we introduced the notion of \emph{structured trace} 811 that come in two flavours: structured traces for total programs (an inductive 812 type) and structured traces for diverging programs (a coinductive type based 813 on the previous one). Roughly speaking, a structured trace represents the 814 execution of a well behaved program that is subject to several constraints 815 like 816 \begin{enumerate} 817 \item All function calls return control just after the calling point 818 \item The execution of all function bodies start with a label and end with 819 a RET (even the ones reached by invoking a function pointer) 820 \item All instructions are covered by a label (required by correctness of 821 the labelling approach) 822 \item The target of all conditional jumps must be labelled (a sufficient 823 but not necessary condition for precision of the labelling approach) 824 \item \label{prop5} Two structured traces with the same structure yield the same 825 cost traces. 826 \end{enumerate} 827 828 Correctness of cost predictions is proved only for structured execution traces, 829 i.e. well behaved programs. The forward simulation proof for all backend 830 passes will actually be a proof of preservation of the structure of 831 the structured traces that, because of property \ref{prop5}, will imply 832 correctness of the cost prediction for the backend. The Clight to RTLabs 833 will also include a proof that associates to each converging execution its 834 converging structured trace and to each diverging execution its diverging 835 structured trace. 836 837 There are also other two issues that invalidate the naive statement of 838 correctness of cost prediciton given above. The algorithm that statically 839 computes the cost of blocks is correct only when the object code is \emph{well 840 formed} and the program counter is \emph{reachable}. 841 A well formed object code is such that 842 the program counter will never overflow after the execution step of 843 the processor. An overflow that occurs during fetching but is overwritten 844 during execution is, however, correct and necessary to accept correct 845 programs that are as large as the program memory. Temporary overflows add 846 complications to the proof. A reachable address is an address that can be 847 obtained by fetching (not executing!) a finite number of times from the 848 beginning of the code memory without ever overflowing. The complication is that 849 the static prediction traverses the code memory assuming that the memory will 850 be read sequentially from the beginning and that all jumps jump only to 851 reachable addresses. When this property is violated, the way the code memory 852 is interpreted is uncorrect and the cost computed is totally meaningless. 853 The reachability relation is closed by fetching for well formed programs. 854 The property that calls to function pointers only target reachable and 855 well labelled locations, however, is not statically predictable and it is 856 enforced in the structured trace. 857 858 The proof of correctness of cost predictions has been quite complex. Setting 859 up the good invariants (structured traces, well formed programs, reachability) 860 and completing the proof has required more than 3 men months while the initally 861 estimated effort was much lower. In the paperandpencil proof for IMP, the 862 corresponding proof was obvious and only took two lines. 863 864 The proof itself is quite involved. We 865 basically need to show as an important lemma that the sum of the execution 866 costs over a structured trace, where the costs are summed in execution order, 867 is equivalent to the sum of the execution costs in the order of prepayment. 868 The two orders are quite different and the proof is by mutual recursion over 869 the definition of the converging structured traces, which is a family of three 870 mutual inductive types. The fact that this property only holds for converging 871 function calls in hidden in the definition of the structured traces. 872 Then we need to show that the order of prepayment 873 corresponds to the order induced by the cost traces extracted from the 874 structured trace. Finally, we need to show that the statically computed cost 875 for one block corresponds to the cost dinamically computed in prepayment 876 order. 786 877 787 878 \section{Overall results}
Note: See TracChangeset
for help on using the changeset viewer.