Abstract
A new approach is presented for detecting whether a particular computation of an asynchronous distributed system satisfies \(\mathop{{\bf Poss}}\Phi\) (read “possibly Φ”), meaning the system could have passed through a global state satisfying predicate Φ, or \(\mathop{{\bf Def}}\Phi\) (read “definitely Φ”), meaning the system definitely passed through a global state satisfying Φ. Detection can be done easily by straightforward state-space search; this is essentially what Cooper and Marzullo proposed. We show that the persistent-set technique, a well-known partial-order method for optimizing state-space search, provides efficient detection. This approach achieves the same worst-case asymptotic time complexity as two special-purpose detection algorithms of Garg and Waldecker that detect \(\mathop{{\bf Poss}}\Phi\) and \(\mathop{{\bf Def}}\Phi\) for a restricted but important class of predicates. For \(\mathop{{\bf Poss}}\Phi\), our approach applies to arbitrary predicates and thus is more general than Garg and Waldecker’s algorithm. We apply our algorithm for \(\mathop{{\bf Poss}}\Phi\) to two examples, achieving a speedup of over 700 in one example and over 70 in the other, compared to unoptimized state-space search.
The authors gratefully acknowledge the support of NSF under Grants CCR-9876058 and CCR-9711253 and the support of ONR under Grants N00014-99-1-0358 and N00014-99-1-0132.
Chapter PDF
Similar content being viewed by others
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
Alur, R., McMillan, K., Peled, D.: Deciding global partial-order properties. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 41–52. Springer, Heidelberg (1998)
Alagar, S., Venkatesan, S.: Techniques to tackle state explosion in global predicate detection. In: Proc. International Conference on Parallel and Distributed Systems, December 1994, pp. 412–417 (1994)
Alur, R., Yannakakis, M.: Model checking of message sequence charts. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 114–129. Springer, Heidelberg (1999)
Chase, C.M., Garg, V.K.: Detection of global predicates: Techniques and their limitations. Distributed Computing 11(4), 169–189 (1998)
Cooper, R., Marzullo, K.: Consistent detection of global predicates. In: Proc. ACM/ONR Workshop on Parallel and Distributed Debugging (1991); ACM SIGPLAN Notices 26(12), 167–174 (December 1991)
Fidge, C.: Timestamps in message-passing systems that preserve the partial ordering. In: Proceedings of the 11th Australian Computer Science Conference, pp. 56–66 (1988)
Fromentin, E., Raynal, M.: Local states in distributed computations: A few relations and formulas. Operating Systems Review 28(2) (April 1994)
Godefroid, P. (ed.): Partial-Order Methods for the Verification of Concurrent Systems. LNCS, vol. 1032. Springer, Heidelberg (1996)
Garg, V.K., Waldecker, B.: Detection of weak unstable predicates in distributed programs. IEEE Transactions on Parallel and Distributed Systems 5(3), 299–307 (1994)
Garg, V.K., Waldecker, B.: Detection of strong unstable predicates in distributed programs. IEEE Transactions on Parallel and Distributed Systems 7(12), 1323–1333 (1996)
Jegou, R., Medina, R., Nourine, L.: Linear space algorithm for on-line detection of global predicates. In: Desel, J. (ed.) Proc. Int’l Workshop on Structures in Concurrency Theory (STRICT 1995), Springer, Heidelberg (1995)
Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Communications of the ACM 21(7), 558–564 (1978)
Mattern, F.: Virtual time and global states of distributed systems. In: Corsnard, M. (ed.) Proc. International Workshop on Parallel and Distributed Algorithms, pp. 120–131. North-Holland, Amsterdam (1989)
Walukiewicz, I.: Difficult configurations - on the complexity of ltrl. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 140–151. Springer, Heidelberg (1998)
Muscholl, A., Peled, D., Su, Z.: Deciding properties for message sequence charts. In: Nivat, M. (ed.) FOSSACS 1998. LNCS, vol. 1378, pp. 226–242. Springer, Heidelberg (1998)
Peled, D., Pratt, V.R., Holzmann, G.J.: Proc. Workshop on Partial Order Methods in Verification. DIMACS Series, vol. 29. American Mathematical Society (1997)
Silberschatz, A., Galvin, P.B.: Operating System Concepts, 5th edn. Addison-Wesley, Reading (1998)
Stoller, S.D., Unnikrishnan, L., Liu, Y.A.: Efficient detection of global properties in distributed systems using partial-order methods. Technical Report 523, Computer Science Dept., Indiana University (1999)
Sistla, A.P., Welch, J.: Efficient distributed recovery using message logging. In: Proc. Eighth ACM Symposium on Principles of Distributed Computing. ACM SIGOPS-SIGACT (1989)
Tomlinson, A.I., Garg, V.K.: 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)
Valmari, A.: Stubborn set methods for process algebras. In: Peled, et al. (eds.) [PPH97], pp. 213–231.
Walukiewicz, I.: Difficult configurations - on the complexity of ltrl. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 140–151. Springer, Heidelberg (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Stoller, S.D., Unnikrishnan, L., Liu, Y.A. (2000). Efficient Detection of Global Properties in Distributed Systems Using Partial-Order Methods. In: Emerson, E.A., Sistla, A.P. (eds) Computer Aided Verification. CAV 2000. Lecture Notes in Computer Science, vol 1855. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10722167_22
Download citation
DOI: https://doi.org/10.1007/10722167_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67770-3
Online ISBN: 978-3-540-45047-4
eBook Packages: Springer Book Archive