fixed command line
[cdsspec-compiler.git] / correctness-model / writeup / abstract.tex
diff --git a/correctness-model/writeup/abstract.tex b/correctness-model/writeup/abstract.tex
deleted file mode 100644 (file)
index 7bf3748..0000000
+++ /dev/null
@@ -1,19 +0,0 @@
-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.