Changeset 3610


Ignore:
Timestamp:
Mar 6, 2017, 2:13:23 PM (8 weeks ago)
Author:
mulligan
Message:

started rewriting conclusions, making it less defensive and going on the attack

File:
1 edited

Legend:

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

    r3609 r3610  
    614614% ---------------------------------------------------------------------------- %
    615615
     616\section{Compiler architecture}
     617\label{sect.compiler.architecture}
     618
     619% ---------------------------------------------------------------------------- %
     620% SECTION                                                                      %
     621% ---------------------------------------------------------------------------- %
     622
     623\section{Compiler proof}
     624\label{sect.compiler.proof}
     625
     626% ---------------------------------------------------------------------------- %
     627% SECTION                                                                      %
     628% ---------------------------------------------------------------------------- %
     629
     630\section{FramaC plugin}
     631\label{sect.framac.plugin}
     632
     633% ---------------------------------------------------------------------------- %
     634% SECTION                                                                      %
     635% ---------------------------------------------------------------------------- %
     636
     637\section{Formal development}
     638\label{sect.formal.development}
     639
     640% ---------------------------------------------------------------------------- %
     641% SECTION                                                                      %
     642% ---------------------------------------------------------------------------- %
     643
    616644\section{Conclusions}
    617645\label{sect.conclusions}
    618646
     647%   Summary
     648%   Related work
     649%   Future work
     650
     651In many application domains the intensional properties of programs---asymptotic or concrete time and space usage, for example---are an important factor in overall correctness.
     652`Soft real time' applications, and cryptography libraries, are two important classes of programs fitting this pattern.
     653
     654Worst Case Execution Time (WCET) tools currently represent the state of the art in determining accurate concrete resource bounds for programs.
     655
     656The 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.
     657The techniques introduced in the compiler proof seem to be scalable, and are amenable to both imperative and functional programming languages.
     658Further, all techniques presented are compatible with every compiler optimisation considered by us to date.
     659
     660To prove that compilers can keep track of optimisations
     661and induce a precise cost model on the source code, we targeted a simple
     662architecture that admits a cost model that is execution history independent.
     663The most important future work is dealing with hardware architectures
     664characterised by history-dependent stateful components, like caches and
     665pipelines. The main issue is to assign a parametric, dependent cost
     666to basic blocks that can be later transferred by the labelling approach to
     667the source code and represented in a meaningful way to the user. The dependent
     668labelling approach that we have studied seems a promising tool to achieve
     669this goal, but more work is required to provide good source level
     670approximations of the relevant processor state.
     671
     672Other examples of future work are to improve the cost invariant
     673generator algorithms and the coverage of compiler optimisations, to combining
     674the labelling approach with the type and effect discipline of~\cite{typeffects}
     675to handle languages with implicit memory management, and to experiment with
     676our tools in the early phases of development. Larger case studies are also necessary
     677to evaluate the CerCo's prototype on realistic, industrial-scale programs.
     678
    619679\begin{acknowledgements}
    620680\end{acknowledgements}
Note: See TracChangeset for help on using the changeset viewer.