# Changeset 3207 for Deliverables

Ignore:
Timestamp:
Apr 29, 2013, 3:31:04 PM (8 years ago)
Message:

Final version up to spellchecking.

File:
1 edited

### Legend:

Unmodified
 r3126 \begin{document} \title{??????} \author{??????} \date{dd/mm/yy} \title{Dependent labelling applied to stateful hardware components} \author{G. Pulcini$^*$, C. Sacerdoti Coen\footnote{The project CerCo acknowledges the financial support of the Future and Emerging Technologies (FET) programme within the Seventh Framework Programme for Research of the European Commission, under FET-Open grant number: 243881}\\~\\ \texttt{\{pulcini,sacerdot\}@cs.unibo.it}\\~ \\Dipartimento di Informatica - Scienza ed Ingegneria\\ Universit\`a di Bologna} \date{03/04/2013} \maketitle \section{Middle and Long Term Improvements} In order to identify the middle and long term improvements, we briefly review \abstract{The Certified Complexity (CerCo) EU Project~\cite{cerco} aims at integrating and unifying the functional and non functional analyses of safety and time critical software by performing both of them together on the source code. It is based on the labelling approach~\cite{labelling} that allows to write compilers that induce on the source code a sound and precise cost model for basic blocks. The cost model is computed on object code blocks and then transferred to the source code by reversing the optimizations to the control flow~\cite{paolo}. In this technical report we address the important issue of stateful hardware whose instructions cost is a function of the internal state. Typical examples are pipelines and caches. In order to avoid loss of precision, the cost model must be parametric on the state, which has no correspondent one at the source level. We show how to enrich the source code with the minimal amount of information that allows to compute costs precisely. We also briefly argue in favour of probabilistic static time analysis and we examine how it is already supported by the labelling approach. } \section{Introduction} The labelling approach~\cite{labelling,paolo} is a new technique to implement compilers that induce on the source code a sound and precise cost model for basic blocks. The cost model is computed on object code blocks and then transferred to the source code by reversing the optimizations to the control flow~\cite{paolo}. In the rest of this technical report we assume reader's knowledge on the labelling approach. At the end of the CerCo project, we are convinced that the labelling approach can support most optimizations currently supported by real world compilers. Moreover, we have formally certified the code of a compiler that transfers cost models according to the labelling approach, greatly reducing the trusted code base of time analysis. The main issue that is left is to identify the classes of cost models that can be expressed at the source level and that we can automatically reason on. In particular, we know that cost models for modern hardware are complex objects that assign to each instruction a cost which also depends on the internal state of stateful hardware components that are designed to optimize the average case. Pipelines, caches, branch predictors are tipical examples of components that have no impact on the functional behavior of the code, but that greatly augment the code performance. Ignorance on the internal state of these components during a WCET analysis forces to assume the worst case, leading to useless time bounds. Therefore, standard WCET tools tend to statically execute code fragments as much as possible, to minimize the ignorance on the state. For loops, for example, are totally unrolled. In CerCo we could do the same, departing from the labelling approach. However, what is more natural is to stay closer to the labelling approach and avoid loosing precision by computing parametric exact costs. This is the topic of this research report. In Section~\ref{premises} we briefly review the premises and goals of the CerCo approach in order to compare the CerCo approach to the traditional WCET one, which is able to deal with modern hardware. In Section~\ref{controlflow} we compare the control flow analyses performed in CerCo and in traditional WCET, arguing that our approach is winning. In Section~\ref{static} we compare the static analyses performed in CerCo and in traditional WCET. Only the latter can deal with modern hardware. Section~\ref{static2} contains the new material. We revise our static analysis and the labelling approach in general to accomodate modern hardware. Temporary conclusions are found in Section~\ref{conclusions}. \section{\label{premises}CerCo: premises and goals} We briefly review here the premises and goals of the CerCo approach to resource analysis. \begin{itemize} choose the cost model in such a way that the cost bounds are high enough to bound the cost of every produced code. This was attempted for instance in the EmBounded project with good success. However, we believe that bounds in the EMBounded project~\cite{embounded} with good success. However, we believe that bounds obtained in this way have few possibilities of being tight. \item Therefore our approach consists in having the compiler generate the techniques need to estimate the cost of control blocks of instructions. \subsection{Control flow analysis} \section{Control flow analysis\label{controlflow}} The first main difference is in the control flow analysis. Traditional WCET techniques. \subsection{Static analysis of costs of basic blocks} \section{Static analysis of costs of basic blocks\label{static}} At the beginning of the project we have deliberately decided to focus our attention on the control flow preservation, the cost model propagation and unlikely that our methodology could contribute to the solution of the problem. \subsubsection{Static analysis of costs of basic blocks revisited} \section{Static analysis of costs of basic blocks revisited\label{static2}} We will now describe what currently seems to be the most interesting technique for the static analysis of the cost of basic blocks in presence of complex Nevertheless, operand insensitivity is an important property for the labelling approach. In~\cite{tranquilli} we introduced \emph{dependent labels} and approach. In~\cite{paolo} we introduced \emph{dependent labels} and \emph{dependent costs}, which are the possibility of assigning costs to basic blocks of instructions which are also dependent on the state of the high level independent cost functions), we need to review the behaviour of probabilistic caches as proposed by PROARTIS. The interested reader can consult~\cite{proartis2-articolo30} for further informations. consult~\cite{proartis2} for further informations. In a randomized cache, the probability of evicting a given line on every access pipelines. \paragraph{Conclusions} \section{Conclusions\label{conclusions}} At the current state of the art functional properties of programs are better proved high level languages, but the non functional ones are proved on the size of the views can be tamed in practice without ruining the whole approach. \begin{thebibliography}{} \bibitem{cerco} \textbf{Certified Complexity}, R. Amadio, A. Asperti, N. Ayache, B. Campbell, D. Mulligan, R. Pollack, Y. Regis-Gianas, C. Sacerdoti Coen, I. Stark, in Procedia Computer Science, Volume 7, 2011, Proceedings of the 2 nd European Future Technologies Conference and Exhibition 2011 (FET 11), 175-177. \bibitem{labelling} \textbf{Certifying and Reasoning on Cost Annotations in C Programs}, N.  Ayache, R.M. Amadio, Y.Régis-Gianas, in Proc. FMICS, Springer LNCS 7437: 32-46, 2012, DOI:10.1007/978-3-642-32469-7\_3. \bibitem{paolo} \textbf{Indexed Labels for Loop Iteration Dependent Costs}, P. Tranquilli, in Proceedings of the 11th International Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL 2013), Rome, 23rd-24th March 2013, Electronic Proceedings in Theoretical Computer Science, to appear in 2013. \bibitem{embounded} \textbf{The EmBounded project (project paper)}, K. Hammond, R. Dyckhoff, C. Ferdinand, R. Heckmann, M. Hofmann, H. Loidl, G. Michaelson, J. Serot, A. Wallace, in Trends in Functional Programming, Volume 6, Intellect Press, 2006. \bibitem{proartis} \textbf{PROARTIS: Probabilistically Analysable Real-Time Systems}, F.J. Cazorla, E. Qui˜nones, T. Vardanega, L. Cucu, B. Triquet, G. Bernat, E. Berger, J. Abella, F. Wartel, M. Houston, et al., in ACM Transactions on Embedded Computing Systems, 2012. \bibitem{proartis2} \textbf{A Cache Design for Probabilistic Real-Time Systems}, L. Kosmidis, J. Abella, E. Quinones, and F. Cazorla, in Design, Automation, and Test in Europe (DATE), Grenoble, France, 03/2013. \end{thebibliography} \end{document}