Ignore:
Timestamp:
Apr 29, 2013, 6:14:15 PM (8 years ago)
Author:
tranquil
Message:

summary for D4.4, and other modifications

File:
1 edited

Legend:

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

    r3194 r3213  
    5858\lstset{extendedchars=false}
    5959\lstset{inputencoding=utf8x}
    60 \DeclareUnicodeCharacter{8797}{:=}
     60\DeclareUnicodeCharacter{8797}{:=\ }
    6161\DeclareUnicodeCharacter{10746}{++}
    6262\DeclareUnicodeCharacter{9001}{\ensuremath{\langle}}
    6363\DeclareUnicodeCharacter{9002}{\ensuremath{\rangle}}
    64 
     64\DeclareUnicodeCharacter{8230}{.\!\!.\!\!.\@\ }
     65\author{Mauro Piccolo, Claudio Sacerdoti Coen and Paolo Tranquilli\\[15pt]
     66\small Department of Computer Science and Engineering, University of Bologna\\
     67\small \verb|\{Mauro.Piccolo, Claudio.SacerdotiCoen, Paolo.Tranquilli\}@unibo.it|}
     68\title{Certifying the back end pass of the CerCo annotating compiler}
    6569\date{}
    66 \author{}
    6770
    6871\begin{document}
    69 
    70 \thispagestyle{empty}
    71 
    72 \vspace*{-1cm}
    73 \begin{center}
    74 \includegraphics[width=0.6\textwidth]{../style/cerco_logo.png}
    75 \end{center}
    76 
    77 \begin{minipage}{\textwidth}
    7872\maketitle
    79 \end{minipage}
    80 
    81 \vspace*{0.5cm}
    82 \begin{center}
    83 \begin{LARGE}
    84 \textbf{
    85 Report n. D4.4\\
    86 ??????????????
    87 }
    88 \end{LARGE}
    89 \end{center}
    90 
    91 \vspace*{2cm}
    92 \begin{center}
    93 \begin{large}
    94 Version 1.1
    95 \end{large}
    96 \end{center}
    97 
    98 \vspace*{0.5cm}
    99 \begin{center}
    100 \begin{large}
    101 Main Authors:\\
    102 ????????????
    103 \end{large}
    104 \end{center}
    105 
    106 \vspace*{\fill}
    107 
    108 \noindent
    109 Project Acronym: \cerco{}\\
    110 Project full title: Certified Complexity\\
    111 Proposal/Contract no.: FP7-ICT-2009-C-243881 \cerco{}\\
    112 
    113 \clearpage
    114 \pagestyle{myheadings}
    115 \markright{\cerco{}, FP7-ICT-2009-C-243881}
    116 
    117 \newpage
    118 
    119 \vspace*{7cm}
    120 \paragraph{Abstract}
    121 BLA BLA BLA
    122 \newpage
    123 
    124 \tableofcontents
    125 
    126 \newpage
     73\begin{abstract}
     74We present the certifying effort of the back end of the CerCo annotating
     75compiler to 8051 assembly. Apart from the usual effort needed in propagating
     76the extensional part of execution traces, additional care must be taken in
     77order to ensure a form of intensional correctness of the pass, necessary to
     78prove the lifting of computational costs correct. We concentrate here on two
     79aspects of the proof: how stack is dealt with during the pass, and how generic graph
     80language passes can be proven correct from an extensional and intensional point
     81of view.
     82\end{abstract}
    12783
    12884\section{The Back-End Correctness Proof at a Glance}
     85\label{sec:glance}
    12986
    13087The back-end part of the compiler takes an \s{RTLabs} program together with
    13188an initialising cost label and gives the assembly code to be fed to the
    13289assembler. From the semantic point of view, at this stage of the compiler,
    133 we are interested in propagating structured traces, as explained in \cite{?}.
     90we are interested in propagating structured traces, as explained in \cite{simulation}.
    13491
    13592A schema with all the back-end passes and the salient and common points of each one is the following:
     
    156113The next two passes live in the graph part of \verb+joint+, and can benefit from
    157114a generic approach to graph translation and its proof of correctness, as described
    158 in~\cite{mauro}.
     115in~\autoref{modular}.
    159116
    160117Next, a generic \verb+joint+ linearisation pass is performed to go from
     
    171128to relate the states in the two languages.
    172129
    173 \subsection{A common invariant} This block of traces with properties is recurrent enough to merit the
     130\subsection{A common invariant}
     131This block of traces with properties is recurrent enough to merit the
    174132\s{matita} definition in \autoref{fig:ft_and_tlr}. We rely on the fact
    175133that all semantics from \s{RTLabs} down to object code can be expressed
     
    201159The additional property \verb+tlr_unrpt+
    202160tells that program counters do not repeat locally (i.e.\ between two labels)
    203 in \verb+tlr+, a property needed for the soundness of the cost static analysis
    204 (cf.~\cite{?}).
     161in \verb+tlr+, a property needed for the soundness of the cost static analysis.
    205162
    206163\subsection{The statement}
     
    212169only with respect to the \s{ASM} to object code correctness
    213170\footnote{\verb+sigma+ and \verb+pol+ are what allows to maps instructions
    214 between \s{ASM} and the produced object code. This information isgained during
    215 the jump expansion pass, cf.~\cite{?}.}.
     171between \s{ASM} and the produced object code. This information is gained during
     172the jump expansion pass, cf.~\cite{policy}.}.
    216173
    217174\begin{figure}
     
    261218front-end traces, and we put it to use during the back-end pass,
    262219where we pass to a unique bounded stack space for all functions. More details
    263 will be presented in \autoref{sec:?}.
     220will be presented in \autoref{sec:stack}.
    264221
    265222The above explanation is why the back-end correctness results requires some additional preconditions
     
    270227actually the initial state).
    271228
    272 \section{Dealing with the stack}
     229\section{Dealing with the Stack}
     230\label{sec:stack}
    273231Setting apart the extensional details of the proofs, a delicate point is how
    274232we deal with stack.
     
    428386with respect to execution. There are more details involved than in a usual
    429387extensional proof, regarding the intensional preservation. The details are
    430 contained in~\cite{?}.
     388contained in~\cite{simulation}.
    431389
    432390Here we concentrate on a particular aspect that eludes the generic treatment:
     
    467425as it is integrated in the fact that the execution step does not fail.
    468426
    469 \include{mauro}
     427\input{mauro.tex}
     428
     429\bibliographystyle{plain}
     430\bibliography{report}
    470431\end{document}
Note: See TracChangeset for help on using the changeset viewer.