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

The object-oriented paradigm in software engineering provides support for t he construction of modular and reusable program components and is attractiv e for the design of large and complex distributed systems. Reachability ana lysis is an important and well-known tool for static analysis of critical p roperties 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 synchronizat ion structure in concurrent programs, such as formal verification. However, direct application of traditional reachability analysis to concurrent obje ct-oriented programs has many problems, such as incomplete analysis for reu sable classes (not safe) and increased computational complexity (not effici ent). We have proposed a novel technique called apportioning, for safe and efficient reachability analysis of concurrent object-oriented programs, tha t is based upon a simple but powerful idea of classification of program ana lysis points as local (having influence within a class) and global (having possible influence outside a class). Given a program and a classification o f 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 po ints. The error to be checked is decomposed into a number of subproperties, which are checked in the appropriate, reachability graphs. Different choic es for the classification of analysis points, provide the flexibility to ha ve many algorithms that are safe and efficient for different subclasses of programs. We have developed a number of apportioning-based algorithms, havi ng different degrees of safety and efficiency. In this paper, we present th e details of one of these algorithms, formally show its safety for an appro priate class of programs, and present experimental results to demonstrate i ts efficiency for various examples.