osr-language-reasoning.tex

% !TEX root = thesis.tex

\subsection{Program Properties and Transformations}
\label{ss:osr-reasoning-and-transformations}

In this section we present a formalism based on {\em computation tree logic} (CTL) to reason about program properties and describe program transformations through rewrite rules with side conditions~\cite{Clarke86,Lacey04,Kalvala09}.

\subsubsection*{Reasoning about Program Properties}

To analyze properties of a program, we use Boolean formulas with free meta-variables that combine facts that must hold globally or at certain points of a program. Formulas can be checked against concrete programs by a {\em model checker}. For any program $\pi$ and formula $\phi$, the checker verifies whether there exists a substitution $\theta$ that binds free meta-variables with program objects so that $\theta(\phi)$ is satisfied in $\pi$. 
In this thesis, by $\cal{A}\models \phi$ we mean that $\phi$ is true in $\cal{A}$, i.e., formula $\phi$ is satisfied by structure $\cal{A}$ (or equivalently, $\cal{A}$ models $\phi$)~\cite{Clarke86}. %We use notation $\cal{A}\models_{\theta} \phi$ as a shortcut for $\cal{A}\models \theta(\phi)$. 

\noindent Two global predicates that we will use later on are ${\tt conlit}(\wc)$, which states that an expression $\wc$ is a constant literal, and ${\tt freevar}(\wx,\we)$, which holds if and only if $\wx$ is a free variable of expression $\we$.

%To support analyses based on facts that involve finite maximal paths in the control flow graph (CFG), such as liveness and dominance, we use formulas based on {\em computation tree logic} (CTL) operators~\cite{Clarke86,Lacey04,Kalvala09}. In order to introduce these operators, we need to formalize the concept of finite maximal paths first.
To support analyses based on facts that involve finite maximal paths in the control flow graph (CFG), such as liveness and dominance, we use formulas based on CTL operators. In order to introduce these operators, we need to formalize the concept of finite maximal paths first.

\begin{definition}[Set of Complete Paths] Given a control flow graph $G=(V,E)$ and an initial node $n_0\in V$, the {\em set of complete paths} $CPaths(n_0,G)$ starting at $n_0$ consists of all finite sequences $\langle n_0,n_1,\ldots,n_k\rangle$ such that $(n_i,n_{i+1})\in E$ for all $n_i$ with $i<k$, and such that there does not exist a $n_{k+1}$ such that $(n_k,n_{k+1})\in E$.
\end{definition}

\noindent Complete paths from a specified node (i.e., instruction) are thus maximal finite sequences of connected nodes through a control flow graph from an initial point to a sink node, which in our setting is unique (unless {\tt abort} instructions are present) and corresponds to the final instruction $I_n$.

First-order CTL can be used to specify properties of nodes and paths in a CFG. In particular, temporal CTL operators can be used to express properties of some or all possible future computational paths, any one of which might be an actual path that is realized. Before formalizing the temporal operators that we are going to use in the remainder of this chapter, we provide an intuitive definition for them. We say that, given a point $l$ in a program $\pi$ and two formulas $\phi$ and $\psi$, the following predicates are satisfied at $l$ if:

\begin{itemize}[parsep=0pt,topsep=3pt]
\item $\overrightarrow{AX}(\phi)$: $\phi$ holds for all immediate successors of $l$;
\item $\overrightarrow{EX}(\phi)$: $\phi$ holds for at least one immediate successor of $l$;
\item $\overrightarrow{A}(\phi~U~\psi)$: $\phi$ holds on all paths from $l$, until $\psi$ holds;
\item $\overrightarrow{E}(\phi~U~\psi)$: $\phi$ holds on at least one path from $l$, until $\psi$ holds.
\end{itemize}
\noindent Corresponding operators $\overleftarrow{AX}$ and $\overleftarrow{EX}$ are defined for immediate predecessors of $l$, while $\overleftarrow{A}$ and $\overleftarrow{E}$ refer to backward paths from $l$.

%\begin{definition}[Until Predicate]
%Given a node $n_0$ in the control flow graph $G$ and a path $p = \langle n_0,n_1,\ldots,n_k\rangle \in CPaths(n_0,G)$, we say that the predicate {\em Until}$(p,\phi,\psi)$ holds if:
%\begin{equation*}
%\exists j: 0 \le j\le k: n_j \models \psi \; \wedge \forall 0 \le i < j: n_i \models \phi
%\end{equation*}
%\end{definition}

\begin{definition}[Temporal Operators]
Given a node $n$ in the control flow graph $G=(V,E)$ of a program $\pi$, we define the following CTL {\em temporal operators} as:

%\begin{equation*}
\begin{align*}
n \models \overrightarrow{AX}(\phi) &\Longleftrightarrow \forall m: (n,m)\in E: \pi,m\models\phi \\
n \models \overrightarrow{EX}(\phi) &\Longleftrightarrow \exists m: (n,m)\in E: \pi, m\models\phi \\
n \models \overrightarrow{A}(\phi~U~\psi) &\Longleftrightarrow \forall p: p\in CPaths(n,G): Until(\pi, p,\phi,\psi) \\
n \models \overrightarrow{E}(\phi~U~\psi) &\Longleftrightarrow \exists p: p\in CPaths(n,G): Until(\pi, p,\phi,\psi) \\
\end{align*}
%\end{equation*}

%\vspace{0.5em}
\vspace{-0.5em}
\noindent where predicate $Until(\pi,p,\phi,\psi)$ holds for $p = \langle n_0,n_1,\ldots,n_k\rangle \in CPaths(n_0,G)$ if:
\vspace{-0.5em}

\begin{equation*}
\exists j: 0 \le j\le k: \pi, n_j \models \psi \; \wedge \: \forall 0 \le i < j: \pi, n_i \models \phi
\end{equation*}

\noindent Operators $\overleftarrow{AX}$, $\overleftarrow{EX}$, $\overleftarrow{A}$, and $\overleftarrow{E}$ can be defined similarly on the reverse control flow graph $\overleftarrow{G}$, which is identical to $G$ but with every edge in $\overleftarrow{E}$ flipped.
\end{definition}

\noindent Operators $A$ and $E$ are quantifiers over paths, while $X$ and $U$ path-specific quantifiers. Notice that $\phi~U~\psi$ requires that $\phi$ has to hold at least until at some node $\psi$ is satisfied: this implies that $\psi$ will be verified in the future.

\myfigure\ref{fig:osr-loc-pred} shows a number of local predicates that will be useful throughout this thesis. For instance, $\pi,l\models \ureachdef(\wx, l')$ ({\em unique reaching definition}) holds if and only if variable $\wx$ is defined at $l$ and on all paths in the control flow graph starting from an immediate successor of $l$, $\wx$ is not redefined until point $l'$ is reached, i.e., there is a unique definition of $\wx$ that reaches $l'$, and this definition is at $l$. \ureachdef's formulation relies on nested CTL operators: $\overrightarrow{AX}$ is used to encode a property for all successors of $l$, while the nested $\overrightarrow{A}$ captures all forward paths starting at such nodes.

The following definition will be useful, too:

\begin{definition}[Live Variables]
\label{de:live-var}
The set of live variables of a program $\pi$ at point $l$ is defined as:
\vspace{-1mm}
\begin{equation*}
\live(\pi,l) \triangleq \{ ~ \wx\in Var ~ | ~ \pi, l\models \islive(\wx) ~ \}
\end{equation*}
\end{definition}

%% THIS EXAMPLE IS NOT CORRECT AS WE HAVE DEFINED use() OVER VARIABLES ONLY!!!
%\begin{example}
%Available expression analysis is a forward data-flow problem. For each point in a program, an algorithm determines the set of of expressions that do not need to be recomputed. Given a program $\pi$ and an instruction $p$, we can check whether an expression $e$ is available at it using:

%\begin{equation*}
 %\pi, p \models \overleftarrow{A}(\wtrans(e)~U~\wuse(e))
%\end{equation*}

%\noindent which captures the idea that for all backward starting at $p$, a calculation of $e$ is reached before any of its constituents is possibly modified.
%\end{example}

\begin{example}
Dominance analysis is widely employed in a number of program analysis and optimization techniques. In a CFG, we say that a node $n$ dominates another node $m$ if every path from the CFG's entry node to $m$ must go through $n$. Using CTL operators, we can easily encode this property. Given a program $\pi$ as in \mydefinition\ref{de:program}, we can write:
\begin{equation*}
 \mytt{dom}(n,m) \Longleftrightarrow \pi,I_1 \models \neg E(\neg\wpoint(n)~U~\wpoint(m))
\end{equation*}

\noindent which captures the idea that there does not exist a path starting at the entry node (i.e, the first instruction in $\pi$) that reaches $m$ without reaching $n$ first.
\end{example}

\begin{figure}[!ht]
\vspace{-3mm}
\begin{small}
\begin{eqnarray*}
\wdef(\wx) & \triangleq & I_l= \texttt{x:=e} ~~ \vee ~~ I_l= \texttt{in} ~ \cdots ~ \texttt{x} \cdots \\
%                            &            & I_l= \texttt{in} ~ \cdots ~ \texttt{x} \cdots \\
                            &            & [\wx ~ \textit{is defined by instruction} ~ I_l ~ \textit{in} ~ \pi] \\
\wuse(\wx) & \triangleq & I_l= \texttt{y:=e[x]} ~ \vee  \\
                            &            & I_l= \texttt{if (e[x]) goto m} ~ \vee \ \\
                            &            & I_l= \texttt{out} ~ \cdots ~ \texttt{x} \cdots \\
                            &            & [\wx ~ \textit{is used by instruction} ~ I_l ~ \textit{in} ~ \pi] \\
\wtrans(\we) & \triangleq & I_l= \texttt{x:=e'} ~ \wedge ~ \neg\wfreevar(\wx,\we) ~ \vee \\
                            &            & I_l\neq\texttt{x:=e'} \\
%                            &            & [\we ~ \textit{is not affected by instruction} ~ I_l ~ \textit{in} ~ \pi] \\
                            &            & [\textit{no constituent of}~\we~\textit{is modified by instruction} ~ I_l ~ \textit{in} ~ \pi] \\
\islive(\wx) & \triangleq & \overleftarrow{AX}\overleftarrow{A}(\text{true} ~ U ~ \wdef(\wx)) ~ \wedge \\
                            &            & \overrightarrow{E}(\neg\wdef(\wx) ~ U ~ \wuse(\wx)) \\
                            &            & [\wx ~ \textit{is live at program point} ~ l ~ \textit{in} ~ \pi] \\
\ureachdef(\wx,l') & \triangleq & \overleftarrow{AX}\overleftarrow{A}(\neg\wdef(\wx) ~ U ~ \point(l')\wedge\wdef(\wx)) \\
                            &            & [\textit{unique definition of}~\wx~{at}~l'~\textit{reaching}~l~\textit{in} ~ \pi] \\
\stmt(I) & \triangleq & I=I_l ~~~ [I ~ \textit{is the instruction at} ~ l ~ \textit{in} ~ \pi]\\
%                 &            & [I ~ \textit{is the instruction at} ~ l ~ \textit{in} ~ \pi] \\
\point(\texttt{m}) & \triangleq & \texttt{m}=l ~~~ [\textit{program point} ~ \wm ~ \textit{is} ~ l ~ \textit{in} ~ \pi]
%                           &            & [\textit{program point} ~ \wm ~ \textit{is} ~ l ~ \textit{in} ~ \pi]
\end{eqnarray*}
\vspace{-4mm}
\end{small}
\caption{\label{fig:osr-loc-pred}Predicates expressing local properties of a point $l\in [1,n]$ in a program $\pi=\langle I_1,\ldots,I_n\rangle$, with meta-variables $\texttt{e},\texttt{e'}\in Expr$, $\texttt{x}, \texttt{y}\in Var$, and $l, \texttt{m}\in Num$.}
\end{figure}

\subsubsection*{Program Transformations}

To describe program transformations, we use rewrite rules with side conditions in a similar manner to~\cite{Lacey04,Kundu09}. We consider generalized rules that transform multiple instructions simultaneously, with side conditions drawn from CTL formulas:

\begin{definition}[Rewrite Rule]
\label{de:rewrite-rule}
A rule $T$ has the form:
\vspace{-1mm}
\begin{equation*}
\begin{array}{lllll}
T = & m_1: \hat{I}_1 \Longrightarrow \hat{I'}_1 %& m_2: I_2 \Longrightarrow I'_2
& \cdots
& m_r: \hat{I}_r \Longrightarrow \hat{I'}_r
& {\tt if} ~ \phi
\end{array}
\vspace{-1mm}
\end{equation*}
\noindent where $\forall k\in[1,r]$, $m_k$ is a meta-variable that denotes a program point, $\hat{I}_k$ and $\hat{I'}_k$ are program instructions that can contain meta-variables, and $\phi$ is a side condition that states whether the rewriting rule can be applied to the input program. We denote by $\Tau$ the set of all possible rewrite rules.
\end{definition}

\noindent An elementary example of rewrite rule with meta-variables $\wm$, $\wx$, and $\wy$ is: $$m: ~ {\tt y:=2*x} ~~ \Longrightarrow ~~ {\tt y:=x+x} ~~~ {\tt if} ~ true$$ which implements a peephole optimization based on a weak form of operator strength reduction~\cite{Cooper01}.

\noindent Rules can be applied to concrete programs by a transformation engine based on model checking: when the checker finds a substitution $\theta$ that binds free meta-variables with program objects so that $\theta(\phi)$ is satisfied in $\pi$ and $\theta(\hat{I}_k)=I_{\theta(m_k)}\in \pi$ for some $k\in[1,t]$, then $I_{\theta(m_k)}$ is replaced with $\theta(\hat{I'}_k)=I'_{\theta(m_k)}\in \pi'$, as formalized next:

\begin{definition}[Rule Semantics]
\label{de:trans-func}
Let $T$ be a rewrite rule as in \ref{de:rewrite-rule}. Transformation function $\mysem{T}: Prog\rightarrow Prog$ is defined as follows:
\vspace{-2mm}
\begin{multline*}
\forall \pi, \pi'\in Prog: \pi'=\mysem{T}(\pi) \Longleftrightarrow
\exists ~ \theta: ~ \pi\models \theta(\phi) ~ \wedge ~ \\
\forall k\in[1,r]: \theta(\hat{I}_k)=I_{\theta(m_k)}\in \pi ~ \wedge ~ \theta(\hat{I'}_k)=I'_{\theta(m_k)}\in \pi'
\end{multline*}
\end{definition}

\noindent In this thesis, we focus on transformations that do not alter the semantics of a program:

\begin{definition}[Semantics-Preserving Rules]
\label{de:sound-trans}
A rewrite rule $T$ is {\em semantics-preserving} if for any program $\pi$ it holds $\mysem{\pi}=\mysem{\pi'}$, where $\pi'=\mysem{T}(\pi)$.
\end{definition}

\noindent Examples of semantics-preserving rules for classic compiler optimizations (as proved in~\cite{Lacey02,Lacey04}) are given in \myfigure\ref{fig:sample-trans}.

\begin{figure}[ht]
\begin{center}
\begin{small}

\begin{tabularx}{0.8\textwidth}{|X|}\hline
{\bf Constant propagation} (CP):\\\hline
$m: ~ {\tt x:=e[v]} ~~ \Longrightarrow ~~ {\tt x:=e[c]}$ \\
${\tt if} ~~ \wconlit(\wc) ~ \wedge ~ m \models \overleftarrow{A}(\neg\wdef(\wv) ~ U ~ \wstmt({\tt v:=c}))$ \\\hline
\end{tabularx}

\vspace{2mm}

\begin{tabularx}{0.8\textwidth}{|X|}\hline
{\bf Dead code elimination} (DCE):\\\hline
$m: ~ {\tt x:=e} ~~ \Longrightarrow ~~ {\tt skip}$ \\
${\tt if} ~~ m \models \overrightarrow{AX} ~ \neg\overrightarrow{E}(true ~ U ~ \wuse(\wx))$ \\\hline
\end{tabularx}

\vspace{2mm}

\begin{tabularx}{0.8\textwidth}{|X|}\hline
{\bf Code hoisting} (Hoist):\\\hline
$p: ~ {\tt skip} ~~ \Longrightarrow ~~ {\tt x:=e}$ \\
$q: ~ {\tt x:=e} ~~ \Longrightarrow ~~ {\tt skip}$ \\
${\tt if} ~~ p \models \overrightarrow{A}(\neg\wuse(\wx) ~ U ~ \wpoint(q)) ~~ \wedge$ \\
$\hphantom{\texttt{if}} ~~ q \models \overleftarrow{A}((\neg\wdef(\wx)\vee\wpoint(q))\wedge \wtrans(e) ~ U ~ \wpoint(p))$ \\\hline
\end{tabularx}

\vspace{-2mm}

\end{small}
\end{center}
\caption{\label{fig:sample-trans} Rewriting rules for defining CP, DCE, and Hoist transformations.}
\end{figure}

The constant propagation (CP) rule replaces uses of a variable $v$ at a node $m$ with a constant $c$. Its side condition is satisfied when in all backward paths starting at $m$, the first definition of $v$ we encounter is always $v:=c$.

The dead code elimination (DCE) rule deletes an instruction at a node $m$ if the result of its computation will never be used later in the program's execution. As we are not interested in uses of the variable itself at $m$, in the side condition we skip past it with $AX$ and specify that there should not exist a forward path that eventually uses (i.e., reads from) the variable. 

Finally, the code hoisting (Hoist) rule moves an assignment of the form $x:=v[e]$ from a node $q$ to a node $p$ provided that two conditions are met. The first requires that in all forward paths starting at the insertion point $p$, $x$ is not used until the original location $q$ is reached. The second requires that in all backward paths starting at $q$, $x$ is not reassigned at any node other than $q$ and the constituents of $e$ are not redefined, until the insertion point $p$ is reached. %Intuitively, \wtrans$(e)$ is used to ensure that $e$ is available at $q$ after the transformation has been applied.