Changeset 514
- Timestamp:
- Feb 15, 2011, 10:58:58 AM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D4.1/ITP-Paper/itp-2011.tex
r513 r514 97 97 To what extent can you trust your compiler in preserving those properties? 98 98 \end{itemize*} 99 100 99 These questions, and others like them, motivate a current `hot topic' in computer science research: \emph{compiler verification}. 101 100 So far, the field has been focused on the first and last questions only. … … 108 107 Therefore both the cost model and intensional specifications are affected by the compilation process. 109 108 110 In the EU Project CerCo (Certified Complexity) we will approach the problem 111 by developing a compiler that induces the cost model on the source code by 112 assigning to each block of high level instructions the cost associated to the 113 obtained object code. The cost model will thus be inherently non compositional, 114 but it can be extremely \emph{precise}, capturing the realistic cost. In 115 particular, we already have a prototype where no approximation of the cost 116 is provided at all. The natural applications of our approach are then in the 117 domain of hard real time programs, where the user can certify the meeting of 118 all dealines while fully exploiting the computational time, that would be 119 wasted in case of over-estimation of the costs. 109 In the current EU Project CerCo (`Certified Complexity') we approach the problem of reasoning about intensional properties of programs as follows. 110 We are currently developing a compiler that induces a cost model on the high level source code. 111 Costs are assigned to each block of high level instructions by considering the costs of the corresponding blocks of compiled object code. 112 The cost model is therefore inherently non compositional. 113 However, the model has the potential to be extremely \emph{precise}, capturing a program's \emph{realistic} cost, by taking into account, not ignoring, the compilation process. 114 A prototype compiler, where no approximation of the cost is provided, has been developed. 115 116 We believe that our approach is especially applicable to certifying real time programs. 117 Here, a user can certify that all `deadlines' are met whilst wringing as many clock cycles from the processor---using a cost model that does not over-estimate---as possible. 120 118 121 119 Other applications of our approach are in the domain of compiler verification
Note: See TracChangeset
for help on using the changeset viewer.