@inproceedings{clockvector, author = "Friedemann Mattern", title = "Virtual Time and Global States of Distributed Systems", booktitle = "Workshop on Parallel and Distributed Algorithms", year = "1989" } @article{scmemorymodel, author = {Lamport, Leslie}, title = { How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs}, journal = {IEEE Transactions on Computers}, issue_date = {September 1979}, volume = {28}, number = {9}, month = sep, year = {1979}, pages = {690--691} } @article{cantin, author = {Cantin, Jason F. and Lipasti, Mikko H. and Smith, James E.}, title = {The Complexity of Verifying Memory Coherence and Consistency}, journal = {IEEE Transactions on Parallel and Distributed Systems}, issue_date = {July 2005}, volume = {16}, number = {7}, month = jul, year = {2005}, issn = {1045-9219}, pages = {663--671} } @inproceedings{roycav, author = {Roy, Amitabha and Zeisset, Stephan and Fleckenstein, Charles J. and Huang, John C.}, title = {Fast and Generalized Polynomial Time Memory Consistency Verification}, booktitle = {Proceedings of the 18th International Conference on Computer Aided Verification}, year = {2006} } @INPROCEEDINGS{qbornotqb, author = {Ganesh Gopalakrishnan and Yue Yang and Hemanthkumar Sivaraj}, title = {{QB} or not {QB}: An efficient execution verification tool for memory orderings}, booktitle = cav04, year = {2004}, pages = {401--413} } @Article{testsm, author = {Phillip B. Gibbons and Ephraim Korach}, title = {Testing Shared Memories}, journal = {SIAM Journal on Computing}, year = {1997}, volume = {26}, number = {4}, pages = {1208-1244}, month = {August} } @inproceedings{koushiksc, author = {Burnim, Jabob and Sen, Koushik and Stergiou, Christos}, title = {Sound and complete monitoring of sequential consistency for relaxed memory models}, booktitle = tacas11, year = {2011} } @inproceedings{burckhardtverif, author = {Burckhardt, Sebastian and Musuvathi, Madanlal}, title = {Effective Program Verification for Relaxed Memory Models}, booktitle = cav08, year = {2008} } @inproceedings{checkfence, author = {Burckhardt, Sebastian and Alur, Rajeev and Martin, Milo M. K.}, title = {CheckFence: Checking consistency of concurrent data types on relaxed memory models}, booktitle = pldi07, year = {2007} } @inproceedings{cdschecker, author = {Norris, Brian and Demsky, Brian}, title = {{CDSChecker}: Checking Concurrent Data Structures Written with {C/C++} Atomics}, booktitle = oopsla13, year = {2013} } @inproceedings{poplabstraction, author = {Batty, Mark and Dodds, Mike and Gotsman, Alexey}, title = {Library abstraction for {C/C++} concurrency}, booktitle = popl13, year = {2013} } @inproceedings{mspcboehm, author = {Boehm, Hans}, title = {Can seqlocks get along with programming language memory models?}, booktitle = mspc12, year = {2012}, } @inproceedings{pldisc, author={Daniel Marino and Abhayendra Singh and Todd Millstein and Madanlal Musuvathi and Satish Narayanasamy}, title={A Case for an SC-Preserving Compiler}, booktitle=pldi11, year={2011} } @inproceedings{ppoppworkstealing, author = {L\^{e}, Nhat Minh and Pop, Antoniu and Cohen, Albert and Zappa Nardelli, Francesco}, title = {Correct and efficient work-stealing for weak memory models}, booktitle = ppopp13, year = {2013} } @inproceedings{adversarialmemory, author = {Flanagan, Cormac and Freund, Stephen N.}, title = {Adversarial memory for detecting destructive races}, booktitle = pldi10, year = {2010} } @inproceedings{verisoft, author = {Godefroid, Patrice}, title = {Model checking for programming languages using {VeriSoft}}, booktitle = popl97, year = {1997} } @ARTICLE{dillmodel, author = {Seungjoon Park and David L. Dill}, title = {An Executable Specification and Verifier for Relaxed Memory Order}, journal = ieeetc, year = {1999}, volume = {48} } @inproceedings{vechevpartialcoherence11, author = {Kuperstein, Michael and Vechev, Martin and Yahav, Eran}, title = {Partial-coherence abstractions for relaxed memory models}, booktitle = pldi11, year = {2011} } @inproceedings{vechevfmcad, author = {Kuperstein, Michael and Vechev, Martin and Yahav, Eran}, title = {Automatic inference of memory fences}, booktitle = fcad10, year = {2010} } @article{sparcmodel, author = {Jonsson, Bengt}, title = {State-space exploration for concurrent algorithms under weak memory orderings}, journal = {SIGARCH Computer Architecture News}, issue_date = {December 2008}, volume = {36}, number = {5}, month = jun, year = {2009}, pages = {65--71}, numpages = {7}, } @inproceedings{inspect1, author = {Yang, Yu and Chen, Xiaofang and Gopalakrishnan, Ganesh and Wang, Chao}, title = {Automatic Discovery of Transition Symmetry in Multithreaded Programs Using Dynamic Analysis}, booktitle = spin09, year = {2009}, location = {Grenoble, France}, pages = {279--295} } @article{sleepset, author = {Godefroid, Patrice}, title = {Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem}, year = {1996}, journal = lncs, vol = {1032} } @Article{inspect2, author = {Chao Wang and Yu Yang and Aarti Gupta and Ganesh Gopalakrishnan}, title = {Dynamic Model Checking with Property Driven Pruning to Detect Race Conditions}, journal = {ATVA LNCS}, year={2008}, number = {126--140} } @InProceedings{inspect3, author = {Yu Yang and Xiaofang Chen and Ganesh Gopalakrishnan and Robert M. Kirby}, title = {Efficient Stateful Dynamic Partial Order Reduction}, booktitle = spin08, year = {2008} } @inproceedings{inspect4, author = {Yang, Yu and Chen, Xiaofang and Gopalakrishnan, Ganesh and Kirby, Robert M.}, title = {Distributed Dynamic Partial Order Reduction Based Verification of Threaded Software}, booktitle = spin07, year = {2007}, pages = {58--75} } @Article{savage1997, author = {Savage, Stefan and Burrows, Michael and Nelson, Greg and Sobalvarro, Patrick and Anderson, Thomas}, title = {Eraser: A Dynamic Data Race Detector for Multithreaded Programs}, journal = tocs, volume = {15}, issue = {4}, month = {Nov.}, year = {1997}, pages = {391--411}, } @inproceedings{Zhou2007, author = {Zhou, Pin and Teodorescu, Radu and Zhou, Yuanyuan}, title = {{HARD}: Hardware-Assisted Lockset-based Race Detection}, booktitle = hpca07, year = {2007}, pages = {121--132} } @article{Gait1986, author = {Gait, Jason}, title = {A probe effect in concurrent programs}, journal = {Software Practice and Experience}, volume = {16}, issue = {3}, month = {March}, year = {1986}, pages = {225--233} } @inproceedings{Gupta2009, author = {Gupta, Shantanu and Sultan, Florin and Cadambi, Srihari and Ivancic, Franjo and Rotteler, Martin}, title = {Using Hardware Transactional Memory for Data Race Detection}, booktitle = ipdps09, year = {2009}, pages = {1--11}, } @inproceedings{Kudrjavets2006, author = {Kudrjavets, Gunnar and Nagappan, Nachiappan and Ball, Thomas}, title = {Assessing the Relationship between Software Assertions and Faults: An Empirical Investigation}, booktitle = {Proceedings of the 17th International Symposium on Software Reliability Engineering}, year = {2006}, pages = {204--212} } @inproceedings{lockfreequeue, author = {Michael, Maged M. and Scott, Michael L.}, title = {Simple, Fast, and Practical Non-Blocking and Blocking Concurrent Queue Algorithms}, booktitle = podc96, year = {1996} } @inproceedings{testera, author = {Marinov, Darko and Khurshid, Sarfraz}, title = {TestEra: A Novel Framework for Automated Testing of {Java} Programs}, booktitle = {Proceedings of the 16th IEEE International Conference on Automated Software Engineering}, year = {2001} } @article{alloy, author = {Jackson, Daniel}, title = {Alloy: A Lightweight Object Modelling Notation}, journal = {ACM Transactions on Software Engineering and Methodology (TOSEM)}, volume = {11}, issue = {2}, month = {April}, year = {2002}, pages = {256--290} } @InProceedings{ltl, author = {Amir Pnueli}, title = {The Temporal Logic of Programs}, booktitle = {Proceedings of the 18th Annual Symposium on Foundations of Computer Science (FOCS)}, pages = {46--57}, Tyear = {1977} } @inproceedings{boehmpldi, author = {Boehm, Hans J. and Adve, Sarita V.}, title = {Foundations of the {C++} concurrency memory model}, booktitle = pldi08, year = {2008} } @Misc{cpp11spec, title = {{ISO/IEC 14882:2011}, {Information} Technology -- Programming Languages -- {C++}}, } @Misc{c11spec, title = {{ISO/IEC 9899:2011}, {Information} Technology -- Programming Languages -- {C}}, } @Misc{ieee1850, title = {1850-2005 {IEEE} Standard for Property Specification Language ({PSL})}, } @Misc{c1xspec, title = {N1548: Programming languages -- {C}}, howpublished = {\url{http://www.open-std.org/jtc1/sc22/wg14/www/docs/n1548.pdf}}, month = {December}, year = {2010}, } @InProceedings{fadinew1, author = {Lu, Shan and Park, Soyeon and Seo, Eunsoo and Zhou, Yuanyuan}, title = {Learning from Mistakes -- A Comprehensive Study on Real World Concurrency Bug Characteristics}, booktitle = pldi08, year = {2008} } @Article{fadinew2, author = {Netzer, Robert H. B. and Miller, Barton P.}, title = {What are Race Conditions?: Some Issues and Formalizations}, journal = {ACM Letters on Programming Languages and Systems}, year = {1992}, volume = {1}, number = {1}, pages = {74--88}, month = {March} } @InProceedings{fadinew3, author = {Jinpeng Wei and Carlton Pu}, title = {Multiprocessors May Reduce System Dependability under File-based Race Condition Attacks}, booktitle = {Proceedings of the 37th Annual IEEE/IFIP International Conference on Dependable Systems and Networks}, year = {2007} } @Article{rcu, author = {Mathie Desnoyers and Paul E McKenney and Alan S Stern and Michel R Dagenais and Jonathan Walpole}, title = {User-Level Implementations of Read-Copy Update}, journal = tpds, year = {2011} } @InProceedings{crugiso, author = {Guoliang Jin and Aditya Thakur and Ben Liblit and Shan Lu}, title = {Instrumentation and Sampling Strategies for {Cooperative} {Concurrency} {Bug} {Isolation}}, booktitle = oopsla10, year = 2010 } @inproceedings{incrementalhashing, author = {Nguyen, Viet Yen and Ruys, Theo C.}, title = {Incremental Hashing for {SPIN}}, booktitle = spin08, year = {2008} } @inproceedings{racetrack, author = {Yu, Yuan and Rodeheffer, Tom and Chen, Wei}, title = {RaceTrack: Efficient Detection of Data Race Conditions via Adaptive Tracking}, booktitle = sosp05, year = {2005} } @inproceedings{nitpicking, author = {Blanchette, Jasmin Christian and Weber, Tjark and Batty, Mark and Owens, Scott and Sarkar, Susmit}, title = {Nitpicking {C++} concurrency}, booktitle = ppdp11, year = {2011} } @inproceedings{c11popl, author = {Batty, Mark and Owens, Scott and Sarkar, Susmit and Sewell, Peter and Weber, Tjark}, title = {Mathematizing {C++} Concurrency}, booktitle = popl11, year = {2011} } @inproceedings{fairstateless, author = {Musuvathi, Madanlal and Qadeer, Shaz}, title = {Fair stateless model checking}, booktitle = pldi08, year = {2008} } @Misc{javaConcurrentHashMap, author = {Doug Lea}, title = {util.concurrent.{ConcurrentHashMap} in java.util.concurrent the {Java Concurrency Package}}, howpublished = {\url{http://docs.oracle.com/javase/8/docs/api/java/util/concurrent/ConcurrentHashMap.html}} } @Misc{clickhashtable, author = {Cliff Click}, title = {A Lock-Free Hash Table}, howpublished = {\url{http://www.azulsystems.com/events/javaone_2007/2007_LockFreeHash.pdf}}, month = {May}, year = {2007} } @inproceedings{racerx, author = {Engler, Dawson and Ashcraft, Ken}, title = {{RacerX}: Effective, Static Detection of Race Conditions and Deadlocks}, booktitle = sosp03, year = {2003} } @inproceedings{conflictexceptions, author = {Lucia, Brandon and Ceze, Luis and Strauss, Karin and Qadeer, Shaz and Boehm, Hans}, title = {Conflict Exceptions: Simplifying Concurrent Language Semantics with Precise Hardware Exceptions for Data-Races}, booktitle = isca10, year = {2010} } @inproceedings{fasttrack, author = {Flanagan, Cormac and Freund, Stephen N.}, title = {{FastTrack}: Efficient and Precise Dynamic Race Detection}, booktitle = pldi09, year = {2009} } @inproceedings{goldilocks, author = {Elmas, Tayfun and Qadeer, Shaz and Tasiran, Serdar}, title = {Goldilocks: A Race and Transaction-Aware {Java} Runtime}, booktitle = pldi07, year = {2007} } @inproceedings{boyapati, author = {Chandrasekhar Boyapati and Robert Lee and Martin Rinard}, title = {{Ownership Types for Safe Programming: Preventing Data Races and Deadlocks}}, booktitle = oopsla02, year = {2002} } @Misc{relacy, author = {Dmitriy Vyukov}, title = {Relacy Race Detector}, howpublished = {\url{http://relacy.sourceforge.net/}}, month = {2011}, year = {Oct.} } @Book{spinmodel, author = {Gerard J. Holzmann}, title = {The {SPIN} Model Checker: Primer and Reference Manual}, publisher = {Addison-Wesley Professional}, year = {2003}, edition = {1st} } @Book{multiprocessorprogramming, author = {Maurice Herlihy and Nir Shavit}, title = {The Art of Multiprocessor Programming}, publisher = {Morgan Kaufmamn}, year = {2012}, edition = {Revised 1st} } @InProceedings{dpor, author = {Cormac Flanagan and Patrice Godefroid}, title = {Dynamic Partial-Order Reduction for Model Checking Software}, booktitle = popl05, month = {Jan.}, year = {2005} } @Article{shavitcacm, author = {Nir Shavit}, title = {Data Structures in the Multicore Age}, journal = cacm, year = {2011}, volume = {54}, number = {3}, month = {March} } % pages = {76--84}, @inproceedings{chess, author = {Madanlal Musuvathi and Shaz Qadeer and Piramanayagam Arumuga Nainar and Thomas Ball and Gerard Basler and Iulian Neamtiu}, title = {Finding and Reproducing {Heisenbugs} in Concurrent Programs}, year = {2008}, booktitle=osdi08 } @inproceedings{lineup, author = {Burckhardt, Sebastian and Dern, Chris and Musuvathi, Madanlal and Tan, Roy}, title = {Line-up: A Complete and Automatic Linearizability Checker}, booktitle = pldi10, year = {2010} } @inproceedings{berger-grace-09, author = {Berger, Emery D. and Yang, Ting and Liu, Tongping and Novark, Gene}, title = {Grace: Safe multithreaded programming for {C}/{C}++}, booktitle = oopsla09, year = {2009}, } @INPROCEEDINGS{charisma, author = {Chao Huang and Laxmikant V. Kale}, title = {Charisma: Orchestrating Migratable Parallel Objects}, booktitle = hpdc07, year = {2007} } @inproceedings{ding-bop-07, author = {Ding, Chen and Shen, Xipeng and Kelsey, Kirk and Tice, Chris and Huang, Ruke and Zhang, Chengliang}, title = {Software behavior oriented parallelization}, booktitle = pldi07, year = {2007}, } @Misc{tilepro64, key = {tilera}, title = {TILEPro64 Processor}, howpublished = {\url{http://tilera.com/products/processors/TILEPRO64}}, month = {December}, year = {2010} } @Misc{magnycour, key = {amd}, title = {{AMD} {Opteron} 6000 Series Platform}, howpublished = {\url{http://www.amd.com/us/products/server/processors/6000-series-platform/pages/6000-series-platform.aspx}}, month = {December}, year = {2010} } @inproceedings{delaunay, author = {Guibas, Leonidas J. and Knuth, Donald E. and Sharir, Micha}, title = {Randomized Incremental Construction of {Delaunay} and {Voronoi} Diagrams}, booktitle = {Proceedings of the Seventeenth International Colloquium on Automata, Languages and Programming}, year = {1990}, location = {Warwick University, England}, pages = {414--431}, numpages = {18}, publisher = {Springer-Verlag New York, Inc.}, address = {New York, NY, USA}, } @inproceedings{1000core, author = {Borkar, Shekhar}, title = {Thousand Core Chips: A Technology Perspective}, booktitle = dac07, year = {2007} } @PhDThesis{r-cilk-98, author = {Keith H. Randall}, title = {Cilk: Efficient Multithreaded Computing}, school = {Massachusetts Institute of Technology}, year = 1998, } @InProceedings{dll-jcilk-05, author = {John S. Danaher and I-Ting Angelina Lee and Charles E. Leiserson}, title = {The {JCilk} Language for Multithreaded Computing}, booktitle = scool05, year = 2005, } @inproceedings{java-grande, author = {Smith, L. A. and Bull, J. M. and Obdrz\'{a}lek, J.}, title = {A Parallel {J}ava {G}rande Benchmark Suite}, booktitle = sc01, year = {2001} } @inproceedings{spin-commit-atomicity, author = {Flanagan, Cormac}, title = {Verifying Commit-Atomicity using Model-Checking}, booktitle = spin04, year = {2004} } @Article{linearizableref, author = {Maurice Herlihy and Jeannette Wing}, title = {Linearizability: a correctness condition for concurrent objects}, journal = {ACM Transactions on Programming Languages and Systems}, year = {1990}, volume = {12}, number = {3}, pages = {463-492}, month = {July} } @Article{refinement-mapping, author = {Abadi, Martine and Lamport, Leslie}, title = {The existence of Refinement Mapping}, journal = {Theoretical Computer Science}, year = {1991}, volume = {82}, number = {2}, pages = {253-284}, month = {May} } @inproceedings{abstraction-linearizability, author = {Amit, D. and Rinetzky, N. and Reps, T. and Sagiv, M. and Yahav, E. }, title = {Comparison under Abstraction for Verifying Linearizability}, booktitle = cav07, year = {2007} } @inproceedings{formal-verification-set, author = {Colvin, R. and Groves, L. and Luchangco, V. and Moir, M.}, title = {Formal Verification of a Lazy Concurrent List-Based Set Algorithm}, booktitle = cav06, year = {2006} } @inproceedings{concurrit, author = {Elmas, T. and Burnim, J. and Necula, G. and Sen, K.}, title = {{CONCURRIT}: A Domain Specific Language for Reproducing Concurrency Bugs}, booktitle = pldi13, year = {2013} } @inproceedings{gambit, author = {Coons, K. E. and Burckhardt, S. and Musuvathi, M.}, title = {{GAMBIT}: Effective Unit Testing for Concurrency Libraries}, booktitle = ppopp10, year = {2010} } @inproceedings{memtest, author = {Burnim, J. and Sen, K. and Stergiou, C.}, title = {Testing Concurrent Programs on Relaxed Memory Models}, booktitle = issta11, year = {2011} } @inproceedings{ndetermin, author = {Burnim, J. and Elmas, T. and Necula, G. and Sen, K.}, title = {{NDetermin}: Inferring Nondeterministic Sequential Specifications for Parallelism Correctness}, booktitle = ppopp12, year = {2012} } @inproceedings{vyrd, author = {Elmas, T. and Tasiran, S. and Qadeer, S.}, title = {{VYRD}: VerifYing Concurrent Programs by Runtime Refinement-Violation Detection}, booktitle = pldi05, year = {2005} } @inproceedings{thread-quantification, author = {Berdine, J. and Lev-Ami, T. and Manivich, R. and Ramalingam, G. and Sagiv, M.}, title = {Thread Quantification for Concurrent Shape Analysis}, booktitle = cav08, year = {2008} } @inproceedings{VechevMCLinear, author = {Vechev, Martin and Yahav, Eran and Yorsh, Greta}, title = {Experience with Model Checking Linearizability}, booktitle = "International SPIN Workshop on Model Checking Software", year = {2009} } @inproceedings{shape-value-abstraction, author = {Vafeiadis, Viktor}, title = {Shape-Value Abstraction for Verifying Linearizability}, booktitle = vmcai09, year = {2009} } @Article{test-verify-concurrent-objects, author = {Wing, Jeannette M. and Gong, Chun}, title = {Testing and Verifying Concurrent Objects}, journal = {Journal of Parallel and Distributed Computing - Special issue on parallel I/O systems}, year = {1993}, volume = {17}, number = {1-2}, pages = {164-182}, month = {Jan./Feb.} } @inproceedings{stamp, title = {{STAMP}: Stanford Transactional Applications for Multi-Processing}, author = {Cao Minh, Chi and Chung, JaeWoong and Kozyrakis, Christos and Olukotun, Kunle}, booktitle = iiswc08, year = {2008} } @article{l-clocks, author = {Lamport, Leslie}, title = {Time, clocks, and the ordering of events in a distributed system}, journal = cacm, issue_date = {July 1978}, volume = {21}, number = {7}, month = jul, year = {1978}, pages = {558--565}, numpages = {8}, acmid = {359563}, publisher = {ACM}, address = {New York, NY, USA}, keywords = {clock synchronization, computer networks, distributed systems, multiprocess systems}, } @inproceedings{reverse-execution, author = {Pan, Douglas Z. and Linton, Mark A.}, title = {Supporting reverse execution for parallel programs}, booktitle = padd88, year = {1988} } @misc{linux, title = {Linux Kernel v3.6}, howpublished = {\url{http://kernel.org/}}, month = {September}, year = {2012}, } @inproceedings{mcs-lock, author = {Mellor-Crummey, John M. and Scott, Michael L.}, title = {Synchronization without contention}, booktitle = asplos91, year = {1991}, location = {Santa Clara, California, United States}, pages = {269--278}, numpages = {10}, acmid = {106999}, } @misc{barrier-url, howpublished = {\url{http://stackoverflow.com/questions/8115267/writing-a-spinning-thread-barrier-using-c11-atomics}}, note = {Oct. 2012}, } @misc{mcs-lock-url, howpublished = {\url{http://cbloomrants.blogspot.com/2011/07/07-18-11-mcs-list-based-lock\_18.html}}, note = {Oct. 2012}, } @misc{spsc-queue-url, howpublished = {\url{https://groups.google.com/forum/#!msg/comp.programming.threads/nSSFT9vKEe0/7eD3ioDg6nEJ}}, note = {Oct. 2012}, } @misc{mpmc-queue-url, howpublished = {\url{http://cbloomrants.blogspot.com/2011/07/07-30-11-look-at-some-bounded-queues.html}}, note = {Oct. 2012}, } @misc{dekker-url, howpublished = {\url{http://www.justsoftwaresolutions.co.uk/threading/}}, note = {Dec. 2012}, }