Changeset 3436
- Timestamp:
- Feb 14, 2014, 7:21:57 PM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Papers/fopara2013/fopara13.tex
r3435 r3436 959 959 \label{sec:exploit} 960 960 We now turn our attention to synthesising high-level costs, such as 961 the execution time of a whole program. We consider as our starting point source level costs961 the reaction time of a real-time program. We consider as our starting point source level costs 962 962 provided by basic labelling, in other words annotations 963 963 on the source code which are constants that provide a sound and sufficiently … … 966 966 967 967 The principle that we have followed in designing the cost synthesis tools is 968 that the synthe ticbounds should be expressed and proved within a general968 that the synthesised bounds should be expressed and proved within a general 969 969 purpose tool built to reason on the source code. In particular, we rely on the 970 970 Frama-C tool to reason on C code and on the Coq proof-assistant to reason on 971 971 higher-order functional programs. 972 973 This principle entails that: 1) 974 The inferred synthetic bounds are indeed correct as long as the general purpose 975 tool is; 2) there is no limitation on the class of programs that can be handled 976 as long as the user is willing to carry on an interactive proof. 972 This principle entails that 973 the inferred synthetic bounds are indeed correct as long as the general purpose 974 tool is, and that there is no limitation on the class of programs that can be handled, 975 for example by resorting to interactive proof. 977 976 978 977 Of course, automation is desirable whenever possible. Within this framework, … … 992 991 concept of an automatic environment exploiting the cost annotations produced by 993 992 the CerCo compiler. It consists of an OCaml program which essentially 994 takes the following actions: 1) it receives as input a C program, 2) it 995 applies the CerCo compiler to produce a related C program with cost annotations, 996 3) it applies some heuristics to produce a tentative bound on the cost of 993 uses the CerCo compiler to produce a related C program with cost annotations, 994 and applies some heuristics to produce a tentative bound on the cost of 997 995 executing the C functions of the program as a function of the value of their 998 parameters , 4) the user can then call the Jessie plugin to discharge the996 parameters. The user can then call the Jessie plugin to discharge the 999 997 related proof obligations. 1000 998 In the following we elaborate on the soundness of the framework and the 1001 experiments we performed with the Cost tool on the C programsproduced by a999 experiments we performed with the Cost tool on C programs, including some produced by a 1002 1000 Lustre compiler. 1003 1001 1004 1002 \paragraph{Soundness.} The soundness of the whole framework depends on the cost 1005 annotations added by the CerCo compiler, the synthetic costs produced by the1006 cost plugin,the verification conditions (VCs) generated by Jessie, and the1007 external provers discharging the VCs. The synthetic costs being in ACSL format,1008 Jessie can be used to verify them. Thus, even if the added synthetic costs are1003 annotations added by the CerCo compiler, 1004 the verification conditions (VCs) generated by Jessie, and the 1005 external provers discharging the VCs. Jessie can be used to verify the 1006 synthesised bounds because our plugin generates them in ACSL format. Thus, even if the added synthetic costs are 1009 1007 incorrect (relatively to the cost annotations), the process as a whole is still 1010 1008 correct: indeed, Jessie will not validate incorrect costs and no conclusion can 1011 1009 be made about the WCET of the program in this case. In other terms, the 1012 soundness does not really depend on the action ofthe cost plugin, which can in1010 soundness does not depend on the cost plugin, which can in 1013 1011 principle produce any synthetic cost. However, in order to be able to actually 1014 1012 prove a WCET of a C function, we need to add correct annotations in a way that … … 1017 1015 composed of branching and assignments (no loops and no recursion) because a fine 1018 1016 analysis of the VCs associated with branching may lead to a complexity blow up. 1017 1019 1018 \paragraph{Experience with Lustre.} Lustre is a data-flow language for programming 1020 1019 synchronous systems, with a compiler which targets C. We designed a 1021 1020 wrapper for supporting Lustre files. 1022 The C function produced by the compiler implements the step function of the 1023 synchronous system and computing the WCET of the function amounts to obtain a 1021 The C function produced by the compiler is relatively simple loop-free 1022 code which implements the step function of the 1023 synchronous system and computing the WCET of the function amounts to obtaining a 1024 1024 bound on the reaction time of the system. We tested the Cost plugin and the 1025 1025 Lustre wrapper on the C programs generated by the Lustre compiler. For programs … … 1035 1035 that update the cost variable and establish the number of times they are passed 1036 1036 through during the flow of execution. To perform the analysis the plugin 1037 makes the following assumptions on the programs: 1038 1) there are no recursive functions; 1039 2) every loop must be annotated with a variant. The variants of `for' loops are 1040 automatically inferred. 1041 1042 The plugin proceeds as follows. 1043 First the call graph of the program is computed. 1044 Then the computation of the cost of the function is performed by traversing its 1045 control flow graph. If the function $f$ calls the function $g$ 1046 then the function $g$ 1047 is processed before the function $f$. The cost at a node is the maximum of the 1037 assumes that there are no recursive functions in the program, and that 1038 every loop is annotated with a variant. In the case of `for' loops the 1039 variants are automatically inferred where a loop counter can be 1040 syntactically detected. 1041 1042 The plugin computes a call-graph and proceeds to calculate bounds for 1043 each function from the leaves up to the main function. 1044 The computation of the cost of each function is performed by traversing its 1045 control flow graph, where the cost of a node is the maximum of the 1048 1046 costs of the successors. 1049 1047 In the case of a loop with a body that has a constant cost for every step of the … … 1058 1056 The cost of the function is directly added as post-condition of the function. 1059 1057 1060 The user can influence the annotation by two different means: 1061 1) by using more precise variants; 1062 2) by annotating functions with cost specifications. The plugin will use this cost 1063 for the function instead of computing it. 1058 The user can also specify more precise variants and annotate functions 1059 with their own cost specifications. The plugin will use these 1060 instead of computing its own, allowing greater precision and the 1061 ability to analyse programs which the variant generator does not 1062 support. 1063 1064 In addition to the loop-free Lustre code, this method was successfully 1065 applied to a small range of cryptographic code. See~\cite{labelling} for more details. 1066 1064 1067 \paragraph{C programs with pointers.} 1065 1068 When it comes to verifying programs involving pointer-based data structures,
Note: See TracChangeset
for help on using the changeset viewer.