1 @inproceedings{clockvector,
2 author = "Friedemann Mattern",
3 title = "Virtual Time and Global States of Distributed Systems",
4 booktitle = "Workshop on Parallel and Distributed Algorithms",
8 @article{scmemorymodel,
9 author = {Lamport, Leslie},
10 title = { How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs},
11 journal = {IEEE Transactions on Computers},
12 issue_date = {September 1979},
21 author = {Cantin, Jason F. and Lipasti, Mikko H. and Smith, James E.},
22 title = {The Complexity of Verifying Memory Coherence and Consistency},
23 journal = {IEEE Transactions on Parallel and Distributed Systems},
24 issue_date = {July 2005},
33 @inproceedings{roycav,
34 author = {Roy, Amitabha and Zeisset, Stephan and Fleckenstein, Charles J. and Huang, John C.},
35 title = {Fast and Generalized Polynomial Time Memory Consistency Verification},
36 booktitle = {Proceedings of the 18th International Conference on Computer Aided Verification},
41 @INPROCEEDINGS{qbornotqb,
42 author = {Ganesh Gopalakrishnan and Yue Yang and Hemanthkumar Sivaraj},
43 title = {{QB} or not {QB}: An efficient execution verification tool for memory orderings},
50 author = {Phillip B. Gibbons and Ephraim Korach},
51 title = {Testing Shared Memories},
52 journal = {SIAM Journal on Computing},
62 @inproceedings{koushiksc,
63 author = {Burnim, Jabob and Sen, Koushik and Stergiou, Christos},
64 title = {Sound and complete monitoring of sequential consistency for relaxed memory models},
69 @inproceedings{burckhardtverif,
70 author = {Burckhardt, Sebastian and Musuvathi, Madanlal},
71 title = {Effective Program Verification for Relaxed Memory Models},
76 @inproceedings{checkfence,
77 author = {Burckhardt, Sebastian and Alur, Rajeev and Martin, Milo M. K.},
78 title = {CheckFence: Checking consistency of concurrent data types on relaxed memory models},
83 @inproceedings{cdschecker,
84 author = {Norris, Brian and Demsky, Brian},
85 title = {{CDSChecker}: Checking Concurrent Data Structures Written with {C/C++} Atomics},
90 @inproceedings{poplabstraction,
91 author = {Batty, Mark and Dodds, Mike and Gotsman, Alexey},
92 title = {Library abstraction for {C/C++} concurrency},
98 @inproceedings{mspcboehm,
99 author = {Boehm, Hans},
100 title = {Can seqlocks get along with programming language memory models?},
106 @inproceedings{pldisc,
107 author={Daniel Marino and Abhayendra Singh and Todd Millstein and Madanlal Musuvathi and Satish Narayanasamy},
108 title={A Case for an SC-Preserving Compiler},
113 @inproceedings{ppoppworkstealing,
114 author = {L\^{e}, Nhat Minh and Pop, Antoniu and Cohen, Albert and Zappa Nardelli, Francesco},
115 title = {Correct and efficient work-stealing for weak memory models},
121 @inproceedings{adversarialmemory,
122 author = {Flanagan, Cormac and Freund, Stephen N.},
123 title = {Adversarial memory for detecting destructive races},
129 @inproceedings{verisoft,
130 author = {Godefroid, Patrice},
131 title = {Model checking for programming languages using {VeriSoft}},
138 author = {Seungjoon Park and David L. Dill},
139 title = {An Executable Specification and Verifier for Relaxed Memory Order},
145 @inproceedings{vechevpartialcoherence11,
146 author = {Kuperstein, Michael and Vechev, Martin and Yahav, Eran},
147 title = {Partial-coherence abstractions for relaxed memory models},
152 @inproceedings{vechevfmcad,
153 author = {Kuperstein, Michael and Vechev, Martin and Yahav, Eran},
154 title = {Automatic inference of memory fences},
161 author = {Jonsson, Bengt},
162 title = {State-space exploration for concurrent algorithms under weak memory orderings},
163 journal = {SIGARCH Computer Architecture News},
164 issue_date = {December 2008},
174 @inproceedings{inspect1,
175 author = {Yang, Yu and Chen, Xiaofang and Gopalakrishnan, Ganesh and Wang, Chao},
176 title = {Automatic Discovery of Transition Symmetry in Multithreaded Programs Using Dynamic Analysis},
179 location = {Grenoble, France},
185 author = {Godefroid, Patrice},
186 title = {Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem},
193 author = {Chao Wang and Yu Yang and Aarti Gupta and Ganesh Gopalakrishnan},
194 title = {Dynamic Model Checking with Property Driven Pruning to Detect Race Conditions},
195 journal = {ATVA LNCS},
202 @InProceedings{inspect3,
203 author = {Yu Yang and Xiaofang Chen and Ganesh Gopalakrishnan and Robert M. Kirby},
204 title = {Efficient Stateful Dynamic Partial Order Reduction},
210 @inproceedings{inspect4,
211 author = {Yang, Yu and Chen, Xiaofang and Gopalakrishnan, Ganesh and Kirby, Robert M.},
212 title = {Distributed Dynamic Partial Order Reduction Based Verification of Threaded Software},
219 author = {Savage, Stefan and Burrows, Michael and Nelson, Greg and Sobalvarro, Patrick and Anderson, Thomas},
220 title = {Eraser: A Dynamic Data Race Detector for Multithreaded Programs},
229 @inproceedings{Zhou2007,
230 author = {Zhou, Pin and Teodorescu, Radu and Zhou, Yuanyuan},
231 title = {{HARD}: Hardware-Assisted Lockset-based Race Detection},
238 author = {Gait, Jason},
239 title = {A probe effect in concurrent programs},
240 journal = {Software Practice and Experience},
249 @inproceedings{Gupta2009,
250 author = {Gupta, Shantanu and Sultan, Florin and Cadambi, Srihari and Ivancic, Franjo and Rotteler, Martin},
251 title = {Using Hardware Transactional Memory for Data Race Detection},
257 @inproceedings{Kudrjavets2006,
258 author = {Kudrjavets, Gunnar and Nagappan, Nachiappan and Ball, Thomas},
259 title = {Assessing the Relationship between Software Assertions and Faults: An Empirical Investigation},
260 booktitle = {Proceedings of the 17th International Symposium on Software Reliability Engineering},
265 @inproceedings{lockfreequeue,
266 author = {Michael, Maged M. and Scott, Michael L.},
267 title = {Simple, Fast, and Practical Non-Blocking and Blocking Concurrent Queue Algorithms},
272 @inproceedings{testera,
273 author = {Marinov, Darko and Khurshid, Sarfraz},
274 title = {TestEra: A Novel Framework for Automated Testing of {Java} Programs},
275 booktitle = {Proceedings of the 16th IEEE International Conference on Automated Software Engineering},
280 author = {Jackson, Daniel},
281 title = {Alloy: A Lightweight Object Modelling Notation},
282 journal = {ACM Transactions on Software Engineering and Methodology (TOSEM)},
292 author = {Amir Pnueli},
293 title = {The Temporal Logic of Programs},
294 booktitle = {Proceedings of the 18th Annual Symposium on Foundations of Computer Science (FOCS)},
299 @inproceedings{boehmpldi,
300 author = {Boehm, Hans J. and Adve, Sarita V.},
301 title = {Foundations of the {C++} concurrency memory model},
307 title = {{ISO/IEC 14882:2011}, {Information} Technology -- Programming Languages -- {C++}},
311 title = {{ISO/IEC 9899:2011}, {Information} Technology -- Programming Languages -- {C}},
315 title = {1850-2005 {IEEE} Standard for Property Specification Language ({PSL})},
319 title = {N1548: Programming languages -- {C}},
320 howpublished = {\url{http://www.open-std.org/jtc1/sc22/wg14/www/docs/n1548.pdf}},
325 @InProceedings{fadinew1,
326 author = {Lu, Shan and Park, Soyeon and Seo, Eunsoo and Zhou, Yuanyuan},
327 title = {Learning from Mistakes -- A Comprehensive Study on Real World Concurrency Bug Characteristics},
334 author = {Netzer, Robert H. B. and Miller, Barton P.},
335 title = {What are Race Conditions?: Some Issues and Formalizations},
336 journal = {ACM Letters on Programming Languages and Systems},
344 @InProceedings{fadinew3,
345 author = {Jinpeng Wei and Carlton Pu},
346 title = {Multiprocessors May Reduce System Dependability under File-based Race Condition Attacks},
347 booktitle = {Proceedings of the 37th Annual IEEE/IFIP International Conference on Dependable Systems and Networks},
352 author = {Mathie Desnoyers and Paul E McKenney and Alan S Stern and Michel R Dagenais and Jonathan Walpole},
353 title = {User-Level Implementations of Read-Copy Update},
358 @InProceedings{crugiso,
359 author = {Guoliang Jin and Aditya Thakur and Ben Liblit and
361 title = {Instrumentation and Sampling Strategies for
362 {Cooperative} {Concurrency} {Bug} {Isolation}},
363 booktitle = oopsla10,
367 @inproceedings{incrementalhashing,
368 author = {Nguyen, Viet Yen and Ruys, Theo C.},
369 title = {Incremental Hashing for {SPIN}},
374 @inproceedings{racetrack,
375 author = {Yu, Yuan and Rodeheffer, Tom and Chen, Wei},
376 title = {RaceTrack: Efficient Detection of Data Race Conditions via Adaptive Tracking},
382 @inproceedings{nitpicking,
383 author = {Blanchette, Jasmin Christian and Weber, Tjark and Batty, Mark and Owens, Scott and Sarkar, Susmit},
384 title = {Nitpicking {C++} concurrency},
390 @inproceedings{c11popl,
391 author = {Batty, Mark and Owens, Scott and Sarkar, Susmit and Sewell, Peter and Weber, Tjark},
392 title = {Mathematizing {C++} Concurrency},
397 @inproceedings{fairstateless,
398 author = {Musuvathi, Madanlal and Qadeer, Shaz},
399 title = {Fair stateless model checking},
404 @Misc{javaConcurrentHashMap,
406 title = {util.concurrent.{ConcurrentHashMap} in java.util.concurrent the {Java Concurrency Package}},
407 howpublished = {\url{http://docs.oracle.com/javase/8/docs/api/java/util/concurrent/ConcurrentHashMap.html}}
410 @Misc{clickhashtable,
411 author = {Cliff Click},
412 title = {A Lock-Free Hash Table},
413 howpublished = {\url{http://www.azulsystems.com/events/javaone_2007/2007_LockFreeHash.pdf}},
418 @inproceedings{racerx,
419 author = {Engler, Dawson and Ashcraft, Ken},
420 title = {{RacerX}: Effective, Static Detection of Race Conditions and Deadlocks},
425 @inproceedings{conflictexceptions,
426 author = {Lucia, Brandon and Ceze, Luis and Strauss, Karin and Qadeer, Shaz and Boehm, Hans},
427 title = {Conflict Exceptions: Simplifying Concurrent Language Semantics with Precise Hardware Exceptions for Data-Races},
433 @inproceedings{fasttrack,
434 author = {Flanagan, Cormac and Freund, Stephen N.},
435 title = {{FastTrack}: Efficient and Precise Dynamic Race Detection},
441 @inproceedings{goldilocks,
442 author = {Elmas, Tayfun and Qadeer, Shaz and Tasiran, Serdar},
443 title = {Goldilocks: A Race and Transaction-Aware {Java} Runtime},
448 @inproceedings{boyapati,
449 author = {Chandrasekhar Boyapati and Robert Lee and Martin Rinard},
450 title = {{Ownership Types for Safe Programming: Preventing Data Races and Deadlocks}},
451 booktitle = oopsla02,
457 author = {Dmitriy Vyukov},
458 title = {Relacy Race Detector},
459 howpublished = {\url{http://relacy.sourceforge.net/}},
465 author = {Gerard J. Holzmann},
466 title = {The {SPIN} Model Checker: Primer and Reference Manual},
467 publisher = {Addison-Wesley Professional},
472 @Book{multiprocessorprogramming,
473 author = {Maurice Herlihy and Nir Shavit},
474 title = {The Art of Multiprocessor Programming},
475 publisher = {Morgan Kaufmamn},
477 edition = {Revised 1st}
481 author = {Cormac Flanagan and Patrice Godefroid},
482 title = {Dynamic Partial-Order Reduction for Model Checking Software},
489 author = {Nir Shavit},
490 title = {Data Structures in the Multicore Age},
499 @inproceedings{chess,
500 author = {Madanlal Musuvathi and Shaz Qadeer and Piramanayagam Arumuga Nainar and Thomas Ball and Gerard Basler and Iulian Neamtiu},
501 title = {Finding and Reproducing {Heisenbugs} in Concurrent Programs},
507 @inproceedings{lineup,
508 author = {Burckhardt, Sebastian and Dern, Chris and Musuvathi, Madanlal and Tan, Roy},
509 title = {Line-up: A Complete and Automatic Linearizability Checker},
514 @inproceedings{berger-grace-09,
515 author = {Berger, Emery D. and Yang, Ting and Liu, Tongping and Novark, Gene},
516 title = {Grace: Safe multithreaded programming for {C}/{C}++},
517 booktitle = oopsla09,
521 @INPROCEEDINGS{charisma,
522 author = {Chao Huang and Laxmikant V. Kale},
523 title = {Charisma: Orchestrating Migratable Parallel Objects},
529 @inproceedings{ding-bop-07,
530 author = {Ding, Chen and Shen, Xipeng and Kelsey, Kirk and Tice, Chris and Huang, Ruke and Zhang, Chengliang},
531 title = {Software behavior oriented parallelization},
538 title = {TILEPro64 Processor},
539 howpublished = {\url{http://tilera.com/products/processors/TILEPRO64}},
546 title = {{AMD} {Opteron} 6000 Series Platform},
547 howpublished = {\url{http://www.amd.com/us/products/server/processors/6000-series-platform/pages/6000-series-platform.aspx}},
552 @inproceedings{delaunay,
553 author = {Guibas, Leonidas J. and Knuth, Donald E. and Sharir, Micha},
554 title = {Randomized Incremental Construction of {Delaunay} and {Voronoi} Diagrams},
555 booktitle = {Proceedings of the Seventeenth International Colloquium on Automata, Languages and Programming},
557 location = {Warwick University, England},
560 publisher = {Springer-Verlag New York, Inc.},
561 address = {New York, NY, USA},
564 @inproceedings{1000core,
565 author = {Borkar, Shekhar},
566 title = {Thousand Core Chips: A Technology Perspective},
571 @PhDThesis{r-cilk-98,
572 author = {Keith H. Randall},
573 title = {Cilk: Efficient Multithreaded Computing},
574 school = {Massachusetts Institute of Technology},
578 @InProceedings{dll-jcilk-05,
579 author = {John S. Danaher and I-Ting Angelina Lee and Charles E. Leiserson},
580 title = {The {JCilk} Language for Multithreaded Computing},
585 @inproceedings{java-grande,
586 author = {Smith, L. A. and Bull, J. M. and Obdrz\'{a}lek, J.},
587 title = {A Parallel {J}ava {G}rande Benchmark Suite},
592 @inproceedings{spin-commit-atomicity,
593 author = {Flanagan, Cormac},
594 title = {Verifying Commit-Atomicity using Model-Checking},
599 @Article{linearizableref,
600 author = {Maurice Herlihy and Jeannette Wing},
601 title = {Linearizability: a correctness condition for concurrent objects},
602 journal = {ACM Transactions on Programming Languages and Systems},
610 @Article{refinement-mapping,
611 author = {Abadi, Martine and Lamport, Leslie},
612 title = {The existence of Refinement Mapping},
613 journal = {Theoretical Computer Science},
621 @inproceedings{abstraction-linearizability,
622 author = {Amit, D. and Rinetzky, N. and Reps, T. and Sagiv, M. and Yahav, E. },
623 title = {Comparison under Abstraction for Verifying Linearizability},
628 @inproceedings{formal-verification-set,
629 author = {Colvin, R. and Groves, L. and Luchangco, V. and Moir, M.},
630 title = {Formal Verification of a Lazy Concurrent List-Based Set Algorithm},
635 @inproceedings{concurrit,
636 author = {Elmas, T. and Burnim, J. and Necula, G. and Sen, K.},
637 title = {{CONCURRIT}: A Domain Specific Language for Reproducing Concurrency Bugs},
642 @inproceedings{gambit,
643 author = {Coons, K. E. and Burckhardt, S. and Musuvathi, M.},
644 title = {{GAMBIT}: Effective Unit Testing for Concurrency Libraries},
649 @inproceedings{memtest,
650 author = {Burnim, J. and Sen, K. and Stergiou, C.},
651 title = {Testing Concurrent Programs on Relaxed Memory Models},
656 @inproceedings{ndetermin,
657 author = {Burnim, J. and Elmas, T. and Necula, G. and Sen, K.},
658 title = {{NDetermin}: Inferring Nondeterministic Sequential Specifications for Parallelism Correctness},
664 author = {Elmas, T. and Tasiran, S. and Qadeer, S.},
665 title = {{VYRD}: VerifYing Concurrent Programs by Runtime Refinement-Violation Detection},
670 @inproceedings{thread-quantification,
671 author = {Berdine, J. and Lev-Ami, T. and Manivich, R. and Ramalingam, G. and Sagiv, M.},
672 title = {Thread Quantification for Concurrent Shape Analysis},
677 @inproceedings{VechevMCLinear,
678 author = {Vechev, Martin and Yahav, Eran and Yorsh, Greta},
679 title = {Experience with Model Checking Linearizability},
680 booktitle = "International SPIN Workshop on Model Checking Software",
684 @inproceedings{shape-value-abstraction,
685 author = {Vafeiadis, Viktor},
686 title = {Shape-Value Abstraction for Verifying Linearizability},
691 @Article{test-verify-concurrent-objects,
692 author = {Wing, Jeannette M. and Gong, Chun},
693 title = {Testing and Verifying Concurrent Objects},
694 journal = {Journal of Parallel and Distributed Computing - Special issue on parallel I/O systems},
702 @inproceedings{stamp,
703 title = {{STAMP}: Stanford Transactional Applications for Multi-Processing},
704 author = {Cao Minh, Chi and Chung, JaeWoong and Kozyrakis, Christos and Olukotun, Kunle},
710 author = {Lamport, Leslie},
711 title = {Time, clocks, and the ordering of events in a distributed system},
713 issue_date = {July 1978},
722 address = {New York, NY, USA},
723 keywords = {clock synchronization, computer networks, distributed systems, multiprocess systems},
726 @inproceedings{reverse-execution,
727 author = {Pan, Douglas Z. and Linton, Mark A.},
728 title = {Supporting reverse execution for parallel programs},
734 title = {Linux Kernel v3.6},
735 howpublished = {\url{http://kernel.org/}},
740 @inproceedings{mcs-lock,
741 author = {Mellor-Crummey, John M. and Scott, Michael L.},
742 title = {Synchronization without contention},
743 booktitle = asplos91,
745 location = {Santa Clara, California, United States},
752 howpublished = {\url{http://stackoverflow.com/questions/8115267/writing-a-spinning-thread-barrier-using-c11-atomics}},
757 howpublished = {\url{http://cbloomrants.blogspot.com/2011/07/07-18-11-mcs-list-based-lock\_18.html}},
761 @misc{spsc-queue-url,
762 howpublished = {\url{https://groups.google.com/forum/#!msg/comp.programming.threads/nSSFT9vKEe0/7eD3ioDg6nEJ}},
766 @misc{mpmc-queue-url,
767 howpublished = {\url{http://cbloomrants.blogspot.com/2011/07/07-30-11-look-at-some-bounded-queues.html}},
772 howpublished = {\url{http://www.justsoftwaresolutions.co.uk/threading/}},