source: Deliverables/addenda/letter.tex @ 800

Last change on this file since 800 was 800, checked in by sacerdot, 9 years ago

Half finished.

  • Property svn:executable set to *
File size: 3.8 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 on 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 to adapt 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 to be feasible. For instance, let us consider the use of
85 a simple abstract interpretation technique to improve accuracy of WCET in
86 case of caches. The analysis performed on loops associates to each memory
87 access an abstract value in the three valued domain made 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 to single
91 instructions as in our approach. Since our approach is totally parametric
92 on the function that assigns costs to target instructions, nothing needs
93 to be changed in this simple case. Realistic tools, however, also use a bound
94 on the number of loops iteration to augment precision of the analysis.
95 Moreover, they assign different costs to the first iteration of a loop and to
96 successive ones. In these cases, the problem posed to our approach consists
97 in formally verifying that bounds specified by the user (or automatically
98 inferred by some invariant generator) on the source code are preserved in the
99 target code. We believe that the labelling technique we have adopted should
100 allow us to accomodate also these invariants. In the following project
101 period we will perform a theoretical investigation of this issue and we will
102 evaluate the feasibility of the implementation of a prototype.
103
104\item The reviewers suggest to quickly outline paper-and-pencil correctness
105 proofs for each of the seven stages of the compiler in order to allow for an
106 estimation.
107
108\end{enumerate}
109
110
111Deliverable~6.2, the \emph{Plan for the Use and Dissemination of Foreground}
112was submitted as the first report of the {\cerco} project.  Following the
113scientific review of the project at the end of its first year, the reviewers
114recommended preparation of an addendum to specifically list future
115dissemination plans.  This is that addendum.
116\end{document}
117
118% LocalWords:  Sacerdoti Coen microcontroller FMCAD VSTTE TPHOLs LPAR Artefacts
Note: See TracBrowser for help on using the repository browser.