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

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

Cut paper into sections, continued introduction rewrite

File size: 2.8 KB
Line 
1\section{Conclusions}
2\label{sect.conclusions}
3
4%   Summary
5%   Related work
6%   Future work
7
8In 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.
9Here, `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.
10`Soft real time' applications and cryptography libraries are two important classes of programs fitting this pattern.
11
12Worst Case Execution Time (WCET) tools currently represent the state of the art in providing static analyses that determine accurate concrete resource bounds for programs.
13These 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.
14
15The 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.
16The techniques introduced in the compiler proof seem to be scalable, and are amenable to both imperative and functional programming languages.
17Further, all techniques presented are compatible with every compiler optimisation considered by us to date.
18
19To prove that compilers can keep track of optimisations
20and induce a precise cost model on the source code, we targeted a simple
21architecture that admits a cost model that is execution history independent.
22The most important future work is dealing with hardware architectures
23characterised by history-dependent stateful components, like caches and
24pipelines. The main issue is to assign a parametric, dependent cost
25to basic blocks that can be later transferred by the labelling approach to
26the source code and represented in a meaningful way to the user. The dependent
27labelling approach that we have studied seems a promising tool to achieve
28this goal, but more work is required to provide good source level
29approximations of the relevant processor state.
30
31Other examples of future work are to improve the cost invariant
32generator algorithms and the coverage of compiler optimisations, to combining
33the labelling approach with the type and effect discipline of~\cite{typeffects}
34to handle languages with implicit memory management, and to experiment with
35our tools in the early phases of development. Larger case studies are also necessary
36to evaluate the CerCo's prototype on realistic, industrial-scale programs.
Note: See TracBrowser for help on using the repository browser.