Changeset 3628


Ignore:
Timestamp:
Mar 6, 2017, 7:37:43 PM (8 months ago)
Author:
mulligan
Message:

refinements to conclusions

File:
1 edited

Legend:

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

    r3625 r3628  
    99Intensional properties of programs---time and space usage, for example---are an important factor in the specification of a program, and therefore overall program correctness.
    1010Here, `intensional' properties can be analysed \emph{asymptotically}, or \emph{concretely}, with the latter analyses computing resource bounds in terms of clock cycles, (milli)seconds, bits transmitted, or other basal units of resource consumption, for a program execution.
    11 For many application domains, it is concrete complexity that is the more fundamental of the two analyses.
    12 `Soft real time' programs, with bounds on application response time, and libraries exporting cryptographic primitives, designed to be hardened to timing side-channel attacks, are two important classes of application fitting this pattern, for example.
     11For many application domains, it is concrete complexity that is the more critical of the two analyses.
     12`Soft real time' programs, with bounds on application response time, and libraries exporting cryptographic primitives, designed to be impervious to timing side-channel attacks, are two important classes of application fitting this pattern, for example.
    1313
    1414Worst Case Execution Time (WCET) tools currently represent the state of the art in providing static analyses that determine accurate concrete resource bounds for programs.
     
    1818
    1919More ideal would be a mechanism to `lift' a cost model from the machine code generated by a compiler, back to the source code level, where analyses could be performed in terms of source code, abstractions, and control-flow constructs written and understood by the programmer.
    20 A major challenge here is obtaining a source-level resource analysis that can compete with the precision offered by traditional WCET tools.
     20A major challenge here is obtaining a source-level resource analysis that can compete with the precision offered by traditional WCET tools, and how to perform this high-level analysis reliably.
    2121
    2222The central insight of the CerCo project is that a compiler for a substantial fragment of the C programming language can be written in a style that facilitates high-level reasoning about concrete resource usage.
    2323CerCo's resource analysis proceeds by fully embracing the compilation process and the implicit knowledge of program translation that the compiler possesses, not ignoring it.
    2424In particular, the CerCo compiler tracks the translation of phrases of high-level source code into machine code, wherein a cost measure is applied, before being reflected back through the compiler to the source-code level.
    25 Thereafter, this cost model is reflected as parametric cost assertions, embellishing the program's source code, which can be used by external reasoning tools to provide hard bounds on a program's resource consumption.
     25Thereafter, this cost model is reflected as parametric cost assertions, embellishing the program's source code, which can be used by external reasoning tools---trusted or untrusted---to provide hard bounds on a program's resource consumption.
    2626
    2727Further, the CerCo verified compiler and associated toolchain presented in this paper have demonstrated that it is indeed possible to perform static concrete resource analysis at the source level with the precision one would expect of traditional WCET tools.
    28 Indeed, for our target hardware, our parametric cost assertions are capable of producing \emph{exact} bounds on resource consumption.
     28Indeed, for the MCS-51, our compiler's target architecture, our parametric cost assertions are capable of producing \emph{exact} bounds on resource consumption.
    2929Further, 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.
    3030
    3131In CerCo, we believe that we have developed a general approach to structuring compilers for lifting cost models to the source-level.
    32 In particular, the 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.
    33 As 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.
    34 Further, 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.
     32In particular, the 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}, the compiler is still a relatively substantial piece of software.
     33As a result, the application of the techniques described herein, first described with pen-and-paper proofs, 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.
     34The techniques that we have presented are not tied to any particular programming language, and are in fact amenable to arbitrary imperative and functional programming languages.
    3535This 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
    3636
Note: See TracChangeset for help on using the changeset viewer.