Changeset 3434 for Papers


Ignore:
Timestamp:
Feb 14, 2014, 4:36:38 PM (5 years ago)
Author:
campbell
Message:

Section 4.3 revised.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/fopara2013/fopara13.tex

    r3433 r3434  
    814814predict the object code behaviour. There are two cost models, one for execution
    815815time and one for stack space consumption. We show the correctness of the prediction
    816 only for those programs that do not exhaust the available machine stack space, a
     816only for those programs that do not exhaust the available stack space, a
    817817property that---thanks to the stack cost model---we can statically analyse on the
    818 source code using our Frama-C tool. The preservation of functional properties we
    819 take as an assumption, not itself formally proved in CerCo.  Other projects have
     818source code in sharp contrast to other certified compilers.  Other projects have
    820819already certified the preservation of functional semantics in similar compilers,
    821 and we have not attempted to directly repeat that work. In order to complete the
    822 proof for non-functional properties, we have introduced a new semantics for
    823 programming languages based on a new kind of structured observables with the
    824 relative notions of forward similarity and the study of the intensional
     820so we have not attempted to directly repeat that work and assume
     821functional correctness for most passes. In order to complete the
     822proof for non-functional properties, we have introduced a new,
     823structured, form of execution traces, with the
     824related notions for forward similarity and the intensional
    825825consequences of forward similarity. We have also introduced a unified
    826826representation for back-end intermediate languages that was exploited to provide
     
    829829The details on the proof techniques employed
    830830and
    831 the proof sketch can be collected from the CerCo deliverables and papers.
     831the proof sketch can be found in the CerCo deliverables and papers.
    832832In this section we will only hint at the correctness statement, which turned
    833 out to be more complex than what we expected at the beginning.
    834 
    835 \paragraph{The statement.}
     833out to be more complex than expected.
     834
     835\paragraph{The correctness statement.}
    836836Real time programs are often reactive programs that loop forever responding to
    837837events (inputs) by performing some computation followed by some action (output)
    838 and the return to the initial state. For looping programs the overall execution
    839 time does not make sense. The same happens for reactive programs that spend an
    840 unpredictable amount of time in I/O. What is interesting is the reaction time
    841 that measure the time spent between I/O events. Moreover, we are interested in
     838and continuing as before. For these programs the overall execution
     839time does not make sense. The same is true for reactive programs that spend an
     840unpredictable amount of time in I/O. Instead, what is interesting is the reaction time ---
     841 the time spent between I/O events. Moreover, we are interested in
    842842predicting and ruling out crashes due to running out of space on certain
    843843inputs.
    844 Therefore we need to look for a statement that talks about sub-runs of a
    845 program. The most natural statement is that the time predicted on the source
     844Therefore we need a statement that talks about sub-runs of a
     845program. A natural candidate is that the time predicted on the source
    846846code and spent on the object code by two corresponding sub-runs are the same.
    847 The problem to solve to make this statement formal is how to identify the
     847To make this statement formal we must identify the
    848848corresponding sub-runs and how to single out those that are meaningful.
    849 The solution we found is based on the notion of measurability. We say that a run
    850 has a \emph{measurable sub-run} when both the prefix of the sub-run and the
    851 sub-run do not exhaust the stack space, the number of function calls and returns
    852 in the sub-run is the same, the sub-run does not perform any I/O and the sub-run
     849We introduce the notion of a \emph{measurable} sub-run of a run
     850which does not exhaust the available stack before or during the
     851sub-run, the number of function calls and returns
     852in the sub-run is the same, the sub-run does not perform any I/O, and the sub-run
    853853starts with a label emission statement and ends with a return or another label
    854 emission statements. The stack usage is estimated using the stack usage model
     854emission statement. The stack usage is bounded using the stack usage model
    855855that is computed by the compiler.
    856856
    857857The statement that we formally proved is: for each C run with a measurable
    858 sub-run, there exists an object code run with a sub-run, such that the observables
    859 of the pairs of prefixes and sub-runs are the same and the time spent by the
    860 object code in the sub-run is the same as the one predicted on the source code
     858sub-run, there exists an object code run with a sub-run, with the same
     859execution trace for both the prefix of the run and the sub-run itself,
     860 and where the time spent by the
     861object code in the sub-run is the same as the time predicted on the source code
    861862using the time cost model generated by the compiler.
     863
     864
    862865We briefly discuss the constraints for measurability. Not exhausting the stack
    863 space is a clear requirement of meaningfulness of a run, because source programs
    864 do not crash for lack of space while object code ones do. The balancing of
     866space is necessary for a run to be meaningful, because the source semantics
     867has no notion of running out of memory. Balancing
    865868function calls and returns is a requirement for precision: the labelling approach
    866 allows the scope of label emission statements to extend after function calls to
    867 minimize the number of labels. Therefore a label pays for all the instructions
    868 in a block, excluding those executed in nested function calls. If the number of
     869allows the scope of a label to extend after function calls to
     870minimize the number of labels. (The scope excludes the called
     871function's execution.) If the number of
    869872calls/returns is unbalanced, it means that there is a call we have not returned
    870873to that could be followed by additional instructions whose cost has already been
    871 taken in account. To make the statement true (but less precise) in this
    872 situation, we could only say that the cost predicted on the source code is a
    873 safe bound, not that it is exact. The last condition on the entry/exit points of
    874 a run is used to identify sub-runs whose code correspond to a sequence of blocks
    875 that we can measure precisely. Any other choice would start or end the run in the
    876 middle of a block and we would be forced again to weaken the statement taking as
    877 a bound the cost obtained counting in all the instructions that precede the
    878 starting one in the block, or follow the final one in the block.
    879 I/O operations can be performed in the prefix of the run, but not in the
     874taken in account.  The last condition on the start and end points of
     875a run is also required to make the bound precise.  With these
     876restrictions and the 8051's simple timing model we obtain \emph{exact}
     877predictions.  If we relax these conditions then we obtain a corollary
     878with an upper bound on the cost.
     879Finally, I/O operations can be performed in the prefix of the run, but not in the
    880880measurable sub-run. Therefore we prove that we can predict reaction times, but
    881881not I/O times, as desired.
Note: See TracChangeset for help on using the changeset viewer.