This Article 
 Bibliographic References 
 Add to: 
Apportioning: A Technique for Efficient Reachability Analysis of Concurrent Object-Oriented Programs
November 2001 (vol. 27 no. 11)
pp. 1037-1056

Abstract—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.

[1] G. Andrews, “Paradigms for Process Interaction in Distributed Programs,” ACM Computing Surveys, Vol. 23, No. 1, Mar. 1991, pp. 49‐90.
[2] K.R. Apt, “A Static Analysis of CSP Programs,” Proc. Workshop Progam Logic, 1984.
[3] G.S. Avrunin, U.A. Buy, J.C. Corbett, L.K. Dillon, and J.C. Wileden, "Automated Analysis of Concurrent Systems with the Constrained Expression Toolset," IEEE Trans. Software Eng. vol. 17, no. 11, pp. 1204-1222, Nov. 1991.
[4] E. Adams and S.S. Muchnick, “Dbxtool: A Window-Based Symbolic Debugger for Sun Workstations,” Software—Practice and Experience, vol. 16, no. 7, pp. 653–669, July 1986.
[5] W.F. Appelbe and C.E. McDowell, “Integrating Tools for Debugging and Developing Multitasking Programs,” Proc. ACM SIGPLAN/SIGOPS Workshop Parallel and Distributed Debugging, vol. 24, no. 1, pp. 78–88, Jan. 1989.
[6] J.P. Bahsoun, S. Merz, and C. Servieres, “Modular Description and Verification of Concurrent Objects,” Proc. Workshop Object-Based Parallel and Distributed Computation, pp. 168–186, June 1995.
[7] S.C. Cheung and J. Kramer, “Contextual Local Analysis for Design of Distributed Systems,” J. Automated Software Eng., vol. 2, no. 1, pp. 5–32, Mar. 1995.
[8] E.M. Clarke, O. Grumberg, and D.E. Long, "Model Checking and Abstraction," Proc. ACM Symp. Principles of Programming Languages, Jan. 1992.
[9] J. Choi, B. Miller, and R. Netzer, "Techniques for Debugging Parallel Programs with Flow Back Analysis," ACM Trans Programming Languages and Systems, vol. 13, no. 4, pp. 491-530, Oct. 1991.
[10] D. Callahan and J. Subhlok, “Static Analysis of Low Level Synchronization,” Proc. ACM SIGPLAN/SIGOPS Workshop Parallel and Distributed Debugging, vol. 24, no. 1, pp. 100–112, Jan. 1989.
[11] J. Gait, “A Debugger for Concurrent Programs,” Software—Practice and Experience, vol. 15, no. 6, pp. 539–554, June 1985.
[12] O. Grumberg and D.E. Long, “Model Checking and Modular Verification,” Proc. CONCUR'91: Second Int'l Conf. Concurrency Theory, 1991.
[13] S. Graf and B. Steffen, “Compositional Minimization of Finite State Systems,” Proc. Second Conf. Computer-Aided Verification, pp. 186-196, 1990.
[14] G.J. Holzmann, Design and Validation of Computer Protocols, Prentice Hall, 1991.
[15] W. Hseush and G. Kaiser, “Modeling Concurrency in Parallel Debugging,” ACM SIGPLAN Notices, vol. 25, no. 3, pp. 11–20, 1990.
[16] S. Iyer, “Efficient Reachability Analysis for Concurrent Object-Oriented Programs,” PhD Thesis, Indian Inst. of Technology, Bombay, 1998.
[17] S. Iyer and S. Ramesh, “A Tool-Suite for Reachability Analysis of Concurrent Object-Oriented Programs,” Proc. Joint Asia-Pacific Software Eng. Conf. and Int'l Computer Science Conf., 1997.
[18] S. Iyer, R. Raghuraman, and A. Majumdar, “Apportioning-Based Analysis of Concurrent Java Programs,” Proc. Int'l Conf. Information Technology, Dec. 1999.
[19] R. Lea, C. Jacquemont, and E. Pillevesse, "COOL: System Support for Distributed Object-Oriented Programming," Comm. ACM, vol. 36, no. 9, pp. 37-46, Nov. 1993.
[20] C.E. McDowell, "A Practical Algorithm for Static Analysis of Parallel Programs," J. Parallel and Distributed Processing, vol. 6, no. 3, pp. 515-536, June 1989.
[21] K.L. McMillan, “Symbolic Model Checking: An Approach to the State-Explosion Problem,” PhD Thesis, Carnegie-Mellon Univ., Pittsburgh, Penn., 1992.
[22] C.E. McDowell and D.P. Helmbold, “Debugging Concurrent Programs,” ACM Computing Surveys, vol. 21, no. 4, pp. 593-622, Dec. 1989.
[23] Z. Manna and A. Pnueli, Temporal Verification of Reactive Systems: Safety.New York: Springer-Verlag, 1995.
[24] A. Tannenbaum, "Amoeba: A Distributed Operating System for the 1990s," Computer, pp. 44-53, 1990.
[25] K.K. Sabnani, A.M. Lapone, and M.U. Uyar, "An Algorithm Procedure for Checking Safety Properties of Protocols," IEEE Trans. Comm., pp. 940-948, vol. 37, no. 9, 1989.
[26] A. Taivalsaari, "On the Notion of Inheritance," ACM Computing Surveys, Vol. 28, No. 3, 1996, pp. 438-479.
[27] R.N. Taylor, "A General-Purpose Algorithm for Analyzing Concurrent Programs," Comm. ACM, vol. 26, no. 5, pp. 362-376, May 1983.
[28] A. Valmari, "A Stubborn Attack on State Explosion," Proc. Second Workshop Computer Aided Verification, vol. 531, Lecture Notes in Computer Science, pp. 156-165. Springer-Verlag, 1991.
[29] P. Wegner, "Concepts and Paradigms of Object-Oriented Programming," OOPS Messenger, vol. 1, no. 1, pp. 7-84, Aug. 1990.
[30] M. Young and R.N. Taylor, Combining Static Concurrency Analysis with Symbolic Execution IEEE Trans. Software Eng., vol. 14, no. 10, Oct. 1988.
[31] M. Young, R.N. Taylor, D.L. Levine, K.A. Nies, and D. Brodbeck, "A Concurrency Analysis Tool Suite: Rationale, Design, and Preliminary Experience," ACM Trans.Software Eng. and Methodology, vol. 4, no. 1, pp. 64-106, Jan. 1995.
[32] W.J. Yeh and M. Young, "Compositional Reachability Analysis Using Process Algebra," Proc. ACM SIGSOFT Symp. Testing, Analysis and Verification, pp. 49-59, Oct. 1991.
[33] J. Zhao, “Slicing of Concurrent Java Programs,” Proc. Seventh IEEE Conf. Program Comprehension, May 1999.
[34] J. Zhao, “Slicing of Concurrent Java Programs,” Proc. Seventh IEEE Conf. Program Comprehension, May 1999.

Index Terms:
Concurrent programs, object-oriented programming, static analysis, reachability analysis.
Sridhar Iyer, S. Ramesh, "Apportioning: A Technique for Efficient Reachability Analysis of Concurrent Object-Oriented Programs," IEEE Transactions on Software Engineering, vol. 27, no. 11, pp. 1037-1056, Nov. 2001, doi:10.1109/32.965343
Usage of this product signifies your acceptance of the Terms of Use.