Changeset 3210


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

Final version.

File:
1 edited

Legend:

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

    r3209 r3210  
    101101\begin{large}
    102102Main Authors:\\
    103 Roberto M.~Amadio, Claudio Sacerdoti Coen
     103Roberto M.~Amadio, Gabriele Pulcini, Claudio Sacerdoti Coen
    104104%Dominic P. Mulligan and Claudio Sacerdoti Coen
    105105\end{large}
     
    121121\vspace*{7cm}
    122122\paragraph{Abstract}
    123 We review the techniques experimented in CerCo for cost annotation exploitement
     123We review the techniques experimented in CerCo for cost annotation exploitment
    124124at the user level. We also report on recent work towards precise time analysis
    125125at the source level for modern hardware architectures whose instructions cost
     
    138138The Grant Agreement describes deliverable D6.3 as follows:
    139139\begin{quotation}
    140 \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.
     140\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.
    141141
    142142\end{quotation}
     
    373373associates a pre-labelling to every function abstraction and a
    374374post-labelling to every application which is not immediately
    375 sourrounded by an abstraction.  In particular, the post-labelling
     375surrounded by an abstraction.  In particular, the post-labelling
    376376takes care of the functions created by the CPS translation.
    377377
     
    430430references and threads.
    431431The first proof of this result  relies on a kind of standardisation theorem and it is of a combinatorial nature.
    432 More recentely, we have shown that a proof of a similar result can be obtained
     432More recently, we have shown that a proof of a similar result can be obtained
    433433by semantic means building on the so called {\em quantitative realizability
    434434models} proposed by Dal Lago and Hofmann.
     
    452452   compute the parametric worst case execution time for all Lustre programs
    453453   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
     454   moment the generator does not degrade gracefully: if the source code does
    455455   not respects the syntactic requirements of the generator, no cost invariants
    456456   are generated at all. This behaviour is consistent with the traditional
     
    465465
    466466   Both kind of improvements can be performed in the middle term.
    467  \item \textbf{Improvements to cost annotation exploitement}
     467 \item \textbf{Improvements to cost annotation exploitment}
    468468   One benefit of CerCo w.r.t. traditional WCET is that the user does not need
    469469   to trust the bound provided by the tool, but it can at least partially
     
    488488   state of hardware components like pipelines, caches or branch predictors.
    489489   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
     490   of how to accommodate in the labelling approach these kind of cost models.
     491   We attach to this document the technical report ``\emph{Dependent labelling
    492492   applied to stateful hardware components}'' which describes what seems to
    493493   be at the moment the most promising approach to the problem. Unsurprisingly,
Note: See TracChangeset for help on using the changeset viewer.