source: Papers/structured-traces-2012/structured-traces.tex @ 2451

Last change on this file since 2451 was 2451, checked in by mulligan, 7 years ago

Structured traces paper for Brian as per e-mail conversation yesterday.

File size: 2.4 KB
Line 
1\documentclass[a4paper, 10pt]{article}
2
3\usepackage[english]{babel}
4\usepackage[colorlinks]{hyperref}
5\usepackage{microtype}
6
7\author{Brian Campbell, Dominic P. Mulligan, Claudio Sacerdoti Coen,\\Ian Stark and Paolo Tranquilli}
8\title{Structured traces}
9\date{}
10
11\begin{document}
12
13\maketitle
14
15\begin{abstract}
16\end{abstract}
17
18%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
19% Section.                                                                    %
20%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
21\section{Introduction}
22\label{sect.introduction}
23
24Compiler correctness proofs are typically based on simulation results for local
25portions of code.  This is because compiler formalisation efforts have focussed
26their attention on providing guarantees about the extensional behaviour of
27generated code.  In contrast, we have found that invariants about the
28structure of program execution are valuable when the compiler also provides
29guarantees about intensional properties of generated code, such as execution
30time.
31
32Our compiler produces assembly code as output.   The structure of assembly program
33execution is unconstrained.  For example, an arbitrary assembly program is free
34to modify the call stack in any way that it
35chooses.  As a result, we cannot assume that the execution path of an assembly
36function call will return to the subsequent instruction after the call is
37complete. This freedom presents a problem when trying to prove that the
38execution costs of a program are correctly predicted by our compiler. Fortunately, we
39are able to preserve information from earlier stages of the compilation chain
40and use this information in the cost preservation proof.  This information is
41passed in the form of a \emph{structured trace}, a novel enrichment of
42execution traces with invariants about the structure of the program.
43
44
45
46%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
47% Section.                                                                    %
48%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
49\section{Body of paper that is complex}
50\label{sect.body}
51
52%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
53% Section.                                                                    %
54%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
55\section{Conclusion}
56\label{sect.conclusion}
57
58\end{document}
Note: See TracBrowser for help on using the repository browser.