Cited By
View all- Arora VBhatia RSingh M(2016)A systematic review of approaches for testing concurrent programsConcurrency and Computation: Practice & Experience10.1002/cpe.371128:5(1572-1611)Online publication date: 10-Apr-2016
Apportioning: A Technique for Efficient Reachability Analysis of Concurrent Object-Oriented Programs
Authors: 
Sridhar Iyer, S. RameshAuthors Info & Claims
Pages 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.
References
[1]
CR. Andrews, "Paradigms for Process Interactions in Distributed Systems," ACM Computing Surveys, vol. 23, no. 1, pp. 49-90, Mar. 1991.
[2]
KR. Apt, "A Static Analysis of CSP Programs," Proc. Workshop Pro gam Logic, 1984.
[3]
G.S. Avrunin, U,A. Buy, J.C. Corbett, LX. 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]
WE. 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. Bahsotm, 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," I. Automated Software Eng., vol. 2, no. 1, pp. 5-32, Mar. 1995.
[8]
EM. Clarke, 0. Grumberg, and D.E. Long, "Model Checking and Abstraction," Proc. ACM Syinp. Principles of Programming Languages, pp. 343-354, 1992.
[9]
J.-D. Choi, B.P. Miller, and R.H.B. Netzer, "Techniques for Debugging Parallel Programs with Flowback Analysis," ACM Trans. Programming Languages and Systems, vol. 13, no. 4, pp. 491530, Oct. 1991.
[10]
D. Callahan and J. Subhlok; "Static Analysis of Low Level Synchronization," Five. ACM SICPLAN/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]
0. Grumberg and D.E. Long, 'Model Checking and Modular Verification," CONCURR '91, J.C.M. Baeten and J.F. Groote eds., pp. 250-265 1991.
[13]
S. Graf and B. Steffen, "Compositional Minimization of Finite State Systems," Proc. Intl Conf. Computer-Aided Verification, pp. 186-196, 1990.
[14]
G.J. Holzmann, Design and Validation of Computer Protocols. New Jersey: prentice-Hall, 1991.
[15]
W. Hseush and G.E. Kaiser, 'Modeling Concurrency in Parallel Debugging," Proc. ACM SIGPLANISICOPS Workshop Principles and Practices of Parallel Programming, pp. 11-20, Mar. 1990.
[16]
S. Iyer, "Efficient Reachability Analysis for Concurrent ObjectOriented Programs," PhD Thesis, Indian Inst. of Technology, Bombay, 1998.
[17]
S. lyer and S. Ramesh, "A Tool-Suite for Reachability Analysis of Concurrent ObjectOriented 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. Jacquemot, and E. Pillevesse, "COOL: System Support for Distributed Programming," Comm. ACM, vol. 36, no. 9, pp. 3746, Sept. 1993.
[20]
CE. McDowell. 'A Practical Algorithm for Static Analysis of Parallel Programs," J. Parallel and Distributed Computing, 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]
CE. 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. Springer-Verlag, 1995.
[24]
S.J. Mullender, C. van Rossum, AS. Tanenbaum, R. van Renesse, and H. van Staveren, 'Amoeba: A Distributed Operating System for the 1990s," Computer, vol. 23, no. 5, pp. 44-53, May 1990.
[25]
K.K. Sabnani, AM. Lapone, and MU. Uyar, "An Algorithmic Procedure for Checking Safety Properties of Protocols\Newblock," IEEE Trans. Comm., vol. 37, no. 9, pp. 940-948, Sept. 1989.
[26]
A. Taivalsaari, 'On the Notion of Inheritance," ACM Computing Surveys, vol. 28, no. 3, pp. 438-479, 1996.
[27]
RN. Taylor, "A General Purpose Algorithm for Analysing Concurrent Programs," Comm. ACM, vol. 26, no. 5, pp. 362-376, May 1983.
[28]
A. Valmari, 'A Stubborn Attack on State Explosion," Proc. Int'l Conf. Computer-Aided Verification, pp. 156-165, 1990.
[29]
P. Wegner, 'Concepts and Paradigms of Object-Oriented Programming,' OOPS Messenger, vol. I, no. 1, pp. 8-87, Aug. 1990.
[30]
M. Young and RN. Taylor. "Combining Static Concurrency Analysis with Symbolic Execution," IEEE Trans. Software Eng., vol. 14, no. 10, pp. 1499-1511, Oct. 1988.
[31]
M. Young, RN. Taylor, DL, Levine, K.A. Nies, and D. Broadbeck, 'A Concurrency Analysis Tool Suite for Ada Programs," ACM Trans. Software Eng. and Methodology, vol. 4, no. 1, pp. 65106, Jan. 1995.
[32]
W.J. Yeh and M. Young, Compositional Reachability Analysis Using Process Algebra," Proc. Symp. Software 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, 5. Cheng, and K. Ushijima, "Static Slicing of Concurrent Object-Oriented Programs," Proc. 20th IEEE Ann. Int'l Computer Software and Applications Conf., Aug. 1996.
Index Terms
- Apportioning: A Technique for Efficient Reachability Analysis of Concurrent Object-Oriented Programs
Recommendations
Verifying General Safety Properties of Ada Tasking Programs
The isolation approach to symbolic execution of Ada tasking programs provides a basis for automating partial correctness proofs. The strength of this approach lies in its isolation nature; tasks are symbolically executed and verified independently, and ...
Compositionality entails sequentializability
TACAS'11/ETAPS'11: Proceedings of the 17th international conference on Tools and algorithms for the construction and analysis of systems: part of the joint European conferences on theory and practice of softwareWe show that any concurrent program that is amenable to compositional reasoning can be effectively translated to a sequential program. More precisely, we give a reduction from the verification problem for concurrent programs against safety ...
Succinct Representation of Concurrent Trace Sets
POPL '15: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming LanguagesWe present a method and a tool for generating succinct representations of sets of concurrent traces. We focus on trace sets that contain all correct or all incorrect permutations of events from a given trace. We represent trace sets as HB-Formulas that ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Copyright © Copyright © 2001 IEEE. All Rights Reserved.
Publisher
IEEE Press
Publication History
Published: 01 November 2001
Author Tags
Qualifiers
- Research-article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 13 Jan 2025
Other Metrics
Citations
Cited By
View all- Arora VBhatia RSingh M(2016)A systematic review of approaches for testing concurrent programsConcurrency and Computation: Practice & Experience10.1002/cpe.371128:5(1572-1611)Online publication date: 10-Apr-2016