Changeset 3322


Ignore:
Timestamp:
Jun 6, 2013, 12:19:29 PM (4 years ago)
Author:
sacerdot
Message:

Down to 17 pages, ugh.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/fopara2013/fopara13.tex

    r3321 r3322  
    415415
    416416\paragraph{The statement}
    417 The most natural statement of correctness for our complexity preserving compiler is that the time spent for execution by a terminating object code program should be the time predicted on the source code by adding up the cost of every label emission statement. This statement, however, is too naïve to be useful for real world real time programs like those used in embedded systems.
    418417Real time programs are often reactive programs that loop forever responding to events (inputs) by performing some computation followed by some action (output) and the return to the initial state. For looping programs the overall execution time does not make sense. The same happens for reactive programs that spend an unpredictable amount of time in I/O. What is interesting is the reaction time that measure the time spent between I/O events. Moreover, we are interested in predicting and ruling out programs that crash running out of space on a certain input.
    419 Therefore we need to look for a more complex statement that talks about sub-runs of a program. The most natural statement is that the time predicted on the source code and spent on the object code by two corresponding sub-runs are the same. The problem to solve to make this statement formal is how to identify the corresponding sub-runs and how to single out those that are meaningful.
    420 The solution we found is based on the notion of measurability. We say that a run has a measurable sub-run when both the prefix of the sub-run and the sub-run do not exhaust the stack space, the number of function calls and returns in the sub-run is the same, the sub-run does not perform any I/O and the sub-run starts with a label emission statement and ends with a return or another label emission statements. The stack usage is estimated using the stack usage model that is computed by the compiler.
    421 
    422 The statement that we want to formally prove is that for each C run with a measurable sub-run there exists an object code run with a sub-run such that the observables of the pairs of prefixes and sub-runs are the same and the time spent by the object code in the sub-run is the same as the one predicted on the source code using the time cost model generated by the compiler.
     418Therefore we need to look for a statement that talks about sub-runs of a program. The most natural statement is that the time predicted on the source code and spent on the object code by two corresponding sub-runs are the same. The problem to solve to make this statement formal is how to identify the corresponding sub-runs and how to single out those that are meaningful.
     419The solution we found is based on the notion of measurability. We say that a run has a \emph{measurable sub-run} when both the prefix of the sub-run and the sub-run do not exhaust the stack space, the number of function calls and returns in the sub-run is the same, the sub-run does not perform any I/O and the sub-run starts with a label emission statement and ends with a return or another label emission statements. The stack usage is estimated using the stack usage model that is computed by the compiler.
     420
     421The statement that we formally proved is that for each C run with a measurable sub-run there exists an object code run with a sub-run such that the observables of the pairs of prefixes and sub-runs are the same and the time spent by the object code in the sub-run is the same as the one predicted on the source code using the time cost model generated by the compiler.
    423422We briefly discuss the constraints for measurability. Not exhausting the stack space is a clear requirement of meaningfulness of a run, because source programs do not crash for lack of space while object code ones do. The balancing of function calls/returns is a requirement for precision: the labelling approach allows the scope of label emission statements to extend after function calls to minimize the number of labels. Therefore a label pays for all the instructions in a block, excluding those executed in nested function calls. If the number of calls/returns is unbalanced, it means that there is a call we have not returned to that could be followed by additional instructions whose cost has already been taken in account. To make the statement true (but less precise) in this situation, we could only say that the cost predicted on the source code is a safe bound, not that it is exact. The last condition on the entry/exit points of a run is used to identify sub-runs whose code correspond to a sequence of blocks that we can measure precisely. Any other choice would start/end the run in the middle of a block and we would be forced again to weaken the statement taking as a bound the cost obtained counting in all the instructions that precede the starting one in the block/follow the final one in the block.
    424423I/O operations can be performed in the prefix of the run, but not in the measurable sub-run. Therefore we prove that we can predict reaction times, but not I/O times, as it should be.
     
    426425\section{Future work}
    427426
    428 All the software described in this paper can be found on-line at the
    429 address \url{http://cerco.cs.unibo.it}. The technical deliverables of the
    430 project are also available at the same address.
     427All the CerCo software and deliverables can be found on-line at the
     428address \url{http://cerco.cs.unibo.it}.
    431429
    432430The results obtained so far are encouraging and provide evidence that
     
    438436considered by us so far.
    439437
    440 In order to prove our claim that compilers can keep track of optimizations
     438To prove that compilers can keep track of optimizations
    441439and induce a precise cost model on the source code, we targeted a simple
    442440architecture that admits a cost model that is execution history independent.
    443 The most important future work is dealing with modern hardware architectures
     441The most important future work is dealing with hardware architectures
    444442characterized by history dependent stateful components, like caches and
    445443pipelines. The main issue consists in assigning a parametric, dependent cost
Note: See TracChangeset for help on using the changeset viewer.