\mysection{\label{sec:related}Related Work}

% Related work should be related to bug finding on concurrent data structures:
% 1. Specification:
% CONCURRIT: A Domain Specific Language for Reproducing Concurrency Bugs (DSL
% for reproducing bugs, allowing specifying a set of thread schedules to explore
% in order to exhibit the bug) (PLDI'13)

% <NDSeq: Runtime Checking for Nondeterministic Sequential Specifications of
% Parallel Correctness> (specify the correctness of concurrent programs using
% nondeterministic sequential specifications, which allows the functional
% correctness to be understood and verified on a sequential version of the
% program) (PLDI'11)

% <NDetermin: Inferring Nondeterministic Sequential Specifications for
% Parallelism Correctness> (this is the extended work of NDSeq, which is
% inferring the specification) (ppopp'12)

% <VYRD: VerifYing Concurrent Programs by Runtime Refinement-Violation
% Detection> (specification, not exhaustive approach, dynamic checking)
% (PLDI'05)


% 2. Linearizability:
% <Verifying Commit-Atomicity using Model-Checking> (a more complete technique
% for verifying atomicity using SPIN model checker)(SPIN Workshop'04)

% <The existence of Refinement mapping> (theoretical paper about proving a lower
% level spscification correctly implements a higher level one) (Theoretical
% Computer Science'91)

% <Comparison Under Abstraction for Verifying Linearizability> (static analysis
% for verifying linearizability of concurrent unbounded linked data
% structures) (CAV'07)

% <Formal Verification of a Lazy Concurrent List-Based Set Algorithm> (a formal
% verification of LazyList, concurrent list-based set algorithm, shows it's
% linearizable) (CAV'06)

% <Line-Up: A Complete and Automatic Linearizability Checker> (no specification,
% run a sequential version in parallel and checks if the concurrent execution
% violates linearizability, rely on CHESS, which assumes SC) (PLDI'10)

% <Thread Quantification for Concurrent Shape Analysis> (using abstract
% interpretation, shape analysis for concurrent data structures, can prove
% linearizability in a limited way) (CAV'08)

% <Experience with Model Checking Linearizability> (SC-based checking
% linearizability) (SPIN Workshop'09)

% <Shape-Value Abstraction for Verifying Linearizability> (heap-allocated data
% structures, shape analysis, assuming SC) (VMCAI'09)

% 3. General concurrency testing
% <GAMBIT: Effective Unit Testing for Concurrency Libraries> (a prioritized
% search technique that combines the speed benefit of heuristic-guided fuzzing
% with the soundness, progress, and reproducibility of stateless model checking)
% (ppopp'10)

% <Testing and Verifying Concurrent Objects> (one of the early paper) (Journal of Parallel and
% Distributed Computing)

% 4. For relaxed M.M.
% <CheckFence: Checking Consistency of Concurrent Data Types on Relaxed Memory
% Models> () (PLDI'07) (TODO: Should read this in more detail)

% <Testing Concurrent Programs on Relaxed Memory Models> (a tool that test
% concurrent programs under relaxed M.M., but no specification, and not
% an exhaustive approach) (issta'11)

Researchers have proposed and designed specifications and approaches
to find bugs in concurrent data structures based on linearization.
Early work by Wing and
Gong~\cite{test-verify-concurrent-objects} proposed using
linearizability to test and verify concurrent objects.
Line-up~\cite{lineup} builds on the Chess~\cite{chess} model checker
to automatically check deterministic linearizability. It
automatically generates the sequential specification by systematically
enumerating all sequential behaviors.
Paraglider~\cite{VechevMCLinear} supports checking with and without
linearization points based on SPIN~\cite{spinmodel}. All of these
approaches assume that there exist a sequential history that is consistent with program order.  Furthermore, they also assume
the SC memory model and a trace that provides an
ordering for method invocation and response events.  Our work extends the notion of equivalence to sequential executions to the relaxed memory models used
by real systems.

Amit \etal~\cite{abstraction-linearizability} present a static
analysis based on TVLA for verifying linearizability of concurrent
linked data structures. Valeiadis~\cite{shape-value-abstraction}
demonstrates a shape-value abstraction which can automatically prove
linearizability.  Thread quantification can also verify
data structure linearizability~\cite{thread-quantification}.
Colvin \etal formally verified a list-based set~\cite{formal-verification-set}.  While these approaches
provide stronger guarantees than \TOOL, they were typically used to
check simpler data structures and require experts to use.
Moreover, they target the SC memory model.

Researchers have proposed specification languages for concurrent
data structures.  Refinement mapping~\cite{refinement-mapping}
provides the theoretical basis for designing and using specifications.
Commit atomicity~\cite{spin-commit-atomicity} can verify atomicity
properties.  Concurrit~\cite{concurrit} is a domain-specific language
that allows programmers to write scripts to specify thread schedules
to reproduce bugs, and is useful when programmers already have some
knowledge about a bug.  NDetermin~\cite{ndetermin} infers
nondeterministic sequential specifications to model the behaviors of
parallel code.  

VYRD~\cite{vyrd} is conceptually similar to \TOOL --- developers
specify commit points for concurrent code.  The parallel code is then
executed and the commit points are used to identify a sequential
execution that should have the same behaviors.  VYRD was designed for
the SC memory model --- it
is unable to construct a sequential refinement for a relaxed memory
model or check synchronization properties.

{\sc Gambit}~\cite{gambit} uses a prioritized search technique that
combines stateless model checking and heuristic-guided fuzzing to unit
test code under the SC memory model.  {\sc Relaxed}~\cite{memtest}
explores SC executions to identify executions with races and then
re-executes the program under the PSO or TSO memory model to test
whether the relaxations expose bugs.  CheckFence~\cite{checkfence} is
a tool for verifying data structures against relaxed memory models and
takes a SAT-based approach instead of the stateless model checking
approach used by \cdschecker.

Researchers have developed verification techniques for code that
admits only SC executions under the TSO and PSO memory
models~\cite{koushiksc,burckhardtverif}.  The basic idea is to develop
an execution monitor that can detect whether non-SC executions exist
by examining only SC executions.


