Ignore:
Timestamp:
Feb 10, 2014, 11:47:15 AM (6 years ago)
Author:
campbell
Message:

Many of the minor reviewer comments about FOPARA paper.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/fopara2013/fopara13.tex

    r3339 r3417  
    146146reduce non-functional verification to the functional case and exploit the state
    147147of the art in automated high-level verification~\cite{survey}. The techniques
    148 currently used by the Worst Case Execution Time (WCET) community, which performs its analysis on object code
    149 , are still available but can now be coupled with an additional source-level
     148currently used by the Worst Case Execution Time (WCET) community, which perform the analysis on object code,
     149are still available but can now be coupled with an additional source-level
    150150analysis. Where the approach produces precise cost models too complex to reason
    151151about, safe approximations can be used to trade complexity with precision.
     
    315315base is an off-the-shelf invariant generator which, in turn, can be proved
    316316correct using an interactive theorem prover. Therefore we achieve the double
    317 objective of allowing the use more off-the-shelf components (e.g. provers and
     317objective of allowing the use of more off-the-shelf components (e.g. provers and
    318318invariant generators) whilst reducing the trusted code base at the same time.
    319319
     
    419419\end{tabular}
    420420\caption{On the left: code to count the array's elements
    421  that are greater or equal to the treshold. On the right: CerCo's interaction
     421 that are less than or equal to the treshold. On the right: CerCo's interaction
    422422 diagram. CerCo's components are drawn solid.}
    423423\label{test1}
     
    594594% set of requirements will be added later.
    595595
    596 The third component is a static object code analyser. It takes in input a labeled
     596The third component is a static object code analyser. It takes as input a labeled
    597597object code and it computes the scope of each of its label emission statements,
    598598i.e.\ the tree of instructions that may be executed after the statement and before
     
    642642loop optimisations like peeling or unrolling are prevented. Moreover, precision
    643643of 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 to
    645 associate a precise constant cost to every instruction. This is not possible in
     644precision: we implicitly assumed that a precise constant cost can be assigned
     645to every instruction. This is not possible in
    646646the presence of stateful hardware whose state influences the cost of operations,
    647647like pipelines and caches. In the next subsection we will see an extension of the
     
    662662scopes.
    663663
    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.
    670675
    671676\subsection{Dependent labeling}
     
    710715in a simple data structure. For example, to handle simple but realistic
    711716pipelines 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
     717of bubbles (stuck instructions) in the pipeline. In any case, it is not necessary
     718for the user to understand the meaning of the state to reason over the properties
     719of the
     720program. Moreover, at any moment the user, or the invariant generator tools that
     721analyse the instrumented source code produced by the compiler, can decide to
     722trade precision of the analysis for simplicity by approximating the parametric
    717723cost with safe non parametric bounds. Interestingly, the functional analysis of
    718724the code can determine which blocks are executed more frequently in order to
     
    728734taking more time.
    729735
    730 By introducing a variable that keep tracks of the iteration number, we can
     736By introducing a variable that keeps track of the iteration number, we can
    731737associate to the label a cost that is a function of the iteration number. The
    732738same technique works for loop unrolling without modifications: the function will
     
    742748We review the cost synthesis techniques developed in the project.
    743749The starting hypothesis is that we have a certified methodology to annotate
    744 blocks in the source code with constants which provide a sound and possibly
     750blocks in the source code with constants which provide a sound and sufficiently
    745751precise upper bound on the cost of executing the blocks after compilation to
    746752object code.
     
    772778We developed the CerCo Cost plugin for the Frama-C platform as a proof of
    773779concept of an automatic environment exploiting the cost annotations produced by
    774 the CerCo compiler. It consists of an OCaml program which in first approximation
     780the CerCo compiler. It consists of an OCaml program which essentially
    775781takes the following actions: 1) it receives as input a C program, 2) it
    776782applies the CerCo compiler to produce a related C program with cost annotations,
     
    799805analysis of the VCs associated with branching may lead to a complexity blow up.
    800806\paragraph{Experience with Lustre.} Lustre is a data-flow language for programming
    801 synchronous systems, with the language coming with a compiler to C. We designed a
     807synchronous systems, with a compiler which targets C. We designed a
    802808wrapper for supporting Lustre files.
    803809The C function produced by the compiler implements the step function of the
     
    907913compilation and external calls. Adding them is a transparent
    908914process to the labeling approach and should create no unknown problem.
    909 \item We target an 8-bit processor. Targeting an 8-bit processor requires
     915\item We target an 8-bit processor, in contrast to CompCert's 32-bit targets. Targeting an 8-bit processor requires
    910916several changes and increased code size, but it is not fundamentally more
    911917complex. The proof of correctness, however, becomes much harder.
     
    968974that is computed by the compiler.
    969975
    970 The statement that we formally proved is that for each C run with a measurable
    971 sub-run there exists an object code run with a sub-run such that the observables
     976The statement that we formally proved is: for each C run with a measurable
     977sub-run, there exists an object code run with a sub-run, such that the observables
    972978of the pairs of prefixes and sub-runs are the same and the time spent by the
    973979object code in the sub-run is the same as the one predicted on the source code
     
    9941000not I/O times, as it should be.
    9951001
    996 \section{Future work}
     1002\section{Conclusions and future work}
    9971003
    9981004All 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.