Changeset 3207

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

Final version up to spellchecking.

1 edited


  • Deliverables/D6.3/pipelines.tex

    r3126 r3207  
    18 \title{??????}
    19 \author{??????}
    20 \date{dd/mm/yy}
     18\title{Dependent labelling applied to stateful hardware components}
     19\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}\\~\\
     21\\Dipartimento di Informatica - Scienza ed Ingegneria\\
     22Universit\`a di Bologna}
    24 \section{Middle and Long Term Improvements}
    25 In order to identify the middle and long term improvements, we briefly review
     27\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}.
     29In 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.
     33The labelling approach~\cite{labelling,paolo} is a new technique to implement
     34compilers that induce on the source code a sound and precise cost model for
     35basic blocks. The cost model is computed on object code blocks and then
     36transferred to the source code by reversing the optimizations to the control
     37flow~\cite{paolo}. In the rest of this technical report we assume reader's
     38knowledge on the labelling approach.
     40At the end of the CerCo project, we are convinced that the labelling approach
     41can support most optimizations currently supported by real world compilers.
     42Moreover, we have formally certified the code of a compiler that transfers
     43cost models according to the labelling approach, greatly reducing the trusted
     44code base of time analysis. The main issue that is left is to identify the
     45classes of cost models that can be expressed at the source level and that we
     46can automatically reason on. In particular, we know that cost models for
     47modern hardware are complex objects that assign to each instruction a cost which
     48also depends on the internal state of stateful hardware components that are
     49designed to optimize the average case. Pipelines, caches, branch predictors are
     50tipical examples of components that have no impact on the functional behavior
     51of the code, but that greatly augment the code performance.
     53Ignorance on the internal state of these components during a WCET analysis
     54forces to assume the worst case, leading to useless time bounds. Therefore,
     55standard WCET tools tend to statically execute code fragments as much as
     56possible, to minimize the ignorance on the state. For loops, for example, are
     57totally unrolled. In CerCo we could do the same, departing from the labelling
     58approach. However, what is more natural is to stay closer to the labelling
     59approach and avoid loosing precision by computing parametric exact costs.
     60This is the topic of this research report.
     62In Section~\ref{premises} we briefly review the premises and goals of the
     63CerCo approach in order to compare the CerCo approach to the traditional
     64WCET one, which is able to deal with modern hardware.
     65In Section~\ref{controlflow} we compare the control flow analyses performed
     66in CerCo and in traditional WCET, arguing that our approach is winning.
     67In Section~\ref{static} we compare the static analyses performed in CerCo
     68and in traditional WCET. Only the latter can deal with modern hardware.
     69Section~\ref{static2} contains the new material. We revise our static analysis
     70and the labelling approach in general to accomodate modern hardware.
     71Temporary conclusions are found in Section~\ref{conclusions}.
     73\section{\label{premises}CerCo: premises and goals}
     75We briefly review
    2676here the premises and goals of the CerCo approach to resource analysis.
    4191   choose the cost model in such a way that the cost bounds are high enough
    4292   to bound the cost of every produced code. This was attempted for instance
    43    in the EmBounded project with good success. However, we believe that bounds
     93   in the EMBounded project~\cite{embounded} with good success. However, we believe that bounds
    4494   obtained in this way have few possibilities of being tight.
    4595 \item Therefore our approach consists in having the compiler generate the
    64114techniques need to estimate the cost of control blocks of instructions.
    66 \subsection{Control flow analysis}
     116\section{Control flow analysis\label{controlflow}}
    68118The first main difference is in the control flow analysis. Traditional WCET
    120 \subsection{Static analysis of costs of basic blocks}
     170\section{Static analysis of costs of basic blocks\label{static}}
    121171At the beginning of the project we have deliberately decided to focus our
    122172attention on the control flow preservation, the cost model propagation and
    140190unlikely that our methodology could contribute to the solution of the problem.
    142 \subsubsection{Static analysis of costs of basic blocks revisited}
     192\section{Static analysis of costs of basic blocks revisited\label{static2}}
    143193We will now describe what currently seems to be the most interesting technique
    144194for the static analysis of the cost of basic blocks in presence of complex
    245295Nevertheless, operand insensitivity is an important property for the labelling
    246 approach. In~\cite{tranquilli} we introduced \emph{dependent labels} and
     296approach. In~\cite{paolo} we introduced \emph{dependent labels} and
    247297\emph{dependent costs}, which are the possibility of assigning costs to basic
    248298blocks of instructions which are also dependent on the state of the high level
    766816independent cost functions), we need to review the behaviour of probabilistic
    767817caches as proposed by PROARTIS. The interested reader can
    768 consult~\cite{proartis2-articolo30} for further informations.
     818consult~\cite{proartis2} for further informations.
    770820In a randomized cache, the probability of evicting a given line on every access
    798 \paragraph{Conclusions}
    799849At the current state of the art functional properties of programs are better
    800850proved high level languages, but the non functional ones are proved on the
    848898size of the views can be tamed in practice without ruining the whole approach.
     902\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.
     904\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
     9057437: 32-46, 2012, DOI:10.1007/978-3-642-32469-7\_3.
     907\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.
     909\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.
     911\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.
     913\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.
Note: See TracChangeset for help on using the changeset viewer.