[pypy-svn] r77663 - pypy/extradoc/talk/pepm2011

[cfbolz at codespeak.net]

Author: cfbolz
Date: Wed Oct  6 21:13:29 2010
New Revision: 77663

Modified:
   pypy/extradoc/talk/pepm2011/paper.tex
Log:
some beautiful and rectangular but not very yellow text about the formal
description of the optimization


Modified: pypy/extradoc/talk/pepm2011/paper.tex
==============================================================================
--- pypy/extradoc/talk/pepm2011/paper.tex	(original)
+++ pypy/extradoc/talk/pepm2011/paper.tex	Wed Oct  6 21:13:29 2010
@@ -651,6 +651,9 @@
 \caption{The Operational Semantics of Simplified Traces}
 \end{figure*}
 
+XXX think of a way to format the operations to make them look distinct from
+normal text
+
 In this section we want to give a formal description of the semantics of the
 traces and of the optimizer and liken the optimization to partial evaluation.
 We concentrate on the operations for manipulating dynamically allocated objects,
@@ -679,8 +682,13 @@
 execution of an operation. The environment is a partial function from variables
 to locations and the heap is a partial function from locations to objects. Note
 that a variable can never be null in the environment, otherwise the trace would
-be malformed. We use some syntax for changing partial functions: $E[v\mapsto l]$
-denotes the environment which is just like $E$, but maps $v$ to $l$.
+be malformed. The environment could not directly map variables to object,
+because several variables can contain a pointer to the \emph{same} object. Thus
+the "indirection" is needed to express sharing.
+
+We use the following notation for updating partial functions:
+$E[v\mapsto l]$ denotes the environment which is just like $E$, but maps $v$ to
+$l$.
 
 The new operation creates a new object $(T,\mathrm{null},\mathrm{null})$, on the
 heap under a fresh location $l$ and adds the result variable to the environment,
@@ -702,6 +710,61 @@
 \subsection{Optimizing Traces}
 \label{sub:formalopt}
 
+To optimize the simple traces from the last section, we use online partial
+evaluation. The partial evaluator optimizes one operation of the trace at a
+time. Every operation in the unoptimized trace is replaced by a list of
+operations in the optimized trace. This list is empty if the operation
+can be optimized away (which hopefully happens often).
+
+The state of the optimizer is stored in an environment $E$ and a \emph{static
+heap} $S$. The environment is a partial function from variables in the
+unoptimized trace to variables in the optimized trace (which are written with a
+$\ ^*$ for clarity). The reason for introducing new variables in the optimized
+trace is that several variables that appear in the unoptimized trace can turn
+into the same variables in the optimized trace. Thus the environment of the
+optimizer serves a function similar to that of the environment in the semantics.
+
+The static heap is a partial function from $V^*$ into the
+set of static objects, which are triples of a type, and two elements of $V^*$.
+An variable $v^*$ is in the domain of the static heap $S$ as long as the
+optimizer can fully keep track of the object. The image of $v^*$ is what is
+statically known about the object stored in it, \ie its type and its fields. The
+fields of objects in the static heap are also elements of $V^*$ (or null, for
+short periods of time).
+
+When the optimizer sees a new operation, it optimistically removes it and
+assumes that the resulting object can stay static. The optimization for all
+further operations is split into two cases. One case is for when the
+involved variables are in the static heap, which means that the operation can be
+removed. The other case is that nothing is known about the variables, which
+means the operation has to be residualized.
+
+If the argument $u$ of a get operation is mapped to something in the static
+heap, the get can be performed at optimization time. Otherwise, the get
+operation needs to be emitted.
+
+If the first argument $v$ to a set operation is mapped to something in the
+static heap, then the set can performed at optimization time and the static heap
+is updated. Otherwise the set operation needs to be emitted. This needs to be
+done carefully, because the new value for the field stored in the variable $u$
+could itself be static, in which case it needs to be lifted first.
+
+I a guard is performed on a variable that is in the static heap, the type check
+can be performed at optimization time, which means the operation can be removed
+if the types match. If the type check fails statically or if the object is not
+in the static heap, the guard is put into the residual trace. This also needs to
+lift the variable on which the guard is performed.
+
+Lifting takes a variable that is potentially in the static heap and makes sure
+that it is turned into a dynamic variable. This means that operations are
+emitted that construct an object that looks like the shape described in the
+static heap, and the variable is removed from the static heap.
+
+Lifting a static object needs to recursively lift its fields. Some care needs to
+be taken when lifting a static object, because the structures described by the
+static heap can be cyclic. To make sure that the same static object is not lifted
+twice, the liftfield operation removes it from the static heap \emph{before}
+recursively lifting its fields.
 
 
 % subsection Optimizing Traces (end)
@@ -710,7 +773,6 @@
 
 \begin{figure*}
 \begin{center}
-\fbox{
 \begin{tabular}{lc}
 \emph{new} & ${\displaystyle \frac{v^{*}\,\mathrm{fresh}}{v=\mathrm{new}(T),E,S\overset{\mathrm{opt}}{\Longrightarrow}\left\langle \,\right\rangle ,E\left[v\mapsto v^{*}\right],S\left[v^{*}\mapsto\left(T,\mathrm{null,null}\right)\right]}}$\tabularnewline[3em]
 \emph{get} & ${\displaystyle \frac{E(u)\in\mathrm{dom}(S)}{v=\mathrm{get}(u,F),E,S\overset{\mathrm{opt}}{\Longrightarrow}\left\langle \,\right\rangle ,E\left[v\mapsto S(E(u))_{F}\right],S}}$\tabularnewline[3em]
@@ -722,9 +784,33 @@
  & ${\displaystyle \frac{E(v)\notin\mathrm{dom}(S)}{\mathrm{guard}(v,T),E,S\overset{\mathrm{opt}}{\Longrightarrow}\left\langle \mathrm{guard}(E\left(v\right),T)\right\rangle ,E,S}}$\tabularnewline[3em]
 \emph{lifting} & ${\displaystyle \frac{v^{*}\notin\mathrm{dom}(S)}{v^{*},S\overset{\mathrm{lift}}{\Longrightarrow}\left\langle \,\right\rangle ,S}}$\tabularnewline[3em]
  & ${\displaystyle \frac{v^{*}\in\mathrm{dom}(S),\,\left(v^{*},S\setminus\left\{ v^{*}\mapsto S\left(v^{*}\right)\right\} \right)\overset{\mathrm{liftfields}}{\Longrightarrow}\left(\mathrm{ops},S^{\prime}\right)}{v^{*},S\overset{\mathrm{lift}}{\Longrightarrow}\left\langle v^{*}=\mathrm{new}\left(T\right)\right\rangle ::ops,S^{\prime}}}$\tabularnewline[3em]
- & ${\displaystyle \frac{\left(S\left(v^{*}\right)_{L},S\right)\overset{\mathrm{lift}}{\Longrightarrow}\left(\mathrm{ops}_{L},S^{\prime}\right),\,\left(S\left(v^{*}\right)_{R},S^{\prime}\right)\overset{\mathrm{lift}}{\Longrightarrow}\left(\mathrm{ops}_{R},S^{\prime\prime}\right)}{v^{*},S\overset{\mathrm{liftfields}}{=\!=\!\Longrightarrow}\mathrm{ops}_{L}::ops_{R}::\left\langle \mathrm{set}\left(v^{*},L,S\left(v^{*}\right)_{L}\right),\,\mathrm{set}\left(v^{*},R,S\left(v^{*}\right)_{R}\right)\right\rangle ,S^{\prime}}}$\tabularnewline
+ & ${\displaystyle
+ \frac{\left(S\left(v^{*}\right)_{L},S\right)\overset{\mathrm{lift}}{\Longrightarrow}\left(\mathrm{ops}_{L},S^{\prime}\right),\,\left(S\left(v^{*}\right)_{R},S^{\prime}\right)\overset{\mathrm{lift}}{\Longrightarrow}\left(\mathrm{ops}_{R},S^{\prime\prime}\right)}{v^{*},S\overset{\mathrm{liftfields}}{=\!=\!\Longrightarrow}\mathrm{ops}_{L}::ops_{R}::\left\langle
+ \mathrm{set}\left(v^{*},L,S\left(v^{*}\right)_{L}\right),\,\mathrm{set}\left(v^{*},R,S\left(v^{*}\right)_{R}\right)\right\rangle ,S^{\prime}}}$\tabularnewline[3em]
 \end{tabular}
-}
+
+\begin{minipage}[b]{7 cm}
+\emph{Object Domains:}
+$$\setlength\arraycolsep{0.1em}
+ \begin{array}{rcll}
+    u,v,w & \in & V & \mathrm{\ variables\ in\ trace}\\
+    u^*,v^*,w^* & \in & V^* & \mathrm{\ variables\ in\ optimized\ trace}\\
+    T & \in & \mathfrak{T} & \mathrm{\ runtime\ types}\\
+    F & \in & \left\{ L,R\right\} & \mathrm{\ fields\ of\ objects}\\
+ \end{array}
+$$
+\end{minipage}
+\begin{minipage}[b]{5 cm}
+\emph{Semantic Values:}
+$$\setlength\arraycolsep{0.1em}
+ \begin{array}{rcll}
+    E & \in & V\rightharpoonup V^* & \mathrm{\ Environment}\\
+    S & \in & V^*\rightharpoonup\mathfrak{T}\times(V^*\cup \{ \mathrm{null} \})\times (V^*\cup \{ \mathrm{null}\} ) & \mathrm{\ Heap}\\
+    \\
+    \\
+ \end{array}
+$$
+\end{minipage}
 \end{center}
 \label{fig:optimization}
 \caption{Optimization Rules}