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

\section{Conclusions}
\label{sect.conclusions}

%   Summary
%   Related work
%   Future work

In 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.
Here, `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.
`Soft real time' applications and cryptography libraries are two important classes of programs fitting this pattern.

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.
These 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.

The 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.
The techniques introduced in the compiler proof seem to be scalable, and are amenable to both imperative and functional programming languages.
Further, all techniques presented are compatible with every compiler optimisation considered by us to date.

To prove that compilers can keep track of optimisations
and induce a precise cost model on the source code, we targeted a simple
architecture that admits a cost model that is execution history independent.
The most important future work is dealing with hardware architectures
characterised by history-dependent stateful components, like caches and
pipelines. The main issue is to assign a parametric, dependent cost
to basic blocks that can be later transferred by the labelling approach to
the source code and represented in a meaningful way to the user. The dependent
labelling approach that we have studied seems a promising tool to achieve
this goal, but more work is required to provide good source level
approximations of the relevant processor state.

Other examples of future work are to improve the cost invariant
generator algorithms and the coverage of compiler optimisations, to combining
the labelling approach with the type and effect discipline of~\cite{typeffects}
to handle languages with implicit memory management, and to experiment with
our tools in the early phases of development. Larger case studies are also necessary
to evaluate the CerCo's prototype on realistic, industrial-scale programs.