An empirical comparison of static concurrency analysis techniques

Developers of concurrent software need cost-effective analysis techniques to acquire confidence in the reliability of that software. Analysis of concurrent programs is difficult because, in many cases, the patterns of communication among the various parts of the program are complicated and the number of possible communications is large. One class of techniques that can be used for analysis of concurrent programs is static analysis, which uses compile-time information to prove properties about a program. Given the variety of concurrency analysis tools available, analysts need assistance when selecting tools to use to check a specific program and property. Despite exponential worst-case bounds for most of the techniques, average case analysis times may help differentiate between the techniques in practice. The techniques provide a range of analysis accuracies, but these accuracies have not been formally or empirically quantified. Empirical tool comparisons can therefore provide useful insight into which tool would be most suitable for a given program and property. The main contribution of the work presented here is the development of a sound methodology for comparing concurrency analysis tools, with a thorough description of the experimental design and constraints, discussion of the issues and tradeoffs involved in developing such a methodology, and valid application of statistical analysis. We apply this methodology to conduct an experiment to compare a number of concurrency analysis tools. Comparisons are accomplished for analysis time, analysis failures, and analysis accuracy of the tools. Secondary contributions of the work presented here include development of predictive models and preliminary examination of several real programs. We develop, with varying degrees of success, predictive models that may help an analyst estimate the analysis time, analysis failure, and analysis accuracy of each tool given a program and a property to be checked. We also provide a preliminary examination of several real programs, including a discussion of the program constructs used in the programs and observations about program characteristics that are likely to affect the applicability of static concurrency analysis tools to these programs