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 the CompCert proofs to Matita or |
---|
123 | b) port D3.1 and D4.1 to Coq and re-use the CompCert proofs. |
---|
124 | |
---|
125 | We will stop and spend some time on the proposed comparison. Nevertheless, |
---|
126 | we now make a few points that we feel are important to understand our |
---|
127 | perspective. |
---|
128 | \begin{enumerate} |
---|
129 | \item CompCert proofs are not open source. All commercial uses are prohibited |
---|
130 | by the licence. One of the strong points of the project proposal was to |
---|
131 | obtain a fully open source verified compiler. This does not allow us to |
---|
132 | re-use at all CompCert proofs (the intermediate languages are instead put |
---|
133 | under GPL). Of course, we could re-discuss the open source project |
---|
134 | requirement, but for reasons I am not listing here we do champion open |
---|
135 | source, in particular for software developed using public money. |
---|
136 | \item CompCert is without doubt part of the state of the art in compiler |
---|
137 | certification. The proofs are very well organized and the authors are |
---|
138 | trying to maximise simplicity and and potential for reuse. Nevertheless, some important design |
---|
139 | decisions have been taken from the very start of the CompCert effortlan that have not been |
---|
140 | questioned extensively. Among them, the use of a non-executable semantics |
---|
141 | for intermediate languages and the use of non-dependent types for the code. |
---|
142 | From our point of view, the CerCo project is first of all a project in |
---|
143 | compiler certification. Therefore, we are interested in exploring the |
---|
144 | design space for compiler certification. For this reason, as early as in the |
---|
145 | project proposal, we decided to start from different assumptions. In |
---|
146 | particular, we favour dependent types and an executable semantics. |
---|
147 | We are not claiming in advance that we will obtain better results than |
---|
148 | CompCert: what we are claiming is the interest in comparing large scale |
---|
149 | solutions based on different techniques. We also note that the ones used |
---|
150 | in CompCert are very reasonable because of the choice of Coq that, |
---|
151 | traditionally, has favoured the use of non-executable, inductive |
---|
152 | specification over executable ones. |
---|
153 | \item If we decide to depart from the choices we made in the project |
---|
154 | proposal and reuse CompCert proofs, this does not imply automatically that |
---|
155 | it is decisively better for us to switch from Matita to Coq. Indeed, the |
---|
156 | effort of just porting verbatim the proofs from Coq to Matita is very small. |
---|
157 | Indeed, as said before, our interest is in changing the proofs themselves. |
---|
158 | We should therefore decide if it would be easier to port verbatim the |
---|
159 | proofs to Matita or if it would be simpler to port the deliverables already |
---|
160 | done in Matita to Coq. Since we have already used some features of Matita |
---|
161 | not available in Coq and since we have more control over Matita, it is not |
---|
162 | obvious \emph{a priori} what solution would be more convenient. |
---|
163 | \item It is clear that one partner is interested in promoting the use of |
---|
164 | Matita. We think that more competition in the domain of interactive theorem |
---|
165 | proving will be rewarding for the community as a whole. Indeed, Coq saw |
---|
166 | many interesting improvements in the period when it co-existed with Lego, |
---|
167 | an alternative implementation of the same calculus. Moreover, some ideas |
---|
168 | developed for Matita have already been ported to Coq itself, and the two |
---|
169 | systems show alternative solutions for similar problems that are still |
---|
170 | under comparison (e.g. Matita's unification hints vs. Coq's type classes). |
---|
171 | One of the major struggles of EU funded research, and FET in particular, |
---|
172 | is the balance between innovation and stability. While the promotion and |
---|
173 | improvement of Matita is not a major goal for the project, we believe that |
---|
174 | it will provide some good outcomes `on the side', as it happened in the past when |
---|
175 | Matita was used for some major formalisations and new techniques were |
---|
176 | developed to solve recurring problems. This would be hardly possible using Coq, since |
---|
177 | nobody in the CerCo team is a member of the Coq development team and has the |
---|
178 | expertise to quickly modify such a large and complex system as Coq. |
---|
179 | \end{enumerate} |
---|
180 | |
---|
181 | \end{enumerate} |
---|
182 | |
---|
183 | ~\\ |
---|
184 | |
---|
185 | Bologna, 13/05/2011 \hspace{6cm} The project co-ordinator. |
---|
186 | |
---|
187 | \end{document} |
---|
188 | |
---|
189 | % LocalWords: Sacerdoti Coen microcontroller FMCAD VSTTE TPHOLs LPAR Artefacts |
---|