Exploiting predicate structure for efficient reachability detection

ABSTRACT

Partial order (p.o.) reduction techniques are a popular and effective approach for tackling state space explosion in the verification of concurrent systems. These techniques generate a reduced search space that could be exponentially smaller than the complete state space. Their major drawback is that the amount of reduction achieved is highly sensitive to the properties being verified. For the same program, different properties could result in very different amounts of reduction achieved.We present a new approach which combines the benefits of p.o. reduction with the added advantage that the size of the constructed state space is completely independent of the properties being verified. As in p.o. reduction, we use the notion of persistent sets to construct a representative interleaving for each maximal trace of the program. However, we retain concurrency information by assigning vector timestamps to the events in each interleaving. Our approach hinges upon the use of efficient algorithms that parse the encoded concurrency information in the representative interleaving to determine whether a safety violation exists in any interleaving of the corresponding trace. We show that, for some types of predicates, reachability detection can be performed in time that is polynomial in the length of the interleaving. Typically, these predicates exhibit certain characteristics that can be exploited by the detection algorithm.We implemented our algorithms in the popular model checker SPIN, and present experimental results that demonstrate the effectiveness of our techniques. For example, we verified a distributed dining philosophers protocol in 0.03 seconds, using 1.253 MB of memory. SPIN, using traditional p.o. reduction techniques, took 759.71 seconds and 439.116 MB of memory.

REFERENCES

• 1: K. M. Chandy , J. Misra, The drinking philosophers problem, ACM Transactions on Programming Languages and Systems (TOPLAS), v.6 n.4, p.632-646, Oct. 1984 [doi>10.1145/1780.1804]
• 2: Craig M. Chase , Vijay K. Garg, Efficient Detection of Restricted Classes of Global Predicates, Proceedings of the 9th International Workshop on Distributed Algorithms, p.303-317, September 13-15, 1995
• 3: E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite state concurrent system using temporal logic specifications: a practical approach, Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.117-126, January 24-26, 1983, Austin, Texas [doi>10.1145/567067.567080]
• 4: B. Davey and H. Priestly. Introduction to Lattices and Order. Cambridge University Press, Cambridge, 1990.
• 5: D. Dolev, M. Klawe, and M. Rodeh. An O(n log n)unidirectional distributed algorithm for extrema finding in a circle. Journal of Algorithms, 3:245--260, 1982.
• 6: Javier Esparza, Model checking using net unfoldings, Selected papers of the colloquium on Formal approaches of software engineering, p.151-195, December 1994, Orsay, France
• 7: Colin Fidge, Logical Time in Distributed Computing Systems, Computer, v.24 n.8, p.28-33, August 1991 [doi>10.1109/2.84874 ]
• 8: F. Mattern. Virtual time and global states of distributed systems. In Proc. of the International Workshop on Distribute Algorithms, pages 215--226, 1989.
• 9: V. K. Garg , B. Waldecker, Detection of Weak Unstable Predicates in Distributed Programs, IEEE Transactions on Parallel and Distributed Systems, v.5 n.3, p.299-307, March 1994 [doi>10.1109/71.277788 ]
• 10: A partial order approach to branching time logic model checking, Proceedings of the 3rd Israel Symposium on the Theory of Computing Systems (ISTCS'95), p.130, January 04-06, 1995
• 11: Patrice Godefroid , J. van Leeuwen , J. Hartmanis , G. Goos , Pierre Wolper, Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem, Springer-Verlag New York, Inc., Secaucus, NJ, 1996
• 12: G. J. Holzmann. The SPINModel Checker: Primer and Reference Manual. Addison-Wesley, Sept. 2003.
• 13: Gerard J. Holzmann , Doron Peled, An improvement in formal verification, Proceedings of the 7th IFIP WG6.1 International Conference on Formal Description Techniques VII, p.197-211, January 1995
• 14: M. Z. Kwiatkowska, Event fairness and non-interleaving concurrency, Formal Aspects of Computing, v.1 n.3, p.213-228, Jul./Sep. 1989
• 15: Leslie Lamport, Time, clocks, and the ordering of events in a distributed system, Communications of the ACM, v.21 n.7, p.558-565, July 1978 [doi>10.1145/359545.359563]
• 16: 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
• 17: Kenneth L. McMillan, Using Unfoldings to Avoid the State Explosion Problem in the Verification of Asynchronous Circuits, Proceedings of the Fourth International Workshop on Computer Aided Verification, p.164-177, June 29-July 01, 1992
• 18: 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
• 19: Doron Peled, Combining Partial Order Reductions with On-the-fly Model-Checking, Proceedings of the 6th International Conference on Computer Aided Verification, p.377-390, June 21-23, 1994
• 20: Doron Peled , Thomas Wilke, Stutter-invariant temporal properties are expressible without the next-time operator, Information Processing Letters, v.63 n.5, p.243-246, Sept. 15, 1997 [doi>10.1016/S0020-0190(97)00133-6 ]
• 21: Glenn Ricart , Ashok K. Agrawala, An optimal algorithm for mutual exclusion in computer networks, Communications of the ACM, v.24 n.1, p.9-17, Jan. 1981 [doi>10.1145/358527.358537]
• 22: Fred B. Schneider , Leslie Lamport, Paradigms for Distributed Programs, Distributed Systems: Methods and Tools for Specification, An Advanced Course, April 3-12, 1984 and April 16-25, 1985 Munich, p.431-480, January 1985
• 23: Alexander I. Tomlinson , Vijay K. Garg, Monitoring functions on global states of distributed programs, Journal of Parallel and Distributed Computing, v.41 n.2, p.173-189, March 15, 1997 [doi>10.1006/jpdc.1996.1298 ]
• 24: A. Valmari. Stubborn Sets for Reduced State Space Generation, volume 483 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany, 1990.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

General Terms:
Verification

Keywords:
Mazurkiewicz traces, model checking, reachability