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

Last change on this file since 2012 was 2012, checked in by Ian Stark, 9 years ago

Added proposed papers to D6.2

  • Property svn:eol-style set to native
  • Property svn:mime-type set to text/x-latex
File size: 13.2 KB
1% CerCo: Certified Complexity
3% Supplement to Deliverable 6.2
5% Plan for Dissemination and Use
7% At the end of year 1, this deliverable was rejected by the reviewers and
8% they asked for an addendum, which I wrote shortly after the review.  At the
9% end of year 1, that was itself rejected by the reviewers.  They said:
11% "The reviewers request the resubmission of the addenda to deliverables D2.1
12% and D6.2 within one month from the receipt of this report.
14% ...
16% Deliverable D6.2 does not contain a specific and clear dissemination
17% strategy or plan till the end of the project.  The reviewers request the
18% resubmission of D6.2 detailing an event targeting at the promoting the
19% results of the CerCo project.  It should be planned at least as a half-day
20% event solely presenting the CerCo project.  In order to attract an audience
21% from academia as well as from industry the event should try to focus on case
22% studies for the dependent labelling approach in more modern processor
23% architectures, e.g., as applied in the embedded domain."
25% I'm writing this supplement to D6.2 as our response to this.  At the May
26% 2012 meeting in Bologna we discussed:
28%  - Plans for the CerCo workshop at ETAPS 2013
29%  - Subject areas for papers to be written and submitted
31% Strictly, the reviewers request only mentions the event.  However, if we can
32% make a good job of the paper list, then that would be an advance on the
33% addendum as of last year — and resubmitting the addendum is what was
34% requested. 
36% Ian Stark
37% 2012-05-24
48\vspace*{1cm}Project FP7-ICT-2009-C-243881 {\cerco}}
69Supplement to Deliverable 6.2\\[\jot]
70CerCo Workshop and Publication Planning
77Version 1.0
84Main Authors:\\
85I. Stark
91Project Acronym: {\cerco}\\
92Project full title: Certified Complexity\\
93Proposal/Contract no.: FP7-ICT-2009-C-243881 {\cerco}
95\clearpage\pagestyle{myheadings}\markright{{\cerco}, FP7-ICT-2009-C-243881}
99In March~2012 the second-year review panel for the {\cerco} project requested
100details of specific plans to promote the final results of the project.  This
101document is a response to that, with the following two contributions.
103\item Plans for the {\cerco} workshop at the ETAPS~2013 conference in
104  Rome (Deliverables 6.4 and~6.5).
105\item A list of proposed publications reporting {\cerco} results.
107This report supplements the \emph{Plan for the Use and Dissemination of
108  Foreground}, Deliverable~6.2, from August 2010 and addendum \emph{Future
109  Dissemination Plans} of April 2011.
111\section{CerCo Workshop}
113The organisers of ETAPS~2013 have accepted a {\cerco} workshop proposal.  The
114ETAPS conferences run for a week during March 2013, in Rome, with workshops
115and tutorials in the adjacent weekends.  {\cerco} will have a full one-day
116workshop as part of this programme.
118This {\cerco} workshop has two objectives:
120\item To publicise the results of {\cerco} to members of the relevant
121  industrial and academic research communities.
122\item To stimulate discussion between the industrial and academic participants
123  about future work building on the current state of the art.
125To support these objectives, we propose to send invitations to a dozen
126industrial and academic research groups working in the field.  While the
127workshop will be open to anyone at ETAPS who wishes to register, we consider
128an invitational workshop to be the most direct way to bring together {\cerco}
129researchers with potential users of the project results.  A list of invitees
130appears below.
132The workshop, with these objectives, is designed to meet the requirements of
133Deliverables 6.4 and~6.5 as set out in the original {\cerco} proposal (Annex~I
134``Description of Work'', Workplan Table 3, Work package~6).  In particular,
135that proposal envisioned overlapping the presentation of {\cerco} results to
136invited industrial and scientific audiences at an event co-located with an
137international conference.
139We plan the following draft structure for the workshop:
141\item Morning: Short talks by {\cerco} partners presenting the project and its
142  results.
143  \begin{itemize}
144  \item Project overview: a trustworthy framework for cost analysis of
145    embedded code.
146  \item Demonstration of Frama-C plugin: high-level static reasoning about
147    global runtime complexity.
148  \item Demonstration of Lustre plugin: automatic analysis of component
149    reaction time.
150  \item The {\cerco} compiler: what makes a certified compiler trustworthy.
151  \item The labelling approach to cost analysis: a modular way to prove
152    correctness.
153  \item Structured traces: tracking high-level structure in low-level
154    execution.
155  \item Dependent labels: managing refined cost information for richer
156    architectures.
157  \item Future directions: the latest very-low-power embedded processors;
158    other runtime costs; further languages.
159  \end{itemize}
160\item Afternoon: Short presentations by some of the invited participants on the
161  state of the art in static analysis of execution costs for embedded systems.
162\item Conclusion: Round-table discussion on potential applications and future
163  challenges.
165This structure addresses both of the listed objectives, with the morning
166dedicated to dissemination of {\cerco} results and the afternoon to promoting
167interaction between academic and industrial researchers working in the field.
169We have identified the following relevant groups to invite to the {\cerco}
172\item[AbsInt]  AbsInt provide tools for validation of safety-critical
173  software, including static analysis for worst-case execution time through
174  abstract interpretation.  They have participated in a previous {\cerco}
175  event, and their insights into the requirements for precise timing analysis
176  are extremely relevant to the domain of {\cerco}.
177\item[Frama-C]  The \emph{Frama-C} platform for static analysis of C source
178  code provides the context for the {\cerco} plugin which demonstrates the use
179  of automated cost annotations on source code.
180\item[Rapita Systems] The \emph{RapiTime} timing analysis tool for real-time
181  embedded systems uses runtime instrumentation of C to identify source-level
182  execution costs and predict worst-cast execution time.
183\item[PASTA]  This research group at the University of Edinburgh are the
184  designers of the \emph{EnCore} family of configurable embedded
185  microprocessors.  Their \emph{ArcSim} tool offers cycle-accurate simulation
186  of these low-energy cores, giving significant insights into the
187  practicalities of precise cost analysis.
188\item[WCET-Aware Compilation]  Dr Heiko Falk at TU Dortmund leads this
189  research project investigating the optimizations and compilation techniques
190  appropriate to the requirements of worst-case rather than average-case
191  timing.
192\item[Hume/EmBounded]  Prof. Kevin Hammond at the University of St Andrews
193  leads a research team working on the quantification and certification of
194  resource use in concurrent real-time embedded software.
195\item[ARM Verification Project]  Gordon, Fox and Myreen at the University of
196  Cambridge have a machine-checked mathematical model of the ARM
197  microprocessor.  With the release of the ARM Cortex-M series of low-power
198  embedded processors, this is a potential application area for {\cerco}
199  technology in the future.
200\item[CompCertTSO]  Sewell's group, also at the University of Cambridge, have
201  a verified C compiler treating concurrency in a relaxed memory model.  Like
202  {\cerco}, they have relevant experience of extending CompCert-based
203  verification to additional code properties.
204\item[Artemis]  The European industry association \emph{Advanced Research \&
205    Technology for Embedded Intelligence and Systems}.  We already have
206  contact with Artemis through the University of Bologna, which is a member of
207  the association.
208\item[IMDEA Software]  Dr Boris K\"opf applies quantitative analysis of code
209  execution time to evaluate potential security weaknesses by side-channel
210  attacks. 
211\item[ADSIG] The \emph{ArtistDesign Special Interest Group on Embedded Systems
212    Design} is a large consortium of experts in embedded systems design,
213  arising from the ARTIST Network of Excellence.
215We propose to invite each of these groups to send participants and, if they
216wish, contribute a short talk on their work to the afternoon session.
219\section{Publication Planning}
221The original Deliverable~6.2 and its addendum, prepared earlier in the
222project, presented a list of conferences and journals suitable for publicising
223{\cerco} results.  Now that the project has progressed, we have reviewed the
224technical activities to date and identified a specific list of topics which we
225propose as suitable for dissemination in individual papers and articles.
228\item[Labelling] As presented in Deliverable~2.1, the use of labelling to
229  build cost annotations and prove their correctness is key to the {\cerco}
230  development.  It allows decoupling the certification of machine code
231  execution properties from the verification of the compilation map between C
232  source and assembler.
233\item[Dependent labelling] The indexing of labels with additional
234  data-dependent information makes is possible to track sources of variation
235  in execution cost: compiler optimizations such as unrolling or loop peeling;
236  or processor features like instruction pipelining and caches.
237\item[The {\cerco} Frama-C plugin] This was demonstrated at the second-year
238  review panel, and a paper would describe its operation and effect.  The
239  plugin annotates C source code with fine-grained cycle costs according to
240  {\cerco} analysis.  This instrumented code is passed to the \emph{Jessie}
241  plugin which can generate the verification conditions necessary to check the
242  cost specifications of complete procedures.  Finally, these conditions can
243  be passed to a range of automatic proof engines.  The overall result is
244  verified declarations of the cycle execution time of identified C functions,
245  in terms of input and other parameters, given in the ACSL specification
246  language.
247\item[Lustre analysis] This was also demonstrated at the review panel.  The
248  {\cerco} tools can perform automated analysis of response time for
249  individual components in the Lustre synchronous control language.  Lustre
250  automatically generates C source code for concurrent components, in a
251  sufficiently standard form to allow precise costing of execution paths.
252\item[Certifying machine code] {\cerco} extends previous work on compilation
253  by also verifying the final step from assembler to binary object code.  In
254  addition, it is essential to prove that cost annotations exactly capture
255  machine execution steps.  These are both substantial proofs with novel
256  features.
257\item[Correctness of branch selection] Many processors provide a range of
258  branch commands at the machine level, typically for different ranges of
259  jump.  Generating efficient and compact assembly code requires appropriate
260  branch selection.  This is non-trivial --- indeed, finding the optimum
261  selection is in some cases NP-hard --- and the complexity of any algorithm
262  here makes it a challenge for proving correctness.  {\cerco} have developed
263  a novel decomposition of branch selection into policy and implementation, to
264  separate concerns and allow for tractable proof.
265\item[Structured traces] {\cerco} reports execution costs at the level of C
266  source, where there is an evident code structure of nested call and return;
267  but these costs arise from unstructured individual steps at the machine
268  level.  We have developed a notion of structure on machine execution traces
269  which captures precisely the information necessary to correctly relay cost
270  information between these levels.  This is essential to the compiler proof,
271  and interesting in itself as a carrier of high-level information in a
272  low-level execution environment.
273\item[The {\cerco} formalisation] The large-scale structure of the {\cerco}
274  formalisation, its components, how they depend upon each other, and what is
275  required of them to complete the correctness proof.  Some parts of these are
276  related to analogous constructions in work such as CompCert; many are novel
277  and arise from our particular attention to verifying non-functional runtime
278  properties of code.
279\item[A survey of {\cerco} results] All the above papers deal with individual
280  parts of the {\cerco} project, or the technical details of its operation.  A
281  final paper should survey the outcome of the project, its achievements and
282  potential future work to build on these.
287%  LocalWords:  Frama AbsInt Rapita RapiTime EnCore ArcSim WCET Heiko
288%  LocalWords:  Falk EmBounded Myreen CompCertTSO ADSIG ArtistDesign
Note: See TracBrowser for help on using the repository browser.