source: Deliverables/D6.2/supplement.tex @ 2579

% CerCo: Certified Complexity
%
% Supplement to Deliverable 6.2
%
% Plan for Dissemination and Use 
%
% At the end of year 1, this deliverable was rejected by the reviewers and
% they asked for an addendum, which I wrote shortly after the review.  At the
% end of year 1, that was itself rejected by the reviewers.  They said:
%
% "The reviewers request the resubmission of the addenda to deliverables D2.1
% and D6.2 within one month from the receipt of this report. 
%
% ...
%
% Deliverable D6.2 does not contain a specific and clear dissemination
% strategy or plan till the end of the project.  The reviewers request the
% resubmission of D6.2 detailing an event targeting at the promoting the
% results of the CerCo project.  It should be planned at least as a half-day
% event solely presenting the CerCo project.  In order to attract an audience
% from academia as well as from industry the event should try to focus on case
% studies for the dependent labelling approach in more modern processor
% architectures, e.g., as applied in the embedded domain."
%
% I'm writing this supplement to D6.2 as our response to this.  At the May
% 2012 meeting in Bologna we discussed:
%
%  - Plans for the CerCo workshop at ETAPS 2013 (later HiPEAC 2013 too)
%  - Subject areas for papers to be written and submitted
%
% Strictly, the reviewers request only mentions the event.  However, if we can
% make a good job of the paper list, then that would be an advance on the
% addendum as of last year — and resubmitting the addendum is what was
% requested.  
%
% Ian Stark
% 2012-05-24

\documentclass[11pt,a4paper]{article}
\usepackage{../style/cerco}

\hypersetup{bookmarksopenlevel=2}

\title{
INFORMATION AND COMMUNICATION TECHNOLOGIES\\
(ICT)\\
PROGRAMME\\
\vspace*{1cm}Project FP7-ICT-2009-C-243881 {\cerco}}

\date{}
\author{}

\begin{document}
\thispagestyle{empty}

\vspace*{-1cm}
\begin{center}
\includegraphics[width=0.6\textwidth]{../style/cerco_logo.png}
\end{center}

\begin{minipage}{\textwidth}
\maketitle
\end{minipage}

\vspace*{0.5cm}
\begin{center}
\begin{LARGE}
\bfseries
Supplement to Deliverable 6.2\\[\jot]
{\cerco} Workshop and Publication Planning
\end{LARGE} 
\end{center}

\vspace*{2cm}
\begin{center}
\begin{large}
Version 1.0
\end{large}
\end{center}

\vspace*{0.5cm}
\begin{center}
\begin{large}
Main Authors:\\
I. Stark
\end{large}
\end{center}

\vspace*{\fill}
\noindent
Project Acronym: {\cerco}\\
Project full title: Certified Complexity\\
Proposal/Contract no.: FP7-ICT-2009-C-243881 {\cerco}

\clearpage\pagestyle{myheadings}\markright{{\cerco}, FP7-ICT-2009-C-243881}

\section{Summary}

In March~2012 the second-year review panel for the {\cerco} project requested
details of specific plans to promote the final results of the project.  This
document is a response to that, with the following two contributions.
\begin{itemize}
\item Plans for the {\cerco} workshop at the HiPEAC~'13 meeting in Berlin
  (Deliverables 6.4 and~6.5).
\item A list of proposed publications reporting {\cerco} results.
\end{itemize}
This report supplements the \emph{Plan for the Use and Dissemination of
  Foreground}, Deliverable~6.2, from August 2010 and addendum \emph{Future
  Dissemination Plans} of April 2011.

\section{{\cerco} Workshop}

We shall hold a {\cerco} one-day workshop for academic and industrial
researchers.  Our preferred destination is \emph{HiPEAC '13}, to be held in
Berlin at the end of January~2013.  This is an international meeting on
high-performance and embedded architectures and compilers, organised by the
European Network of Excellence in the field, and as such provides an ideal
audience for {\cerco} results.  The conference workshops for 2013 have not yet
been selected, but we have submitted our {\cerco} proposal for consideration.
In case this is not successful, we are also holding an offer of a workshop day
at ETAPS~2013, the European Joint Conferences on Theory and Practice of
Software.  This too is a forum for a range of academic and industrial
researchers, but it takes place in March 2013 and so does not fall within the
{\cerco} timetable.

This {\cerco} workshop has two objectives:
\begin{itemize}
\item To publicise the results of {\cerco} to members of the relevant
  industrial and academic research communities.
\item To stimulate discussion between the industrial and academic participants
  about future work building on the current state of the art.
\end{itemize}
To support these objectives, we propose to send invitations to a dozen
industrial and academic research groups working in the field.  While the
workshop will be open to anyone at HiPEAC who wishes to register, we consider
an invitational workshop to be the most direct way to bring together {\cerco}
researchers with potential users of the project results.  A list of possible
invitees appears below.

The workshop, with these objectives, is designed to meet the requirements of
Deliverables 6.4 and~6.5 as set out in the original {\cerco} proposal (Annex~I
``Description of Work'', Workplan Table 3, Work package~6).  In particular,
that proposal envisioned overlapping the presentation of {\cerco} results to
invited industrial and scientific audiences at an event co-located with an
international conference.

We plan the following draft structure for the workshop:
\begin{itemize}
\item Morning: Short talks by {\cerco} partners presenting the project and its
  results.
  \begin{itemize}
  \item Project overview: a trustworthy framework for cost analysis of
    embedded code.
  \item Demonstration of Frama-C plugin: high-level static reasoning about
    global runtime complexity.
  \item Demonstration of Lustre plugin: automatic analysis of component
    reaction time.
  \item The {\cerco} compiler: what makes a certified compiler trustworthy.
  \item The labelling approach to cost analysis: a modular way to prove
    correctness.
  \item Structured traces: tracking high-level structure in low-level
    execution.
  \item Dependent labels: managing refined cost information for richer
    architectures.
  \item Future directions: the latest very-low-power embedded processors;
    other runtime costs; further languages.
  \end{itemize}
\item Afternoon: Short presentations by some of the invited participants on the
  state of the art in static analysis of execution costs for embedded systems.
\item Conclusion: Round-table discussion on potential applications and future
  challenges.
\end{itemize}
This structure addresses both of the listed objectives, with the morning
dedicated to dissemination of {\cerco} results and the afternoon to promoting
interaction between academic and industrial researchers working in the field.

We have identified the following relevant groups as some initial invitees to
the {\cerco} workshop.
\begin{description}
\item[AbsInt aIT] \emph{AbsInt} provide tools for validation of
  safety-critical software, including static analysis for worst-case execution
  time through abstract interpretation.  They have participated in a previous
  {\cerco} event, and their insights into the requirements for precise timing
  analysis are extremely relevant to the domain of {\cerco}.
\item[Frama-C]  The \emph{Frama-C} platform for static analysis of C source
  code provides the context for the {\cerco} plugin which demonstrates the use
  of automated cost annotations on source code.
\item[Rapita Systems] The \emph{RapiTime} timing analysis tool for real-time
  embedded systems uses runtime instrumentation of C to identify source-level
  execution costs and predict worst-cast execution time.
\item[PASTA]  This research group at the University of Edinburgh are the
  designers of the \emph{EnCore} family of configurable embedded
  microprocessors.  Their \emph{ArcSim} tool offers cycle-accurate simulation
  of these low-energy cores, giving significant insights into the
  practicalities of precise cost analysis.
\item[WCET-Aware Compilation]  Dr Heiko Falk at TU Dortmund leads this
  research project investigating the optimizations and compilation techniques
  appropriate to the requirements of worst-case rather than average-case
  timing.
\item[York RTS] The \emph{Real-Time Systems} research group at the University
  of York are active in worst-case execution time analysis and the design of
  time-predictable architectures.
% \item[Hume/EmBounded]  Prof. Kevin Hammond at the University of St Andrews
%   leads a research team working on the quantification and certification of
%   resource use in concurrent real-time embedded software.
\item[ARM Verification Project]  Gordon, Fox and Myreen at the University of
  Cambridge have a machine-checked mathematical model of the ARM
  microprocessor.  With the release of the ARM Cortex-M series of low-power
  embedded processors, this is a potential application area for {\cerco}
  technology in the future.
\item[CompCertTSO]  Sewell's group, also at the University of Cambridge, have
  a verified C compiler treating concurrency in a relaxed memory model.  Like
  {\cerco}, they have relevant experience of extending CompCert-based
  verification to additional code properties.
\item[Gliwa Embedded Systems] The software consultancy \emph{Gliwa GmbH}
  develop specialist tools for measurement and verification of execution time
  in embedded systems.
\item[Artemis]  The European industry association \emph{Advanced Research \&
    Technology for Embedded Intelligence and Systems}.  We already have
  contact with Artemis through the University of Bologna, which is a member of
  the association.
\item[IMDEA Software]  Dr Boris K\"opf applies quantitative analysis of code
  execution time to evaluate potential security weaknesses by side-channel
  attacks.  
\item[ADSIG] The \emph{ArtistDesign Special Interest Group on Embedded Systems
    Design} is a large consortium of experts in embedded systems design,
  arising from the ARTIST Network of Excellence.
\end{description}
We propose to invite each of these groups to send participants and, if they
wish, contribute a short talk on their work to the afternoon session.  We
shall also invite the {\cerco} project reviewers, who are experts in the area.
This is not a closed list --- depending on responses, we are open to inviting
further participants as appropriate.


\section{Publication Planning}

The original Deliverable~6.2 and its addendum, prepared earlier in the
project, presented a list of conferences and journals suitable for publicising
{\cerco} results.  Now that the project has progressed, we have reviewed the
technical activities to date and identified a specific list of topics and
results for dissemination in individual papers and articles.  Some of these
have already been submitted, or accepted for publication: in particular, an
FMICS~2012 paper on the labelling approach which also references the Frama-C
plugin and Lustre case study.
\begin{description}
\item[Labelling] As presented in Deliverable~2.1, the use of labelling to
  build cost annotations and prove their correctness is key to the {\cerco}
  development.  It allows decoupling the certification of machine code
  execution properties from the verification of the compilation map between C
  source and assembler.
\item[Dependent labelling] The indexing of labels with additional
  data-dependent information makes is possible to track sources of variation
  in execution cost: compiler optimizations such as unrolling or loop peeling;
  or processor features like instruction pipelining and caches.
\item[The {\cerco} Frama-C plugin] This was demonstrated at the second-year
  review panel, and a paper would describe its operation and effect.  The
  plugin annotates C source code with fine-grained cycle costs according to
  {\cerco} analysis.  This instrumented code is passed to the \emph{Jessie}
  plugin which can generate the verification conditions necessary to check the
  cost specifications of complete procedures.  Finally, these conditions can
  be passed to a range of automatic proof engines.  The overall result is
  verified declarations of the cycle execution time of identified C functions,
  in terms of input and other parameters, given in the ACSL specification
  language.
\item[Lustre analysis] This was also demonstrated at the review panel.  The
  {\cerco} tools can perform automated analysis of response time for
  individual components in the Lustre synchronous control language.  Lustre
  automatically generates C source code for concurrent components, in a
  sufficiently standard form to allow precise costing of execution paths.
\item[Certifying machine code] {\cerco} extends previous work on compilation
  by also verifying the final step from assembler to binary object code.  In
  addition, it is essential to prove that cost annotations exactly capture
  machine execution steps.  These are both substantial proofs with novel
  features.
\item[Correctness of branch selection] Many processors provide a range of
  branch commands at the machine level, typically for different ranges of
  jump.  Generating efficient and compact assembly code requires appropriate
  branch selection.  This is non-trivial --- indeed, finding the optimum
  selection is in some cases NP-hard --- and the complexity of any algorithm
  here makes it a challenge for proving correctness.  {\cerco} have developed
  a novel decomposition of branch selection into policy and implementation, to
  separate concerns and allow for tractable proof.
\item[Structured traces] {\cerco} reports execution costs at the level of C
  source, where there is an evident code structure of nested call and return;
  but these costs arise from unstructured individual steps at the machine
  level.  We have developed a notion of structure on machine execution traces
  which captures precisely the information necessary to correctly relay cost
  information between these levels.  This is essential to the compiler proof,
  and interesting in itself as a carrier of high-level information in a
  low-level execution environment.
\item[The {\cerco} formalisation] The large-scale structure of the {\cerco}
  formalisation, its components, how they depend upon each other, and what is
  required of them to complete the correctness proof.  Some parts of these are
  related to analogous constructions in work such as CompCert; many are novel
  and arise from our particular attention to verifying non-functional runtime
  properties of code.
\item[A survey of {\cerco} results] All the above papers deal with individual
  parts of the {\cerco} project, or the technical details of its operation.  A
  final paper should survey the outcome of the project, its achievements and
  potential future work to build on these.
\end{description}

\end{document}

%  LocalWords:  Frama AbsInt Rapita RapiTime EnCore ArcSim WCET Heiko HiPEAC
%  LocalWords:  Falk EmBounded Myreen CompCertTSO ADSIG ArtistDesign ACSL FMICS
%  LocalWords:  Gliwa GmbH