+++ /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