\section{XRef}
\label{Se:XRef}
It is useful for a programmer to know what record fields are accessed in the
dynamic transactions during program execution. This is important both for
program understanding and debugging. For example, when adding fields to a
record type or splitting a large record type into two, the programmer must be
aware of the fact that the fields of an instance of that record are guarded by
a software transaction. We are able to present to the programmer an
approximation of this information through XRef analysis. XRef analysis
approximates the set of fields accessed in dynamic transactions by annotating
the fields of each record type with the static transactions in which they are
referenced. XRef analysis can be viewed as inferring annotated types, where
the annotations are the static transactions in which each field of a
record type is referenced. 

%XRef analysis does not distinguish between different instances of a record
%type. Later, in \sectref{XProtect}, we present an analysis that is capable of
%attaching different annotations to different instances of a record type.

\subsection{Structured Software Transactions}
\label{Se:xrefAtomic}
When the program being analyzed makes use of the \atomic-block construct,
XRef analysis can be performed by a flow-insensitive interprocedural analysis
(similar to GMOD/GUSE analysis \cite{DBLP:conf/pldi/CooperK88}).
Because of the similiarities between XRef analysis (for the \atomic-block
construct) and GMOD/GUSE analysis, we only sketch
the algorithm.

Let $R$ be the set of all record-type names, and $F$ be the set of all field
names. For each static transaction, the algorithm computes a set of pairs $s$,
where each pair is of the form $(r,f)$ with $r \in R$ and $f \in F$. For each
function of the program, perform an intraprocedural analysis that determines
all record-type field accesses performed by that function. The accesses are
represented by a set of pairs $s$. This can be accomplished with a single pass
over each program node in a function's control-flow graph (similar to IUSE
analysis). Once this information has been computed, next perform a fixpoint
calculation over the callgraph to determine the field accesses made
transitively by each function (similar to GUSE analysis). Finally, for each
function that contains an \atomic\ block, traverse the program statements that
are in the scope of the \atomic\ block, unioning the accesses for each program
statement. If a program statement is a function call, the set of accesses is
retrieved from the sets that were calculated from the fixpoint computation on
the callgraph. Once this information has been computed for each static
transaction, the fields of each record type are annotated with the static
transaction(s) in which it is accessed.


\subsection{Unstructured Software Transactions}
\label{Se:xrefNonAtomic}
\begin{sloppypar}
We make use of the framework presented in \sectref{staticNonAtomic} to analyze
lock-based programs converted to use \begxact\ and \endxact. To do this, we
add to each \delt's annotation a set of pairs, as defined in
\sectref{xrefAtomic}.
Specifically, for each \delt\ in the top row of
\tableref{Transformers}, we add to the annotation a set of pairs $s$, which is 
shown in \tableref{Rules}. 
We make a few changes to the composition of \delts. For brevity, we
enumerate the changes here instead of replicating \tableref{Transformers}. We
use the notation $(s,\delta)$ to represent an annotated \delt\ extended with
the set of pairs $s$. Likewise, we use the notation $(s_1, \tEB{(e,b)}, s_2)$ to
represent that $\tEB{(e,b)}$ has two sets, $s_1$ and $s_2$. We define
``$\xJoin$'' as follows (see below for an explanation):
\begin{enumerate}
\item $(s_1, \tB{b}); (s_2, \tE{e}) = (\emptyset,\tBE), (b,e,s_1 \cup s_2)$
\item $(s_1, \tid); (s_2, \tB{b}) = (s_2,\tB{b})$
\item $(s_1, \tBE); (s_2, \tB{b}) = (s_2,\tB{b})$
\item $(s_1, \tE{e}) ; (s_2, \tB{b}) = (s_1,\tEB{(e,b)},s_2)$
\item $(s_1, \tE{e}) ; (s_2, \tid) = (s_1,\tE{e})$
\item $(s_1, \tE{e}) ; (s_2, \tBE) = (s_1,\tE{e})$
\item $(s_1, \tid) ; (s_2, \tEB{(e_1,b_1)}, s_3) = (s_1 \cup s_2, \tEB{(e_1,b_1},s_3)$
\item $(s_1, \tEB{(e_1,b_1)}, s_2) ; (s_3,\tid) = (s_1, \tEB{(e_1,b_1},s_2 \cup s_3)$
\item $(s_1, \tB{b_1}) ; (s_2, \tEB{(e_2,b_2)}, s_3) = (s_3, \tB{b_2}), (b_1, e_2, s_1 \cup s_2)$
\item $(s_1, \tEB{(e_1,b_1)},s_2) ; (s_3, \tE{e_2}) = (s_1,\tE{e_1}), (b_1,e_2,s_2 \cup s_3)$
\item $(s_1, \tEB{(e_1,b_1)},s_2) ; (s_3, \tEB{(e_2,b_2)}, s_4) = (s_1, \tEB{(e_1,b_2},s_4), (b_1, e_2, s_2 \cup s_3)$
\item otherwise $(s_1, \delta_1) ; (s_2, \delta_2) = (s_1 \cup s_2, (\delta_1 ; \delta_2))$
\end{enumerate}
\end{sloppypar}


Let us now explain this definition by means of a few examples. Intuitively,
we want to only record field accesses that occur within a static transaction.
This is exemplified by rule (1). The composition $(s_1, \tid); (s_2,
\tB{b})$ results in $(s_2,\tB{b})$. This has the effect that the composition
ignores all field accesses that occur {\em before} the \begxact\ statement.
Similiarly, rules (3) and (4) ignore all field accesses that occur {\em after}
an \endxact\ statement. Notice that the cases specified in rules (6) and
(7) each produce an auxiliary triple. This is because those rules result from the
matching of a \begxact\ and \endxact\ statement. Specifically, for rule (6),
the composition of $(s_1, \tEB{(e_1,b_1)},s_2) ; (s_3, \tE{e_2})$ results in
the annotated \delt\ $(s_1,\tE{e_1})$ along with the auxiliary triple
$(b_1,e_2,s_2 \cup s_3)$. The triple denotes that static transaction
$(b_1,e_2)$ accessed the fields contained in the set $s_2 \cup s_3$. When an
auxiliary triple is produced, we record this information in a global database.

\input{Rules}

Each node of the ICFG is annotated with its corresponding dataflow transformer
as in \sectref{staticNonAtomic}. As before, we use standard techniques to
compute the MOP dataflow transformer for each program node in the ICFG. Once
the dataflow analysis has completed, the global database contains triples
of the form $(b,e,s)$, such that $b \in B$, $e \in E$, and $s$ is a set of
record-type-field accesses. We use this information to annotate the fields of
each record type with the static transactions in which it is accessed.

When interpreting the results our experiments, we found XRef analysis to be
extremely helpful. Analyzing the information obtained from XRef
analysis led us to realize that dynamic transactions were aborting because of
false conflicts. We address this issue with our next analysis, XOrder.
