# Changeset 3637

Ignore:
Timestamp:
Mar 8, 2017, 12:25:31 PM (8 weeks ago)
Message:

...

Location:
Papers/jar-cerco-2017
Files:
2 edited

### Legend:

Unmodified
 r3636 Since modern compilers---as discussed previously---may compile each expression and statement occurrence in radically different ways, optimisations may change control flow, and the cost of an object code instruction may depend on the runtime state of hardware components like pipelines and caches, none of which are visible in the source code, it has not been clear how one could go about defining such a cost model. In this paper, we report on the scientific and technical contributions of the Certified Complexity (CerCo') project, an EU-funded collaboration between the Universities of Bologna, Edinburgh, and Paris 7. We first present a uniform, precise cost model for a large fragment of the C programming language---\emph{CerCo C}, which is similar to early versions of \emph{CompCert C}. In this paper, we report on the scientific and technical contributions of the Certified Complexity (CerCo') project~\cite{cerco}, an EU FET-Open funded collaboration between the Universities of Bologna, Edinburgh, and Paris 7. We first present a uniform, precise cost model for a large fragment of the C programming language---\emph{CerCo C}, which is based on early versions of \emph{CompCert C}~\cite{compcert}. To define this cost model, we have developed a technical device, which we have dubbed \emph{the labelling approach}~\cite{labelling}, a technique to implement compilers that induce cost models on source programs by a very lightweight tracking of code changes through the compilation pipeline. decouple execution time from execution history by introducing randomisation. In CerCo~\cite{cerco} we do not address this problem, optimistically assuming In CerCo we do not address this problem, optimistically assuming that improvements in low-level timing analysis or architecture will make verification feasible in the longer term.