changes

[cdsspec-compiler.git] / correctness-model / writeup / abstract.tex

diff --git a/correctness-model/writeup/abstract.tex b/correctness-model/writeup/abstract.tex
new file mode 100644 (file)
index 0000000..7bf3748
--- /dev/null
+++ b/correctness-model/writeup/abstract.tex
@@ -0,0 +1,19 @@
+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.