Data flow analysis for verifying properties of concurrent programs

Abstract

In this paper we present an approach, based on data flow analysis, that can provide cost-effective analysis of concurrent programs with respect to explicitly stated correctness properties. Using this approach, a developer specifies a property of a concurrent program as a pattern of selected program events and asks the analysis to verify that all or no program executions satisfy the given property. We have developed a family of polynomial-time, conservative data flow anlysis algorithms that support reasoning about these questions. To overcome the traditional inaccuracies of static analysis, we have also developed a range of techniques for improving the accuracy of the analysis results. One strength of our approach is the flexibility allowed in choosing and combining these techniques so as to increase accuracy without making analysis time impractical.We have implemented a prototype toolset that automates the analysis for programs with explicit tasking and rendezvous style communication. We present preliminary experimental results using this toolset.