Changeset 2609 for Papers/itp-2013/ccexec.tex
- Timestamp:
- Feb 6, 2013, 1:56:01 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Papers/itp-2013/ccexec.tex
r2607 r2609 93 93 architectures and caches. 94 94 95 In the European Project CerCo (Certified Complexity~\footnote{\url{http://cerco.cs.unibo.it}}) we are certifying a labelling approach based compiler for a large subset of C to95 In the European Project CerCo (Certified Complexity~\footnote{\url{http://cerco.cs.unibo.it}})~\cite{cerco} we are certifying a labelling approach based compiler for a large subset of C to 96 96 8051 object code. The compiler is 97 97 moderately optimizing and implements a compilation chain that is largely 98 inspired to that of CompCert~\cite{compcert }. Compared to work done in~\cite{easylabelling}, the main novely and source of difficulties is due to the presence98 inspired to that of CompCert~\cite{compcert1,compcert2}. Compared to work done in~\cite{easylabelling}, the main novely and source of difficulties is due to the presence 99 99 of function calls. Surprisingly, the addition of function calls require a 100 100 rivisitation of the proof technique given in~\cite{easylabelling}. In … … 172 172 This correctness property is called in the litterature a forward simulation 173 173 and is sufficient for correctness when the target language is 174 deterministic~\cite{ leroy}.174 deterministic~\cite{compcert3}. 175 175 We also require a stronger, non-functional preservation property: after each 176 176 pass all basic blocks must start with an emission statement, and all labels … … 890 890 precise cost model on the source code in order to establish non-functional 891 891 properties of programs on an high level language. Traditional certifications 892 of compilers, like~\cite{compcert ,python}, only explicitly prove preservation892 of compilers, like~\cite{compcert2,piton}, only explicitly prove preservation 893 893 of the functional properties via forward simulations. 894 894
Note: See TracChangeset
for help on using the changeset viewer.