Concurrent data structures often provide better performance on
multi-core platforms, but are significantly more difficult to design and
verify than their sequential counterparts.  The C/C++11 standard
introduced a weak language memory model supporting low-level atomic
operations such as compare and swap (CAS).  While these
atomic operations can significantly improve the performance
of concurrent data structures, programming at this level
introduces
non-intuitive behaviors that significantly increase the difficulty of
developing code.

In this paper, we present \TOOL, a specification language checker that
allows developers to write simple specifications for low-level
concurrent data structures that make use of C/C++11 atomics and check
the correctness of concurrent data structures against these
specifications.  \TOOL is designed to be used in conjunction with
model checking tools and we have implemented it as a plugin
to \cdschecker.  We have evaluated \TOOL by annotating and checking
several concurrent data structures.
