Changeset 3417
- Timestamp:
- Feb 10, 2014, 11:47:15 AM (7 years ago)
- Location:
- Papers/fopara2013
- Files:
-
- 1 added
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Papers/fopara2013/fopara13.tex
r3339 r3417 146 146 reduce non-functional verification to the functional case and exploit the state 147 147 of the art in automated high-level verification~\cite{survey}. The techniques 148 currently used by the Worst Case Execution Time (WCET) community, which perform s its analysis on object code149 ,are still available but can now be coupled with an additional source-level148 currently used by the Worst Case Execution Time (WCET) community, which perform the analysis on object code, 149 are still available but can now be coupled with an additional source-level 150 150 analysis. Where the approach produces precise cost models too complex to reason 151 151 about, safe approximations can be used to trade complexity with precision. … … 315 315 base is an off-the-shelf invariant generator which, in turn, can be proved 316 316 correct using an interactive theorem prover. Therefore we achieve the double 317 objective of allowing the use more off-the-shelf components (e.g. provers and317 objective of allowing the use of more off-the-shelf components (e.g. provers and 318 318 invariant generators) whilst reducing the trusted code base at the same time. 319 319 … … 419 419 \end{tabular} 420 420 \caption{On the left: code to count the array's elements 421 that are greateror equal to the treshold. On the right: CerCo's interaction421 that are less than or equal to the treshold. On the right: CerCo's interaction 422 422 diagram. CerCo's components are drawn solid.} 423 423 \label{test1} … … 594 594 % set of requirements will be added later. 595 595 596 The third component is a static object code analyser. It takes ininput a labeled596 The third component is a static object code analyser. It takes as input a labeled 597 597 object code and it computes the scope of each of its label emission statements, 598 598 i.e.\ the tree of instructions that may be executed after the statement and before … … 642 642 loop optimisations like peeling or unrolling are prevented. Moreover, precision 643 643 of the object code labeling is not sufficient \emph{per se} to obtain global 644 precision: we also implicitly assumed the static analysis to be able to645 associate a precise constant costto every instruction. This is not possible in644 precision: we implicitly assumed that a precise constant cost can be assigned 645 to every instruction. This is not possible in 646 646 the presence of stateful hardware whose state influences the cost of operations, 647 647 like pipelines and caches. In the next subsection we will see an extension of the … … 662 662 scopes. 663 663 664 Phases 1, 2 and 3 can be applied as well to logic languages (e.g. Prolog). 665 However, the instrumentation phase cannot: in standard Prolog there is no notion 666 of (global) variable whose state is not retracted during backtracking. 667 Therefore, the cost of executing computations that are later backtracked would 668 not be correctly counted in. Any extension of logic languages with 669 non-backtrackable state could support our labeling approach. 664 % Brian: one of the reviewers pointed out that standard Prolog implementations 665 % do have some global state that apparently survives backtracking and might be 666 % used. As we haven't experimented with this, I think it's best to elide it 667 % entirely. 668 669 % Phases 1, 2 and 3 can be applied as well to logic languages (e.g. Prolog). 670 % However, the instrumentation phase cannot: in standard Prolog there is no notion 671 % of (global) variable whose state is not retracted during backtracking. 672 % Therefore, the cost of executing computations that are later backtracked would 673 % not be correctly counted in. Any extension of logic languages with 674 % non-backtrackable state could support our labeling approach. 670 675 671 676 \subsection{Dependent labeling} … … 710 715 in a simple data structure. For example, to handle simple but realistic 711 716 pipelines it is sufficient to remember a short integer that encodes the position 712 of bubbles (stuck instructions) in the pipeline. In any case, the user does not 713 need to understand the meaning of the state to reason over the properties of the 714 program. Moreover, at any moment the user or the invariant generator tools that 715 analyse the instrumented source code produced by the compiler can decide to 716 trade precision of the analysis with simplicity by approximating the parametric 717 of bubbles (stuck instructions) in the pipeline. In any case, it is not necessary 718 for the user to understand the meaning of the state to reason over the properties 719 of the 720 program. Moreover, at any moment the user, or the invariant generator tools that 721 analyse the instrumented source code produced by the compiler, can decide to 722 trade precision of the analysis for simplicity by approximating the parametric 717 723 cost with safe non parametric bounds. Interestingly, the functional analysis of 718 724 the code can determine which blocks are executed more frequently in order to … … 728 734 taking more time. 729 735 730 By introducing a variable that keep tracksof the iteration number, we can736 By introducing a variable that keeps track of the iteration number, we can 731 737 associate to the label a cost that is a function of the iteration number. The 732 738 same technique works for loop unrolling without modifications: the function will … … 742 748 We review the cost synthesis techniques developed in the project. 743 749 The starting hypothesis is that we have a certified methodology to annotate 744 blocks in the source code with constants which provide a sound and possibly750 blocks in the source code with constants which provide a sound and sufficiently 745 751 precise upper bound on the cost of executing the blocks after compilation to 746 752 object code. … … 772 778 We developed the CerCo Cost plugin for the Frama-C platform as a proof of 773 779 concept of an automatic environment exploiting the cost annotations produced by 774 the CerCo compiler. It consists of an OCaml program which in first approximation780 the CerCo compiler. It consists of an OCaml program which essentially 775 781 takes the following actions: 1) it receives as input a C program, 2) it 776 782 applies the CerCo compiler to produce a related C program with cost annotations, … … 799 805 analysis of the VCs associated with branching may lead to a complexity blow up. 800 806 \paragraph{Experience with Lustre.} Lustre is a data-flow language for programming 801 synchronous systems, with the language coming with a compiler toC. We designed a807 synchronous systems, with a compiler which targets C. We designed a 802 808 wrapper for supporting Lustre files. 803 809 The C function produced by the compiler implements the step function of the … … 907 913 compilation and external calls. Adding them is a transparent 908 914 process to the labeling approach and should create no unknown problem. 909 \item We target an 8-bit processor . Targeting an 8-bit processor requires915 \item We target an 8-bit processor, in contrast to CompCert's 32-bit targets. Targeting an 8-bit processor requires 910 916 several changes and increased code size, but it is not fundamentally more 911 917 complex. The proof of correctness, however, becomes much harder. … … 968 974 that is computed by the compiler. 969 975 970 The statement that we formally proved is thatfor each C run with a measurable971 sub-run there exists an object code run with a sub-runsuch that the observables976 The statement that we formally proved is: for each C run with a measurable 977 sub-run, there exists an object code run with a sub-run, such that the observables 972 978 of the pairs of prefixes and sub-runs are the same and the time spent by the 973 979 object code in the sub-run is the same as the one predicted on the source code … … 994 1000 not I/O times, as it should be. 995 1001 996 \section{ Future work}1002 \section{Conclusions and future work} 997 1003 998 1004 All the CerCo software and deliverables can be found on the CerCo homepage at~\url{http://cerco.cs.unibo.it}.
Note: See TracChangeset
for help on using the changeset viewer.