# Changeset 1847 for Deliverables/D1.2

Ignore:
Timestamp:
Mar 15, 2012, 3:04:50 PM (9 years ago)
Message:

More changes to presentation based on comments

Location:
Deliverables/D1.2/Presentations
Files:
3 edited

Unmodified
Added
Removed
• ## Deliverables/D1.2/Presentations/WP4-dominic.tex

 r1844 \begin{frame} \frametitle{Backend intermediate languages II} \vspace{-1em} \begin{small} \begin{tabbing} \quad \=\,\quad \=\ \\ \textsf{RTLabs}\\ \> $\downarrow$ \> copy propagation ($\times$) \\ \> $\downarrow$ \> instruction selection (\checkmark) \\ \> $\downarrow$ \> change of memory models in compiler (\checkmark) \\ \> $\downarrow$ \> copy propagation \color{red}{$\times$} \\ \> $\downarrow$ \> instruction selection \color{green}{{\checkmark}} \\ \> $\downarrow$ \> change of memory models in compiler \color{green}{{\checkmark}} \\ \textsf{RTL}\\ \> $\downarrow$ \> constant propagation ($\times$) \\ \> $\downarrow$ \> calling convention made explicit (\checkmark) \\ \> $\downarrow$ \> layout of activation records (\checkmark) \\ \> $\downarrow$ \> constant propagation \color{red}{$\times$} \\ \> $\downarrow$ \> calling convention made explicit \color{green}{{\checkmark}} \\ \> $\downarrow$ \> layout of activation records \color{green}{{\checkmark}} \\ \textsf{ERTL}\\ \> $\downarrow$ \> register allocation and spilling (\checkmark) \\ \> $\downarrow$ \> dead code elimination (\checkmark) \\ \> $\downarrow$ \> register allocation and spilling \color{green}{{\checkmark}} \\ \> $\downarrow$ \> dead code elimination \color{green}{{\checkmark}} \\ \textsf{LTL}\\ \> $\downarrow$ \> function linearisation (\checkmark) \\ \> $\downarrow$ \> branch compression ($\times$) \\ \> $\downarrow$ \> function linearisation \color{green}{{\checkmark}} \\ \> $\downarrow$ \> branch compression \color{red}{$\times$} \\ \textsf{LIN}\\ \> $\downarrow$ \> relabeling (\checkmark) \\ \> $\downarrow$ \> relabeling \color{green}{{\checkmark}} \\ \textsf{ASM} \end{tabbing} \begin{column}[b]{0.5\linewidth} \centering In C: \begin{lstlisting} int main(int argc, char** argv) { \begin{column}[b]{0.5\linewidth} \centering In ASM: \begin{lstlisting} ... main: ... \begin{itemize} \item Question: where do we put cost labels to capture execution costs? Where do we put cost labels to capture execution costs? \item Proof obligations complicated by panoply of labels Doesn't work well with \texttt{g(h() + 2 + f())} \item Is \texttt{cost\_label2} ever reached? \texttt{some\_function()} must terminate! Is \texttt{cost\_label2} ever reached? \item \texttt{some\_function()} may not return correctly \begin{frame} \frametitle{Structured traces I} \begin{itemize} \item We introduced a notion of structured traces' \item These are intended to statically capture the (good) execution traces of a program \item To borrow a slogan: they are the computational content of a well-formed program's execution' \item Come in two variants: inductive and coinductive \item Inductive captures program execution traces that eventually halt, coinductive ones that diverge \end{itemize} \end{frame} \begin{frame} \frametitle{Structured traces II} \begin{itemize} \item I focus on the inductive variety, as used the most (for now) in the backend \item In particular, used in the proof that static and dynamic cost computations coincide \item Traces preserved by backend compilation, initially created at RTL \item This will be explained later \end{itemize} \end{frame} \begin{frame} \frametitle{Structured traces III} \begin{itemize} \item Central insight is that program execution is always in the body of some function (from \texttt{main} onwards) \item A well formed program must have labels appearing at certain spots \item Similarly, the final instruction executed when executing a function must be a \texttt{RET} \item Execution must then continue in body of calling function, at correct place \item These invariants, and others, are crystalised in the specific syntactic form of a structured trace \end{itemize} \end{frame} \begin{frame} \frametitle{Recursive structure of good' execution} Structure captured by structured traces: \begin{center} \includegraphics[scale=0.33]{recursive_structure.png} \begin{frame} \frametitle{Structured traces I} \begin{itemize} \item We introduced a notion of structured traces' \item These are intended to statically capture the (good) execution traces of a program \item To borrow a slogan: they are the `computational content of a well-formed program's execution' \item Come in two variants: inductive and coinductive \item Inductive captures program execution traces that eventually halt, coinductive ones that diverge \end{itemize} \end{frame} \begin{frame} \frametitle{Structured traces II} \begin{itemize} \item I focus on the inductive variety, as used the most (for now) in the backend \item In particular, used in the proof that static and dynamic cost computations coincide \item Traces preserved by backend compilation, initially created at RTL \item This will be explained later \end{itemize} \end{frame} \begin{frame} \frametitle{Structured traces III} \begin{itemize} \item Central insight is that program execution is always in the body of some function (from \texttt{main} onwards) \item A well formed program must have labels appearing at certain spots \item Similarly, the final instruction executed when executing a function must be a \texttt{RET} \item Execution must then continue in body of calling function, at correct place \item These invariants, and others, are crystalised in the specific syntactic form of a structured trace \end{itemize} \end{frame} \begin{frame} \frametitle{Static and dynamic costs I} \begin{itemize} \item Given a structured trace, we can compute its associated cost \item In previous slide, cost of trace is cost assigned to \texttt{label\_1} + \texttt{label\_2} + \texttt{label\_3} (+ \texttt{label\_4}) \item This is the \emph{static} cost of a program execution
• ## Deliverables/D1.2/Presentations/recursive_structure.svg

 r1843 version="1.1" inkscape:version="0.48.2 r9819" inkscape:export-filename="/home/dpm/Documents/Projects/Cerco/cerco/Deliverables/D1.2/Presentations/recursive_structure.jpg.png" inkscape:export-filename="/home/dpm/Documents/Projects/Cerco/cerco/Deliverables/D1.2/Presentations/recursive_structure.png" inkscape:export-xdpi="90" inkscape:export-ydpi="90" sodipodi:docname="New document 2"> sodipodi:docname="recursive_structure.svg"> inkscape:pageshadow="2" inkscape:zoom="0.6" inkscape:cx="400" inkscape:cx="130" inkscape:cy="300" inkscape:current-layer="layer1" inkscape:groupmode="layer"> Start style="font-size:36px;font-style:italic;font-variant:normal;font-weight:normal;font-stretch:normal;font-family:LMRoman17;-inkscape-font-specification:LMRoman17 Italic;fill:#000000">Start Final style="font-size:36px;font-style:italic;font-variant:normal;font-weight:normal;font-stretch:normal;font-family:LMRoman17;-inkscape-font-specification:LMRoman17 Italic;fill:#000000">Final Start style="font-size:36px;font-style:italic;font-variant:normal;font-weight:normal;font-stretch:normal;font-family:LMRoman17;-inkscape-font-specification:LMRoman17 Italic;fill:#000000">Start Final style="font-size:36px;font-style:italic;font-variant:normal;font-weight:normal;font-stretch:normal;font-family:LMRoman17;-inkscape-font-specification:LMRoman17 Italic;fill:#000000">Final Start style="font-size:36px;font-style:italic;font-variant:normal;font-weight:normal;font-stretch:normal;font-family:LMRoman17;-inkscape-font-specification:LMRoman17 Italic;fill:#000000">Start Final style="font-size:36px;font-style:italic;font-variant:normal;font-weight:normal;font-stretch:normal;font-family:LMRoman17;-inkscape-font-specification:LMRoman17 Italic;fill:#000000">Final CALL style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-family:LMMono12;-inkscape-font-specification:LMMono12;font-size:36px;fill:#000000">CALL CALL style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-family:LMMono12;-inkscape-font-specification:LMMono12;font-size:36px;fill:#000000">CALL RET style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-family:LMMono12;-inkscape-font-specification:LMMono12;font-size:36px;fill:#000000">RET RET RET label label2 label label3 label style="font-size:36px;font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-family:LMMono8;-inkscape-font-specification:LMMono8;fill:#000000">label1 label style="font-size:36px;font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-family:LMMono12;-inkscape-font-specification:LMMono12;fill:#000000">label4 RET RET
Note: See TracChangeset for help on using the changeset viewer.