# Changeset 3209

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

Final version up to spelling.

File:
1 edited

### Legend:

Unmodified
 r3152 \vspace*{7cm} \paragraph{Abstract} xxx We review the techniques experimented in CerCo for cost annotation exploitement at the user level. We also report on recent work towards precise time analysis at the source level for modern hardware architectures whose instructions cost is a function of the internal hardware state (pipelines, caches, branch prediction units, etc.). \newpage \section{Middle and Long Term Improvements} The future improvements that will affect the user experience falls into two categories: \begin{enumerate} \item \textbf{Improvements to invariant generators} The invariant generator that we implemented in the plug-in allows to compute the parametric worst case execution time for all Lustre programs and for almost all the C tests that we targeted. Nevertheless, at the moment the generator does not degrage gracefully: if the source code does not respects the syntactic requirements of the generator, no cost invariants are generated at all. This behaviour is consistent with the traditional use in proving functional properties, but for non functional ones we are interested in always providing a worst case bound, possibly by dropping the dependencies and computing a very rough one. That is the behaviour of standard WCET analyzers (that, most of the time, are not parametric anyway). Other future improvements consist in enlarging the class of recognized program shapes by integrating more advanced techniques or interacting with existing tools. Both kind of improvements can be performed in the middle term. \item \textbf{Improvements to cost annotation exploitement} One benefit of CerCo w.r.t. traditional WCET is that the user does not need to trust the bound provided by the tool, but it can at least partially verify it manually or using automated techniques. The combinations of techniques described in the previous section allowed to automatically certify the parametric worst case execution time for all Lustre programs and for the majority of simple C tests we had at our disposal. Nevertheless, we expect automation to fail more frequently on real world, industrial examples. In the middle term we should experiment with more complex code and enlarge the set of techniques according to the observed results. In particular, we should implement at the source level at least all those that are used on the object code in standard WCET tools. It may well be the case that we identify a set of recurrent proof obligations that are not solved by the existing theorem provers, but that admit a solution by means of a uniform strategy. In any case, the failure to automatically prove sound a cost invariant does not invalidate the invariant itself, assuming that the invariant generator is correct. \item \textbf{Applications to time analysis for modern hardware} At the moment, the main drawback of the CerCo Prototype is that it cannot be ported to modern architectures whose instruction cost depend on the internal state of hardware components like pipelines, caches or branch predictors. The major long term improvement to the CerCo Prototype will be the study of how to accomodate in the labelling approach these kind of cost models. We attach to this document the techinical report \emph{Dependent labelling applied to stateful hardware components}'' which describes what seems to be at the moment the most promising approach to the problem. Unsurprisingly, the solution uses dependent labels, that allow to associate a different cost to multiple executions of the same block. Dependent labels were developed in CerCo to allow loop optimizations, where the dependency was over the number of iterations of the loops. In the case of modern hardware, the dependency is on approximations of the internal hardware state, that needs to be made manifest in the source code too. The strategy described in the technical report is assumed to work on pipelines, while additional research is expected for caches. Moreover, in the middle term we need to be implement the solution for pipelines to be able to perform experiments. In particular, we need to understand the behaviour on automated provers on the more complex generated cost invariants, and we need to understand to which extent the cost invariants can work with the more precise cost models before introducing severe approximations. \end{enumerate} \newpage