correctness-model/writeup/related.tex

   1 \mysection{\label{sec:related}Related Work}
   2
   3 % Related work should be related to bug finding on concurrent data structures:
   4 % 1. Specification:
   5 % CONCURRIT: A Domain Specific Language for Reproducing Concurrency Bugs (DSL
   6 % for reproducing bugs, allowing specifying a set of thread schedules to explore
   7 % in order to exhibit the bug) (PLDI'13)
   8
   9 % <NDSeq: Runtime Checking for Nondeterministic Sequential Specifications of
  10 % Parallel Correctness> (specify the correctness of concurrent programs using
  11 % nondeterministic sequential specifications, which allows the functional
  12 % correctness to be understood and verified on a sequential version of the
  13 % program) (PLDI'11)
  14
  15 % <NDetermin: Inferring Nondeterministic Sequential Specifications for
  16 % Parallelism Correctness> (this is the extended work of NDSeq, which is
  17 % inferring the specification) (ppopp'12)
  18
  19 % <VYRD: VerifYing Concurrent Programs by Runtime Refinement-Violation
  20 % Detection> (specification, not exhaustive approach, dynamic checking)
  21 % (PLDI'05)
  22
  23
  24 % 2. Linearizability:
  25 % <Verifying Commit-Atomicity using Model-Checking> (a more complete technique
  26 % for verifying atomicity using SPIN model checker)(SPIN Workshop'04)
  27
  28 % <The existence of Refinement mapping> (theoretical paper about proving a lower
  29 % level spscification correctly implements a higher level one) (Theoretical
  30 % Computer Science'91)
  31
  32 % <Comparison Under Abstraction for Verifying Linearizability> (static analysis
  33 % for verifying linearizability of concurrent unbounded linked data
  34 % structures) (CAV'07)
  35
  36 % <Formal Verification of a Lazy Concurrent List-Based Set Algorithm> (a formal
  37 % verification of LazyList, concurrent list-based set algorithm, shows it's
  38 % linearizable) (CAV'06)
  39
  40 % <Line-Up: A Complete and Automatic Linearizability Checker> (no specification,
  41 % run a sequential version in parallel and checks if the concurrent execution
  42 % violates linearizability, rely on CHESS, which assumes SC) (PLDI'10)
  43
  44 % <Thread Quantification for Concurrent Shape Analysis> (using abstract
  45 % interpretation, shape analysis for concurrent data structures, can prove
  46 % linearizability in a limited way) (CAV'08)
  47
  48 % <Experience with Model Checking Linearizability> (SC-based checking
  49 % linearizability) (SPIN Workshop'09)
  50
  51 % <Shape-Value Abstraction for Verifying Linearizability> (heap-allocated data
  52 % structures, shape analysis, assuming SC) (VMCAI'09)
  53
  54 % 3. General concurrency testing
  55 % <GAMBIT: Effective Unit Testing for Concurrency Libraries> (a prioritized
  56 % search technique that combines the speed benefit of heuristic-guided fuzzing
  57 % with the soundness, progress, and reproducibility of stateless model checking)
  58 % (ppopp'10)
  59
  60 % <Testing and Verifying Concurrent Objects> (one of the early paper) (Journal of Parallel and
  61 % Distributed Computing)
  62
  63 % 4. For relaxed M.M.
  64 % <CheckFence: Checking Consistency of Concurrent Data Types on Relaxed Memory
  65 % Models> () (PLDI'07) (TODO: Should read this in more detail)
  66
  67 % <Testing Concurrent Programs on Relaxed Memory Models> (a tool that test
  68 % concurrent programs under relaxed M.M., but no specification, and not
  69 % an exhaustive approach) (issta'11)
  70
  71 Researchers have proposed and designed specifications and approaches
  72 to find bugs in concurrent data structures based on linearization.
  73 Early work by Wing and
  74 Gong~\cite{test-verify-concurrent-objects} proposed using
  75 linearizability to test and verify concurrent objects.
  76 Line-up~\cite{lineup} builds on the Chess~\cite{chess} model checker
  77 to automatically check deterministic linearizability. It
  78 automatically generates the sequential specification by systematically
  79 enumerating all sequential behaviors.
  80 Paraglider~\cite{VechevMCLinear} supports checking with and without
  81 linearization points based on SPIN~\cite{spinmodel}. All of these
  82 approaches assume that there exist a sequential history that is consistent with program order.  Furthermore, they also assume
  83 the SC memory model and a trace that provides an
  84 ordering for method invocation and response events.  Our work extends the notion of equivalence to sequential executions to the relaxed memory models used
  85 by real systems.
  86
  87 Amit \etal~\cite{abstraction-linearizability} present a static
  88 analysis based on TVLA for verifying linearizability of concurrent
  89 linked data structures. Valeiadis~\cite{shape-value-abstraction}
  90 demonstrates a shape-value abstraction which can automatically prove
  91 linearizability.  Thread quantification can also verify
  92 data structure linearizability~\cite{thread-quantification}.
  93 Colvin \etal formally verified a list-based set~\cite{formal-verification-set}.  While these approaches
  94 provide stronger guarantees than \TOOL, they were typically used to
  95 check simpler data structures and require experts to use.
  96 Moreover, they target the SC memory model.
  97
  98 Researchers have proposed specification languages for concurrent
  99 data structures.  Refinement mapping~\cite{refinement-mapping}
 100 provides the theoretical basis for designing and using specifications.
 101 Commit atomicity~\cite{spin-commit-atomicity} can verify atomicity
 102 properties.  Concurrit~\cite{concurrit} is a domain-specific language
 103 that allows programmers to write scripts to specify thread schedules
 104 to reproduce bugs, and is useful when programmers already have some
 105 knowledge about a bug.  NDetermin~\cite{ndetermin} infers
 106 nondeterministic sequential specifications to model the behaviors of
 107 parallel code.
 108
 109 VYRD~\cite{vyrd} is conceptually similar to \TOOL --- developers
 110 specify commit points for concurrent code.  The parallel code is then
 111 executed and the commit points are used to identify a sequential
 112 execution that should have the same behaviors.  VYRD was designed for
 113 the SC memory model --- it
 114 is unable to construct a sequential refinement for a relaxed memory
 115 model or check synchronization properties.
 116
 117 {\sc Gambit}~\cite{gambit} uses a prioritized search technique that
 118 combines stateless model checking and heuristic-guided fuzzing to unit
 119 test code under the SC memory model.  {\sc Relaxed}~\cite{memtest}
 120 explores SC executions to identify executions with races and then
 121 re-executes the program under the PSO or TSO memory model to test
 122 whether the relaxations expose bugs.  CheckFence~\cite{checkfence} is
 123 a tool for verifying data structures against relaxed memory models and
 124 takes a SAT-based approach instead of the stateless model checking
 125 approach used by \cdschecker.
 126
 127 Researchers have developed verification techniques for code that
 128 admits only SC executions under the TSO and PSO memory
 129 models~\cite{koushiksc,burckhardtverif}.  The basic idea is to develop
 130 an execution monitor that can detect whether non-SC executions exist
 131 by examining only SC executions.
 132
 133