\section{Related Work}
\label{Se:Related}
The use of tranformers for performing interprocedural-dataflow analysis was
introduced by Cousot and Cousot \cite{IFIP:CC78} and Sharir and Pnueli
\cite{kn:SP81}. Sagiv et al. showed how this framework, where the transformers
are relations annotated with ``values'' that exhibit certain algebraic properties, can
be used to precisely solve instances of copy propagation, namely copy-constant
propataion and linear-constant propagation \cite{kn:SRH96}. We used this
framework for analyzing programs that adhere to our programming model. 

Abstract interpretation was defined in the seminal work by Cousot and Cousot
\cite{POPL:CC77}. The analyses that we present can be viewed as an abstract
interpretation of the program, where the abstract semantics of a program
statement is its effect on the property automaton that checks a policy for
correct usage of the transactional primitives.

XOrder analysis is a program optimization whose goal is to reduce false
conflicts of a transactional program executing on a hardware ISA that supports
transactional memory. The HTM implementation we target performs conflict
detection through the cache-coherence protocol \cite{moore:logtm:hpca:2006}.
Chilimbi, Davidson, and Larus also used record-layout reordering as an
optimization to improve a program's effective use of hardware caches
\cite{CDL99}. Their analyses incorporated profile information attained from
runs of the program. Our optimization, XOrder, is a purely static analysis. In
contrast to the work by Chilimbi et al., we reorder a record type's layout
according to its accesses in static transactions. This is because the focus of
XOrder is to reduce false conflicts, and not necessarily improve cache
utilization. It is left to future work to determine if incorporating dynamic
profiling information into XOrder's record layout algorithm could improve our
optimization.

Recent work by Harris et al. \cite{DBLP:conf/pldi/HarrisPST06} and Adl-Tabatabai et al.
\cite{DBLP:conf/pldi/Adl-TabatabaiLMMSS06} was concerned with optimizing a program's use of
software transactional memory (STM). Their work is based on the observation
that, by breaking down the inserted calls to the STM's runtime
system, standard compiler optimizations, such as dead-code elimination and common
subexpression elimination, can be used to optimize a program with respect to
the number of calls it makes to the STM's runtime system. XOrder analysis is
also concerned with optimizing a program that runs on a system that supports
transactional memory. In our case, we optimize the program itself (i.e., the
layout of the record types), and not the inserted program statements. It would
be interesting to see if our techniques would result in additional
performance gains in these other systems.

There have been many tools that detect data races. Eraser by Savage et al is a
tool that dynamically detects race conditions
\cite{DBLP:journals/tocs/SavageBNSA97}. RacerX by Engler et al. uses software
model checking techniques to statically find data races in a concurrent
program \cite{DBLP:conf/sosp/EnglerA03}. Most similiar to our analysis,
XProtect, is the LOCKSMITH tool by Pratikaks et al.
\cite{pratikakis:locksmith:pldi:2006}. Their tool infers a consistency
correlation on shared objects in a program. A program is data-race free if it
all accesses to shared objects are consistently correlated. Whereas they use an
extended type system to provide this guarantee, XProtect guarantees data race
freedom by by verifying that all accesses to shared records (objects) are
consistently protected by a static transaction. This is accomplished by
extending XRef analysis with a sound pointer analysis.
