Changeset 3209

Apr 29, 2013, 4:52:23 PM (8 years ago)

Final version up to spelling.

1 edited


  • Deliverables/D6.3/report.tex

    r3152 r3209  
    123 xxx
     123We review the techniques experimented in CerCo for cost annotation exploitement
     124at the user level. We also report on recent work towards precise time analysis
     125at the source level for modern hardware architectures whose instructions cost
     126is a function of the internal hardware state (pipelines, caches, branch
     127prediction units, etc.).
     446\section{Middle and Long Term Improvements}
     447The future improvements that will affect the user experience falls into two
     450 \item \textbf{Improvements to invariant generators}
     451   The invariant generator that we implemented in the plug-in allows to
     452   compute the parametric worst case execution time for all Lustre programs
     453   and for almost all the C tests that we targeted. Nevertheless, at the
     454   moment the generator does not degrage gracefully: if the source code does
     455   not respects the syntactic requirements of the generator, no cost invariants
     456   are generated at all. This behaviour is consistent with the traditional
     457   use in proving functional properties, but for non functional ones we
     458   are interested in always providing a worst case bound, possibly by dropping
     459   the dependencies and computing a very rough one. That is the behaviour of
     460   standard WCET analyzers (that, most of the time, are not parametric anyway).
     462   Other future improvements consist in enlarging the class of recognized
     463   program shapes by integrating more advanced techniques or interacting with
     464   existing tools.
     466   Both kind of improvements can be performed in the middle term.
     467 \item \textbf{Improvements to cost annotation exploitement}
     468   One benefit of CerCo w.r.t. traditional WCET is that the user does not need
     469   to trust the bound provided by the tool, but it can at least partially
     470   verify it manually or using automated techniques.
     472   The combinations of techniques described in the previous section allowed
     473   to automatically certify the parametric worst case execution time for all
     474   Lustre programs and for the majority of simple C tests we had at our
     475   disposal. Nevertheless, we expect automation to fail more frequently on
     476   real world, industrial examples. In the middle term we should experiment
     477   with more complex code and enlarge the set of techniques according to the
     478   observed results. In particular, we should implement at the source level
     479   at least all those that are used on the object code in standard WCET tools.
     480   It may well be the case that we identify a set of recurrent proof obligations
     481   that are not solved by the existing theorem provers, but that admit a
     482   solution by means of a uniform strategy. In any case, the failure to
     483   automatically prove sound a cost invariant does not invalidate the invariant
     484   itself, assuming that the invariant generator is correct.
     485 \item \textbf{Applications to time analysis for modern hardware}
     486   At the moment, the main drawback of the CerCo Prototype is that it cannot be
     487   ported to modern architectures whose instruction cost depend on the internal
     488   state of hardware components like pipelines, caches or branch predictors.
     489   The major long term improvement to the CerCo Prototype will be the study
     490   of how to accomodate in the labelling approach these kind of cost models.
     491   We attach to this document the techinical report ``\emph{Dependent labelling
     492   applied to stateful hardware components}'' which describes what seems to
     493   be at the moment the most promising approach to the problem. Unsurprisingly,
     494   the solution uses dependent labels, that allow to associate a different cost
     495   to multiple executions of the same block. Dependent labels were developed
     496   in CerCo to allow loop optimizations, where the dependency was over the
     497   number of iterations of the loops. In the case of modern hardware, the
     498   dependency is on approximations of the internal hardware state, that needs
     499   to be made manifest in the source code too.
     501   The strategy described in the technical report is assumed to work on
     502   pipelines, while additional research is expected for caches. Moreover, in
     503   the middle term we need to be implement the solution for pipelines to be
     504   able to perform experiments. In particular, we need to understand the
     505   behaviour on automated provers on the more complex generated cost invariants,
     506   and we need to understand to which extent the cost invariants can work with
     507   the more precise cost models before introducing severe approximations.
Note: See TracChangeset for help on using the changeset viewer.