Changeset 3638


Ignore:
Timestamp:
Mar 8, 2017, 12:34:21 PM (7 weeks ago)
Author:
mulligan
Message:

moved big chunk of material out of intro, into conclusions

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

Legend:

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

    r3632 r3638  
    3838\label{subsect.related.work}
    3939
    40 Many different approaches to resource analysis---both asymptotic and concrete---are present within the literature.
     40Many different approaches to resource analysis---asymptotic and concrete, working at low- and high-levels of abstraction---are present within the literature.
     41We now survey these approaches.
     42
     43\subsubsection{Object-code approaches}
     44
     45Analysis currently takes place on object code for two main reasons.
     46
     47Firstly, there cannot be a uniform, precise cost model for source code
     48instructions (or even basic blocks). During compilation, high level
     49instructions are broken up and reassembled in context-specific ways so that
     50identifying a fragment of object code and a single high level instruction is
     51unfeasible.
     52
     53Additionally, the control flow of the object and source code can be very
     54different as a result of optimisations. For example, aggressive loop
     55optimisations can completely transform source level loops.
     56
     57Despite the lack of a uniform, compilation- and program-independent cost model
     58on the source language, research on the analysis of non-asymptotic execution
     59time on high level languages assuming such a model is growing and gaining
     60momentum.
     61
     62Unless such cost models are developed, the future practical impact of this
     63research looks to be minimal. One existing approach is the EmBounded
     64project~\cite{embounded}, which compositionally compiles high-level code to a
     65byte code that is executed by an interpreter with guarantees on the maximal
     66execution time spent for each byte code instruction. This provides a model
     67that is uniform, though at the expense of precision (each cost is a pessimistic
     68upper bound) and the performance of the executed code (the byte code is
     69interpreted compositionally).
     70
     71The second reason to perform analysis on the object code is that bounding
     72the worst case execution time of small code fragments in isolation (e.g. loop
     73bodies) and then adding up the bounds yields very poor estimates as no
     74knowledge of the hardware state prior to executing the fragment can be assumed.
     75
     76By analysing longer runs the bound obtained becomes more precise because the
     77lack of information about the initial state has a relatively small impact.
     78
     79To calculate the cost of an execution, value and control flow analyses are
     80required to bound the number of times each basic block is executed. Currently,
     81state of the art WCET analysis tools, such as AbsInt's aiT
     82toolset~\cite{absint}, perform these analyses on object code, where the logic
     83of the program is harder to reconstruct and most information available at the
     84source code level has been lost; see~\cite{stateart} for a survey.
     85
     86Imprecision in the analysis can lead to useless bounds. To augment precision,
     87currently tools ask the user to provide constraints on the object code control
     88flow, usually in the form of bounds on the number of iterations of loops or
     89linear 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
     90wrong) to object code constraints. This task is hard and error-prone,
     91especially in the presence of complex compiler optimisations.
     92
     93Traditional techniques for WCET that work on object code are also affected by
     94another problem: they cannot be applied before the generation of the object
     95code. Functional properties can be analysed in early development stages, while
     96analysis of non-functional properties may come too late to avoid expensive
     97changes to the program architecture.
     98
     99\paragraph{WCET, and Abstract Interpretation}
     100As 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.
     101
     102Unlike 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.
     103However, 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.
     104Note 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.
     105Indeed, 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
     106As 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.
     107
     108\subsubsection{High-level approaches}
    41109
    42110\paragraph{Compiler-based cost-model lifting}
     
    49117Carbonneaux \emph{at al} lift their model from the assembly generated by the CompCert compiler; we must go further, to the level of machine code, in order to lift our timing cost model, necessitating the development of a verified assembler.
    50118Nevertheless, despite these differences, the two projects are clearly closely related.
    51 
    52 \paragraph{WCET, and Abstract Interpretation}
    53 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.
    54 
    55 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.
    56 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.
    57 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.
    58 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
    59 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.
    60119
    61120\paragraph{Type-based analyses}
  • Papers/jar-cerco-2017/introduction.tex

    r3637 r3638  
    9595when components have been specified but not implemented, as modularity means
    9696that it is enough to specify the non-functional behaviour of missing components.
    97 
    98 \subsection{Project context and approach}
    99 
    100 Formal methods for verifying functional properties of programs have now reached
    101 such a level of maturity and automation that their adoption is slowly
    102 increasing in production environments.
    103 
    104 For safety critical code, it is becoming commonplace to combine rigorous
    105 software engineering methodologies and testing with static analyses, taking the
    106 strengths of each and mitigating their weaknesses. Of particular interest are
    107 open frameworks for the combination of different formal methods, where the
    108 programs can be progressively specified and enriched with new safety
    109 guarantees: every method contributes knowledge (e.g. new invariants) that
    110 can be built upon by other analysis methods.
    111 
    112 The outlook for verification of non-functional properties of programs (time
    113 spent, memory used, energy consumed) is bleaker. In most cases, verifying that
    114 real-time systems meet their deadlines is done by simply performing many runs
    115 of the system and timing their execution, computing the maximum time and adding
    116 an empirical safety margin, claiming the result to be a bound for the WCET of
    117 the program.
    118 
    119 Formal methods and software to statically analyse the WCET of programs exist,
    120 but they often produce bounds that are too pessimistic to be useful. Recent
    121 advances in hardware architecture have focused on improving average case
    122 performance, not predictability of the worst case.
    123 
    124 Execution time is becoming increasingly dependent on execution history and the
    125 internal state of hardware components like pipelines and caches. Multi-core
    126 processors and non-uniform memory models are drastically reducing the
    127 possibility of performing static analysis in isolation, because programs are
    128 less and less time-composable. Clock-precise hardware models are necessary for
    129 static analysis, and obtaining them is becoming harder due to the increased
    130 sophistication of hardware design.
    131 
    132 The need for reliable real-time systems and programs is increasing, and there
    133 is pressure from the research community for the introduction of hardware with
    134 more predictable behaviour, which would be more suitable for static analysis.
    135 One example, being investigated by the Proartis project~\cite{proartis}, is to
    136 decouple execution time from execution history by introducing randomisation.
    137 
    138 In CerCo we do not address this problem, optimistically assuming
    139 that improvements in low-level timing analysis or architecture will make
    140 verification feasible in the longer term.
    141 
    142 Instead, the main objective of our work is to bring together static analysis of
    143 functional and non-functional properties, which in the current state of the art
    144 are independent activities with limited exchange of information: while the
    145 functional properties are verified on the source code, the analysis of
    146 non-functional properties is performed on object code to exploit clock-precise
    147 hardware models.
    148 
    149 \subsection{Current object code methods}
    150 
    151 Analysis currently takes place on object code for two main reasons.
    152 
    153 Firstly, there cannot be a uniform, precise cost model for source code
    154 instructions (or even basic blocks). During compilation, high level
    155 instructions are broken up and reassembled in context-specific ways so that
    156 identifying a fragment of object code and a single high level instruction is
    157 unfeasible.
    158 
    159 Additionally, the control flow of the object and source code can be very
    160 different as a result of optimisations. For example, aggressive loop
    161 optimisations can completely transform source level loops.
    162 
    163 Despite the lack of a uniform, compilation- and program-independent cost model
    164 on the source language, research on the analysis of non-asymptotic execution
    165 time on high level languages assuming such a model is growing and gaining
    166 momentum.
    167 
    168 Unless such cost models are developed, the future practical impact of this
    169 research looks to be minimal. One existing approach is the EmBounded
    170 project~\cite{embounded}, which compositionally compiles high-level code to a
    171 byte code that is executed by an interpreter with guarantees on the maximal
    172 execution time spent for each byte code instruction. This provides a model
    173 that is uniform, though at the expense of precision (each cost is a pessimistic
    174 upper bound) and the performance of the executed code (the byte code is
    175 interpreted compositionally).
    176 
    177 The second reason to perform analysis on the object code is that bounding
    178 the worst case execution time of small code fragments in isolation (e.g. loop
    179 bodies) and then adding up the bounds yields very poor estimates as no
    180 knowledge of the hardware state prior to executing the fragment can be assumed.
    181 
    182 By analysing longer runs the bound obtained becomes more precise because the
    183 lack of information about the initial state has a relatively small impact.
    184 
    185 To calculate the cost of an execution, value and control flow analyses are
    186 required to bound the number of times each basic block is executed. Currently,
    187 state of the art WCET analysis tools, such as AbsInt's aiT
    188 toolset~\cite{absint}, perform these analyses on object code, where the logic
    189 of the program is harder to reconstruct and most information available at the
    190 source code level has been lost; see~\cite{stateart} for a survey.
    191 
    192 Imprecision in the analysis can lead to useless bounds. To augment precision,
    193 currently tools ask the user to provide constraints on the object code control
    194 flow, usually in the form of bounds on the number of iterations of loops or
    195 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
    196 wrong) to object code constraints. This task is hard and error-prone,
    197 especially in the presence of complex compiler optimisations.
    198 
    199 Traditional techniques for WCET that work on object code are also affected by
    200 another problem: they cannot be applied before the generation of the object
    201 code. Functional properties can be analysed in early development stages, while
    202 analysis of non-functional properties may come too late to avoid expensive
    203 changes to the program architecture.
    20497
    20598\subsection{The CerCo approach}
Note: See TracChangeset for help on using the changeset viewer.