\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.

Flanagan and Qadeer proposed that program methods exhibit the atomicity
property \cite{pldi:flanagan:types:2003}. Their work made use of a type system
to ensure this property. XProtect detects inconsistency violations in a program.
We view this as a heuristic that searches for the manifestation of a function not
exhibiting the atomicity property. The Locksmith tool
\cite{pratikakis:locksmith:pldi:2006} detects data races
by finding occurrences where shared data is not consistently protected by the
same lock. XProtect is similiar to this work because they both involve
consistency checking; however, XProtect detects consistencies with respect to
software transactions.

%used a similiar heuristic
%to detect data races. Their 
%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.
