% 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 the 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 now make a few points that we feel are important to understand 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 without doubt 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 and potential for reuse. Nevertheless, some important design
decisions have been taken from the very start of the CompCert effortlan that have not been
questioned extensively. Among them, the use of a 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, as early as in the
project proposal, we decided to start from different assumptions. In
particular, we favour dependent types and an 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 ones 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 \emph{a priori} what solution would be more convenient.
\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's 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 outcomes `on the side', as it happened in the past when
Matita was used for some major formalisations and new techniques were
developed to solve recurring problems. This would be hardly possible using Coq, since
nobody in the CerCo team is a member of the Coq development team and has the
expertise to quickly modify such a large and complex system as Coq.
\end{enumerate}
\end{enumerate}
~\\
Bologna, 13/05/2011 \hspace{6cm} The project co-ordinator.
\end{document}
% LocalWords: Sacerdoti Coen microcontroller FMCAD VSTTE TPHOLs LPAR Artefacts