correctness-model/writeup/abstract.tex

   1 Concurrent data structures often provide better performance on
   2 multi-core platforms, but are significantly more difficult to design and
   3 verify than their sequential counterparts.  The C/C++11 standard
   4 introduced a weak language memory model supporting low-level atomic
   5 operations such as compare and swap (CAS).  While these
   6 atomic operations can significantly improve the performance
   7 of concurrent data structures, programming at this level
   8 introduces
   9 non-intuitive behaviors that significantly increase the difficulty of
  10 developing code.
  11
  12 In this paper, we present \TOOL, a specification language checker that
  13 allows developers to write simple specifications for low-level
  14 concurrent data structures that make use of C/C++11 atomics and check
  15 the correctness of concurrent data structures against these
  16 specifications.  \TOOL is designed to be used in conjunction with
  17 model checking tools and we have implemented it as a plugin
  18 to \cdschecker.  We have evaluated \TOOL by annotating and checking
  19 several concurrent data structures.