Changeset 3136


Ignore:
Timestamp:
Apr 12, 2013, 6:47:11 PM (4 years ago)
Author:
mckinna
Message:

Updates: form and content, incorporating comments from Brian, and from CSC's orignal "Reports" email!

Location:
Deliverables/D6.4-6.5
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D6.4-6.5/report.tex

    r3134 r3136  
    6464\textbf{
    6565Report n. D6.4-6.5\\
    66 Final Report on User Validation}
     66Dissemination Events}
    6767\end{LARGE}
    6868\end{center}
     
    7979\begin{large}
    8080Main Authors:\\
    81 XXXX %James McKinna and Brian Campbell
     81Brian~Campbell, Ilias~Garnier, James~McKinna, Ian~Stark
    8282\end{large}
    8383\end{center}
  • Deliverables/D6.4-6.5/workshops.ltx

    r3135 r3136  
    3030  \texttt{http://cerco.cs.unibo.it/innovative\_techniques\_on\_timing\_analysis\_technical\_day}
    3131
    32 It ran in parallel with a two-day workshop on Quantitative Aspects of Programming Languages (QAPL 11), sharing three sessions with that meeting. The CerCo workshop also included presentations from Tullio Vartanegra, representing the PROARTIS Consortium (FP7-ICT-2009.3.4), and an invited talk from Prof. Bj{\"o}rn Lisper (M{\"a}lardalen University, SE) on Parametric WCET analysis.
     32It ran in parallel with a two-day workshop on Quantitative Aspects of Programming Languages (QAPL 11), sharing three sessions with that meeting. The \cerco{} workshop also included presentations from Tullio Vartanegra, representing the PROARTIS Consortium (FP7-ICT-2009.3.4), and an invited talk from Prof. Bj{\"o}rn Lisper (M{\"a}lardalen University, SE) on Parametric WCET analysis.
    3333
    3434\paragraph{Scientific Outcomes}
    3535
    36 The HiPEAC workshop was one of 24 such meetings in a highly parallel programme organised over the 3 days of the main conference, while the ETAPS workshop was one of 20 workshops organised over 4 days, the two weekends which book-ended the main conference, and was thus the better attended, and scientifically more fruitful, meeting.
     36The HiPEAC workshop was one of 24 such meetings in a highly parallel programme organised over the 3 days of the main conference, while the ETAPS workshop was one of 20 workshops organised over 4 days, the two weekends which book-ended the main conference, and was thus the better attended, and scientifically more successful, meeting.
    3737
    38 Nonetheless, a fruitful discussion emerged at HiPEAC concerning
    39 source-level cost reasoning.  Kevin Hammond's group use amortized
    40 analysis techniques to connect local costs about embedded programs in
    41 the Hume language to global costs, technology which it may be possible
    42 to transfer to the CerCo setting.  A key difference in our approaches
    43 is that their Hume implementation used the high predictability of
    44 their virtual machine implementation to obtain the local cost
    45 information, whereas CerCo produces such information for a complex
    46 native-code compiler.
     38Nonetheless, a fruitful discussion emerged at HiPEAC concerning source-level cost reasoning.  Kevin Hammond's group use amortized analysis techniques to connect local costs about embedded programs in the Hume language to global costs, technology which it may be possible to transfer to the \cerco{} setting.  A key difference in our approaches is that their Hume implementation uses the high predictability of their virtual machine implementation to obtain local cost information, whereas \cerco{} produces such information for a complex native-code compiler.
    4739
    48 At the ETAPS workshop Bj{\"o}rn Lisper drew attention to the many points of common interest and related techniques between the work on CerCo and his own on Parametric WCET analysis. In addition to his own technical talk, he took the opportunity to advertise, and solicit interest in, the recently formed COST Action IC1202 Timing Analysis and Cost-Level Estimation (TACLe), of which he is Chair. This offers very promising potential for future collaborations and the wider communication of results from CerCo.
     40At the ETAPS workshop Bj{\"o}rn Lisper drew attention to the many points of common interest and related techniques between the work on \cerco{} and his own on Parametric WCET analysis. The main difference between what we do and what is done in the WCET community is that we use (automated) theorem proving to deal with the control-flow (i.e. to put an upper bound to the executions). The standard technique in WCET consists in using polyhedral analysis to bound the number of loop
     41iterations.  That analysis produces constraints which are solved with the aid of off-the-shelf linear programming tools. So the effectiveness of theorem proving in computing precise costs in \cerco{} interested him.
     42
     43
     44In addition to his own technical talk, he took the opportunity to advertise, and solicit interest in, the recently formed COST Action IC1202 Timing Analysis and Cost-Level Estimation (TACLe), of which he is Chair. This offers very promising potential for future collaborations and the wider communication of results from \cerco{}.
    4945
    5046A common theme emerged from the shared sessions with QAPL, and in particular the invited talk there from prof. Alessandra di Pierro on \emph{probabilistic} timing analysis: the parametrisation of a given timing analysis with respect to different cost \emph{algebras}. In the case of probabilistic analyses, costs are taken with respect to given probability distributions, with \emph{expected} costs being computed. prof. Vartanegra's talk emphasised a radical approach to such analyses, by making assumptions about the processor/cache architecture to yield an essentially deterministic analysis.
    5147
    52 In the deterministic case studied in CerCo, we have taken a given, fixed, cost algebra of natural numbers (obtained from Siemens data-sheet clock timings) under addition, but already Tranquili's work on \emph{dependent labelling} suggests a move to computing costs in algebras of \emph{functions} (in the case of his analysis of loop unrolling, of cost expressions parametrised with respect to valuations of the loop index variables). The implications of such a move are yet to be explored.
     48In the deterministic case studied in \cerco{}, we have taken a given, fixed, cost algebra of natural numbers (obtained from Siemens data-sheet clock timings) under addition, but already Tranquili's work on \emph{dependent labelling} suggests a move to computing costs in algebras of \emph{functions} (in the case of his analysis of loop unrolling, of cost expressions parametrised with respect to valuations of the loop index variables). The implications of such a move are yet to be explored.
    5349
    5450
Note: See TracChangeset for help on using the changeset viewer.