Changeset 2012

Jun 1, 2012, 11:49:46 PM (5 years ago)

Added proposed papers to D6.2

1 edited


  • Deliverables/D6.2/supplement.tex

    r2007 r2012  
    6969Supplement to Deliverable 6.2\\[\jot]
    70 CerCo Workshop and Dissemination Plans
     70CerCo Workshop and Publication Planning
    158158    other runtime costs; further languages.
    159159  \end{itemize}
    160 \item Afternoon: Presentations by some of the invited participants on the
     160\item Afternoon: Short presentations by some of the invited participants on the
    161161  state of the art in static analysis of execution costs for embedded systems.
    162162\item Conclusion: Round-table discussion on potential applications and future
    169169We have identified the following relevant groups to invite to the {\cerco}
    171 \begin{itemize}
    172 \item AbsInt.  AbsInt provide tools for validation of safety-critical
     172\item[AbsInt]  AbsInt provide tools for validation of safety-critical
    173173  software, including static analysis for worst-case execution time through
    174174  abstract interpretation.  They have participated in a previous {\cerco}
    175175  event, and their insights into the requirements for precise timing analysis
    176176  are extremely relevant to the domain of {\cerco}.
    177 \item Frama-C.  The \emph{Frama-C} platform for static analysis of C source
     177\item[Frama-C]  The \emph{Frama-C} platform for static analysis of C source
    178178  code provides the context for the {\cerco} plugin which demonstrates the use
    179179  of automated cost annotations on source code.
    180 \item Rapita Systems. The \emph{RapiTime} timing analysis tool for real-time
     180\item[Rapita Systems] The \emph{RapiTime} timing analysis tool for real-time
    181181  embedded systems uses runtime instrumentation of C to identify source-level
    182182  execution costs and predict worst-cast execution time.
    183 \item PASTA.  This research group at the University of Edinburgh are the
     183\item[PASTA]  This research group at the University of Edinburgh are the
    184184  designers of the \emph{EnCore} family of configurable embedded
    185185  microprocessors.  Their \emph{ArcSim} tool offers cycle-accurate simulation
    186186  of these low-energy cores, giving significant insights into the
    187187  practicalities of precise cost analysis.
    188 \item WCET-Aware Compilation.  Dr Heiko Falk at TU Dortmund leads this
     188\item[WCET-Aware Compilation]  Dr Heiko Falk at TU Dortmund leads this
    189189  research project investigating the optimizations and compilation techniques
    190190  appropriate to the requirements of worst-case rather than average-case
    191191  timing.
    192 \item Hume/EmBounded.  Prof. Kevin Hammond at the University of St Andrews
     192\item[Hume/EmBounded]  Prof. Kevin Hammond at the University of St Andrews
    193193  leads a research team working on the quantification and certification of
    194194  resource use in concurrent real-time embedded software.
    195 \item ARM Verification Project.  Gordon, Fox and Myreen at the University of
     195\item[ARM Verification Project]  Gordon, Fox and Myreen at the University of
    196196  Cambridge have a machine-checked mathematical model of the ARM
    197197  microprocessor.  With the release of the ARM Cortex-M series of low-power
    198198  embedded processors, this is a potential application area for {\cerco}
    199199  technology in the future.
    200 \item CompCertTSO.  Sewell's group, also at the University of Cambridge, have
     200\item[CompCertTSO]  Sewell's group, also at the University of Cambridge, have
    201201  a verified C compiler treating concurrency in a relaxed memory model.  Like
    202202  {\cerco}, they have relevant experience of extending CompCert-based
    203203  verification to additional code properties.
    204 \item Artemis.  The European industry association \emph{Advanced Research \&
     204\item[Artemis]  The European industry association \emph{Advanced Research \&
    205205    Technology for Embedded Intelligence and Systems}.  We already have
    206206  contact with Artemis through the University of Bologna, which is a member of
    207207  the association.
    208 \item IMDEA Software.  Dr Boris K\"opf applies quantitative analysis of code
     208\item[IMDEA Software]  Dr Boris K\"opf applies quantitative analysis of code
    209209  execution time to evaluate potential security weaknesses by side-channel
    210210  attacks. 
    211 \item ADSIG. The \emph{ArtistDesign Special Interest Group on Embedded Systems
     211\item[ADSIG] The \emph{ArtistDesign Special Interest Group on Embedded Systems
    212212    Design} is a large consortium of experts in embedded systems design,
    213213  arising from the ARTIST Network of Excellence.
    214 \end{itemize}
    215215We propose to invite each of these groups to send participants and, if they
    216216wish, contribute a short talk on their work to the afternoon session.
    219219\section{Publication Planning}
    221 \hrule
    223 A paper about...
    225 Labelling
    227 Dependent labelling
    229 The {\cerco} Frama-C plugin
    231 Automated analysis by {\cerco} of component reaction time in Lustre
    233 Certifying compilation to object code (or is it certifying the costs?)
    235 Branch displacement and proving correctness of branch selection
    237 Structured traces
    239 The {\cerco} formalisation
    241 A survey of {\cerco} results
     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.
Note: See TracChangeset for help on using the changeset viewer.