source: Papers/jar-cerco-2017/conclusions.tex @ 3615

Last change on this file since 3615 was 3615, checked in by boender, 3 years ago

Moved paper structure comments to their relevant sections

File size: 2.8 KB
[3615]1% Conclusions
[3613]2%   Summary
3%   Related work
4%   Future work
[3613]9In many application domains the 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.
10Here, `intensional' properties can be analysed \emph{asymptotically}, or \emph{concretely}, with the latter computing resource bounds in terms of clock cycles, seconds, bits transmitted, or other concrete resource measures, for a program execution.
11`Soft real time' applications and cryptography libraries are two important classes of programs fitting this pattern.
13Worst Case Execution Time (WCET) tools currently represent the state of the art in providing static analyses that determine accurate concrete resource bounds for programs.
14These tools however possess a number of disadvantages: for instance, they require that the analysis be performed on machine code produced by a compiler, where all high-level program structure has been `compiled away', rather than permitting an analysis at the source-code level.
16The CerCo verified compiler and associated toolchain has demonstrated that it is possible to perform static time and space analysis at the source level without losing accuracy, reducing the trusted code base and reconciling the study of functional and non-functional properties of programs.
17The techniques introduced in the compiler proof seem to be scalable, and are amenable to both imperative and functional programming languages.
18Further, all techniques presented are compatible with every compiler optimisation considered by us to date.
20To prove that compilers can keep track of optimisations
21and induce a precise cost model on the source code, we targeted a simple
22architecture that admits a cost model that is execution history independent.
23The most important future work is dealing with hardware architectures
24characterised by history-dependent stateful components, like caches and
25pipelines. The main issue is to assign a parametric, dependent cost
26to basic blocks that can be later transferred by the labelling approach to
27the source code and represented in a meaningful way to the user. The dependent
28labelling approach that we have studied seems a promising tool to achieve
29this goal, but more work is required to provide good source level
30approximations of the relevant processor state.
32Other examples of future work are to improve the cost invariant
33generator algorithms and the coverage of compiler optimisations, to combining
34the labelling approach with the type and effect discipline of~\cite{typeffects}
35to handle languages with implicit memory management, and to experiment with
36our tools in the early phases of development. Larger case studies are also necessary
37to evaluate the CerCo's prototype on realistic, industrial-scale programs.
Note: See TracBrowser for help on using the repository browser.