Changeset 3436

Timestamp:

Feb 14, 2014, 7:21:57 PM (6 years ago)

Author:

campbell

Message:

Section 4.5 revisions.

File:

• Papers/fopara2013/fopara13.tex (modified) (6 diffs)

Papers/fopara2013/fopara13.tex

@@ -959 +959 @@
 \label{sec:exploit}
 We now turn our attention to synthesising high-level costs, such as
-the execution time of a whole program.  We consider as our starting point source level costs
+the reaction time of a real-time program.  We consider as our starting point source level costs
 provided by basic labelling, in other words annotations 
 on the source code which are constants that provide a sound and sufficiently
@@ -966 +966 @@
 
 The principle that we have followed in designing the cost synthesis tools is 
-that the synthetic bounds should be expressed and proved within a general 
+that the synthesised bounds should be expressed and proved within a general 
 purpose tool built to reason on the source code. In particular, we rely on the 
 Frama-C tool to reason on C code and on the Coq proof-assistant to reason on 
 higher-order functional programs.
-
-This principle entails that: 1)
-The inferred synthetic bounds are indeed correct as long as the general purpose 
-tool is; 2) there is no limitation on the class of programs that can be handled 
-as long as the user is willing to carry on an interactive proof.
+This principle entails that
+the inferred synthetic bounds are indeed correct as long as the general purpose 
+tool is, and that there is no limitation on the class of programs that can be handled,
+for example by resorting to interactive proof.
 
 Of course, automation is desirable whenever possible. Within this framework, 
@@ -992 +991 @@
 concept of an automatic environment exploiting the cost annotations produced by 
 the CerCo compiler. It consists of an OCaml program which essentially
-takes the following actions: 1) it receives as input a C program, 2) it 
-applies the CerCo compiler to produce a related C program with cost annotations, 
-3) it applies some heuristics to produce a tentative bound on the cost of 
+uses the CerCo compiler to produce a related C program with cost annotations, 
+and applies some heuristics to produce a tentative bound on the cost of 
 executing the C functions of the program as a function of the value of their 
-parameters, 4) the user can then call the Jessie plugin to discharge the 
+parameters. The user can then call the Jessie plugin to discharge the 
 related proof obligations.
 In the following we elaborate on the soundness of the framework and the 
-experiments we performed with the Cost tool on the C programs produced by a 
+experiments we performed with the Cost tool on C programs, including some produced by a 
 Lustre compiler.
 
 \paragraph{Soundness.} The soundness of the whole framework depends on the cost 
-annotations added by the CerCo compiler, the synthetic costs produced by the 
-cost plugin, the verification conditions (VCs) generated by Jessie, and the 
-external provers discharging the VCs. The synthetic costs being in ACSL format, 
-Jessie can be used to verify them. Thus, even if the added synthetic costs are 
+annotations added by the CerCo compiler,
+the verification conditions (VCs) generated by Jessie, and the 
+external provers discharging the VCs. Jessie can be used to verify the
+synthesised bounds because our plugin generates them in ACSL format. Thus, even if the added synthetic costs are 
 incorrect (relatively to the cost annotations), the process as a whole is still 
 correct: indeed, Jessie will not validate incorrect costs and no conclusion can 
 be made about the WCET of the program in this case. In other terms, the 
-soundness does not really depend on the action of the cost plugin, which can in 
+soundness does not depend on the cost plugin, which can in 
 principle produce any synthetic cost. However, in order to be able to actually 
 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 
 analysis of the VCs associated with branching may lead to a complexity blow up.
+
 \paragraph{Experience with Lustre.} Lustre is a data-flow language for programming
 synchronous systems, with a compiler which targets C. We designed a 
 wrapper for supporting Lustre files.
-The C function produced by the compiler implements the step function of the 
-synchronous system and computing the WCET of the function amounts to obtain a 
+The C function produced by the compiler is relatively simple loop-free
+code which implements the step function of the 
+synchronous system and computing the WCET of the function amounts to obtaining a 
 bound on the reaction time of the system. We tested the Cost plugin and the 
 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 
 through during the flow of execution. To perform the analysis the plugin 
-makes the following assumptions on the programs:
-1) there are no recursive functions;
-2) every loop must be annotated with a variant. The variants of `for' loops are 
-automatically inferred.
-
-The plugin proceeds as follows.
-First the call graph of the program is computed.
-Then the computation of the cost of the function is performed by traversing its 
-control flow graph. If the function $f$ calls the function $g$ 
-then the function $g$ 
-is processed before the function $f$. The cost at a node is the maximum of the 
+assumes that there are no recursive functions in the program, and that
+every loop is annotated with a variant. In the case of `for' loops the
+variants are automatically inferred where a loop counter can be
+syntactically detected.
+
+The plugin computes a call-graph and proceeds to calculate bounds for
+each function from the leaves up to the main function.
+The computation of the cost of each function is performed by traversing its 
+control flow graph, where the cost of a node is the maximum of the 
 costs of the successors.
 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.
 
-The user can influence the annotation by two different means:
-1) by using more precise variants;
-2) by annotating functions with cost specifications. The plugin will use this cost 
-for the function instead of computing it.
+The user can also specify more precise variants and annotate functions
+with their own cost specifications. The plugin will use these
+instead of computing its own, allowing greater precision and the
+ability to analyse programs which the variant generator does not
+support.
+
+In addition to the loop-free Lustre code, this method was successfully
+applied to a small range of cryptographic code.  See~\cite{labelling} for more details.
+
 \paragraph{C programs with pointers.}
 When it comes to verifying programs involving pointer-based data structures,