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

added pages to included papers. final version.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.4/paolo.tex

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