Conchord: Analysis of Concurrent Programs

The Conchord project is investigating scalable techniques and tools for testing, debugging, and verifying concurrent programs. The focus is on checking lightweight concurrency correctness properties like datarace freedom, deadlock freedom, and atomicity for large, real-world, multi-threaded programs.

Note: Some of the below publications report results that were obtained in the context of the CalFuzzer and Ivy projects.

• Pallavi Joshi, Mayur Naik, Koushik Sen, and David Gay. An Effective Dynamic Analysis for Detecting Generalized Deadlocks. FSE'10.
  
  
• Pallavi Joshi, Mayur Naik, Chang-Seo Park, and Koushik Sen. CalFuzzer: An Extensible Active Testing Framework for Concurrent Programs (Tool Paper). CAV'09.
  
  
• Zachary Anderson, David Gay, and Mayur Naik. Lightweight Annotations for Controlling Sharing in Concurrent Data Structures. PLDI'09.
  
  
• Pallavi Joshi, Chang-Seo Park, Koushik Sen, and Mayur Naik. A Randomized Dynamic Program Analysis Technique for Detecting Real Deadlocks. PLDI'09.
  
  
• Mayur Naik, Chang-Seo Park, Koushik Sen, and David Gay. Effective Static Deadlock Detection. ICSE'09.
  
  
• Mayur Naik and Alex Aiken. Conditional Must Not Aliasing for Static Race Detection. POPL'07.
  
  
• Mayur Naik, Alex Aiken, and John Whaley. Effective Static Race Detection for Java. PLDI'06.

Most of the concurrent Java benchmarks used in the above papers are available in the SVN repository hosted here.

Implementations of various static and dynamic concurrency analyses for detecting dataraces, deadlocks, and atomicity violations in Java programs, including those in the above PLDI'06, ICSE'09, and FSE'10 papers, are publicly available in the Chord distribution. See the below information for more details. You will need to download Chord; see the Chord project website for more details.

• Static Datarace Checker: The datarace checker from our PLDI'06 paper.

  Getting Started: Run the datarace checker on the example Java program in directory main/examples/datarace_test/ of the Chord 2.0 distribution by following the instructions in the README file in that directory.

  Upon successful completion, the checker should produce files dataraces_by_fld.html and dataraces_by_obj.html.

  Configuration: Read the section titled ``Static Datarace Analysis" in the chapter on Predefined Analyses in Chord's user guide for how to configure aspects of the datarace checker that affect its performance, precision, and soundness.

  Experimental Results: Details of the experimental evaluation from our PLDI'06 paper are available here.

• Static Deadlock Checker: The deadlock checker from our ICSE'09 paper.

  Getting Started: Run the deadlock checker on the example Java program in directory main/examples/deadlock_test/ of the Chord 2.0 distribution by following the instructions in the README file in that directory.

  Upon successful completion, the checker should produce file deadlocks.html.

  Configuration: Read the section titled ``Static Datarace Analysis" in the chapter on Predefined Analyses in Chord's user guide for how to configure aspects of the deadlock checker that affect its performance, precision, and soundness.

  Experimental Results: Details of the experimental evaluation from our ICSE'09 paper are available here.