\section{Static Transaction}
\label{Se:StaticTransactions}
A program-analysis tool for understanding transactional software must be able
to distinguish between program statements that occur within a dynamic
transaction and those that do not. Because a dynamic transaction is a runtime
notion, a static-analysis tool cannot work with dynamic transactions directly.
For the static analysis of transactional software, we introduce the
notion of a \emph{static transaction}.
A static transaction is defined in terms of {\em valid paths} in the program. 
\begin{definition}
\label{De:ValidPath}
A path in a program's interprocedural control-flow graph (ICFG) is valid if it
respects the fact that when a procedure finishes, it returns to the site of
the most recent call \cite{kn:SP81}.
\end{definition}
Note that a given valid path may not actually be executable, e.g., due to
correlations in the path's branch-conditions.

As we did for dynamic transactions, we present the definition of a static
transaction both for (1) programs that make use of structured software
transactions, and for (2) programs that make use of unstructured software
transactions.
\begin{definition}
\label{De:AtomicStaticXact}
A static transaction consists of all program statements that lie on a 
valid path within an {\em \atomic} block. A static transaction is represented
by the program locations that demarcate the block.
\end{definition}

\begin{definition}
\label{De:staticxact}
\begin{sloppypar}
A static transaction consists of all program statements that lie on a valid
path between a matched pair of \emph{\begxact} and \emph{\endxact} statements.
A static transaction is represented by the pair of program locations for the 
{\em \begxact} and {\em \endxact} statements.
\end{sloppypar}
\end{definition}

A static transaction represents a set of dynamic transactions, namely, those
that start at the \begxact\ point and end at the \endxact\ point. Our analyses
use sets of static transactions to over-approximate sets of dynamic
transactions. We next show, for both structured and unstructured transactions,
how the sets of static transactions are determined.

% TODO : NAK
%\section{Determining Static Transactions}
%Each of our static analyses are based on the knowledge of a program's static
%transactions. Because static transactions are not dependent on thread
%interleavings, we are able to apply analysis techniques for sequential
%programs to multithreaded programs. To do this, we augment the program with a
%``supermain'' function. The supermain function nondeterministically branches
%to the entry point of each thread. When a function's control-flow graph starts
%a thread, we convert this program statement into a ``noop''. This effectively
%converts the multithreaded program into a sequential one. Later analyes are
%extensions to the analysis that determines a program's static transactions.
%Therefore, the rest of our analyses are also able to reason about
%multithreaded program's using sequential techniques.

%It is interesting to note that the we analyze a multithreaded program
%in a sequential setting. We are able to do this because we are not reasoning
%about properties of the program that are affected by thread interleavings. To
%model the concurrent program as a sequential one, we annotate the program with
%a ``supermain'' function.


\subsection{Structured Software Transactions}
\label{Se:staticAtomic}
It is trivial to determine a program's static transactions when
the programming language supports \atomic\ blocks. In standard 
compiler infrastructures, the parser will check for correct syntax of
the program and return an abstract syntax tree (AST). The parser can be
augmented to record the location of each atomic block in the program. With this
information, the node set of a static transaction consists of all program
nodes that are within the scope of its \atomic\ block and the program nodes of
all functions (transitively) called from within that scope.


\subsection{Unstructured Software Transactions}
\label{Se:staticNonAtomic}
To analyze traditional lock-based code in a transactional setting, we treat
each lock-acquire and lock-release operation as a \begxact\ and \endxact,
respectively \cite{rajwar:tlr:asplos:2002,chung:common-case:hpca:2006}.
This adds considerable difficulty to determining the static transactions of the
program---we cannot rely on the parser to verify each software transaction has
a matching begin and end. Additionally, we cannot use the reachability
relation on the programs's ICFG to determine a programs's static transactions.
In this section,  we present an interprocedural dataflow analysis to address
these problems. Namely, the analysis (1) verifies correct usage of 
the transactional primitives, and (2) determines the static transactions of a
program.


Because converted lock-based programs are allowed to specify the beginning and
ending of a software transaction separately, we must take care not to make the
detection of static transactions undecidable. The problem is that we are close
to having to contend with two interleaved sets of matched parentheses, one
(valid paths) for modeling the control flow of the program, and one for
modeling the matched \begxact\ and \endxact\ statements.
Reps \cite{DBLP:journals/toplas/Reps00} proved that a program-analysis problem
that must meet the matching constraints of
two interleaved (i.e., shuffled) sets of matched parentheses is undecidable
in the general case. To sidestep this undecidability result, we restrict our
programming model to allow transactions to be nested to only a finite depth.
For the purposes of presenting our analyses, we set the nesting depth to be
zero. That is, we will not consider nested transactions in this paper. With a
finite nesting depth, we can verify correct usage of the software-transaction
primitives using a property automaton
\cite{DBLP:conf/osdi/EnglerCCH00,DBLP:conf/ccs/ChenW02}. The property
automaton for checking correct usage of the \begxact\ and \endxact\ primitives
with nesting depth of zero is shown in \figref{Property}. It is trivial to
expand this automaton to allow for any finite number of nested transactions.

\input{PropertyAutomaton}

Property automata are useful for answering reachability questions, like
incorrect usage of the transactional primitives. This is often done by
creating a dataflow-analysis problem in which the automaton's transition
relation (often denoted by $\delta$) is used as a state transformer. (More
precisely, each transformer is $\delta$ restricted to one or more alphabet
symbols.) \tableref{Transformers} shows the transformers that model the
property automaton from \figref{Property} (for now ignore the bracketed
symbols in the subscripts). In \tableref{Transformers}, the transformer states
model the states of the property automaton. To reduce clutter,
transitions to the $err$ state are not modeled explicitly; instead, they are
modeled by a state $q$ on the left-hand side being disconnected from every
state on the right-hand side. This represents an implicit transition from $q$
to the $err$ state. In \tableref{Transformers}, the top row displays the
transformers that correspond to the program statements. Transformer $\tB{b}$
corresponds to a \begxact\ statement, transformer $\tE{e}$ corresponds to an
\endxact\ statement, and transformer $\tid$ corresponds to all other program
statements. The second row shows the transformers that can arise through
transformer composition.

\begin{sloppypar}
To verify correct usage of the \begxact\ and \endxact\ primitives, we solve an
interprocedural dataflow-analysis problem. We associate dataflow transformers
with each edge in the ICFG. To make clear the distinction between dataflow
transformers and transformers that model the transition relation of an
automaton, we will refer to the latter as \delts, and use the symbol $\tau$
for dataflow transformers.
\end{sloppypar}

To determine correct usage of the transactional primitives, our
dataflow-analysis transformers ($\tau$-transformers) are sets of \delts\ that
model the property automaton.
%The \delts\ are relations on the states on
%the property automaton. Therefore, the dataflow-analysis transformers could be
%implemented as just one \delt. However, later analyses will annotate the
%\delts\ with additional dataflow information. By using sets of \delts, each
%\delt\ has only one annotation.
Associated with each edge in the ICFG is a
singleton set containing the \delt\ that encodes the effect of abstractly
executing that edge (with respect to the property automaton).
%
%
Composition of two transformers $\tau_1$ and $\tau_2$ involves taking the cross product of
the two sets of \delts, and performing relational composition on the resulting pairs of
\delts. We denote relational composition by ``$\xJoin$'' (e.g., $\tid \xJoin \tB{b}
= \tB{b}$ and $\tB{b} \xJoin \tE{e} = \tBE$). 

To solve the dataflow-analysis problem, we use standard techniques
\cite{kn:SP81} to compute a fixpoint. The result of this computation is a set
of \delts\ for each node in the ICFG, where a node's set contains the
meet-over-all-paths (MOP) value along valid paths from program entry to that
node. To check for correct usage of the transactional primitives, one need
only verify that $\wexit \subseteq \{\tid,\tBE\}$, where $\wexit$ is the
dataflow transformer associated with the exit node of the {\tt main} function.

\input{Transformers}

We extend the $\tau$-transformers to collect additional information about the
program. Sagiv et al. showed how relations can be annotated with ``values''
that satisfy certain algebraic properties \cite{kn:SRH96}. Since our dataflow
transformers are sets of relations on the states of the property
automaton, we use this framework to provide a more general framework for
analyzing programs that make use of software transactions (in a manner similar
to our programming model). Our first usage of this framework is to determine
all of the static transactions of a program.


Let $B$ and $E$ be the set of all \begxact\ and \endxact\ program locations,
respectively. We annotate certain \delts\ with either an element in $B$
or $E$ or a tuple from $E \times B$. Revisiting \tableref{Transformers}, the
\delts\ that contain annotations are marked by the 
bracketed symbols in their subscript.
Intuitively, the annotation on a \delt\ is an ``explanation'' why
that \delt\ does not contain the edge $init \rightarrow init$. For
example, the \delt\ $\tEB{(e,b)}$ in table entry (e) arises from
$\tE{e} \xJoin \tB{b}$. It is annotated with $(e,b)$, which records
the unmatched \endxact\ and \begxact\ program statements that caused this
\delt\ to arise.

With these annotated \delts, \tableref{TransformerJoin} defines $\delta_1
\xJoin \delta_2$. Some of the entries in \tableref{TransformerJoin} are
highlighted. This is because for those entries, the composition of two
annotated \delts\ also produces an auxiliary tuple $(b,e)$, where $b \in B$
and $e \in E$, which is placed in a global database. These tuples allow us to
determine the static transactions of a program. 

To use our dataflow transformers in the framework defined in
\cite{kn:SRH96}, we must show that they adhere to certain algebraic
properties. This requires proving that our dataflow transformers form a
finite-height meet semi-lattice. Semi-lattice elements are sets of \delts. Let
$\Delta$ be the set of all \delts. The semi-lattice is finite-height because
there is only a finite number of \delt\ sets, i.e., $\mathcal{P}(\Delta)$. We
define the meet operation, $\sqcap$, as set union. Semi-lattice elements
are ordered by superset. Because composition of $\tau$-transformers is
performed pointwise (i.e., on a per-\delt\ basis), composition distributes
over $\sqcap$; hence, the problem is distributive.

For determining the static transactions of a program, each dataflow
transformer is a set of annotated \delts. We associate with each edge in the
ICFG the singleton set containing the annotated \delt\ that corresponds to
abstractly executing that edge. Then, using standard techniques
\cite{kn:SP81}, the meet-over-all-paths value for each node is found by
computing a fixpoint. When the composition of two \delts\ produces a tuple, we
record it in a global database. After the fixpoint has been reached, the
database contains all of the program's static transactions. Because we build
on the framework that verifies correct usage of the transactional primitives,
this analysis also verifies correct usage of the primitives. 

Our implementation uses weighted pushdown systems (WPDSs) \cite{BET03,RSJM}
as the dataflow analysis solver. Reps et al. showed the connection between
WPDSs and dataflow analysis \cite{RSJM}. The WPDS algorithms for solving a
dataflow-analysis query have the capability to return a \emph{witness trace}
\cite{RSJM} for the answer found for each program node. A
witness trace can be thought of as a proof for the computed 
answer. We exploit this capability for alerting the programmer of
possible incorrect usage of the \begxact\ and \endxact\ primitives. That is,
if after solving the dataflow analysis, $\wexit \cap
\{\tB{b},\tE{e},\tEB{(e,b)},\tErr\} \neq \emptyset$,  then there is possible
incorrect usage of the primitives. We present to the programmer a path through
the program that produces this erroneous result. Due to the abstraction
being used, the path may not actually be executable (e.g., due to correlated branches).
The programmer can analyze the path and determine if there exists an actual
misuse of the primitives in the program.
