Abstract
A new approach is presented for detecting whether a computation of an asynchronous distributed system satisfies Poss Φ (read “possibly Φ”), meaning the system could have passed through a global state satisfying property Φ. Previous general-purpose algorithms for this problem explicitly enumerate the set of global states through which the system could have passed during the computation. The new approach is to represent this set symbolically, in particular, using ordered binary decision diagrams. We describe an implementation of this approach, suitable for off-line detection of properties, and compare its performance to the enumeration-based algorithm of Alagar & Venkatesan. In typical cases, the new algorithm is significantly faster. We have measured over 400-fold speedup in some cases.
Chapter PDF
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Sridhar Alagar and S. Venkatesan. Techniques to tackle state explosion in global predicate detection. Submitted to IEEE Transactions on Software Engineering, 1997. Preliminary version appeared in International Conference on Parallel and Distributed Systems (ICPDS'94), pp. 412–417, 1994.
The BDD Library (ver. 1.0). http://www.es.cmu.edu/ modelcheck/bdd.html.
R.E. Bryant. Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys, 24(3), 1992.
E. M. Clarke et al. Automatic verification of sequential circuit design. In C. A. R. Hoare and M. J. C. Gordon, editors, Mechanized Reasoning and Hardware Design. Prentice-Hall, 1992.
James M. Crawford and Larry D. Auton. Experimental results on the crossover point in random 3-SAT. Artificial Intelligence, 81(1):31–57, 1996.
Robert Cooper and Keith Marzullo. Consistent detection of global predicates. In Proc. ACM/ONR Workshop on Parallel and Distributed Debugging, 1991. Appeared as ACM SIGPLAN Notices 26(12):167–174, December 1991.
Eddy Fromentin and Michel Raynal. Local states in distributed computations: A few relations and formulas. Operating Systems Review, 28(2), April 1994.
Eddy Fromentin and Michel Raynal. Inevitable global states: a concept to detect unstable properties of distributed computations in an observer independent way. Journal of Computer and System Sciences, 55(3), Dec. 1997.
Vijay K. Garg and Brian Waldecker. Detection of weak unstable predicates in distributed programs. IEEE Transactions on Parallel and Distributed Systems, 5(3):299–307, 1994.
Leslie Lamport. Time, clocks, and the ordering of events in a distributed system. Communications of the ACM, 21(7):558–564, 1978.
Nancy A. Lynch. Distributed Algorithms. Morgan Kaufmann, 1996.
Friedemann Mattern. Virtual time and global states of distributed systems. In M. Corsnard, editor, Proc. International Workshop on Parallel and Distributed Algorithms, pages 120–131. North-Holland, 1989.
Keith Marzullo and Gil Neiger. Detection of global state predicates. In Proc. 5th Int'l. Workshop on Distributed Algorithms (WDAG '91), volume 579 of Lecture Notes in Computer Science, pages 254–272. Springer-Verlag, 1991.
SMV. http://www.cs.cmu.edu/ modelcheck/smv.html.
Scott D. Stoller. Detecting global predicates in distributed systems with clocks. In Marios Mavronikolas, editor, Proc. 11th International Workshop on Distributed Algorithms (WDAG '97), volume 1320 of Lecture Notes in Computer Science, pages 185–199. Springer-Verlag, 1997.
Alexander I. Tomlinson and Vijay K. Garg. Detecting relational global predicates in distributed systems. In Proc. ACM/ONR Workshop on Parallel and Distributed Debugging, 1993. ACM SIGPLAN Notices 28(12), December 1993.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Stoller, S.D., Liu, Y.A. (1998). Efficient symbolic detection of global properties in distributed systems. In: Hu, A.J., Vardi, M.Y. (eds) Computer Aided Verification. CAV 1998. Lecture Notes in Computer Science, vol 1427. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0028758
Download citation
DOI: https://doi.org/10.1007/BFb0028758
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64608-2
Online ISBN: 978-3-540-69339-0
eBook Packages: Springer Book Archive