Changeset 3647


Ignore:
Timestamp:
Mar 13, 2017, 12:10:59 PM (4 months ago)
Author:
mulligan
Message:

Reworked section on object-code approaches to resource analysis. Lots of new citations...

Location:
Papers/jar-cerco-2017
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • Papers/jar-cerco-2017/cerco.bib

    r3643 r3647  
    2222  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/pldi/Carbonneaux0RS14},
    2323  bibsource = {dblp computer science bibliography, http://dblp.org}
     24}
     25
     26@misc { stackanalyzer,
     27  title = {{AbsInt} {Gmbh} {StackAnalyzer} stack space analysis tool},
     28  url = {https://www.absint.com/stackanalyzer/index.htm},
     29  note = {Accessed March 2017},
     30  year = {2017},
     31  key = {stackanalyzer}
     32}
     33
     34@article{Regehr:2005:ESO:1113830.1113833,
     35 author = {Regehr, John and Reid, Alastair and Webb, Kirk},
     36 title = {Eliminating Stack Overflow by Abstract Interpretation},
     37 journal = {ACM Trans. Embed. Comput. Syst.},
     38 issue_date = {November 2005},
     39 volume = {4},
     40 number = {4},
     41 month = nov,
     42 year = {2005},
     43 issn = {1539-9087},
     44 pages = {751--778},
     45 numpages = {28},
     46 url = {http://doi.acm.org/10.1145/1113830.1113833},
     47 doi = {10.1145/1113830.1113833},
     48 acmid = {1113833},
     49 publisher = {ACM},
     50 address = {New York, NY, USA},
     51 keywords = {Microcontroller, abstract interpretation, call stack, context sensitive, dataflow analysis, interrupt-driven, sensor network},
     52}
     53
     54
     55
     56@misc { bound-T,
     57  title = {bound-T {WCET} analysis tool, user guide},
     58  url = {http://www.bound-t.com/manuals/user-guide.pdf},
     59  author = {Tidorum Ltd.},
     60  note = {Accessed March 2017},
     61  year = {2017},
     62  key = {bound-T user guide}
     63}
     64
     65@misc { otawa,
     66  title = {{OTAWA} {WCET} analysis tool, user guide},
     67  url = {http://www.tracesgroup.net/otawa//doc/manuals/manual/manual.html},
     68  author = {{TRACES team}, {IRIT labs}, {University of Toulouse}},
     69  note = {Accessed March 2017},
     70  year = {2017},
     71  key = {otawa user guide}
     72}
     73
     74@misc { heptane,
     75  title = {Heptane {WCET} analysis tool},
     76  url = {https://team.inria.fr/pacap/software/heptane/},
     77  author = {{Inria} / {IRISA} project-team {PACAP}},
     78  note = {Accessed March 2017},
     79  year = {2017},
     80  key = {Heptane}
     81}
     82
     83@Inbook{Lisper2014,
     84author="Lisper, Bj{\"o}rn",
     85editor="Margaria, Tiziana
     86and Steffen, Bernhard",
     87title="SWEET -- A Tool for WCET Flow Analysis (Extended Abstract)",
     88bookTitle="Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications: 6th International Symposium, ISoLA 2014, Imperial, Corfu, Greece, October 8-11, 2014, Proceedings, Part II",
     89year="2014",
     90publisher="Springer Berlin Heidelberg",
     91address="Berlin, Heidelberg",
     92pages="482--485",
     93isbn="978-3-662-45231-8",
     94doi="10.1007/978-3-662-45231-8_38",
     95url="http://dx.doi.org/10.1007/978-3-662-45231-8_38"
     96}
     97
     98
     99@inproceedings{Cousot:1977:AIU:512950.512973,
     100 author = {Cousot, Patrick and Cousot, Radhia},
     101 title = {Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints},
     102 booktitle = {Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages},
     103 series = {POPL '77},
     104 year = {1977},
     105 location = {Los Angeles, California},
     106 pages = {238--252},
     107 numpages = {15},
     108 url = {http://doi.acm.org/10.1145/512950.512973},
     109 doi = {10.1145/512950.512973},
     110 acmid = {512973},
     111 publisher = {ACM},
     112 address = {New York, NY, USA},
     113}
     114
     115
     116
     117@inproceedings{BoneAFerdCHH2007:IFL,
     118  volume = {4449},
     119  pdf = {http://www-fp.cs.st-andrews.ac.uk/embounded/pubs/papers/ifl06.pdf},
     120  author = {Armelle Bonenfant and Christian Ferdinand and Kevin Hammond and Reinhold
     121    Heckmann},
     122  series = {Lecture Notes in Computer Science},
     123  booktitle = {Proc. Implementation of Functional Languages (IFL 2006)},
     124  title = {Worst-Case Execution Times for a Purely Functional Language},
     125  publisher = {Springer},
     126  year = {2007},
     127  bibsource = {http://www-fp.cs.st-andrews.ac.uk/hume/papers/bib.shtml?2007}
     128}
     129
     130@inproceedings{DBLP:conf/wcet/MaronezeBPP14,
     131  author    = {Andr{\'{e}} Oliveira Maroneze and
     132               Sandrine Blazy and
     133               David Pichardie and
     134               Isabelle Puaut},
     135  title     = {A Formally Verified {WCET} Estimation Tool},
     136  booktitle = {14th International Workshop on Worst-Case Execution Time Analysis,
     137               {WCET} 2014, July 8, 2014, Ulm, Germany},
     138  pages     = {11--20},
     139  year      = {2014},
     140  crossref  = {DBLP:conf/wcet/2014},
     141  url       = {http://dx.doi.org/10.4230/OASIcs.WCET.2014.11},
     142  doi       = {10.4230/OASIcs.WCET.2014.11},
     143  timestamp = {Thu, 30 Jun 2016 12:29:27 +0200},
     144  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/wcet/MaronezeBPP14},
     145  bibsource = {dblp computer science bibliography, http://dblp.org}
     146}
     147
     148@inproceedings{BoneAChenZHMWW2007:ACM,
     149  location = {Seoul, Korea},
     150  pdf = {http://www-fp.cs.st-andrews.ac.uk/embounded/pubs/papers/sac2007.pdf},
     151  author = {Armelle Bonenfant and Zezhi Chen and Kevin Hammond and Greg Michaelson and
     152    Andy Wallace and Iain Wallace},
     153  note = {To appear.},
     154  keywords = {hume,embounded},
     155  booktitle = {ACM Symposium on Applied Computing (SAC '07), Seoul, Korea, March 11-15},
     156  url = {http://www.acm.org/conferences/sac/sac2007/},
     157  title = {Towards Resource-Certified Software: A Formal Cost Model for Time and its
     158    Application to an Image-Processing Example},
     159  year = {2007},
     160  bibsource = {http://www-fp.cs.st-andrews.ac.uk/hume/papers/bib.shtml?2007}
    24161}
    25162
  • Papers/jar-cerco-2017/conclusions.tex

    r3646 r3647  
    88
    99The concrete, non-functional properties of programs---time and space usage, for example---are an important factor in the specification of a program, and therefore overall program correctness.
    10 For many application domains, it is concrete complexity that is the more critical of the two analyses.
    11 `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.
     10Indeed, for many application domains, concrete complexity is a critical component of overall correctness: `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.
    1211
    13 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.
    14 These tools possess a number of disadvantages.
     12Worst Case Execution Time (WCET) static analysers currently represent the state of the art in determining accurate concrete resource bounds for programs.
     13These tools possess a number of disadvantages, however.
    1514For instance, their analyses are at once sophisticated and opaque, with trust in the analysis devolving to trust in the complex WCET tool implementation.
    1615Further, they also require that the analysis be performed on machine code produced by a compiler, where all high-level program structure has been `compiled away', making analyses potentially hard to understand for programmers accustomed to reasoning at the source-code level.
    1716
    1817More 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.
    19 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.
     18A major challenge here is obtaining a source-level resource analysis that can compete with the precision offered by traditional WCET tools.
     19Further, how to perform this high-level analysis reliably is an open question.
    2020
    2121In this paper we have presented an approach to engineering a realistic, mildly-optimising compiler for a large fragment of the C programming language that combines the ergonomics of reasoning at the source-level, with the accuracy and precision one would expect of traditional static analyses for non-functional properties of programs.
     
    3232In particular, the CerCo verified C 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.
    3333As 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.
    34 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.
     34Further, the techniques that we have presented are not tied to any particular programming language, or to any one programming paradigm, 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
     
    5050\subsubsection{Object-code approaches}
    5151
    52 Analysis currently takes place on object code for two main reasons.
     52One existing approach to predicting concrete program execution time at the object-code level was developed in the EmBounded project~\cite{embounded}.
     53The EmBounded compiler compositionally compiles high-level Hume programs to the byte code of the Hume Abstract Machine (HAM).
     54The HAM provides strong guarantees on the maximal execution time spent for each byte code instruction, derived from empirically testing the maximum running time taken for each instruction on a given architecture~\cite{BoneAFerdCHH2007:IFL}.
     55This provides a model that is uniform, though at the expense of precision---each cost is a pessimistic upper bound---and the performance of the executed code---the byte code is interpreted compositionally.
     56Experiments were conducted using a prototype static analysis tool, and a mainstream WCET analyser, to derive upper bounds for running time of a Hume program.
     57Case studies demonstrated the feasibility of using the Hume programming language for developing resource-constrained applications~~\cite{BoneAChenZHMWW2007:ACM}.
    5358
    54 Firstly, there cannot be a uniform, precise cost model for source code
    55 instructions (or even basic blocks). During compilation, high level
    56 instructions are broken up and reassembled in context-specific ways so that
    57 identifying a fragment of object code and a single high level instruction is
    58 unfeasible.
     59The current state of the art in concrete timing analysis is represented by WCET tools, which use Abstract Interpretation~\cite{Cousot:1977:AIU:512950.512973}, control flow analyses, and detailed models of hardware to derive tight time bounds on expected program execution time.
     60See~\cite{stateart} for a survey of state-of-the-art techniques in the WCET field.
     61A variety of academic and commercial sources provide advanced WCET tooling: for example, aiT~\cite{absint}, bound-T~\cite{bound-T}, SWEET~\cite{Lisper2014}, Heptane~\cite{heptane}, and OTAWA~\cite{otawa}.
     62Unlike 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.
    5963
    60 Additionally, the control flow of the object and source code can be very
    61 different as a result of optimisations. For example, aggressive loop
    62 optimisations can completely transform source level loops.
    63 
    64 Despite the lack of a uniform, compilation- and program-independent cost model
    65 on the source language, research on the analysis of non-asymptotic execution
    66 time on high level languages assuming such a model is growing and gaining
    67 momentum.
    68 
    69 Unless such cost models are developed, the future practical impact of this
    70 research looks to be minimal. One existing approach is the EmBounded
    71 project~\cite{embounded}, which compositionally compiles high-level code to a
    72 byte code that is executed by an interpreter with guarantees on the maximal
    73 execution time spent for each byte code instruction. This provides a model
    74 that is uniform, though at the expense of precision (each cost is a pessimistic
    75 upper bound) and the performance of the executed code (the byte code is
    76 interpreted compositionally).
    77 
    78 The second reason to perform analysis on the object code is that bounding
    79 the worst case execution time of small code fragments in isolation (e.g. loop
    80 bodies) and then adding up the bounds yields very poor estimates as no
    81 knowledge of the hardware state prior to executing the fragment can be assumed.
    82 
    83 By analysing longer runs the bound obtained becomes more precise because the
    84 lack of information about the initial state has a relatively small impact.
    85 
    86 To calculate the cost of an execution, value and control flow analyses are
    87 required to bound the number of times each basic block is executed. Currently,
    88 state of the art WCET analysis tools, such as AbsInt's aiT
    89 toolset~\cite{absint}, perform these analyses on object code, where the logic
    90 of the program is harder to reconstruct and most information available at the
    91 source code level has been lost; see~\cite{stateart} for a survey.
    92 
    93 Imprecision in the analysis can lead to useless bounds. To augment precision,
    94 currently tools ask the user to provide constraints on the object code control
    95 flow, usually in the form of bounds on the number of iterations of loops or
    96 linear inequalities on them. This requires the user to manually link the source and object code, translating their assumptions on the source code (which may be
    97 wrong) to object code constraints. This task is hard and error-prone,
    98 especially in the presence of complex compiler optimisations.
    99 
    100 Traditional techniques for WCET that work on object code are also affected by
    101 another problem: they cannot be applied before the generation of the object
    102 code. Functional properties can be analysed in early development stages, while
    103 analysis of non-functional properties may come too late to avoid expensive
    104 changes to the program architecture.
    105 
    106 \paragraph{WCET, and Abstract Interpretation}
    107 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.
    108 
    109 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.
    110 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.
     64However, recent work on the CompCert verified C compiler has investigated the verification of loop-bound analysis, a subcomponent of wider WCET analyses for the Clight intermediate language~\cite{DBLP:conf/wcet/MaronezeBPP14}.
    11165Note 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.
    11266Indeed, 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
    11367As 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.
     68
     69Abstract Interpretation may also be used to derive upper bounds for stack usage (e.g.~\cite{Regehr:2005:ESO:1113830.1113833}), and abstract interpretation tools for predicting stack space usage, for example the StackAnalyzer tool~\cite{stackanalyzer}, are also commercially available.
    11470
    11571\subsubsection{High-level approaches}
     
    12985Resource Aware ML (RAML) developed by Hoffmann and Hoffmann is a first-order statically typed functional programming language.%cite
    13086RAML's sophisticated type system is able to
    131 
    132 \paragraph{Other approaches}
    133 
    134 The 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
    135 Each instruction of the HAM has a fixed concrete timing cost, derived experimentally by executing the abstract machine instruction repeatedly on target hardware and averaging.
    136 These 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.
    13787
    13888\subsection{Further work}
Note: See TracChangeset for help on using the changeset viewer.