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{ |
---|
17 | INFORMATION AND COMMUNICATION TECHNOLOGIES\\ |
---|
18 | (ICT)\\ |
---|
19 | PROGRAMME\\ |
---|
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 |
---|
42 | Commitment 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 |
---|
63 | Project Acronym: {\cerco}\\ |
---|
64 | Project full title: Certified Complexity\\ |
---|
65 | Proposal/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} |
---|
72 | The first Scientific Review Report contains several valuable comments and |
---|
73 | recommendations by the scientific reviewers. We discuss here the three |
---|
74 | main recommendations, committing ourselves to taking them in account during the |
---|
75 | next 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 for the complexity of completing the formalisation, and time required |
---|
109 | to do so. |
---|
110 | |
---|
111 | We plan to depart from CompCert when carrying out our proof since we want to |
---|
112 | experiment different proof strategies where possible. In particular, we will |
---|
113 | try to exploit dependent types in our formalisation, as dependent types were |
---|
114 | avoided as a design principle in CompCert. For this reason, we have already |
---|
115 | started to formalise in Matita the intermediate languages of our compiler, |
---|
116 | recording invariants in the types themselves and rearranging some code. |
---|
117 | This should be completed at month 18. At this point we will be able to |
---|
118 | correctly state the intermediate proof statements and to estimate the |
---|
119 | complexity and effort needed for the formalisation. |
---|
120 | |
---|
121 | \item The reviewers suggest we use this estimation to compare two possible |
---|
122 | scenarios: a) proceed as planned, porting all CompCert proofs to Matita or |
---|
123 | b) port D3.1 and D4.1 to Coq and re-use the CompCert proofs. |
---|
124 | |
---|
125 | |
---|
126 | |
---|
127 | \end{enumerate} |
---|
128 | |
---|
129 | \end{document} |
---|
130 | |
---|
131 | % LocalWords: Sacerdoti Coen microcontroller FMCAD VSTTE TPHOLs LPAR Artefacts |
---|