Changeset 3436


Ignore:
Timestamp:
Feb 14, 2014, 7:21:57 PM (5 years ago)
Author:
campbell
Message:

Section 4.5 revisions.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/fopara2013/fopara13.tex

    r3435 r3436  
    959959\label{sec:exploit}
    960960We 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 costs
     961the reaction time of a real-time program.  We consider as our starting point source level costs
    962962provided by basic labelling, in other words annotations
    963963on the source code which are constants that provide a sound and sufficiently
     
    966966
    967967The principle that we have followed in designing the cost synthesis tools is
    968 that the synthetic bounds should be expressed and proved within a general
     968that the synthesised bounds should be expressed and proved within a general
    969969purpose tool built to reason on the source code. In particular, we rely on the
    970970Frama-C tool to reason on C code and on the Coq proof-assistant to reason on
    971971higher-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.
     972This principle entails that
     973the inferred synthetic bounds are indeed correct as long as the general purpose
     974tool is, and that there is no limitation on the class of programs that can be handled,
     975for example by resorting to interactive proof.
    977976
    978977Of course, automation is desirable whenever possible. Within this framework,
     
    992991concept of an automatic environment exploiting the cost annotations produced by
    993992the 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
     993uses the CerCo compiler to produce a related C program with cost annotations,
     994and applies some heuristics to produce a tentative bound on the cost of
    997995executing 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 the
     996parameters. The user can then call the Jessie plugin to discharge the
    999997related proof obligations.
    1000998In the following we elaborate on the soundness of the framework and the
    1001 experiments we performed with the Cost tool on the C programs produced by a
     999experiments we performed with the Cost tool on C programs, including some produced by a
    10021000Lustre compiler.
    10031001
    10041002\paragraph{Soundness.} The soundness of the whole framework depends on the cost
    1005 annotations added by the CerCo compiler, the synthetic costs produced by the
    1006 cost plugin, the verification conditions (VCs) generated by Jessie, and the
    1007 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 are
     1003annotations added by the CerCo compiler,
     1004the verification conditions (VCs) generated by Jessie, and the
     1005external provers discharging the VCs. Jessie can be used to verify the
     1006synthesised bounds because our plugin generates them in ACSL format. Thus, even if the added synthetic costs are
    10091007incorrect (relatively to the cost annotations), the process as a whole is still
    10101008correct: indeed, Jessie will not validate incorrect costs and no conclusion can
    10111009be made about the WCET of the program in this case. In other terms, the
    1012 soundness does not really depend on the action of the cost plugin, which can in
     1010soundness does not depend on the cost plugin, which can in
    10131011principle produce any synthetic cost. However, in order to be able to actually
    10141012prove a WCET of a C function, we need to add correct annotations in a way that
     
    10171015composed of branching and assignments (no loops and no recursion) because a fine
    10181016analysis of the VCs associated with branching may lead to a complexity blow up.
     1017
    10191018\paragraph{Experience with Lustre.} Lustre is a data-flow language for programming
    10201019synchronous systems, with a compiler which targets C. We designed a
    10211020wrapper 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
     1021The C function produced by the compiler is relatively simple loop-free
     1022code which implements the step function of the
     1023synchronous system and computing the WCET of the function amounts to obtaining a
    10241024bound on the reaction time of the system. We tested the Cost plugin and the
    10251025Lustre wrapper on the C programs generated by the Lustre compiler. For programs
     
    10351035that update the cost variable and establish the number of times they are passed
    10361036through 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
     1037assumes that there are no recursive functions in the program, and that
     1038every loop is annotated with a variant. In the case of `for' loops the
     1039variants are automatically inferred where a loop counter can be
     1040syntactically detected.
     1041
     1042The plugin computes a call-graph and proceeds to calculate bounds for
     1043each function from the leaves up to the main function.
     1044The computation of the cost of each function is performed by traversing its
     1045control flow graph, where the cost of a node is the maximum of the
    10481046costs of the successors.
    10491047In the case of a loop with a body that has a constant cost for every step of the
     
    10581056The cost of the function is directly added as post-condition of the function.
    10591057
    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.
     1058The user can also specify more precise variants and annotate functions
     1059with their own cost specifications. The plugin will use these
     1060instead of computing its own, allowing greater precision and the
     1061ability to analyse programs which the variant generator does not
     1062support.
     1063
     1064In addition to the loop-free Lustre code, this method was successfully
     1065applied to a small range of cryptographic code.  See~\cite{labelling} for more details.
     1066
    10641067\paragraph{C programs with pointers.}
    10651068When it comes to verifying programs involving pointer-based data structures,
Note: See TracChangeset for help on using the changeset viewer.