\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) % (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) % (this is the extended work of NDSeq, which is % inferring the specification) (ppopp'12) % (specification, not exhaustive approach, dynamic checking) % (PLDI'05) % 2. Linearizability: % (a more complete technique % for verifying atomicity using SPIN model checker)(SPIN Workshop'04) % (theoretical paper about proving a lower % level spscification correctly implements a higher level one) (Theoretical % Computer Science'91) % (static analysis % for verifying linearizability of concurrent unbounded linked data % structures) (CAV'07) % (a formal % verification of LazyList, concurrent list-based set algorithm, shows it's % linearizable) (CAV'06) % (no specification, % run a sequential version in parallel and checks if the concurrent execution % violates linearizability, rely on CHESS, which assumes SC) (PLDI'10) % (using abstract % interpretation, shape analysis for concurrent data structures, can prove % linearizability in a limited way) (CAV'08) % (SC-based checking % linearizability) (SPIN Workshop'09) % (heap-allocated data % structures, shape analysis, assuming SC) (VMCAI'09) % 3. General concurrency testing % (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) % (one of the early paper) (Journal of Parallel and % Distributed Computing) % 4. For relaxed M.M. % () (PLDI'07) (TODO: Should read this in more detail) % (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.