Using shape analysis to reduce finite-state models of concurrent Java programs

ABSTRACT

Finite-state verification (e.g., model checking) provides a powerful means to detect concurrency errors, which are often subtle and difficult to reproduce. Nevertheless, widespread use of this technology by developers is unlikely until tools provide automated support for extracting the required finite-state models directly from program source. Unfortunately, the dynamic features of modern languages such as Java complicate the construction of compact finite-state models for verification. In this article, we show how shape analysis, which has traditionally been used for computing alias information in optimizers, can be used to greatly reduce the size of finite-state models of concurrent Java programs by determining which heap-allocated variables are accessible only by a single thread, and which shared variables are protected by locks. We also provide several other state-space reductions based on the semantics of Java monitors. A prototype of the reductions demonstrates their effectiveness.

REFERENCES

• 1: ASHCROFT, E. AND MANNA, Z. 1971. Formalization of properties of parallel programs. Mach. Intell. 6, 1, 17-41.
• 2: George S. Avrunin , Ugo A. Buy , James C. Corbett , Laura K. Dillon , Jack C. Wileden, Automated Analysis of Concurrent Systems with the Constrained Expression Toolset, IEEE Transactions on Software Engineering, v.17 n.11, p.1204-1222, November 1991 [doi>10.1109/32.106975]
• 3: Tevfik Bultan , Jeffrey Fischer , Richard Gerber, Compositional verification by model checking for counter-examples, ACM SIGSOFT Software Engineering Notes, v.21 n.3, p.224-238, May 1996
• 4: Tevfik Bultan , Richard Gerber , Christopher League, Verifying systems with integer constraints and Boolean predicates: a composite approach, ACM SIGSOFT Software Engineering Notes, v.23 n.2, p.113-123, March 1998
• 5: BURCH, J. R., CLARKE, E. M., MCMILLAN, K. L., DILL, D. L., AND HWANG, L.J. 1990. Symbolic model checking: 1020 states and beyond. In Proceedings of the 5th Annual IEEE Symposium on Logic in Computer Science (LICS '90, June), IEEE Press, Piscataway, NJ, 428-439.
• 6: David R. Chase , Mark Wegman , F. Kenneth Zadeck, Analysis of pointers and structures, ACM SIGPLAN Notices, v.25 n.6, p.296-310, Jun. 1990
• 7: S. C. Cheung , J. Kramer, Enhancing compositional reachability analysis with context constraints, Proceedings of the 1st ACM SIGSOFT symposium on Foundations of software engineering, p.115-125, December 08-10, 1993, Los Angeles, California, United States
• 8: Rance Cleaveland , Joachim Parrow , Bernhard Steffen, The concurrency workbench: a semantics-based tool for the verification of concurrent systems, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.1, p.36-72, Jan. 1993 [doi>10.1145/151646.151648]
• 9: James C. Corbett, Evaluating Deadlock Detection Methods for Concurrent Software, IEEE Transactions on Software Engineering, v.22 n.3, p.161-180, March 1996 [doi>10.1109/32.489078]
• 10: James C. Corbett, Timing Analysis of Ada Tasking Programs, IEEE Transactions on Software Engineering, v.22 n.7, p.461-483, July 1996 [doi>10.1109/32.538604]
• 11: James C. Corbett, Constructing compact models of concurrent Java programs, ACM SIGSOFT Software Engineering Notes, v.23 n.2, p.1-10, March 1998
• 12: Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
• 13: David L. Dill , Andreas J. Drexler , Alan J. Hu , C. Han Yang, Protocol Verification as a Hardware Design Aid, Proceedings of the 1991 IEEE International Conference on Computer Design on VLSI in Computer & Processors, p.522-525, October 11-14, 1992
• 14: S. Duri , U. Buy , R. Devarapalli , S. M. Shatz, Using state space reduction methods for deadlock analysis in Ada tasking, ACM SIGSOFT Software Engineering Notes, v.18 n.3, p.51-60, July 1993
• 15: Matthew B. Dwyer , Lori A. Clarke, Data flow analysis for verifying properties of concurrent programs, Proceedings of the 2nd ACM SIGSOFT symposium on Foundations of software engineering, p.62-75, December 06-09, 1994, New Orleans, Louisiana, United States
• 16: Matthew B. Dwyer , George S. Avrunin , James C. Corbett, Patterns in property specifications for finite-state verification, Proceedings of the 21st international conference on Software engineering, p.411-420, May 16-22, 1999, Los Angeles, California, United States [doi>10.1145/302405.302672]
• 17: Patrice Godefroid , Pierre Wolper, Using Partial Orders for the Efficient Verification of Deadlock Freedom and Safety Properties, Proceedings of the 3rd International Workshop on Computer Aided Verification, p.332-342, July 01-04, 1991
• 18: James Gosling , Bill Joy , Guy L. Steele, The Java Language Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1996
• 19: HATCLIFF, J., CORBETT, J. C., DWYER, M. B., SOKOLOWSKI, S., AND ZHENG, H. 1999. A formal study of slicing for multi-threaded programs with JVM concurrency primitives. Tech. Rep. KSU CIS TR 99-6. Kansas State Univ., Manhattan, KS.
• 20: John Hatcliff , Matthew B. Dwyer , Shawn Laubach, Staging Static Analyses Using Abstraction-Based Program Specialization, Proceedings of the 10th International Symposium on Principles of Declarative Programming, p.134-151, September 16-18, 1998
• 21: HAVELUND, K. AND PRESSBURGER, T. 2000. Model checking Java programs using Java PathFinder. Int. J. Softw. Tools Tech. Transfer. To be published.
• 22: Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, v.23 n.5, p.279-295, May 1997 [doi>10.1109/32.588521]
• 23: Gerard J. Holzmann, Designing executable abstractions, Proceedings of the second workshop on Formal methods in software practice, p.103-108, March 04-05, 1998, Clearwater Beach, Florida, United States [doi>10.1145/298595.298864]
• 24: IOSIF, R., DEMARTINI, C., AND SISTO, R. 1998. Modeling and validation of Java multithreaded applications using SPIN. In Proceedings of the 4th SPIN Workshop (Paris, France, Nov.),
• 25: Daniel Jackson , Craig A. Damon, Elements of style: analyzing a software design feature with a counterexample detector, ACM SIGSOFT Software Engineering Notes, v.21 n.3, p.239-249, May 1996
• 26: William Landi , Barbara G. Ryder, Pointer-induced aliasing: a problem taxonomy, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.93-103, January 21-23, 1991, Orlando, Florida, United States [doi>10.1145/99583.99599]
• 27: Douglas Lea , Doug Lea, Concurrent Programming in Java: Design Principles and Patterns, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1996
• 28: Orna Lichtenstein , Amir Pnueli, Checking that finite state concurrent programs satisfy their linear specification, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.97-107, January 14-16, 1985, New Orleans, Louisiana, United States [doi>10.1145/318593.318622]
• 29: Tim Lindholm , Frank Yellin, Java Virtual Machine Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1999
• 30: MASTICOLA, S. P. AND RYDER, B. G. 1990. Static infinite wait anomaly detection in polynomial time. In Proceedings of the International Conference on Parallel Processing, 78-87.
• 31: Antoni W. Mazurkiewicz, Basic notions of trace theory, Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, School/Workshop, p.285-363, May 30-June 03, 1988
• 32: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 33: Tadao Murata , Sol M. Shatz , Boris Shenker, Detection of Ada Static Deadlocks Using Petri Net Invariants, IEEE Transactions on Software Engineering, v.15 n.3, p.314-326, March 1989 [doi>10.1109/32.21759]
• 34: Gleb Naumovich , George S. Avrunin , Lori A. Clarke, Data flow analysis for checking properties of concurrent Java programs, Proceedings of the 21st international conference on Software engineering, p.399-410, May 16-22, 1999, Los Angeles, California, United States [doi>10.1145/302405.302663]
• 35: Doron Peled, All from One, One for All: on Model Checking Using Representatives, Proceedings of the 5th International Conference on Computer Aided Verification, p.409-423, June 28-July 01, 1993
• 36: Mooly Sagiv , Thomas Reps , Reinhard Wilhelm, Solving shape-analysis problems in languages with destructive updating, ACM Transactions on Programming Languages and Systems (TOPLAS), v.20 n.1, p.1-50, Jan. 1998 [doi>10.1145/271510.271517]
• 37: Antti Valmari, A stubborn attack on state explosion, Formal Methods in System Design, v.1 n.4, p.297-322, Dec. 1992 [doi>10.1007/BF00709154]
• 38: VERMEULEN, A. 1997. Java deadlock. Dr. Dobb's J. 22.
• 39: Wei Jen Yeh , Michal Young, Compositional reachability analysis using process algebra, Proceedings of the symposium on Testing, analysis, and verification, p.49-59, October 08-10, 1991, Victoria, British Columbia, Canada [doi>10.1145/120807.120812]
• 40: M. Young , R. Taylor , K. Forester , D. Brodbeck, Integrated concurrency analysis in a software development enviornment, ACM SIGSOFT Software Engineering Notes, v.14 n.8, p.200-209, Dec. 1989

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING

General Terms:
Verification

Keywords:
Java, concurrent systems, finite-state verification, model extraction, modeling, shape analysis, state-space reductions