Changeset 1761 for Deliverables


Ignore:
Timestamp:
Feb 27, 2012, 11:31:21 AM (8 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D1.2/CompilerProofOutline/outline.tex

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