root/Deliverables/addenda/letter.tex @ 804

% CerCo: Certified Complexity
%
% Addendum to Deliverable 6.2
%
% Plan for Dissemination and Use
% Addendum requested by project reviewers at end of year 1.
%
% Ian Stark
% 2011-05

\documentclass[11pt,a4paper]{article}
\usepackage{../style/cerco}

\hypersetup{bookmarksopenlevel=2}

\title{
INFORMATION AND COMMUNICATION TECHNOLOGIES\\
(ICT)\\
PROGRAMME\\
\vspace*{1cm}Project FP7-ICT-2009-C-243881 {\cerco}}

\date{ }
\author{}

\begin{document}
\thispagestyle{empty}

\vspace*{-1cm}
\begin{center}
\includegraphics[width=0.6\textwidth]{../style/cerco_logo.png}
\end{center}

\begin{minipage}{\textwidth}
\maketitle
\end{minipage}


\vspace*{0.5cm}
\begin{center}
\begin{LARGE}
\bf
Commitment to the Consideration of Reviewer's Reccomendations
\end{LARGE} 
\end{center}

\vspace*{2cm}
\begin{center}
\begin{large}
%Version 1.0
\end{large}
\end{center}

\vspace*{0.5cm}
\begin{center}
\begin{large}
%Main Authors:\\
%I. Stark
\end{large}
\end{center}

\vspace*{\fill}
\noindent
Project Acronym: {\cerco}\\
Project full title: Certified Complexity\\
Proposal/Contract no.: FP7-ICT-2009-C-243881 {\cerco}\\

\clearpage \pagestyle{myheadings} \markright{{\cerco}, FP7-ICT-2009-C-243881}

\tableofcontents

%\section{Premise}
The first Scientific Review Report contains several valuable comments and
recommendations by the scientific reviewers. We discuss here the three
main recommendations, committing ourselves to taking them in account during the
next project period.

\begin{enumerate}
\item The reviewers are worried by the possible limitations that derive from
 the choice of a very old architecture layout. They recommend we adopt a
 modified form of labelling such that basic complexity annotations can be
 obtained from program pieces of larger granularity.

 We will investigate this issue. In particular, the integration of some WCET
 techniques seem feasible. For instance, let us consider the use of
 a simple abstract interpretation technique to improve the accuracy of WCET in
 the presence of caches. The analysis performed on loops, associates to each memory
 access an abstract value in a three valued domain, consisting of cache-hits,
 cache misses and unknown cache behaviour. With this valuable information, we
 can assign a different cost to each single instruction: while the analysis
 is done on a large chunk of code, the cost is finally associated with single
 instructions, as in our approach. Since our approach is totally parametric
 in the function that assigns costs to target instructions, nothing needs
 to be changed in this simple case.

 Realistic tools, however, also use a bound
 on the number of loop iterations to augment precision of the analysis.
 Moreover, they assign different costs to the first iteration of a loop and to
 successive ones. In these cases, the problem posed with our approach consists
 of formally verifying that bounds specified by the user (or automatically
 inferred by some invariant generator) on the source code are preserved in the
 target code. We believe that the labelling technique we have adopted should
 allow us to also accomodate these invariants. In the following project
 period we will perform a theoretical investigation of this issue and we will
 evaluate the feasibility of the implementation of a prototype.

\item The reviewers suggest to quickly outline pencil-and-paper correctness
 proofs for each of the seven stages of the compiler in order to establish an
 estimation for the complexity of completing the formalisation, and time required
 to do so.

 We plan to depart from CompCert when carrying out our proof since we want to
 experiment different proof strategies where possible. In particular, we will
 try to exploit dependent types in our formalisation, as dependent types were
 avoided as a design principle in CompCert. For this reason, we have already
 started to formalise in Matita the intermediate languages of our compiler,
 recording invariants in the types themselves and rearranging some code.
 This should be completed at month 18. At this point we will be able to
 correctly state the intermediate proof statements and to estimate the
 complexity and effort needed for the formalisation.

\item The reviewers suggest we use this estimation to compare two possible
 scenarios: a) proceed as planned, porting all CompCert proofs to Matita or
 b) port D3.1 and D4.1 to Coq and re-use the CompCert proofs.

 We will stop and spend some time on the proposed comparison. Nevertheless,
 we remark here a few points that are important to put the project in our
 perspective.
 \begin{enumerate}
  \item CompCert proofs are not open source. All commercial uses are prohibited
   by the licence. One of the strong points of the project proposal was to
   obtain a fully open source verified compiler. This does not allow us to
   re-use at all CompCert proofs (the intermediate languages are instead put
   under GPL). Of course, we could re-discuss the open source project
   requirement, but for reasons I am not listing here we do champion open
   source, in particular for software developed using public money.
  \item CompCert is surely part of the state of the art in compiler
   certification. The proofs are very well organized and the authors are
   trying to maximise simplicity and reusal. Nevertheless, some important design
   decisions have been taken from the very beginning and have not been
   questioned estensively. Among them, the use of non executable semantics
   for intermediate languages and the use of non dependent types for the code.
   From our point of view, the CerCo project is first of all a project in
   compiler certification. Therefore, we are interested in exploring the
   design space for compiler certification. For this reason, already in the
   project proposal, we decided to start from different assumptions. In
   particular, we will favour dependent types and executable semantics.
   We are not claiming in advance that we will obtain better results than
   CompCert: what we are claiming is the interest in comparing large scale
   solutions based on different techniques. We also note that the one used
   in CompCert are very reasonable because of the choice of Coq that,
   traditionally, has favoured the use of non executable, inductive
   specification over executable ones.
  \item If we decide to depart from the choices we made in the project
   proposal and reuse CompCert proofs, this does not imply automatically that
   it is decisively better for us to switch from Matita to Coq. Indeed, the
   effort of just porting verbatim the proofs from Coq to Matita is very small.
   Indeed, as said before, our interest is in changing the proofs themselves.
   We should therefore decide if it would be easier to port verbatim the
   proofs to Matita or if it would be simpler to port the deliverables already
   done in Matita to Coq. Since we have already used some features of Matita
   not available in Coq and since we have more control over Matita, it is not
   obvious a priori what solution would be lighter for us.
  \item It is clear that one partner is interested in promoting the use of
   Matita. We think that more competition in the domain of interactive theorem
   proving will be rewarding for the community as a whole. Indeed, Coq saw
   many interesting improvements in the period when it co-existed with Lego,
   an alternative implementation of the same calculus. Moreover, some ideas
   developed for Matita have already been ported to Coq itself, and the two
   systems show alternative solutions for similar problems that are still
   under comparison (e.g. Matita's unification hints vs Coq type classes).
   One of the major struggles of EU funded research, and FET in particular,
   is the balance between innovation and stability. While the promotion and
   improvement of Matita is not a major goal for the project, we believe that
   it will provide some good side outcomes, as it happened in the past when
   Matita was used for some major formalizations and new techniques were
   develop recurring problems. This would be hardly possible using Coq since
   nobody in the CerCo team is part of the Coq developing team and has enough
   expertise to quickly modify such a large system as Coq.
 \end{enumerate}

\end{enumerate}

\end{document}

% LocalWords:  Sacerdoti Coen microcontroller FMCAD VSTTE TPHOLs LPAR Artefacts