# Changeset 3628

Ignore:
Timestamp:
Mar 6, 2017, 7:37:43 PM (3 weeks ago)
Message:

refinements to conclusions

File:
1 edited

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

 r3625 Intensional properties of programs---time and space usage, for example---are an important factor in the specification of a program, and therefore overall program correctness. Here, 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. For many application domains, it is concrete complexity that is the more fundamental of the two analyses. 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. For many application domains, it is concrete complexity that is the more critical of the two analyses. 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. Worst Case Execution Time (WCET) tools currently represent the state of the art in providing static analyses that determine accurate concrete resource bounds for programs. More 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. A major challenge here is obtaining a source-level resource analysis that can compete with the precision offered by traditional WCET tools. A 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. The 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. CerCo's resource analysis proceeds by fully embracing the compilation process and the implicit knowledge of program translation that the compiler possesses, not ignoring it. In 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. 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. Thereafter, 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. Further, 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. Indeed, for our target hardware, our parametric cost assertions are capable of producing \emph{exact} bounds on resource consumption. Indeed, for the MCS-51, our compiler's target architecture, our parametric cost assertions are capable of producing \emph{exact} bounds on resource consumption. Further, 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. In CerCo, we believe that we have developed a general approach to structuring compilers for lifting cost models to the source-level. 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. 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. 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. 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}, the compiler is still a relatively substantial piece of software. As 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. The 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. This 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
Note: See TracChangeset for help on using the changeset viewer.