\def\raccess{s_{\text{access}}}
\def\rwarn{s_{\text{warn}}}
\def\rcheck{s_{\text{check}}}
\def\rxact{s_{\text{xact}}}

%from data races. A data race occurs when two (or more) threads concurrently
%access the same memory location, and one of them is a write.

\section{XProtect}
\label{Se:XProtect}
Software transactions are arguably superior to traditional locks; however,
they do not eliminate all programming errors due to concurrency. For example,
when used incorrectly, programs that inconsistenly use software transactions
can produce erroneous results. In the program shown in \figref{Example}, 
the value returned from the call to {\tt sumx} can have five possibilities
instead of two. This is due to the nondeterminism of the thread scheduler.
Specifically, it depends on how the thread that is started started at location
{\tt n4}, $\tn{4}$, is interleaved with the thread started at location {\tt
n5}, $\tn{5}$. If $\tn{4}$ commits before $\tn{5}$ begins, then the result
will be 0. If $\tn{4}$ commits after $\tn{5}$ has read {\tt s.x1}, the result
will be {\tt s.x1}. This pattern continues up to the case where $\tn{4}$
commits after $\tn{5}$ has read all of the {\tt x} fields. Had the programmer
protected the call to {\tt sumx} with a transaction, there would be only two
possible results, namely, (i) 0 in the case that $\tn{4}$ commits before
$\tn{5}$, and (ii) the sum of the values of all the {\tt x} fields otherwise.

The underlying problem is that the call to {\tt sumx} is not protected by a
software transaction. In the terms of Flanagan and Qadeer, the function {\tt
sumx} does not have the {\tt atomicity} property \cite{pldi:flanagan:types:2003}.
From \cite{pldi:flanagan:types:2003}, ``if a method is atomic, then
any interaction between that method and steps of other threads is
guaranteed to be benign[.]''

We use XProtect analysis to address this problem. XProtect analysis is
a heuristic to check for atomicity violations. Similiar to the work in
\cite{pratikakis:locksmith:pldi:2006}, XProtect checks that accesses to a
shared-record instance are consistently protected by a software transaction.
This does not guarantee the atomicity property (e.g., enclosing every program
statement in a software transaction is consistent); however,
an inconsistent program is likely to violate the atomicity property.

XProtect is an extension of XRef analysis. It can be viewed as further
refining the type annotations inferred by XRef analysis for the fields of each
record type. The refinement consists of adding the results from a sound
pointer analysis to the annotations. We chose Steensgaard's
\cite{DBLP:conf/popl/Steensgaard96} analysis because it is sound for
concurrent programs: a flow-insensitive analysis considers all interleavings
of the various threads that make up the concurrent program. 
% TODO: NAK
%(
Other more
expensive pointer analyses that are still sound for concurrent programs would
work just as well.
%) Because XProtect is an extension of XRef, XProtect is able
%to analyze concurrent programs using interprocedural dataflow-analysis
%algorithms for sequential code.

As before, we describe XProtect analysis for programs that make use of the
\atomic-block construct and those that specify the beginning and ending of a
software transaction separately. In both cases, we compute the results from
two dataflow-analaysis problems, and the answer we are interested in is
computed from the differences in the values computed by the two analysis
phases.


%With respect to the function {\tt sumx}, the
%roblem is that the accesses to the

%he atis notTo determine this
%Specifically,
%due to the nondeterminism of the thread scheduler, the value
%returned from the call to {\tt sumx} can have five possible results instead of
%two: the results depending on when the thread 


%The research literature has defined two types of data races, {\em low-level}
%and {\em high-level} data races. A low-level data race occurs when there are two
%concurrent accesses to the same memory location and one of them is a write.

%A high-level data race occurs when dependent operations of program execution
%do not see the same view of the world---that is, when two or more operations
%that the programmer intended to be executed atomically are not executed
%atomically \cite{DBLP:conf/popl/VaziriTD06}. The classic example of a
%high-level data race is in the {\tt java.util.Vector} constructor from the Sun
%JDK release 1.4.2 \cite{DBLP:conf/tldi/FlanaganFL05}. In this example, the
%constructor takes as an input parameter an instance of the class {\tt
%java.util.Collection}. It then allocates an array whose size is equal to the
%size of the collection. After being allocated, the array is passed to the
%collection parameter, which copies its contents into the array. The problem
%comes from the fact that the collection can be modified between the allocation
%and the filling of the array. For example, if all of the elements in the
%collection are removed, then the vector's internal size counter
%and the array's data contents will be inconsistent.

%Even with software transactions, data races can
%still exist. For example,
%n a large software system, the programmer may not
%now which records are shared between threads and may omit a software
%ransaction. In other cases, the programmer may simply forget to guard a
%equence of program statements with a transaction. For the example program in
%figref{Example}, there is a data race on the field {\tt s.x1}. The data race
%ccurs because the main thread writes to {\tt s.x1} at location {\tt n6}.
%oncurrently, the thread that begins at location {\tt n5} reads the field {\tt
%.x1}. We address this problem with our analysis XProtect.


%Consider the
%case where one thread transactionally writes a double word of memory (e.g., a
%{\tt float} in the program). In another thread, the same double word is
%modified outside of a software transaction. To the underlying system, these
%writes appear as two separate instructions. Therefore, the underlying TM
%system is free to place the two writes from the transactional thread between
%the two writes of the nontransactional thread. This results in the double word
%containing a partial update from {\em both} threads. We address this problem
%via one more enhancement of our interprocedural static analysis, called
%XProtect, which builds on the XRef analysis described in \sectref{XRef}.


%XProtect analysis warns the programmer if accesses to fields of a shared
%record instance are not consistently protected by a software transaction. Even
%though this does not guarantee race freedom (e.g., a concurrent program that
%uses no synchronization is consistent), consistency checking is a common
%technique for data race detection \cite{pratikakis:locksmith:pldi:2006}.
%We add a sound\footnote{Many pointer analyses are unsound in the presence of
%uninitialized variables
%\cite{DBLP:conf/popl/Steensgaard96,DBLP:conf/popl/ShapiroH97}.
%This can be rectified by also performing uninitialized-variables analysis.
%}
%flow-insensitive, context-insensitive pointer analysis to XRef. Our
%implementation
%uses Steensgaard's analysis
%\cite{DBLP:conf/popl/Steensgaard96}.
%We chose this algorithm because it is sound for concurrent programs: a
%flow-insensitive analysis considers all interleavings of the various threads
%that make up the concurrent program. Other more expensive pointer analyses
%that are still sound for concurrent programs would work just as well.


\subsection{Structured Software Transactions}
\label{Se:xprotectAtomic}
For programs that make use of the \atomic-block construct, XProtect is a
straightforward extension of XRef. The key is to extend the sets of pairs to
include both the abstract record-allocation site that is accessed, as well as
an indication of what type of memory-access is made, i.e., either a read or a
write. (We use the term ``abstract record-allocation site'' to mean the set of
record-allocation sites obtained after pointer analysis has finished.)
Additionally tracking reads and writes enables XProtect to ignore cases when
shared memory is only read and never written.

Specifically, we modify the XRef algorithm to compute, for each static
transaction, a set of tuples of the form $(R,A,F,T)$, where $R$ and $F$ are as
in XRef, $A$ is the set of abstract record-allocation sites, and $T \in
\{read,write\}$. We label each node of the program with a set of tuples $s$
that corresponds to that node's accesses, and the manner in which they are
made. For example, a program node that represents the program statement $x =
r_1.f_1$ is labeled with the tuple set $\{(r_1.a.f_1.read)\ |\ a \in
A_{r_1}\}$, where $A_{r_1}$ is the set of abstract record-allocation sites
that are accessed. Using the extended sets of tuples, the algorithm for
solving XRef (defined in \sectref{xrefAtomic}) computes, for each abstract
record-allocation site, the set of fields either read or written by each
static transaction. We denote this set by $\rxact$.

To verify that the field accesses to all shared record instances are
consistently protected by a software transaction, we solve a second
dataflow-analysis problem, which determines all field accesses that occur
outside every static transaction. A second dataflow-analysis problem is
required because a function may be called both from within a transaction and
outside of one. Therefore, it is possible for that function to make accesses
to the same shared record instance in a transactional and nontransactional
context.


We collect all nontransactional accesses via a simple trick. We treat each
\atomic\ block as a ``{\tt noop}'' instruction. This effectively ignores all
static transactions in the program. For each function, we compute the set of
field accesses to the abstract record-allocation sites by visiting each node
in the function's control flow graph (CFG) and taking the union of their
accesses. Next, we solve a set of equations on the program's call-graph to
compute the set of abstract record-allocation site field accesses made
(transitively) by each function. All nontransactional field accesses to
abstract record-allocation sites are precisely the label on the {\tt main}
function in the call-graph. We denote this set by $\raccess$.

Once $\raccess$ has been computed, we check to see whether a field is accessed
both transactionally and nontransactionally, with one of the accesses being a
write. For each read access in $\rxact$, we check to see whether $\raccess$
contains a write access to the same field. For example, if $(r_1.a.f_1.read)
\in \rxact$, which denotes a read of the $f_1$ field of record type $r_1$ for
abstract record-allocation site $a \in A$, we check whether $(r_1.a.f_1.write)
\in \raccess$. Similarly, for each write access in $\rxact$, we check whether
there is a corresponding read or write access to the same field in $\raccess$.
If either of these checks succeed, then we warn the programmer that there is a
potential data race. The warning includes the field and abstract
record-allocation site that is inconsistently guarded by a software
transaction.


\subsection{Unstructured Software Transactions}
\label{Se:xprotectNonAtomic}
To perform XProtect analysis on programs that specify the beginning and ending
of software transactions separately, we extend the XRef analysis presented in
\sectref{xrefNonAtomic}.
The sets of pairs used in XRef analysis are extended to be sets of tuples.
Each tuple is of the form $(R,A,F,T)$, where $R$ is the set of all record type
names, $A$ is the set of abstract record-allocation sites, $F$ is the set
of all record-type fields, and $T \in \{read,write\}$. With respect to XRef
analysis, the extensions are propagated along. In particular, they
have no additional effect when \delts\ are composed. We note
that we only increase the size of the annotations by a finite amount.
Moreover, all algebraic properties that were shown to hold earlier are still
valid.

As in XRef analysis, we label each edge of the ICFG with its corresponding set
of annotated \delts. We then solve the dataflow-analysis problem as before,
which populates the global database with the set of fields accessed in a
static transaction for each abstract record-allocation site. We denote 
the set of abstract record-allocation site fields accessed in some static
transaction by $\rxact$.

To determine the field accesses made to abstract record-allocation sites
while not in a static transaction, we to run XProtect again;
however, for this second run we modify the definition of ``$\xJoin$''. The key
is to realize that the information sought is the {\em opposite} of the
information computed by XProtect. We compute these unprotected accesses by
``inverting'' the operations on the annotations of the \delts\ when composing
\delts.
Intuitively, we modify the definition of ``$\xJoin$'' to be such that
it only records accesses that occur {\em outside} of a static transaction.
This can be accomplished by making the following changes to ``$\xJoin$'' (we use
the same notation as in \sectref{xrefNonAtomic}). For instance, in rule (1)
below, the tuples in $s_2$ are dropped because they represent accesses that
occur inside of a static transaction.
\begin{enumerate}
\item $(s_1, \tB{b}) ; (s_2, \tid) = (s_1, \tB{b})$
\item $(s_1, \tid) ; (s_2, \tE{e}) = (s_2, \tE{e})$
\item $(s_1, \tid) ; (s_2, \tEB{(e_1,b_1)},s_3) = (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)$
\item $(s_1, \tE{e}) ; (s_2, \tB{b}) = (s_1 \cup s_2, \tEB{(e,b)}, \emptyset)$
\item $(s_1, \tB{b_1}) ; (s_2, \tEB{(e_2,b_2)}, s_3) =  (s_1 \cup s_2 \cup s_3, \tB{b_2})$
\item $(s_1, \tEB{(e_1,b_1)}, s_2) ; (s_3, \tE{e_2}) = (s_1 \cup s_2 \cup s_3, \tE{e_1})$
\item $(s_1, \tEB{(e_1,b_1)}, s_2) ; (s_3, \tEB{(e_2,b_2)},s_4) = \\ (s_1 \cup s_2 \cup s_3 \cup s_4, \tEB{(e_1,b_2},\emptyset)$
\item otherwise $(s_1, \delta_1) ; (s_2, \delta_2) = (s_1 \cup s_2, \delta_1 ; \delta_2)$
\end{enumerate}
Using this modified composition of \delts, we perform a second fixpoint
calculation.  All non-transactional field accesses (i.e., $\raccess$) are the annotations
associated with $\tid$ and $\tBE$ in the dataflow transformer on the {\tt main}
function's exit node.

Finally, we perform the check with respect to $\rxact$ and $\raccess$ described in
\sectref{xprotectAtomic} to see if there are potential inconsistencies with
respect to the use of static transactions when accessing the fields of a shared
record. If an inconsistency exists, we report it to the programmer.

Again, because we use WPDSs as our dataflow-analysis solver, we take advantage
of their witness-tracing capabilities. (A witness trace is a
``proof'' for a computed dataflow value and encodes the set of program paths
that gave rise to it, along with their intermediate dataflow values.)
We extract from the witness trace a path that accesses a field of the shared
record while not in a static transaction. We present to the programmer this
path as well as a static transaction that accesses the same field in a
conflicting manner, e.g., a read and a write.

\subsection{XProtect Discussion}
\label{Se:XProtectExp}
For the example program in \figref{Example}, XProtect emits twelve warnings.
Eight of these are benign consistency violations. This is due to the fact that
the program initializes the {\tt x} and {\tt y} fields of the shared {\tt
ColoredShape} record {\tt s} before starting any threads. Adopting the policy
of tools such as Eraser \cite{DBLP:journals/tocs/SavageBNSA97}, which make a
special case for the initialization of global variables, could eliminate these
cases.

The other four warnings have more severe consequences. The problem is because
the reads of the {\tt x} fields from $\tn{5}$'s call to {\tt sumx} execute
concurrently with the writes to the {\tt x} fields from $\tn{4}$'s call to
{\tt mulx}. As explained earlier, this causes the program to have more
behaviors than the programmer intended. XProtect alerts the programmer of
these inconsistency violations. In doing so, XProtect implicitly notifies the
programmer that the call to {\tt sumx} was not guarded with a software
transaction.

%The data race is on the
%{\tt x1} field of the record {\tt s}. The data race occurs from the concurrent
%write to {\tt s.x1} by the main thread and the read of {\tt s.x1} by the
%thread that begins at program location {\tt n5}, $\tn{5}$. The other five
%warnings are from the execution of the thread that begins at program location
%{\tt n4}, $\tn{4}$. $\tn{4}$ writes to each of the {\tt x} fields. $\tn{5}$
%reads all of the {\tt x} fields and the main thread writes to the field {\tt
%s.x1}. Because $\tn{4}$ is guarded by a static transaction, it does not cause
%any data races. 

%It is interesting to note that the warnings alert the programmer
%This is an example of a {\em high-level} data race
%\cite{AHB03}.


We note that due to the imprecision of pointer analysis and the abstract model
of the program that we analyze (i.e., we do not interpret conditions), a
warning does not guarantee that there exists an inconsistency. Additionally,
XProtect emits warnings for benign inconsistencies.
%Even our small
%test example contained benign inconsistencies (though not because of imprecise
%pointer-analysis).
However, we believe that XProtect is a useful analysis to aid programmers in
reasoning about their software. Proving that a program consistently protects
shared data with a software transaction takes a step toward verifying
correctness. That is, XProtect can be used as an inexpensive analysis that
alerts the programmer of inconsistencies. If inconsistencies exist, the
programmer can then apply other
more heavy-weight
analyses.
%This could include
%software-model checkers that consider thread interleavings
%\cite{magic,BET03},
%data race detectors
%\cite{DBLP:journals/tocs/SavageBNSA97,DBLP:conf/sosp/EnglerA03}, and extended
%type systems that guarantee race freedom
%\cite{pldi:flanagan:types:2003,racefreejava}.

%For example,
%XProtect Incorporating
%other analysis tools, such as software model checkers and static race
%detectors, 
%
%Even
%though it does not guarantee correctness (or even data race freedom), proving
%that a program is consistent
%Alternative techniques, such as
%software model checking, might be able to find true protection violations.
