Data Flow Analysis for Checking Properties of Concurrent Java Programs

13 years 9 months ago

Download laser.cs.umass.edu

In this paper we show how the FLAVERS data ﬂow analysis technique, originally formulated for programs with the rendezvous model of concurrency, can be applied to concurrent Java programs. The general approach of FLAVERS is based on modeling a concurrent program as a ﬂow graph and using a data ﬂow analysis algorithm over this graph to check statically if a property holds on all executions of the program. The accuracy of this analysis can be improved by supplying additional information, represented as ﬁnite state automata, to the data ﬂow analysis algorithm. In this paper we present a straightforward approach for modeling Java programs that uses the accuracy improving mechanism to represent the possible communications among threads in Java programs, instead of representing them directly in the ﬂow 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.

Gleb Naumovich, George S. Avrunin, Lori A. Clarke

Real-time Traffic