Changeset 3621

Mar 6, 2017, 4:19:05 PM (3 weeks ago)

refinements to summary, starting work on related work section

1 edited


  • Papers/jar-cerco-2017/conclusions.tex

    r3617 r3621  
    2727Further, as the CerCo compiler's lifting of the cost model is fully verified in Matita, the trusted code base is minimised---one no longer need rely on the correctness of a WCET tool to obtain a trustworthy analysis.
    29 Lastly, the techniques introduced in the compiler proof seem to be scalable, and are amenable to both imperative and functional programming languages.
    30 Further, all techniques presented in this paper are compatible with all compiler optimisation considered by us so far.
     29Lastly, a note on the generality of the techniques presented herein.
     30The CerCo compiler itself is a lightly-optimising compiler for a large subset of the C programming language, and whilst not as aggressive in its optimisation passes as commercial and open-source C compilers, such as \texttt{gcc}, \texttt{clang}, or \texttt{icc}, is a substantial piece of software.
     31As a result, the application of the techniques described in this paper to the full CerCo compiler is, in our view, already evidence of their scalability, and we see no reason why these techniques could not be applied to a more aggressively optimising compiler, given that none of our techniques are tied to any particular choice of intermediate language or set of optimisations.
     32Further, the techniques that we have presented are not tied to the C programming language, and are in fact amenable to arbitrary imperative and functional programming languages.
     33This last claim is bolstered by a pen-and-paper proof of the correctness of the labelling approach applied to a `toy' compiler for an applicative language. %cite
    3235\subsection{Related work}
     38Many different approaches to resource analysis---both asymptotic and concrete---are present within the literature.
     40As 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 uses abstract interpretation, coupled with faithful, detailed models of hardware, to derive tight time bounds on expected program execution time.
     41Further, 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.
    3544\subsection{Further work}
Note: See TracChangeset for help on using the changeset viewer.