CHESS: Find and Reproduce Heisenbugs in Concurrent Programs

Effective Data-Race Detection for the Kernel

John Erickson, Madan Musuvathi, Sebastian Burckhardt, Kirk Olynyk

Operating System Design and Implementation (OSDI'10) | October 2010

Operating System Design and Implementation (OSDI'10)

Publication Project

Line-Up: A Complete and Automatic Linearizability Checker

Sebastian Burckhardt, Chris Dern, Madan Musuvathi, Roy Tan

Programming Language Design and Implementation (PLDI) | June 2010

Programming Language Design and Implementation (PLDI)

Publication

GAMBIT: Effective Unit Testing for Concurrency Libraries

Katherine E. Coons, Madan Musuvathi, Sebastian Burckhardt

Proceedings of the 15th ACM SIGPLAN Annual Symposium on Principles and Practice of Parallel Programming | January 2010

Proceedings of the 15th ACM SIGPLAN Annual Symposium on Principles and Practice of Parallel Programming

Publication

LiteRace: Effective Sampling for Lightweight Data-Race Detection

Daniel Marino, Madanlal Musuvathi, Satish Narayanasamy, Madan Musuvathi

Conference on Programming Language Design and Implementation (PLDI '09) | June 2009

Publication

Finding and Reproducing Heisenbugs in Concurrent Programs

Madan Musuvathi, Shaz Qadeer, Thomas Ball, Gerard Basler, Piramanayakam Arumuga Nainar, Iulian Neamtiu

OSDI 08: Eigth Symposium on Operating Systems Design & Implementation | December 2008

Publication

Effective Program Verification for Relaxed Memory Models

Sebastian Burckhardt, Madan Musuvathi

Computer-Aided Verification (CAV) | July 2008

The files above are full-text pdf, and the original powerpoint presentation from CAV. See also the companion tech report with the same title, it has additional material (including equivalence proofs for operational/axiomatic memory models of SC and TSO) in the appendix.

Publication Publication

Memory Model Safety of Programs

Sebastian Burckhardt, Madan Musuvathi

July 2008

Workshop on Exploiting Concurrency Efficiently and Correctly (EC^2)

Publication Publication

Effective Program Verification for Relaxed Memory Models

Sebastian Burckhardt, Madan Musuvathi

MSR-TR-2008-12 | January 2008

A shorter version of this TR appeared in CAV (Computer-Aided Verification) 2008.

Publication

CHESS: A systematic testing tool for concurrent software

Madan Musuvathi, Shaz Qadeer, Thomas Ball

MSR-TR-2007-149 | November 2007

Publication

Memory Model Sensitive Analysis of Concurrent Data Types

Sebastian Burckhardt

August 2007

August 2007

Doctoral Dissertation

Publication Publication

Iterative context bounding for systematic testing of multithreaded programs

Madanlal Musuvathi, Shaz Qadeer, Madan Musuvathi

PLDI 07: Programming Language Design and Implementation | June 2007

PLDI 07: Programming Language Design and Implementation

Publication

Iterative Context Bounding for Systematic Testing of Multithreaded Programs

Madan Musuvathi, Shaz Qadeer

MSR-TR-2007-14 | January 2007

Publication

CMC: A pragmatic approach to model checking real code

Madanlal Musuvathi, David Park, Andy Chou, Dawson R. Engler, David L. Dill, Madan Musuvathi

OSDI 02: Fifth Symposium on Operating Systems Design and Implementation | December 2002

OSDI 02: Fifth Symposium on Operating Systems Design and Implementation

Publication

Effective Data-Race Detection for the Kernel

John Erickson, Madan Musuvathi, Sebastian Burckhardt, Kirk Olynyk

Operating System Design and Implementation (OSDI'10) | October 2010

Operating System Design and Implementation (OSDI'10)

Publication Project

Line-Up: A Complete and Automatic Linearizability Checker

Sebastian Burckhardt, Chris Dern, Madan Musuvathi, Roy Tan

Programming Language Design and Implementation (PLDI) | June 2010

Programming Language Design and Implementation (PLDI)

Publication

GAMBIT: Effective Unit Testing for Concurrency Libraries

Katherine E. Coons, Madan Musuvathi, Sebastian Burckhardt

Proceedings of the 15th ACM SIGPLAN Annual Symposium on Principles and Practice of Parallel Programming | January 2010

Proceedings of the 15th ACM SIGPLAN Annual Symposium on Principles and Practice of Parallel Programming

Publication

LiteRace: Effective Sampling for Lightweight Data-Race Detection

Daniel Marino, Madanlal Musuvathi, Satish Narayanasamy, Madan Musuvathi

Conference on Programming Language Design and Implementation (PLDI '09) | June 2009

Publication

Finding and Reproducing Heisenbugs in Concurrent Programs

Madan Musuvathi, Shaz Qadeer, Thomas Ball, Gerard Basler, Piramanayakam Arumuga Nainar, Iulian Neamtiu

OSDI 08: Eigth Symposium on Operating Systems Design & Implementation | December 2008

Publication

Effective Program Verification for Relaxed Memory Models

Sebastian Burckhardt, Madan Musuvathi

Computer-Aided Verification (CAV) | July 2008

The files above are full-text pdf, and the original powerpoint presentation from CAV. See also the companion tech report with the same title, it has additional material (including equivalence proofs for operational/axiomatic memory models of SC and TSO) in the appendix.

Publication Publication

Memory Model Safety of Programs

Sebastian Burckhardt, Madan Musuvathi

July 2008

Workshop on Exploiting Concurrency Efficiently and Correctly (EC^2)

Publication Publication

Effective Program Verification for Relaxed Memory Models

Sebastian Burckhardt, Madan Musuvathi

MSR-TR-2008-12 | January 2008

A shorter version of this TR appeared in CAV (Computer-Aided Verification) 2008.

Publication

Memory Model Sensitive Analysis of Concurrent Data Types

Sebastian Burckhardt

August 2007

August 2007

Doctoral Dissertation

Publication Publication

Iterative context bounding for systematic testing of multithreaded programs

Madanlal Musuvathi, Shaz Qadeer, Madan Musuvathi

PLDI 07: Programming Language Design and Implementation | June 2007

PLDI 07: Programming Language Design and Implementation

Publication

Iterative Context Bounding for Systematic Testing of Multithreaded Programs

Madan Musuvathi, Shaz Qadeer

MSR-TR-2007-14 | January 2007

Publication

CMC: A pragmatic approach to model checking real code

Madanlal Musuvathi, David Park, Andy Chou, Dawson R. Engler, David L. Dill, Madan Musuvathi

OSDI 02: Fifth Symposium on Operating Systems Design and Implementation | December 2002

OSDI 02: Fifth Symposium on Operating Systems Design and Implementation

Publication

Finding and Reproducing Heisenbugs in Concurrent Programs

Madan Musuvathi, Shaz Qadeer, Thomas Ball, Gerard Basler, Piramanayakam Arumuga Nainar, Iulian Neamtiu

OSDI 08: Eigth Symposium on Operating Systems Design & Implementation | December 2008

Publication

CHESS: A systematic testing tool for concurrent software

Madan Musuvathi, Shaz Qadeer, Thomas Ball

MSR-TR-2007-149 | November 2007

Publication

CMC: A pragmatic approach to model checking real code

Madanlal Musuvathi, David Park, Andy Chou, Dawson R. Engler, David L. Dill, Madan Musuvathi

OSDI 02: Fifth Symposium on Operating Systems Design and Implementation | December 2002

OSDI 02: Fifth Symposium on Operating Systems Design and Implementation

Publication

Iterative context bounding for systematic testing of multithreaded programs

Madanlal Musuvathi, Shaz Qadeer, Madan Musuvathi

PLDI 07: Programming Language Design and Implementation | June 2007

PLDI 07: Programming Language Design and Implementation

Publication

Iterative Context Bounding for Systematic Testing of Multithreaded Programs

Madan Musuvathi, Shaz Qadeer

MSR-TR-2007-14 | January 2007

Publication

CMC: A pragmatic approach to model checking real code

Madanlal Musuvathi, David Park, Andy Chou, Dawson R. Engler, David L. Dill, Madan Musuvathi

OSDI 02: Fifth Symposium on Operating Systems Design and Implementation | December 2002

OSDI 02: Fifth Symposium on Operating Systems Design and Implementation

Publication

Effective Data-Race Detection for the Kernel

John Erickson, Madan Musuvathi, Sebastian Burckhardt, Kirk Olynyk

Operating System Design and Implementation (OSDI'10) | October 2010

Operating System Design and Implementation (OSDI'10)

Publication Project

Line-Up: A Complete and Automatic Linearizability Checker

Sebastian Burckhardt, Chris Dern, Madan Musuvathi, Roy Tan

Programming Language Design and Implementation (PLDI) | June 2010

Programming Language Design and Implementation (PLDI)

Publication

GAMBIT: Effective Unit Testing for Concurrency Libraries

Katherine E. Coons, Madan Musuvathi, Sebastian Burckhardt

Proceedings of the 15th ACM SIGPLAN Annual Symposium on Principles and Practice of Parallel Programming | January 2010

Proceedings of the 15th ACM SIGPLAN Annual Symposium on Principles and Practice of Parallel Programming

Publication

LiteRace: Effective Sampling for Lightweight Data-Race Detection

Daniel Marino, Madanlal Musuvathi, Satish Narayanasamy, Madan Musuvathi

Conference on Programming Language Design and Implementation (PLDI '09) | June 2009

Publication

Finding and Reproducing Heisenbugs in Concurrent Programs

Madan Musuvathi, Shaz Qadeer, Thomas Ball, Gerard Basler, Piramanayakam Arumuga Nainar, Iulian Neamtiu

OSDI 08: Eigth Symposium on Operating Systems Design & Implementation | December 2008

Publication

Effective Program Verification for Relaxed Memory Models

Sebastian Burckhardt, Madan Musuvathi

Computer-Aided Verification (CAV) | July 2008

The files above are full-text pdf, and the original powerpoint presentation from CAV. See also the companion tech report with the same title, it has additional material (including equivalence proofs for operational/axiomatic memory models of SC and TSO) in the appendix.

Publication Publication

Iterative context bounding for systematic testing of multithreaded programs

Madanlal Musuvathi, Shaz Qadeer, Madan Musuvathi

PLDI 07: Programming Language Design and Implementation | June 2007

PLDI 07: Programming Language Design and Implementation

Publication

CMC: A pragmatic approach to model checking real code

Madanlal Musuvathi, David Park, Andy Chou, Dawson R. Engler, David L. Dill, Madan Musuvathi

OSDI 02: Fifth Symposium on Operating Systems Design and Implementation | December 2002

OSDI 02: Fifth Symposium on Operating Systems Design and Implementation

Publication

Memory Model Safety of Programs

Sebastian Burckhardt, Madan Musuvathi

July 2008

Workshop on Exploiting Concurrency Efficiently and Correctly (EC^2)

Publication Publication

Effective Program Verification for Relaxed Memory Models

Sebastian Burckhardt, Madan Musuvathi

MSR-TR-2008-12 | January 2008

A shorter version of this TR appeared in CAV (Computer-Aided Verification) 2008.

Publication

CHESS: A systematic testing tool for concurrent software

Madan Musuvathi, Shaz Qadeer, Thomas Ball

MSR-TR-2007-149 | November 2007

Publication

Iterative Context Bounding for Systematic Testing of Multithreaded Programs

Madan Musuvathi, Shaz Qadeer

MSR-TR-2007-14 | January 2007

Publication

Memory Model Sensitive Analysis of Concurrent Data Types

Sebastian Burckhardt

August 2007

August 2007

Doctoral Dissertation

Publication Publication