Changeset 3630


Ignore:
Timestamp:
Mar 6, 2017, 9:09:30 PM (8 months ago)
Author:
mulligan
Message:

more on related work: mention of hume, and start of talk of raml

split related work up into grouped paragraphs

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/jar-cerco-2017/conclusions.tex

    r3629 r3630  
    4040Many different approaches to resource analysis---both asymptotic and concrete---are present within the literature.
    4141
    42 As mentioned above, the current state of the art in concrete resource analysis is represented by WCET tools such as AbsInt's aiT static analyser, which use abstract interpretation, control flow analyses, and detailed models of hardware to derive tight time bounds on expected program execution time.
    43 Unlike the approach presented in this paper, the analyses performed by mainstream WCET tools are unverified: the WCET tool itself, typically a large, complex piece of software, must become part of one's trusted code base.
    44 However, recent work has investigated the verification of loop-bound analysis, a subcomponent of wider WCET analyses, for an intermediate language of the CompCert verified C compiler.
    45 Note that this work is related but orthogonal to the work presented in this paper: our cost annotations at the C source-level are \emph{parametric} in the number of iterations of loops appearing in the source code.
    46 Indeed, to obtain a final resource analysis using our toolchain, the user must manually bound loop iterations.\footnote{This is typical for embedded and safety- or mission-critical applications, where unrestricted looping and recursion are not permitted.  See for example rule 16.2 of MISRA C 2004, which prohibits recursive function calls entirely in safety-critical code, and Nasa JPL's programming guidelines, which states all loops must have a bounded number of iterations.} %cite
    47 As a result, one could potentially imagine pairing the loop-bound analysis with our parametric cost model to reduce the amount of user interaction required when using it.
    48 
     42\paragraph{Compiler-based cost-model lifting}
    4943Perhaps the most similar piece of work to our own is the recent work by Carbonneaux \emph{et al}, who extended the CompCert verified C compiler in order to lift a concrete cost model for stack space usage back to the C source-level.
    5044Like CerCo, this work was verified within a theorem prover---in this case Coq, rather than Matita.
     
    5650Nevertheless, despite the differences, the two projects are clearly closely related.
    5751
     52\paragraph{WCET, and Abstract Interpretation}
     53As mentioned above, the current state of the art in concrete resource analysis is represented by WCET tools such as AbsInt's aiT static analyser, which use Abstract Interpretation, control flow analyses, and detailed models of hardware to derive tight time bounds on expected program execution time.
    5854
     55Unlike the approach presented in this paper, the analyses performed by mainstream WCET tools are unverified: the WCET tool itself, typically a large, complex piece of software, must become part of one's trusted code base.
     56However, recent work has investigated the verification of loop-bound analysis, a subcomponent of wider WCET analyses, for an intermediate language of the CompCert verified C compiler.
     57Note that this work is related but orthogonal to the work presented in this paper: our cost annotations at the C source-level are \emph{parametric} in the number of iterations of loops appearing in the source code.
     58Indeed, to obtain a final resource analysis using our toolchain, the user must manually bound loop iterations.\footnote{This is typical for embedded and safety- or mission-critical applications, where unrestricted looping and recursion are not permitted.  See for example rule 16.2 of MISRA C 2004, which prohibits recursive function calls entirely in safety-critical code, and Nasa JPL's programming guidelines, which states all loops must have a bounded number of iterations.} %cite
     59As a result, one could potentially imagine pairing the loop-bound analysis with our parametric cost model to reduce the amount of user interaction required when using it.
     60
     61\paragraph{Type-based analyses}
     62
     63Resource Aware ML (RAML) developed by Hoffmann and Hoffmann is a first-order statically typed functional programming language.%cite
     64RAML's sophisticated type system is able to
     65
     66\paragraph{Other approaches}
     67
     68The Hume programming language, developed as part of the EU's EmBounded project, is a typed functional programming language intended for embedded applications that is compiled to a custom abstract machine---the Hume Abstract Machine (HAM). %cite
     69Each instruction of the HAM has a fixed concrete timing cost, derived experimentally by executing the abstract machine instruction repeatedly on target hardware and averaging.
     70These costs induce a cost model on compiled Hume code, which can be used by a prototype static analysis tool, or AbsInt's aiT WCET analyser, to derive upper bounds for running time of a given Hume program.
    5971
    6072\subsection{Further work}
Note: See TracChangeset for help on using the changeset viewer.