correctness-model/writeup/paper.bbl

   1 \begin{thebibliography}{10}
   2
   3 \bibitem{cpp11spec}
   4 {ISO/IEC 14882:2011}, {Information} technology -- programming languages --
   5   {C++}.
   6
   7 \bibitem{c11spec}
   8 {ISO/IEC 9899:2011}, {Information} technology -- programming languages -- {C}.
   9
  10 \bibitem{c11popl}
  11 M.~Batty, S.~Owens, S.~Sarkar, P.~Sewell, and T.~Weber.
  12 \newblock Mathematizing {C++} concurrency.
  13 \newblock In {\em Proceedings of the Symposium on Principles of Programming
  14   Languages}, 2011.
  15
  16 \bibitem{boehmpldi}
  17 H.~J. Boehm and S.~V. Adve.
  18 \newblock Foundations of the {C++} concurrency memory model.
  19 \newblock In {\em Proceedings of the 2008 ACM SIGPLAN Conference on Programming
  20   Language Design and Implementation}, 2008.
  21
  22 \bibitem{lineup}
  23 S.~Burckhardt, C.~Dern, M.~Musuvathi, and R.~Tan.
  24 \newblock Line-up: A complete and automatic linearizability checker.
  25 \newblock In {\em Proceedings of the 2010 ACM SIGPLAN Conference on Programming
  26   Language Design and Implementation}, 2010.
  27
  28 \bibitem{rcu}
  29 M.~Desnoyers, P.~E. McKenney, A.~S. Stern, M.~R. Dagenais, and J.~Walpole.
  30 \newblock User-level implementations of read-copy update.
  31 \newblock {\em IEEE Transactions on Parallel and Distributed Systems}, 2011.
  32
  33 \bibitem{vyrd}
  34 T.~Elmas, S.~Tasiran, and S.~Qadeer.
  35 \newblock {VYRD}: Verifying concurrent programs by runtime refinement-violation
  36   detection.
  37 \newblock In {\em Proceedings of the 2005 ACM SIGPLAN Conference on Programming
  38   Language Design and Implementation}, 2005.
  39
  40 \bibitem{linearizableref}
  41 M.~Herlihy and J.~Wing.
  42 \newblock Linearizability: a correctness condition for concurrent objects.
  43 \newblock {\em ACM Transactions on Programming Languages and Systems},
  44   12(3):463--492, July 1990.
  45
  46 \bibitem{scmemorymodel}
  47 L.~Lamport.
  48 \newblock How to make a multiprocessor computer that correctly executes
  49   multiprocess programs.
  50 \newblock {\em IEEE Transactions on Computers}, 28(9):690--691, Sept. 1979.
  51
  52 \bibitem{javaConcurrentHashMap}
  53 D.~Lea.
  54 \newblock util.concurrent.{ConcurrentHashMap} in java.util.concurrent the {Java
  55   Concurrency Package}.
  56 \newblock
  57   \url{http://docs.oracle.com/javase/8/docs/api/java/util/concurrent/ConcurrentHashMap.html}.
  58
  59 \bibitem{lockfreequeue}
  60 M.~M. Michael and M.~L. Scott.
  61 \newblock Simple, fast, and practical non-blocking and blocking concurrent
  62   queue algorithms.
  63 \newblock In {\em Proceedings of the Fifteenth Annual ACM Symposium on
  64   Principles of Distributed Computing}, 1996.
  65
  66 \bibitem{cdschecker}
  67 B.~Norris and B.~Demsky.
  68 \newblock {CDSChecker}: Checking concurrent data structures written with
  69   {C/C++} atomics.
  70 \newblock In {\em Proceeding of the 28th ACM SIGPLAN Conference on
  71   Object-Oriented Programming, Systems, Languages, and Applications}, 2013.
  72
  73 \bibitem{VechevMCLinear}
  74 M.~Vechev, E.~Yahav, and G.~Yorsh.
  75 \newblock Experience with model checking linearizability.
  76 \newblock In {\em International SPIN Workshop on Model Checking Software},
  77   2009.
  78
  79 \bibitem{relacy}
  80 D.~Vyukov.
  81 \newblock Relacy race detector.
  82 \newblock \url{http://relacy.sourceforge.net/}, 2011 Oct.
  83
  84 \end{thebibliography}