Changeset 514


Ignore:
Timestamp:
Feb 15, 2011, 10:58:58 AM (6 years ago)
Author:
mulligan
Message:

more tidying

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/ITP-Paper/itp-2011.tex

    r513 r514  
    9797To what extent can you trust your compiler in preserving those properties?
    9898\end{itemize*}
    99 
    10099These questions, and others like them, motivate a current `hot topic' in computer science research: \emph{compiler verification}.
    101100So far, the field has been focused on the first and last questions only.
     
    108107Therefore both the cost model and intensional specifications are affected by the compilation process.
    109108
    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.
     109In the current EU Project CerCo (`Certified Complexity') we approach the problem of reasoning about intensional properties of programs as follows.
     110We are currently developing a compiler that induces a cost model on the high level source code.
     111Costs are assigned to each block of high level instructions by considering the costs of the corresponding blocks of compiled object code.
     112The cost model is therefore inherently non compositional.
     113However, 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.
     114A prototype compiler, where no approximation of the cost is provided, has been developed.
     115
     116We believe that our approach is especially applicable to certifying real time programs.
     117Here, 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.
    120118
    121119Other applications of our approach are in the domain of compiler verification
Note: See TracChangeset for help on using the changeset viewer.