changes
[cdsspec-compiler.git] / correctness-model / writeup / paper.bbl
diff --git a/correctness-model/writeup/paper.bbl b/correctness-model/writeup/paper.bbl
deleted file mode 100644 (file)
index e7f99db..0000000
+++ /dev/null
@@ -1,84 +0,0 @@
-\begin{thebibliography}{10}
-
-\bibitem{cpp11spec}
-{ISO/IEC 14882:2011}, {Information} technology -- programming languages --
-  {C++}.
-
-\bibitem{c11spec}
-{ISO/IEC 9899:2011}, {Information} technology -- programming languages -- {C}.
-
-\bibitem{c11popl}
-M.~Batty, S.~Owens, S.~Sarkar, P.~Sewell, and T.~Weber.
-\newblock Mathematizing {C++} concurrency.
-\newblock In {\em Proceedings of the Symposium on Principles of Programming
-  Languages}, 2011.
-
-\bibitem{boehmpldi}
-H.~J. Boehm and S.~V. Adve.
-\newblock Foundations of the {C++} concurrency memory model.
-\newblock In {\em Proceedings of the 2008 ACM SIGPLAN Conference on Programming
-  Language Design and Implementation}, 2008.
-
-\bibitem{lineup}
-S.~Burckhardt, C.~Dern, M.~Musuvathi, and R.~Tan.
-\newblock Line-up: A complete and automatic linearizability checker.
-\newblock In {\em Proceedings of the 2010 ACM SIGPLAN Conference on Programming
-  Language Design and Implementation}, 2010.
-
-\bibitem{rcu}
-M.~Desnoyers, P.~E. McKenney, A.~S. Stern, M.~R. Dagenais, and J.~Walpole.
-\newblock User-level implementations of read-copy update.
-\newblock {\em IEEE Transactions on Parallel and Distributed Systems}, 2011.
-
-\bibitem{vyrd}
-T.~Elmas, S.~Tasiran, and S.~Qadeer.
-\newblock {VYRD}: Verifying concurrent programs by runtime refinement-violation
-  detection.
-\newblock In {\em Proceedings of the 2005 ACM SIGPLAN Conference on Programming
-  Language Design and Implementation}, 2005.
-
-\bibitem{linearizableref}
-M.~Herlihy and J.~Wing.
-\newblock Linearizability: a correctness condition for concurrent objects.
-\newblock {\em ACM Transactions on Programming Languages and Systems},
-  12(3):463--492, July 1990.
-
-\bibitem{scmemorymodel}
-L.~Lamport.
-\newblock How to make a multiprocessor computer that correctly executes
-  multiprocess programs.
-\newblock {\em IEEE Transactions on Computers}, 28(9):690--691, Sept. 1979.
-
-\bibitem{javaConcurrentHashMap}
-D.~Lea.
-\newblock util.concurrent.{ConcurrentHashMap} in java.util.concurrent the {Java
-  Concurrency Package}.
-\newblock
-  \url{http://docs.oracle.com/javase/8/docs/api/java/util/concurrent/ConcurrentHashMap.html}.
-
-\bibitem{lockfreequeue}
-M.~M. Michael and M.~L. Scott.
-\newblock Simple, fast, and practical non-blocking and blocking concurrent
-  queue algorithms.
-\newblock In {\em Proceedings of the Fifteenth Annual ACM Symposium on
-  Principles of Distributed Computing}, 1996.
-
-\bibitem{cdschecker}
-B.~Norris and B.~Demsky.
-\newblock {CDSChecker}: Checking concurrent data structures written with
-  {C/C++} atomics.
-\newblock In {\em Proceeding of the 28th ACM SIGPLAN Conference on
-  Object-Oriented Programming, Systems, Languages, and Applications}, 2013.
-
-\bibitem{VechevMCLinear}
-M.~Vechev, E.~Yahav, and G.~Yorsh.
-\newblock Experience with model checking linearizability.
-\newblock In {\em International SPIN Workshop on Model Checking Software},
-  2009.
-
-\bibitem{relacy}
-D.~Vyukov.
-\newblock Relacy race detector.
-\newblock \url{http://relacy.sourceforge.net/}, 2011 Oct.
-
-\end{thebibliography}