Apportioning : a technique for efficient reachability analysis of concurrent object-oriented programs

The object-oriented paradigm in software engineering provides support for the construction of modular and reusable program components and is attractive for the design of large and complex distributed systems. Reachability analysis is an important and well-known tool for static analysis of critical properties in concurrent programs, such as deadlock freedom. It involves the systematic enumeration of all possible global states of program execution and provides the same level of assurance for properties of the synchronization structure in concurrent programs, such as formal verification. However, direct application of traditional reachability analysis to concurrent object-oriented programs has many problems, such as incomplete analysis for reusable classes (not safe) and increased computational complexity (not efficient). We have proposed a novel technique called apportioning, for safe and efficient reachability analysis of concurrent object-oriented programs, that is based upon a simple but powerful idea of classification of program analysis points as local (having influence within a class) and global (having possible influence outside a class). Given a program and a classification of its analysis points, reachability graphs are generated for 1) an abstract version of each class in the program having only local analysis points and 2) an abstract version of the whole program having only global analysis points. The error to be checked is decomposed into a number of subproperties, which are checked in the appropriate, reachability graphs. Different choices for the classification of analysis points, provide the flexibility to have many algorithms that are safe and efficient for different subclasses of programs. We have developed a number of apportioning-based algorithms, having different degrees of safety and efficiency. In this paper, we present the details of one of these algorithms, formally show its safety for an appropriate class of programs, and present experimental results to demonstrate its efficiency for various examples