Changeset 3125
 Timestamp:
 Apr 11, 2013, 7:10:40 PM (6 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

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