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

Ignore:
Timestamp:
Apr 28, 2013, 4:20:54 PM (8 years ago)
Message:

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

File:
1 edited

### Legend:

Unmodified
 r3180 \usepackage{caption,subcaption} \usepackage{url} \usepackage{tikz} \usetikzlibrary{positioning,calc,patterns} \title{ INFORMATION AND COMMUNICATION TECHNOLOGIES\\ to relate the states in the two languages. \subsection{A common invariant.} This block of traces with properties is recurrent enough to merit the \subsection{A common invariant} This block of traces with properties is recurrent enough to merit the \s{matita} definition in \autoref{fig:ft_and_tlr}. We rely on the fact that all semantics from \s{RTLabs} down to object code can be expressed (cf.~\cite{?}). \subsection{The statement.} \subsection{The statement} The back-end correctness theorem proves the \s{matita} statement in \autoref{fig:statement}. The output of the a proof is actually the initial state). \section{From an unbounded to a bounded stack} \section{Dealing with the stack} Setting apart the extensional details of the proofs, a delicate point is how we deal with stack. A first minor issue is that the information we have about stack usage of each function call evolves along the back-end passes: \begin{itemize} \item in \s{RTL} we must allocate some stack for what where referenced local variables (including local arrays) in source code; \item in \s{ERTL} we add up the stack used to pass parameters that overflow the hardware registers available for the task; \item finally in \s{LTL} we add the space necessary for spilled pseudo-registers, and the stack usage of functions is finally fixed. \end{itemize} Another issue that we already mentioned above is that somewhere during the back-end pass we must pass from a semantics with no stack overflow error to one that can fail. In the following we describe the approach we have taken to these issues. \subsection{An evolving stack usage} \label{subsec:evolvingstack} The stack size we know each function must at least have is written in a field of \verb+joint+ internal functions (called \verb+joint_if_stacksize+), and as already said evolves during the back-end pass. The \emph{naïve} approach to defining semantics of these languages is to allocate the minimal necessary space for each function call, reading it from this syntactic field. The drawback is that then at each update of the stack size we must remap the data pointers in memory, moreover in a way that is dependent on the call stack. This is exemplified by the picture in \autoref{subfig:stacktight}. \begin{figure} \begin{subfigure}{.475\linewidth} \centering $\begin{tikzpicture}[thick, line cap=round, m/.style = {execute at begin node=$, execute at end node=$}] \begin{scope}[every node/.style={draw, rectangle, minimum width=1.25cm, m}, every label/.style={minimum width=0, draw=none}] \node (main src) [minimum height=.5cm] [label=left:main] {}; \node (f1 src) [above=-1pt of main src,minimum height=1cm] [label=left:f] {}; \node (g src) [above=-1pt of f1 src,minimum height=.75cm] [label=left:g] {}; \node (f2 src) [above=-1pt of g src,minimum height=1cm] [label=left:f] {}; \node (main tgt) at ([xshift=2cm]main src.south east) [anchor=south west,minimum height=1cm] [label=right:main] {}; \node (f1 tgt) [above=-1pt of main tgt,minimum height=1.25cm] [label=right:f] {}; \node (g tgt) [above=-1pt of f1 tgt,minimum height=1.5cm] [label=right:g] {}; \node (f2 tgt) [above=-1pt of g tgt,minimum height=1.25cm] [label=right:f] {}; \end{scope} \foreach \x/\off in {main/.5, f1/1, g/.75, f2/1} { \draw [densely dashed, semithick] ([yshift=1pt]\x\space src.south east) -- ([yshift=1pt]\x\space tgt.south west); \draw [densely dashed, semithick] (\x\space src.north east) -- ([yshift=\off cm]\x\space tgt.south west) coordinate (tmp) -- (tmp-|\x\space tgt.east); \fill [pattern=dots, opacity=.5] (tmp) |- (\x\space tgt.north east) |- (tmp); \path (\x\space src.east) -- node [sloped] {$\hookrightarrow$} ($(\x\space tgt.south west)!.5!(tmp)$); } \node (heading tgt) [above=.125cm of f2 tgt] {target stack}; \node (heading src) at (heading tgt-|f2 src) {source stack}; \draw [|->] (heading src) -- (heading tgt); \end{tikzpicture}$ \caption{How stack is remapped if we use tight stack spaces for each language. Dotted areas are the new parts of the local stacks.} \label{subfig:stacktight} \end{subfigure} \hfill \begin{subfigure}{.475\linewidth} \centering $\begin{tikzpicture}[thick, line cap=round, m/.style = {execute at begin node=$, execute at end node=$}] \begin{scope}[every node/.style={draw, rectangle, minimum width=1.25cm, m}, every label/.style={minimum width=0, draw=none}] \node (main src) [minimum height=1.25cm] [label=left:main] {}; \node (f1 src) [above=-1pt of main src,minimum height=1.75cm] [label=left:f] {}; \node (g src) [above=-1pt of f1 src,minimum height=1.75cm] [label=left:g] {}; \node (f2 src) [above=-1pt of g src,minimum height=1.75cm] [label=left:f] {}; \node (main tgt) at ([xshift=2cm]main src.south east) [anchor=south west,minimum height=1.25cm] [label=right:main] {}; \node (f1 tgt) [above=-1pt of main tgt,minimum height=1.75cm] [label=right:f] {}; \node (g tgt) [above=-1pt of f1 tgt,minimum height=1.75cm] [label=right:g] {}; \node (f2 tgt) [above=-1pt of g tgt,minimum height=1.75cm] [label=right:f] {}; \end{scope} \foreach \x/\off/\o in {main/.5/1, f1/1/1.25, g/.75/1.5, f2/1/1.25} { \draw [densely dashed, semithick] ([yshift=1pt]\x\space src.south east) -- ([yshift=1pt]\x\space tgt.south west); \draw [densely dashed, semithick] ([yshift=\off cm]\x\space src.south west) -- ([yshift=\off cm]\x\space tgt.south west) coordinate (tmp) -- (tmp-|\x\space tgt.east); \fill [pattern=dots, opacity=.5] (tmp) -- ([yshift=\o cm]\x\space tgt.south west) coordinate (tmp2) -| (tmp-|\x\space tgt.east) -- (tmp); \draw [densely dashed] (tmp2) -- (tmp2-|\x\space tgt.east); \fill [pattern=north east lines, opacity=.5] (tmp2) |- (\x\space tgt.north east) |- (tmp2); \path ($(\x\space src.south east)!.5!(\x\space src.east|-tmp)$) -- node {$\hookrightarrow$} ($(\x\space tgt.south west)!.5!(tmp)$); \fill [pattern=north east lines, opacity=.5] (\x\space src.west|-tmp) coordinate (tmp) |- (\x\space src.north east) |- (tmp); } \node (heading tgt) [above=.125cm of f2 tgt] {target stack}; \node (heading src) at (heading tgt-|f2 src) {source stack}; \draw [|->] (heading src) -- (heading tgt); \end{tikzpicture}$ \caption{Constant stack usage taken as a semantic parameter across languages. Shaded areas are unused parts of the stack.} \label{subfig:stacksame} \end{subfigure} \caption{Comparison between using tight stack sizes across langauges, 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 is $main, f, g, f$.} \label{fig:stacktightsame} \end{figure} We decided to take another approach, where stack sizes of each function call are a parameter to the semantics, and all passes are proved correct for the same stack sizes in source and target language, possibly with a hypothesis on these semantic'' stack sizes to be greater than the syntactic'' ones (but not all passes require it). The picture becomes thus the one in \autoref{subfig:stacksame}. The advantage is that now the data in memory does not change along the evolving of stack usage, apart from the first time we pass from separate independent stack spaces and a unique one, a situation we describe in the next subsection. \subsection{From an unbounded to a bounded stack} The way the \verb+ft_and_tlr+ is propagated is almost everwhere by means of the proof of existence of a special relation between states that is a simulation is delicate for two reasons. Firstly, while usually we can assure forward simulation of an execution step by simply depending on that step not producing an error, here is no more the case, as the stack overflow must start happening somewhere in here is no more the case, as the stack overflow error must start happening somewhere in the back-end. Secondly, merging the stack spaces of the function calls requires mapping the pointer values contained in memory. The first one, called \verb+RTL_semantics_separate+, mimics how stack is modelled in \s{RTLabs}: each function gets allocated upon call an independent stack space. in \s{RTLabs}: each function call gets allocated an independent stack space. Passing from \s{RTLabs} to this semantics involves the usual simulation relation. A peculiarity is that data pointers need not change. The middle, second one, is very similar to the two above. Called \verb+RTL_semantics_separate_overflow+, it has separate allocated stack spaces just as \verb+RTL_semantics_separate+. However the execution is defined A peculiarity is that data pointers in memory need not change. The middle, second one, is called \verb+RTL_semantics_separate_overflow+, and it has separate allocated stack spaces just as above. However the execution is defined so that if the call stack as a whole uses more space than (later) physically available, an error is issued. The actual states are identical, available (as provided by a parameter), an error is issued. The actual states are identical, and the simulation is an almost trivial 1-to-1, where the stack correctness inherited from \verb+back_end_preconditions+ can be easily put to use even 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 pieces of program counters remain the same. However in order to show a pieces of program counters remain the same, as specified in \autoref{subsec:evolvingstack}. However in order to show a forwarding simulation from \verb+RTL_semantics_separate_overflow+, one needs to remap data pointers. No further hypothesis on stack usage needs to be employed, as it is integrated in the fact that the execution step does not fail. \include{mauro} \end{document}