Changeset 3125

Apr 11, 2013, 7:10:40 PM (4 years ago)


1 edited


  • Deliverables/D6.3/report.tex

    r3124 r3125  
     891At the current state of the art functional properties of programs are better
     892proved high level languages, but the non functional ones are proved on the
     893corresponding object code. The non functional analysis, however, depends on
     894functional invariants, e.g. to bound or correlate the number of executions of
     897The aim of the CerCo project is to reconcile the two analysis by performing
     898non functional analysis on the source code. This requires computing a cost
     899model on the object code and reflecting the cost model on the source code.
     900We achieve this in CerCo by designing a certified Cost Annotating Compiler that
     901keeps tracks of transformations of basic blocks, in order to create a
     902correspondence (not necessaritly bijection) between the basic blocks of the
     903source and target language. We then prove that the sequence of basic blocks
     904that are met in the source and target executions is correlated. Then,
     905we perform a static analysis of the cost of basic blocks on the target language
     906and we use it to compute the cost model for the source language basic blocks.
     907Finally, we compute cost invariants on the source code from the inferred cost
     908model and from the functional program invariants; we generate proof obligations
     909for the invariants; we use automatic provers to try to close the proof
     912The cost of single instructions on modern architectures depend on the internal
     913state of various hardware components (pipelines, caches, branch predicting
     914units, etc.). The internal states are determined by the previous execution
     915history. Therefore the cost of basic blocks is parametric on the execution
     916history, which means both the instructions executed and the data manipulated
     917by the instructions. The CerCo approach is able to correlate the sequence
     918of blocks of source instructions with the sequence of blocks of target
     919instructions. It does not correlate the high level and the low level data.
     920Therefore we are not able in the general case to lift a cost model parametric
     921on the execution history on the source code.
     923To overcome the problem, we have identified a particular class of cost models
     924that are not dependent on the data manipulated. We argue that the CerCo
     925approach can cover this scenario by exposing in the source program a finite
     926data type of views over internal machine states. The costs of basic blocks
     927is parametric on these views, and the current view is updated at basic block
     928entry according to some abstraction of the machine hardware that does not
     929need to be understood. Further studies are needed to understand how invariant
     930generators and automatic provers can cope with these updates and parametric
     933We have argued how pipelines, at least simple ones, are captured by the
     934previous scenario and can in principle be manipulated using CerCo tools.
     935The same is not true for caches, whose behaviour deeply depends on the
     936data manipulated. By embracing the PROARTIS proposal of turning caches into
     937probabilistic components, we can break the data dependency. Nevertheless,
     938cache analysis remains more problematic because of the size of the views.
     939Further studies need to be focused on caches to understand if the problem of
     940size of the views can be tamed in practice without ruining the whole approach.
Note: See TracChangeset for help on using the changeset viewer.