--- /dev/null
+\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.
+
+
projects / cdsspec-compiler.git / blobdiff