Changeset 3610

Mar 6, 2017, 2:13:23 PM (3 weeks ago)

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

1 edited


  • Papers/jar-cerco-2017/cerco.tex

    r3609 r3610  
    614614% ---------------------------------------------------------------------------- %
     616\section{Compiler architecture}
     619% ---------------------------------------------------------------------------- %
     620% SECTION                                                                      %
     621% ---------------------------------------------------------------------------- %
     623\section{Compiler proof}
     626% ---------------------------------------------------------------------------- %
     627% SECTION                                                                      %
     628% ---------------------------------------------------------------------------- %
     630\section{FramaC plugin}
     633% ---------------------------------------------------------------------------- %
     634% SECTION                                                                      %
     635% ---------------------------------------------------------------------------- %
     637\section{Formal development}
     640% ---------------------------------------------------------------------------- %
     641% SECTION                                                                      %
     642% ---------------------------------------------------------------------------- %
     647%   Summary
     648%   Related work
     649%   Future work
     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.
     654Worst Case Execution Time (WCET) tools currently represent the state of the art in determining accurate concrete resource bounds for programs.
     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.
     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.
     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.
Note: See TracChangeset for help on using the changeset viewer.