Data flow analysis for checking properties of concurrent Java programs

In this paper we show how the FLAVERS data flow analysis technique, originally formulated for systems using a rendezvous concurrency model, can be applied to the various concurrency models used in Java programs. The general approach of FLAVERS is based on modeling a concurrent system as a flow graph and, using a data flow analysis algorithm over this graph, statically checking if a property holds on all (or no) executions of the program. The accuracy of this analysis can be iteratively improved, as needed, by supplying additional constraints, represented as finite state automata, to the data flow analysis algorithm. In this paper we present an approach for analyzing Java programs that uses the constraint mechanism to model the possible communications among threads in Java programs, instead of representing them directly in the flow graph model. We also discuss a number of error-prone thread communication patterns that can arise in Java and describe how FLAVERS can be used to check for the presence of these. A preliminary evaluation of this approach is carried out by analyzing some small concurrent Java programs for these error-prone communication patterns and other, program-specific, faults.