writeup/paper.bib

   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",
   5     year = "1989"
   6 }
   7
   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},
  13  volume = {28},
  14  number = {9},
  15  month = sep,
  16  year = {1979},
  17  pages = {690--691}
  18 }
  19
  20 @article{cantin,
  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},
  25  volume = {16},
  26  number = {7},
  27  month = jul,
  28  year = {2005},
  29  issn = {1045-9219},
  30  pages = {663--671}
  31 }
  32
  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},
  37  year = {2006}
  38 }
  39
  40
  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},
  44     booktitle = cav04,
  45     year = {2004},
  46     pages = {401--413}
  47 }
  48
  49 @Article{testsm,
  50   author =       {Phillip B. Gibbons and Ephraim Korach},
  51   title =        {Testing Shared Memories},
  52   journal =      {SIAM Journal on Computing},
  53   year =         {1997},
  54   volume =    {26},
  55   number =    {4},
  56   pages =     {1208-1244},
  57   month =     {August}
  58 }
  59
  60
  61
  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},
  65  booktitle = tacas11,
  66  year = {2011}
  67 }
  68
  69 @inproceedings{burckhardtverif,
  70  author = {Burckhardt, Sebastian and Musuvathi, Madanlal},
  71  title = {Effective Program Verification for Relaxed Memory Models},
  72  booktitle = cav08,
  73  year = {2008}
  74 }
  75
  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},
  79  booktitle = pldi07,
  80  year = {2007}
  81 }
  82
  83 @inproceedings{cdschecker,
  84  author = {Norris, Brian and Demsky, Brian},
  85  title = {{CDSChecker}: Checking Concurrent Data Structures Written with {C/C++} Atomics},
  86  booktitle = oopsla13,
  87  year = {2013}
  88 }
  89
  90 @inproceedings{poplabstraction,
  91  author = {Batty, Mark and Dodds, Mike and Gotsman, Alexey},
  92  title = {Library abstraction for {C/C++} concurrency},
  93  booktitle = popl13,
  94  year = {2013}
  95 }
  96
  97
  98 @inproceedings{mspcboehm,
  99  author = {Boehm, Hans},
 100  title = {Can seqlocks get along with programming language memory models?},
 101  booktitle = mspc12,
 102  year = {2012},
 103 }
 104
 105
 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},
 109  booktitle=pldi11,
 110  year={2011}
 111 }
 112
 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},
 116  booktitle = ppopp13,
 117  year = {2013}
 118 }
 119
 120
 121 @inproceedings{adversarialmemory,
 122  author = {Flanagan, Cormac and Freund, Stephen N.},
 123  title = {Adversarial memory for detecting destructive races},
 124  booktitle = pldi10,
 125  year = {2010}
 126 }
 127
 128
 129 @inproceedings{verisoft,
 130  author = {Godefroid, Patrice},
 131  title = {Model checking for programming languages using {VeriSoft}},
 132  booktitle = popl97,
 133  year = {1997}
 134 }
 135
 136
 137 @ARTICLE{dillmodel,
 138     author = {Seungjoon Park and David L. Dill},
 139     title = {An Executable Specification and Verifier for Relaxed Memory Order},
 140     journal = ieeetc,
 141     year = {1999},
 142     volume = {48}
 143 }
 144
 145 @inproceedings{vechevpartialcoherence11,
 146  author = {Kuperstein, Michael and Vechev, Martin and Yahav, Eran},
 147  title = {Partial-coherence abstractions for relaxed memory models},
 148  booktitle = pldi11,
 149  year = {2011}
 150 }
 151
 152 @inproceedings{vechevfmcad,
 153  author = {Kuperstein, Michael and Vechev, Martin and Yahav, Eran},
 154  title = {Automatic inference of memory fences},
 155  booktitle = fcad10,
 156  year = {2010}
 157 }
 158
 159
 160 @article{sparcmodel,
 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},
 165  volume = {36},
 166  number = {5},
 167  month = jun,
 168  year = {2009},
 169  pages = {65--71},
 170  numpages = {7},
 171 }
 172
 173
 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},
 177  booktitle = spin09,
 178  year = {2009},
 179  location = {Grenoble, France},
 180  pages = {279--295}
 181 }
 182
 183
 184 @article{sleepset,
 185  author = {Godefroid, Patrice},
 186  title = {Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem},
 187  year = {1996},
 188  journal = lncs,
 189  vol = {1032}
 190 }
 191
 192 @Article{inspect2,
 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},
 196   year={2008},
 197   number =       {126--140}
 198 }
 199
 200
 201
 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},
 205   booktitle = spin08,
 206   year =         {2008}
 207 }
 208
 209
 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},
 213  booktitle = spin07,
 214  year = {2007},
 215  pages = {58--75}
 216 }
 217
 218 @Article{savage1997,
 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},
 221  journal = tocs,
 222  volume = {15},
 223  issue = {4},
 224  month = {Nov.},
 225  year = {1997},
 226  pages = {391--411},
 227 }
 228
 229 @inproceedings{Zhou2007,
 230  author = {Zhou, Pin and Teodorescu, Radu and Zhou, Yuanyuan},
 231  title = {{HARD}: Hardware-Assisted Lockset-based Race Detection},
 232  booktitle = hpca07,
 233  year = {2007},
 234  pages = {121--132}
 235 }
 236
 237 @article{Gait1986,
 238  author = {Gait, Jason},
 239  title = {A probe effect in concurrent programs},
 240  journal = {Software Practice and Experience},
 241  volume = {16},
 242  issue = {3},
 243  month = {March},
 244  year = {1986},
 245  pages = {225--233}
 246 }
 247
 248
 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},
 252  booktitle = ipdps09,
 253  year = {2009},
 254  pages = {1--11},
 255 }
 256
 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},
 261  year = {2006},
 262  pages = {204--212}
 263 }
 264
 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},
 268  booktitle = podc96,
 269  year = {1996}
 270 }
 271
 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},
 276  year = {2001}
 277 }
 278
 279 @article{alloy,
 280  author = {Jackson, Daniel},
 281  title = {Alloy: A Lightweight Object Modelling Notation},
 282  journal = {ACM Transactions on Software Engineering and Methodology (TOSEM)},
 283  volume = {11},
 284  issue = {2},
 285  month = {April},
 286  year = {2002},
 287  pages = {256--290}
 288 }
 289
 290
 291 @InProceedings{ltl,
 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)},
 295   pages =        {46--57},
 296   Tyear =        {1977}
 297 }
 298
 299 @inproceedings{boehmpldi,
 300  author = {Boehm, Hans J. and Adve, Sarita V.},
 301  title = {Foundations of the {C++} concurrency memory model},
 302  booktitle = pldi08,
 303  year = {2008}
 304 }
 305
 306 @Misc{cpp11spec,
 307   title =        {{ISO/IEC 14882:2011}, {Information} Technology -- Programming Languages -- {C++}},
 308 }
 309
 310 @Misc{c11spec,
 311   title =        {{ISO/IEC 9899:2011}, {Information} Technology -- Programming Languages -- {C}},
 312 }
 313
 314 @Misc{ieee1850,
 315   title =        {1850-2005 {IEEE} Standard for Property Specification Language ({PSL})},
 316 }
 317
 318 @Misc{c1xspec,
 319   title =        {N1548: Programming languages -- {C}},
 320   howpublished = {\url{http://www.open-std.org/jtc1/sc22/wg14/www/docs/n1548.pdf}},
 321   month =        {December},
 322   year =         {2010},
 323 }
 324
 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},
 328   booktitle = pldi08,
 329   year =         {2008}
 330 }
 331
 332
 333 @Article{fadinew2,
 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},
 337   year =         {1992},
 338   volume =       {1},
 339   number =       {1},
 340   pages =        {74--88},
 341   month =        {March}
 342 }
 343
 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},
 348   year =         {2007}
 349 }
 350
 351 @Article{rcu,
 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},
 354   journal =     tpds,
 355   year =         {2011}
 356 }
 357
 358 @InProceedings{crugiso,
 359   author =       {Guoliang Jin and Aditya Thakur and Ben Liblit and
 360                   Shan Lu},
 361   title =        {Instrumentation and Sampling Strategies for
 362                   {Cooperative} {Concurrency} {Bug} {Isolation}},
 363   booktitle =    oopsla10,
 364   year =         2010
 365 }
 366
 367 @inproceedings{incrementalhashing,
 368  author = {Nguyen, Viet Yen and Ruys, Theo C.},
 369  title = {Incremental Hashing for {SPIN}},
 370  booktitle = spin08,
 371  year = {2008}
 372 }
 373
 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},
 377  booktitle = sosp05,
 378  year = {2005}
 379 }
 380
 381
 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},
 385  booktitle = ppdp11,
 386  year = {2011}
 387 }
 388
 389
 390 @inproceedings{c11popl,
 391  author = {Batty, Mark and Owens, Scott and Sarkar, Susmit and Sewell, Peter and Weber, Tjark},
 392  title = {Mathematizing {C++} Concurrency},
 393  booktitle = popl11,
 394  year = {2011}
 395 }
 396
 397 @inproceedings{fairstateless,
 398  author = {Musuvathi, Madanlal and Qadeer, Shaz},
 399  title = {Fair stateless model checking},
 400  booktitle = pldi08,
 401  year = {2008}
 402 }
 403
 404 @Misc{javaConcurrentHashMap,
 405   author =       {Doug Lea},
 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}}
 408 }
 409
 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}},
 414   month =        {May},
 415   year =         {2007}
 416 }
 417
 418 @inproceedings{racerx,
 419  author = {Engler, Dawson and Ashcraft, Ken},
 420  title = {{RacerX}: Effective, Static Detection of Race Conditions and Deadlocks},
 421  booktitle = sosp03,
 422  year = {2003}
 423 }
 424
 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},
 428  booktitle = isca10,
 429  year = {2010}
 430 }
 431
 432
 433 @inproceedings{fasttrack,
 434  author = {Flanagan, Cormac and Freund, Stephen N.},
 435  title = {{FastTrack}: Efficient and Precise Dynamic Race Detection},
 436  booktitle = pldi09,
 437  year = {2009}
 438 }
 439
 440
 441 @inproceedings{goldilocks,
 442  author = {Elmas, Tayfun and Qadeer, Shaz and Tasiran, Serdar},
 443  title = {Goldilocks: A Race and Transaction-Aware {Java} Runtime},
 444  booktitle = pldi07,
 445  year = {2007}
 446 }
 447
 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,
 452  year = {2002}
 453  }
 454
 455
 456 @Misc{relacy,
 457   author =       {Dmitriy Vyukov},
 458   title =        {Relacy Race Detector},
 459   howpublished = {\url{http://relacy.sourceforge.net/}},
 460   month =        {2011},
 461   year =         {Oct.}
 462 }
 463
 464 @Book{spinmodel,
 465   author =       {Gerard J. Holzmann},
 466   title =        {The {SPIN} Model Checker: Primer and Reference Manual},
 467   publisher =    {Addison-Wesley Professional},
 468   year =         {2003},
 469   edition =      {1st}
 470 }
 471
 472 @Book{multiprocessorprogramming,
 473   author =       {Maurice Herlihy and Nir Shavit},
 474   title =        {The Art of Multiprocessor Programming},
 475   publisher =    {Morgan Kaufmamn},
 476   year =         {2012},
 477   edition =      {Revised 1st}
 478 }
 479
 480 @InProceedings{dpor,
 481   author =       {Cormac Flanagan and Patrice Godefroid},
 482   title =        {Dynamic Partial-Order Reduction for Model Checking Software},
 483   booktitle = popl05,
 484   month = {Jan.},
 485   year =         {2005}
 486 }
 487
 488 @Article{shavitcacm,
 489   author =       {Nir Shavit},
 490   title =        {Data Structures in the Multicore Age},
 491   journal =      cacm,
 492   year =         {2011},
 493   volume =       {54},
 494   number =       {3},
 495   month =        {March}
 496 }
 497 %  pages =       {76--84},
 498
 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},
 502     year = {2008},
 503     booktitle=osdi08
 504 }
 505
 506
 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},
 510  booktitle = pldi10,
 511  year = {2010}
 512 }
 513
 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,
 518   year = {2009},
 519 }
 520
 521 @INPROCEEDINGS{charisma,
 522 author = {Chao Huang and Laxmikant V. Kale},
 523 title = {Charisma: Orchestrating Migratable Parallel Objects},
 524 booktitle = hpdc07,
 525 year = {2007}
 526 }
 527
 528
 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},
 532   booktitle = pldi07,
 533   year = {2007},
 534 }
 535
 536 @Misc{tilepro64,
 537   key =          {tilera},
 538   title =        {TILEPro64 Processor},
 539   howpublished = {\url{http://tilera.com/products/processors/TILEPRO64}},
 540   month =        {December},
 541   year =         {2010}
 542 }
 543
 544 @Misc{magnycour,
 545   key =          {amd},
 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}},
 548   month =        {December},
 549   year =         {2010}
 550 }
 551
 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},
 556  year = {1990},
 557  location = {Warwick University, England},
 558  pages = {414--431},
 559  numpages = {18},
 560  publisher = {Springer-Verlag New York, Inc.},
 561  address = {New York, NY, USA},
 562 }
 563
 564 @inproceedings{1000core,
 565  author = {Borkar, Shekhar},
 566  title = {Thousand Core Chips: A Technology Perspective},
 567  booktitle = dac07,
 568  year = {2007}
 569  }
 570
 571 @PhDThesis{r-cilk-98,
 572   author = {Keith H. Randall},
 573   title = {Cilk: Efficient Multithreaded Computing},
 574   school = {Massachusetts Institute of Technology},
 575   year = 1998,
 576 }
 577
 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},
 581   booktitle = scool05,
 582   year = 2005,
 583 }
 584
 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},
 588   booktitle = sc01,
 589   year = {2001}
 590 }
 591
 592 @inproceedings{spin-commit-atomicity,
 593  author = {Flanagan, Cormac},
 594  title = {Verifying Commit-Atomicity using Model-Checking},
 595  booktitle = spin04,
 596  year = {2004}
 597 }
 598
 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},
 603         year =  {1990},
 604         volume =        {12},
 605         number =        {3},
 606         pages = {463-492},
 607         month = {July}
 608 }
 609
 610 @Article{refinement-mapping,
 611   author =       {Abadi, Martine and Lamport, Leslie},
 612   title =        {The existence of Refinement Mapping},
 613   journal =      {Theoretical Computer Science},
 614   year =         {1991},
 615   volume =    {82},
 616   number =    {2},
 617   pages =     {253-284},
 618   month =     {May}
 619 }
 620
 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},
 624  booktitle = cav07,
 625  year = {2007}
 626 }
 627
 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},
 631  booktitle = cav06,
 632  year = {2006}
 633 }
 634
 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},
 638  booktitle = pldi13,
 639  year = {2013}
 640 }
 641
 642 @inproceedings{gambit,
 643  author = {Coons, K. E. and Burckhardt, S. and Musuvathi, M.},
 644  title = {{GAMBIT}: Effective Unit Testing for Concurrency Libraries},
 645  booktitle = ppopp10,
 646  year = {2010}
 647 }
 648
 649 @inproceedings{memtest,
 650  author = {Burnim, J. and Sen, K. and Stergiou, C.},
 651  title = {Testing Concurrent Programs on Relaxed Memory Models},
 652  booktitle = issta11,
 653  year = {2011}
 654 }
 655
 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},
 659  booktitle = ppopp12,
 660  year = {2012}
 661 }
 662
 663 @inproceedings{vyrd,
 664  author = {Elmas, T. and Tasiran, S. and Qadeer, S.},
 665  title = {{VYRD}: VerifYing Concurrent Programs by Runtime Refinement-Violation Detection},
 666  booktitle = pldi05,
 667  year = {2005}
 668 }
 669
 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},
 673  booktitle = cav08,
 674  year = {2008}
 675 }
 676
 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",
 681  year = {2009}
 682 }
 683
 684 @inproceedings{shape-value-abstraction,
 685  author = {Vafeiadis, Viktor},
 686  title = {Shape-Value Abstraction for Verifying Linearizability},
 687  booktitle = vmcai09,
 688  year = {2009}
 689 }
 690
 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},
 695   year =         {1993},
 696   volume =    {17},
 697   number =    {1-2},
 698   pages =     {164-182},
 699   month =     {Jan./Feb.}
 700 }
 701
 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},
 705     booktitle = iiswc08,
 706     year      = {2008}
 707 }
 708
 709 @article{l-clocks,
 710   author = {Lamport, Leslie},
 711   title = {Time, clocks, and the ordering of events in a distributed system},
 712   journal = cacm,
 713   issue_date = {July 1978},
 714   volume = {21},
 715   number = {7},
 716   month = jul,
 717   year = {1978},
 718   pages = {558--565},
 719   numpages = {8},
 720   acmid = {359563},
 721   publisher = {ACM},
 722   address = {New York, NY, USA},
 723   keywords = {clock synchronization, computer networks, distributed systems, multiprocess systems},
 724 }
 725
 726 @inproceedings{reverse-execution,
 727   author = {Pan, Douglas Z. and Linton, Mark A.},
 728   title = {Supporting reverse execution for parallel programs},
 729   booktitle = padd88,
 730   year = {1988}
 731 }
 732
 733 @misc{linux,
 734   title = {Linux Kernel v3.6},
 735   howpublished = {\url{http://kernel.org/}},
 736   month = {September},
 737   year = {2012},
 738 }
 739
 740 @inproceedings{mcs-lock,
 741   author = {Mellor-Crummey, John M. and Scott, Michael L.},
 742   title = {Synchronization without contention},
 743   booktitle = asplos91,
 744   year = {1991},
 745   location = {Santa Clara, California, United States},
 746   pages = {269--278},
 747   numpages = {10},
 748   acmid = {106999},
 749 }
 750
 751 @misc{barrier-url,
 752   howpublished = {\url{http://stackoverflow.com/questions/8115267/writing-a-spinning-thread-barrier-using-c11-atomics}},
 753   note =        {Oct. 2012},
 754 }
 755
 756 @misc{mcs-lock-url,
 757   howpublished = {\url{http://cbloomrants.blogspot.com/2011/07/07-18-11-mcs-list-based-lock\_18.html}},
 758   note =        {Oct. 2012},
 759 }
 760
 761 @misc{spsc-queue-url,
 762   howpublished = {\url{https://groups.google.com/forum/#!msg/comp.programming.threads/nSSFT9vKEe0/7eD3ioDg6nEJ}},
 763   note =        {Oct. 2012},
 764 }
 765
 766 @misc{mpmc-queue-url,
 767   howpublished = {\url{http://cbloomrants.blogspot.com/2011/07/07-30-11-look-at-some-bounded-queues.html}},
 768   note =        {Oct. 2012},
 769 }
 770
 771 @misc{dekker-url,
 772   howpublished = {\url{http://www.justsoftwaresolutions.co.uk/threading/}},
 773   note =        {Dec. 2012},
 774 }