# Changeset 3210

Ignore:
Timestamp:
Apr 29, 2013, 4:55:37 PM (6 years ago)
Message:

Final version.

File:
1 edited

Unmodified
Added
Removed
• ## Deliverables/D6.3/report.tex

 r3209 \begin{large} Main Authors:\\ Roberto M.~Amadio, Claudio Sacerdoti Coen Roberto M.~Amadio, Gabriele Pulcini, Claudio Sacerdoti Coen %Dominic P. Mulligan and Claudio Sacerdoti Coen \end{large} \vspace*{7cm} \paragraph{Abstract} We review the techniques experimented in CerCo for cost annotation exploitement We review the techniques experimented in CerCo for cost annotation exploitment 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 The Grant Agreement describes deliverable D6.3 as follows: \begin{quotation} \textbf{Final Report on User Validation}: An articulated analysis and critics of the user validation experiences. In particular we will review the effectiveness of the techniques for cost annotation exploitement that have been employed in the project and that have been validated on simple and non trivial examples. We will also identify additional techniques that could be exploited in the middle and long term to bring the CerCo compiler to its full potentialities. \textbf{Final Report on User Validation}: An articulated analysis and critics of the user validation experiences. In particular we will review the effectiveness of the techniques for cost annotation exploitment that have been employed in the project and that have been validated on simple and non trivial examples. We will also identify additional techniques that could be exploited in the middle and long term to bring the CerCo compiler to its full potentialities. \end{quotation} associates a pre-labelling to every function abstraction and a post-labelling to every application which is not immediately sourrounded by an abstraction.  In particular, the post-labelling surrounded by an abstraction.  In particular, the post-labelling takes care of the functions created by the CPS translation. references and threads. The first proof of this result  relies on a kind of standardisation theorem and it is of a combinatorial nature. More recentely, we have shown that a proof of a similar result can be obtained More recently, we have shown that a proof of a similar result can be obtained by semantic means building on the so called {\em quantitative realizability models} proposed by Dal Lago and Hofmann. 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 moment the generator does not degrade 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 Both kind of improvements can be performed in the middle term. \item \textbf{Improvements to cost annotation exploitement} \item \textbf{Improvements to cost annotation exploitment} 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 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 of how to accommodate in the labelling approach these kind of cost models. We attach to this document the technical 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,
Note: See TracChangeset for help on using the changeset viewer.