changes

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

diff --git a/correctness-model/writeup/conclusion.tex b/correctness-model/writeup/conclusion.tex
new file mode 100644 (file)
index 0000000..ae07691
--- /dev/null
+++ b/correctness-model/writeup/conclusion.tex
@@ -0,0 +1,11 @@
+\mysection{Conclusion\label{sec:conclusion}}
+
+The \TOOL specification language and checking system makes it easier
+to unit test concurrent data structures written for the C/C++11 memory
+model.  It extends and modifies classic approaches to defining the
+desired behaviors of concurrent data structures with respect to
+sequential versions of the same data structure to
+apply to the C/C++ memory model.  Our evaluation shows
+that the approach can be used to specify and test correctness
+properties for a range of data structures including a
+lock-free hashtable, work-stealing deque, queues and locks.