# Changeset 3443

Ignore:
Timestamp:
Feb 17, 2014, 12:09:32 PM (6 years ago)
Message:

More changes, including more missing references (including to CerCo?'s site with deliverables and papers) added. Finished up to Section 4.3.

Location:
Papers/fopara2013
Files:
2 edited

Unmodified
Added
Removed
• ## Papers/fopara2013/fopara13.bib

 r3442 author    = {Mulligan, Dominic P.  and Sacerdoti Coen, Claudio}, title     = {On the Correctness of an Optimising Assembler for the Intel MCS-51 Microprocessor}, title     = {On the Correctness of an Optimising Assembler for the {Intel MCS-51} Microprocessor}, booktitle = {CPP}, year      = {2012}, Jocelyn S{\'e}rot and Andy Wallace}, title     = {{The Embounded Project (Project Start Paper)}}, title     = {{The {EmBounded} Project (Project Start Paper)}}, booktitle = {TFP}, year      = {2005}, Claudio Sacerdoti Coen and Enrico Tassi}, title     = {The Matita Interactive Theorem Prover}, title     = {The {Matita} Interactive Theorem Prover}, booktitle = {CADE}, year      = {2011}, @misc { absint, year = {2014}, url = {http://www.absint.com/ait/}, author = {{AbsInt}}, title = {{aiT WCET} analysis tools} } @misc { cerco-deliverables, url = {http://cerco.cs.unibo.it}, title = {The {Certified Complexity} ({CerCo}) project papers and deliverables}, key = {cerco} }
• ## Papers/fopara2013/fopara13.tex

 r3442 char a[4] = {3, 2, 7, 14};  char threshold = 4; /*@ behavior stack_cost: /*@ behaviour stack_cost: ensures __stack_max <= __max(\old(__stack_max), 4+\old(__stack)); ensures __stack == \old(__stack); behavior time_cost: behaviour time_cost: ensures __cost <= \old(__cost)+(178+214*__max(1+\at(len,Pre), 0)); */ } /*@ behavior stack_cost: /*@ behaviour stack_cost: ensures __stack_max <= __max(\old(__stack_max), 6+\old(__stack)); ensures __stack == \old(__stack); behavior time_cost: behaviour time_cost: ensures __cost <= \old(__cost)+1358; */ \subsection{The (basic) labelling approach} The labelling approach is the foundational insight that underlies all the developments in CerCo. It allows the tracking of the evolution of basic blocks during the compilation process in order to propagate the cost model from the It facilitates the tracking of basic block evolution during the compilation process in order to propagate the cost model from the object code to the source code without losing precision in the process. \paragraph{Problem statement.} Given a source program $P$, we want to obtain an way to achieve that is to impose correctness and precision requirements on the source code labelling produced at the start, and to demand that the compiler to preserve these to demand that the compiler preserves these properties too. The latter requirement imposes serious limitations on the compilation strategy and optimizations: the compiler may not duplicate any code that contains label emission statements, like loop bodies. Therefore several compilation strategy and optimisations: the compiler may not duplicate any code that contains label emission statements, like loop bodies. Therefore various loop optimisations like peeling or unrolling are prevented. Moreover, precision of the object code labelling is not sufficient \emph{per se} to obtain global `while' language, all remaining compilers target realistic source languages---a pure higher order functional language and a large subset of C with pointers, gotos and all data structures---and real world of C with pointers, \texttt{goto}s and all data structures---and real world target processors---MIPS and the Intel 8051/8052 processor family. Moreover, they achieve a level of optimisation that ranges the C language and the 8051/8052 family, and does not yet implement any advanced optimisations. Its user interface, however, is the same as the other version for interoperability. In other version for interoperability purposes. In particular, the Frama-C CerCo plugin descibed in Section~\ref{sec:exploit} can work without recompilation The (trusted) CerCo compiler implements the following optimisations: cast simplification, constant propagation in expressions, liveness analysis driven spilling of registers, dead code elimination, branch displacement, and tunneling. spilling of registers, dead code elimination, branch displacement, and tunnelling. The two latter optimisations are performed by our optimising assembler \cite{correctness}. The back-end of the compiler works on three address the front-end are directly taken from CompCert, while the back-end is a redesign of a compiler from Pascal to MIPS used by Fran\c{c}ois Pottier for a course at the Ecole Polytechnique. \'{E}cole Polytechnique. The main differences in the CerCo compiler are: functional correctness for most passes. In order to complete the proof for non-functional properties, we have introduced a new, structured, form of execution traces, with the structured, form of execution trace, with the related notions for forward similarity and the intensional consequences of forward similarity. We have also introduced a unified The details on the proof techniques employed and the proof sketch can be found in the CerCo deliverables and papers. the proof sketch can be found in the CerCo deliverables and papers~\cite{cerco-deliverables}. In this section we will only hint at the correctness statement, which turned out to be more complex than expected. Other examples of future work are to improve the cost invariant generator algorithms and the coverage of compiler optimizations, to combining generator algorithms and the coverage of compiler optimisations, to combining the labelling approach with the type and effect discipline of~\cite{typeffects} to handle languages with implicit memory management, and to experiment with
Note: See TracChangeset for help on using the changeset viewer.