source: Deliverables/addenda/letter.tex @ 802

Last change on this file since 802 was 802, checked in by sacerdot, 10 years ago

...

  • Property svn:executable set to *
File size: 4.4 KB
Line 
1% CerCo: Certified Complexity
2%
3% Addendum to Deliverable 6.2
4%
5% Plan for Dissemination and Use
6% Addendum requested by project reviewers at end of year 1.
7%
8% Ian Stark
9% 2011-05
10
11\documentclass[11pt,a4paper]{article}
12\usepackage{../style/cerco}
13
14\hypersetup{bookmarksopenlevel=2}
15
16\title{
17INFORMATION AND COMMUNICATION TECHNOLOGIES\\
18(ICT)\\
19PROGRAMME\\
20\vspace*{1cm}Project FP7-ICT-2009-C-243881 {\cerco}}
21
22\date{ }
23\author{}
24
25\begin{document}
26\thispagestyle{empty}
27
28\vspace*{-1cm}
29\begin{center}
30\includegraphics[width=0.6\textwidth]{../style/cerco_logo.png}
31\end{center}
32
33\begin{minipage}{\textwidth}
34\maketitle
35\end{minipage}
36
37
38\vspace*{0.5cm}
39\begin{center}
40\begin{LARGE}
41\bf
42Commitment to the Consideration of Reviewer's Reccomendations
43\end{LARGE} 
44\end{center}
45
46\vspace*{2cm}
47\begin{center}
48\begin{large}
49%Version 1.0
50\end{large}
51\end{center}
52
53\vspace*{0.5cm}
54\begin{center}
55\begin{large}
56%Main Authors:\\
57%I. Stark
58\end{large}
59\end{center}
60
61\vspace*{\fill}
62\noindent
63Project Acronym: {\cerco}\\
64Project full title: Certified Complexity\\
65Proposal/Contract no.: FP7-ICT-2009-C-243881 {\cerco}\\
66
67\clearpage \pagestyle{myheadings} \markright{{\cerco}, FP7-ICT-2009-C-243881}
68
69\tableofcontents
70
71%\section{Premise}
72The first Scientific Review Report contains several valuable comments and
73recommendations by the scientific reviewers. We discuss here the three
74main recommendations, committing ourselves to taking them in account during the
75next project period.
76
77\begin{enumerate}
78\item The reviewers are worried by the possible limitations that derive from
79 the choice of a very old architecture layout. They recommend we adopt a
80 modified form of labelling such that basic complexity annotations can be
81 obtained from program pieces of larger granularity.
82
83 We will investigate this issue. In particular, the integration of some WCET
84 techniques seem feasible. For instance, let us consider the use of
85 a simple abstract interpretation technique to improve the accuracy of WCET in
86 the presence of caches. The analysis performed on loops, associates to each memory
87 access an abstract value in a three valued domain, consisting of cache-hits,
88 cache misses and unknown cache behaviour. With this valuable information, we
89 can assign a different cost to each single instruction: while the analysis
90 is done on a large chunk of code, the cost is finally associated with single
91 instructions, as in our approach. Since our approach is totally parametric
92 in the function that assigns costs to target instructions, nothing needs
93 to be changed in this simple case.
94
95 Realistic tools, however, also use a bound
96 on the number of loop iterations to augment precision of the analysis.
97 Moreover, they assign different costs to the first iteration of a loop and to
98 successive ones. In these cases, the problem posed with our approach consists
99 of formally verifying that bounds specified by the user (or automatically
100 inferred by some invariant generator) on the source code are preserved in the
101 target code. We believe that the labelling technique we have adopted should
102 allow us to also accomodate these invariants. In the following project
103 period we will perform a theoretical investigation of this issue and we will
104 evaluate the feasibility of the implementation of a prototype.
105
106\item The reviewers suggest to quickly outline pencil-and-paper correctness
107 proofs for each of the seven stages of the compiler in order to establish an
108 estimation of the complexity and time required to complete the formalization.
109
110 We plan to perform the proof departing from CompCert since we want to
111 experiment different proof strategies were possible. In particular, we will
112 try to exploit dependent types in our formalization. Dependent types were
113 avoided as a design principle in CompCert. For this reason, we have already
114 started to formalize in Matita the intermediate languages of our compiler
115 recording invariants in the types themselves and rearranging some code.
116 This should be completed at month 18. At this point we will be able to
117 correctly state the intermediate proof statements and to estimate the
118 complexity and effort for the formalization.
119
120\item The reviewers suggest to use this estimation to compare two possible
121 scenarios: a) proceed as planned, porting all CompCert proofs to Matita or
122 b) port D3.1 and D4.1 to Coq and re-use the CompCert proofs.
123
124
125
126\end{enumerate}
127
128\end{document}
129
130% LocalWords:  Sacerdoti Coen microcontroller FMCAD VSTTE TPHOLs LPAR Artefacts
Note: See TracBrowser for help on using the repository browser.