Changeset 3194 for Deliverables

Apr 28, 2013, 4:20:54 PM (7 years ago)

more on the role of the stack in the back end pass.
moved mauro.tex as an include of paolo.tex

3 edited


  • Deliverables/D4.4/mauro.tex

    r3127 r3194  
    1 \documentclass[11pt, epsf, a4wide]{article}
    3 \usepackage{../style/cerco}
    5 \usepackage{amsfonts}
    6 \usepackage{amsmath}
    7 \usepackage{amssymb}
    8 \usepackage[english]{babel}
    9 \usepackage{graphicx}
    10 \usepackage[utf8x]{inputenc}
    11 \usepackage{listings}
    12 \usepackage[all]{xy}
    14 \newcommand{\unif}{\ensuremath{\stackrel{\scriptscriptstyle ?}{\equiv}}}
    15 \newcommand{\founif}{\ensuremath{\stackrel{\scriptscriptstyle ?}{=}}}
    16 \newcommand{\vect}[1]{\ensuremath{\stackrel{\to}{#1}}}
    17 \newcommand{\sem}[1]{\ensuremath{[\![#1]\!]}}
    18 \newcommand{\bsem}[2]{\ensuremath{[\![#1;\;#2]\!]}}
    20 \renewcommand{\verb}{\lstinline}
    21 \def\lstlanguagefiles{lst-grafite.tex}
    22 \lstset{language=Grafite}
    24 \usepackage{lscape}
    25 \usepackage{stmaryrd}
    26 \usepackage{threeparttable}
    27 \usepackage{url}
    28 \title{
    30 (ICT)\\
    31 PROGRAMME\\
    32 \vspace*{1cm}Project FP7-ICT-2009-C-243881 \cerco{}}
    34 \lstdefinelanguage{matita-ocaml}
    35   {keywords={definition,coercion,lemma,theorem,remark,inductive,record,qed,let,in,rec,match,return,with,Type,try},
    36    morekeywords={[2]whd,normalize,elim,cases,destruct},
    37    morekeywords={[3]type,of},
    38    mathescape=true,
    39   }
    41 \lstset{language=matita-ocaml,basicstyle=\small\tt,columns=flexible,breaklines=false,
    42         keywordstyle=\color{red}\bfseries,
    43         keywordstyle=[2]\color{blue},
    44         keywordstyle=[3]\color{blue}\bfseries,
    45         commentstyle=\color{green},
    46         stringstyle=\color{blue},
    47         showspaces=false,showstringspaces=false}
    49 \lstset{extendedchars=false}
    50 \lstset{inputencoding=utf8x}
    51 \DeclareUnicodeCharacter{8797}{:=}
    52 \DeclareUnicodeCharacter{10746}{++}
    53 \DeclareUnicodeCharacter{9001}{\ensuremath{\langle}}
    54 \DeclareUnicodeCharacter{9002}{\ensuremath{\rangle}}
    56 \date{}
    57 \author{}
    59 \begin{document}
    61 \thispagestyle{empty}
    63 \vspace*{-1cm}
    64 \begin{center}
    65 \includegraphics[width=0.6\textwidth]{../style/cerco_logo.png}
    66 \end{center}
    68 \begin{minipage}{\textwidth}
    69 \maketitle
    70 \end{minipage}
    72 \vspace*{0.5cm}
    73 \begin{center}
    74 \begin{LARGE}
    75 \textbf{
    76 Report n. D4.4\\
    77 ??????????????
    78 }
    79 \end{LARGE}
    80 \end{center}
    82 \vspace*{2cm}
    83 \begin{center}
    84 \begin{large}
    85 Version 1.1
    86 \end{large}
    87 \end{center}
    89 \vspace*{0.5cm}
    90 \begin{center}
    91 \begin{large}
    92 Main Authors:\\
    93 ????????????
    94 \end{large}
    95 \end{center}
    97 \vspace*{\fill}
    99 \noindent
    100 Project Acronym: \cerco{}\\
    101 Project full title: Certified Complexity\\
    102 Proposal/Contract no.: FP7-ICT-2009-C-243881 \cerco{}\\
    104 \clearpage
    105 \pagestyle{myheadings}
    106 \markright{\cerco{}, FP7-ICT-2009-C-243881}
    108 \newpage
    110 \vspace*{7cm}
    111 \paragraph{Abstract}
    112 BLA BLA BLA
    113 \newpage
    115 \tableofcontents
    117 \newpage
    119 \section{A modular approach to the correctness of each Compiler's Backend Pass}
     1\section{A modular approach to the correctness of the graph passes}
    1213An instance of the record \verb=sem_graph_params= contains all common information about
    956838The module formalizing the formal machienary we described in this document consists of about 3000 lines of
    957839Matita code. We stress the fact that this machienary proves general properties that do not depend on the
    958 specific backend compiler pass. Without this layer one would have to prove these properties each specific
    959 pass multiplying the number of Matita's lines by $n$ where $n$ is the number of backend pass.
    966 \end{document}
     840specific backend graph compiler pass.
  • Deliverables/D4.4/paolo.tex

    r3180 r3194  
    169171to relate the states in the two languages.
    171 \subsection{A common invariant.} This block of traces with properties is recurrent enough to merit the
     173\subsection{A common invariant} This block of traces with properties is recurrent enough to merit the
    172174\s{matita} definition in \autoref{fig:ft_and_tlr}. We rely on the fact
    173175that all semantics from \s{RTLabs} down to object code can be expressed
    204 \subsection{The statement.}
     206\subsection{The statement}
    205207The back-end correctness theorem proves the \s{matita} statement in
    206208\autoref{fig:statement}. The output of the a proof is
    268270actually the initial state).
    270 \section{From an unbounded to a bounded stack}
     272\section{Dealing with the stack}
     273Setting apart the extensional details of the proofs, a delicate point is how
     274we deal with stack.
     276A first minor issue is that the information we have about stack usage of
     277each function call evolves along the back-end passes:
     279 \item in \s{RTL} we must allocate some stack for what where referenced
     280 local variables (including local arrays) in source code;
     281 \item in \s{ERTL} we add up the stack used to pass parameters that overflow
     282 the hardware registers available for the task;
     283 \item finally in \s{LTL} we add the space necessary for spilled
     284 pseudo-registers, and the stack usage of functions is finally fixed.
     287Another issue that we already mentioned above is that somewhere during the
     288back-end pass we must pass from a semantics with no stack overflow error to
     289one that can fail.
     291In the following we describe the approach we have taken to these issues.
     293\subsection{An evolving stack usage}
     295The stack size we know each function must at least have is written in
     296a field of \verb+joint+ internal functions (called \verb+joint_if_stacksize+),
     297and as already said
     298evolves during the back-end pass. The \emph{naïve} approach to defining
     299semantics of these languages is to allocate the minimal necessary space for
     300each function call, reading it from this syntactic field. The drawback is
     301that then at each update of the stack size we must remap the data pointers
     302in memory, moreover in a way that is dependent on the call stack. This is
     303exemplified by the picture in \autoref{subfig:stacktight}.
     308\begin{tikzpicture}[thick, line cap=round,
     309    m/.style = {execute at begin node=$, execute at end node=$}]
     310\begin{scope}[every node/.style={draw, rectangle,
     311    minimum width=1.25cm, m}, every label/.style={minimum width=0, draw=none}]
     312    \node (main src) [minimum height=.5cm]
     313        [label=left:main] {};
     314    \node (f1 src) [above=-1pt of main src,minimum height=1cm]
     315        [label=left:f] {};
     316    \node (g src) [above=-1pt of f1 src,minimum height=.75cm]
     317        [label=left:g] {};
     318    \node (f2 src) [above=-1pt of g src,minimum height=1cm]
     319        [label=left:f] {};
     321    \node (main tgt) at ([xshift=2cm]main src.south east) [anchor=south west,minimum height=1cm]
     322        [label=right:main] {};
     323    \node (f1 tgt) [above=-1pt of main tgt,minimum height=1.25cm]
     324        [label=right:f] {};
     325    \node (g tgt) [above=-1pt of f1 tgt,minimum height=1.5cm]
     326        [label=right:g] {};
     327    \node (f2 tgt) [above=-1pt of g tgt,minimum height=1.25cm]
     328        [label=right:f] {};
     331\foreach \x/\off in {main/.5, f1/1, g/.75, f2/1} {
     332    \draw [densely dashed, semithick]
     333        ([yshift=1pt]\x\space src.south east) --
     334        ([yshift=1pt]\x\space tgt.south west);
     335    \draw [densely dashed, semithick] (\x\space src.north east) --
     336        ([yshift=\off cm]\x\space tgt.south west) coordinate (tmp)
     337        -- (tmp-|\x\space tgt.east);
     338    \fill [pattern=dots, opacity=.5] (tmp) |- (\x\space tgt.north east) |- (tmp);
     339    \path (\x\space src.east) -- node [sloped] {$\hookrightarrow$}
     340        ($(\x\space tgt.south west)!.5!(tmp)$);
     342\node (heading tgt) [above=.125cm of f2 tgt] {target stack};
     343\node (heading src) at (heading tgt-|f2 src) {source stack};
     345\draw [|->] (heading src) -- (heading tgt);
     348\caption{How stack is remapped if we use tight stack spaces for each language.
     349Dotted areas are the new parts of the local stacks.}
     356\begin{tikzpicture}[thick, line cap=round,
     357    m/.style = {execute at begin node=$, execute at end node=$}]
     358\begin{scope}[every node/.style={draw, rectangle,
     359    minimum width=1.25cm, m}, every label/.style={minimum width=0, draw=none}]
     360    \node (main src) [minimum height=1.25cm]
     361        [label=left:main] {};
     362    \node (f1 src) [above=-1pt of main src,minimum height=1.75cm]
     363        [label=left:f] {};
     364    \node (g src) [above=-1pt of f1 src,minimum height=1.75cm]
     365        [label=left:g] {};
     366    \node (f2 src) [above=-1pt of g src,minimum height=1.75cm]
     367        [label=left:f] {};
     369    \node (main tgt) at ([xshift=2cm]main src.south east) [anchor=south west,minimum height=1.25cm]
     370        [label=right:main] {};
     371    \node (f1 tgt) [above=-1pt of main tgt,minimum height=1.75cm]
     372        [label=right:f] {};
     373    \node (g tgt) [above=-1pt of f1 tgt,minimum height=1.75cm]
     374        [label=right:g] {};
     375    \node (f2 tgt) [above=-1pt of g tgt,minimum height=1.75cm]
     376        [label=right:f] {};
     379\foreach \x/\off/\o in {main/.5/1, f1/1/1.25, g/.75/1.5, f2/1/1.25} {
     380    \draw [densely dashed, semithick]
     381        ([yshift=1pt]\x\space src.south east) --
     382        ([yshift=1pt]\x\space tgt.south west);
     383    \draw [densely dashed, semithick]
     384        ([yshift=\off cm]\x\space src.south west) --
     385        ([yshift=\off cm]\x\space tgt.south west) coordinate (tmp)
     386        -- (tmp-|\x\space tgt.east);
     387    \fill [pattern=dots, opacity=.5] (tmp) --
     388        ([yshift=\o cm]\x\space tgt.south west) coordinate (tmp2) -| (tmp-|\x\space tgt.east) -- (tmp);
     389    \draw [densely dashed] (tmp2) -- (tmp2-|\x\space tgt.east);
     390    \fill [pattern=north east lines, opacity=.5]
     391        (tmp2) |- (\x\space tgt.north east) |- (tmp2);
     392    \path ($(\x\space src.south east)!.5!(\x\space src.east|-tmp)$) --
     393        node {$\hookrightarrow$}
     394        ($(\x\space tgt.south west)!.5!(tmp)$);
     395    \fill [pattern=north east lines, opacity=.5]
     396        (\x\space src.west|-tmp) coordinate (tmp) |- (\x\space src.north east) |- (tmp);
     398\node (heading tgt) [above=.125cm of f2 tgt] {target stack};
     399\node (heading src) at (heading tgt-|f2 src) {source stack};
     401\draw [|->] (heading src) -- (heading tgt);
     404\caption{Constant stack usage taken as a semantic parameter across languages.
     405Shaded areas are unused parts of the stack.}
     408\caption{Comparison between using tight stack sizes across langauges, i.e.\
     409reading how much stack is required from the function, and using the same
     410stack sizes provided as a parameter to the semantics. We suppose the call stack
     411is $main, f, g, f$.}
     415We decided to take another approach, where stack sizes of each function call
     416are a parameter to the semantics, and all passes are proved correct for the
     417same stack sizes in source and target language, possibly with a hypothesis
     418on these ``semantic'' stack sizes to be greater than the ``syntactic'' ones
     419(but not all passes require it). The picture becomes thus the one in
     420\autoref{subfig:stacksame}. The advantage is that now the data in memory does
     421not change along the evolving of stack usage, apart from the first time we
     422pass from separate independent stack spaces and a unique one, a situation
     423we describe in the next subsection.
     425\subsection{From an unbounded to a bounded stack}
    271426The way the \verb+ft_and_tlr+ is propagated is almost everwhere by means of
    272427the proof of existence of a special relation between states that is a simulation
    279434is delicate for two reasons. Firstly, while usually we can assure forward simulation
    280435of an execution step by simply depending on that step not producing an error,
    281 here is no more the case, as the stack overflow must start happening somewhere in
     436here is no more the case, as the stack overflow error must start happening somewhere in
    282437the back-end. Secondly, merging the stack spaces of the function calls requires
    283438mapping the pointer values contained in memory.
    290445The first one, called \verb+RTL_semantics_separate+, mimics how stack is modelled
    291 in \s{RTLabs}: each function gets allocated upon call an independent stack space.
     446in \s{RTLabs}: each function call gets allocated an independent stack space.
    292447Passing from \s{RTLabs} to this semantics involves the usual simulation relation.
    293 A peculiarity is that data pointers need not change.
    295 The middle, second one, is very similar to the two above. Called
    296 \verb+RTL_semantics_separate_overflow+, it has separate allocated stack spaces
    297 just as \verb+RTL_semantics_separate+. However the execution is defined
     448A peculiarity is that data pointers in memory need not change.
     450The middle, second one, is called
     451\verb+RTL_semantics_separate_overflow+, and it has separate allocated stack spaces
     452just as above. However the execution is defined
    298453so that if the call stack as a whole uses more space than (later) physically
    299 available, an error is issued. The actual states are identical,
     454available (as provided by a parameter), an error is issued. The actual states are identical,
    300455and the simulation is an almost trivial 1-to-1, where the stack correctness
    301456inherited from \verb+back_end_preconditions+ can be easily put to use even
    306461a single, bounded stack space, where moreover memory has already been granted to
    307462globals too. From this semantics down to \s{LIN}, all data in memory excluding
    308 pieces of program counters remain the same. However in order to show a
     463pieces of program counters remain the same, as specified in \autoref{subsec:evolvingstack}.
     464However in order to show a
    309465forwarding simulation from \verb+RTL_semantics_separate_overflow+, one needs to
    310466remap data pointers. No further hypothesis on stack usage needs to be employed,
    311467as it is integrated in the fact that the execution step does not fail.
  • Deliverables/D4.4/report.tex

    r3143 r3194  
    119 \includepdf[pages={-}]{mauro.pdf}
Note: See TracChangeset for help on using the changeset viewer.