# Changeset 3222 for Deliverables/D4.4/paolo.tex

Ignore:
Timestamp:
Apr 30, 2013, 11:45:00 AM (8 years ago)
Message:

added pages to included papers. final version.

File:
1 edited

### Legend:

Unmodified
 r3213 \usepackage{listings} \usepackage[all]{xy} % \usepackage{supertabular} \newcommand{\clap}[1]{\hbox to 0pt{\hss#1\hss}} \small Department of Computer Science and Engineering, University of Bologna\\ \small \verb|\{Mauro.Piccolo, Claudio.SacerdotiCoen, Paolo.Tranquilli\}@unibo.it|} \title{Certifying the back end pass of the CerCo annotating compiler} \title{Certifying the back-end pass of the CerCo annotating compiler} \date{} \maketitle \begin{abstract} We present the certifying effort of the back end of the CerCo annotating compiler to 8051 assembly. Apart from the usual effort needed in propagating We present the certifying effort of the back-end of the CerCo annotating compiler to 8051 assembly. Apart from the proofs needed for propagating the extensional part of execution traces, additional care must be taken in order to ensure a form of intensional correctness of the pass, necessary to prove the lifting of computational costs correct. We concentrate here on two prove that the lifting of computational costs is correct. We concentrate here on two aspects of the proof: how stack is dealt with during the pass, and how generic graph language passes can be proven correct from an extensional and intensional point Care must be taken in dealing with the stack. The back-end pass produces a \emph{stack model}: the amount of stack needed by each function (\verb+stack_m+), together with the maximal usable stack (\verb+max_stack+, $2^{16}$ minus the size occupied by globals). together with the maximal usable stack (\verb+max_stack+, $2^{16}$ minus the size occupied by global variables). While programs in the front end do not fail for stack overflow, the stack information is lifted to source much in the same ways as time consumption information, \label{subfig:stacksame} \end{subfigure} \caption{Comparison between using tight stack sizes across langauges, i.e.\ \caption{Comparison between using tight stack sizes across languages, i.e.\ reading how much stack is required from the function, and using the same stack sizes provided as a parameter to the semantics. We suppose the call stack \subsection{From an unbounded to a bounded stack} The way the \verb+ft_and_tlr+ is propagated is almost everwhere by means of The way the \verb+ft_and_tlr+ is propagated is almost everywhere by means of the proof of existence of a special relation between states that is a simulation with respect to execution. There are more details involved than in a usual The third one, defined as \verb+RTL_semantics_unique+, switches to a semantics with a single, bounded stack space, where moreover memory has already been granted to globals too. From this semantics down to \s{LIN}, all data in memory excluding global variables too. From this semantics down to \s{LIN}, all data in memory excluding pieces of program counters remain the same, as specified in \autoref{subsec:evolvingstack}. However in order to show a