On Checking Whether a Predicate Definitely Holds

  • Alper Sen
  • Vijay K. Garg
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2931)


Predicate detection is an important problem in testing and debugging distributed programs. Cooper and Marzullo introduced two modalities possibly and definitely as a solution to this problem. Given a predicate p, a computation satisfies possibly:p if p is true for some global state in the computation. A computation satisfies definitely:p if all paths from the initial to the final global state go through some global state that satisfies p. In general, definitely modality is used to detect good conditions such as “a leader is eventually chosen by all processes”, or “a commit point is reached by every process”, whereas possibly modality is used to detect bad conditions such as violation of mutual exclusion. There are several efficient algorithms for possibly modality in the literature [10,14,1,2,30]. However, this is not the case for definitely modality. Cooper and Marzullo’s definitely:p algorithm for arbitrary p has a worst-case space and time complexity exponential in the number of processes. This is due to the state explosion problem. In this paper we present efficient algorithms for detecting definitely:p. In particular, we give a simple algorithm that uses polynomial space. Then, we present an algorithm that can significantly reduce the global state-space. We determine necessary conditions and sufficient conditions under which detecting definitely:p may be efficiently solved. We apply our algorithms to example protocols, achieving a speedup of over 100, compared to partial order reduction based technique of SPIN [13].


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Charron-Bost, B., Delporte-Gallet, C., Fauconnier, H.: Local and Temporal Predicates in Distributed Systems. ACM Transactions on Programming Languages and Systems 17(1), 157–179 (January 1995)CrossRefGoogle Scholar
  2. 2.
    Chase, C., Garg, V.K.: Detection of Global Predicates: Techniques and their Limitations. Distributed Computing 11(4), 191–201 (1998)CrossRefGoogle Scholar
  3. 3.
    Clarke, E.M., Emerson, E.A.: Design and Synthesis of Synchronization Skeletons using Branching Time Temporal Logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131. Springer, Heidelberg (1981)Google Scholar
  4. 4.
    Cooper, R., Marzullo, K.: Consistent Detection of Global Predicates. In: Proceedings of the ACM/ONR Workshop on Parallel and Distributed Debugging, Santa Cruz, California, pp. 163–173 (1991)Google Scholar
  5. 5.
    Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order. Cambridge University Press, Cambridge (1990)zbMATHGoogle Scholar
  6. 6.
    Drusinsky, D.: The Temporal Rover and the ATG Rover. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, pp. 323–330. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  7. 7.
    Fromentin, E., Raynal, M.: Inevitable global states: A concept to detect unstable properties of distributed computations in an observer independent way. In: Proceedings of the 6th IEEE Symposium on Parallel and Distributed Processing (SPDP), Los Alamitos, CA, pp. 242–248 (1994)Google Scholar
  8. 8.
    Garg, V.K.: Elements of Distributed Computing. John Wiley & Sons, Chichester (2002)Google Scholar
  9. 9.
    Garg, V.K., Mittal, N.: On Slicing a Distributed Computation. In: Proceedings of the 21st IEEE International Conference on Distributed Computing Systems (ICDCS), Phoenix, Arizona, April 2001, pp. 322–329 (2001)Google Scholar
  10. 10.
    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)CrossRefGoogle Scholar
  11. 11.
    Hallal, H., Petrenko, A., Ulrich, A., Boroday, S.: Using SDL Tools to Test Properties of Distributed Systems. In: Proc. FATES 2001, Workshop on Formal Approaches to Testing of Software (August 2001)Google Scholar
  12. 12.
    Havelund, K., Rosu, G.: Monitoring Java Programs with Java PathExplorer. In: Runtime Verification 2001. ENTCS, vol. 55 (2001)Google Scholar
  13. 13.
    Holzmann, G.J.: The Model Checker Spin. IEEE Trans. on Software Engineering 23(5), 279–295 (1997)CrossRefMathSciNetGoogle Scholar
  14. 14.
    Hurfin, M., Mizuno, M., Raynal, M., Singhal, M.: Efficient Distributed Detection of Conjunctions of Local Predicates in Asynchronous Computations. In: Proceedings of the 8th IEEE Symposium on Parallel and Distributed Processing (SPDP), New Orleans, October 1996, pp. 588–594 (1996)Google Scholar
  15. 15.
    Hurfin, M., Mizuno, M., Raynal, M., Singhal, M.: Efficient Detection of Conjuntions of Local Predicates. IEEE Transactions on Software Engineering 24(8), 664–677 (1998)CrossRefGoogle Scholar
  16. 16.
    Kamel, M., Leue, S.: Formalization and Validation of the General Inter-ORB Protocol (GIOP) Using Promela and SPIN. Software Tools for Technology Transfer 2(4), 394–409 (2000)zbMATHCrossRefGoogle Scholar
  17. 17.
    Kim, M., Kannan, S., Lee, I., Sokolsky, O., Viswanathan, M.: Java-MaC: a Run-time Assurance Tool for Java Programs. In: Runtime Verification 2001. ENTCS, vol. 55 (2001)Google Scholar
  18. 18.
    Lamport, L.: Time, Clocks, and the Ordering of Events in a Distributed System. Communications of the ACM (CACM) 21(7), 558–565 (1978)zbMATHCrossRefGoogle Scholar
  19. 19.
    Mattern, F.: Virtual Time and Global States of Distributed Systems. In: Parallel and Distributed Algorithms: Proceedings of the Workshop on Distributed Algorithms (WDAG), pp. 215–226. Elsevier Science Publishers B. V., North-Holland (1989)Google Scholar
  20. 20.
    Mittal, N., Garg, V.K.: Computation Slicing: Techniques and Theory. In: Welch, J.L. (ed.) DISC 2001. LNCS, vol. 2180, pp. 78–92. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  21. 21.
    Preusse, G., Ruskey, F.: Generating Linear Extensions Fast. SIAM J. Comput. 23, 373–386 (1994)CrossRefMathSciNetGoogle Scholar
  22. 22.
    Schwartz, R., Mattern, F.: Detecting Causal Relationships in Distributed Computations: In Search of the Holy Grail. Distributed Computing 7(3), 149–174 (1994)CrossRefGoogle Scholar
  23. 23.
    Sen, A., Garg, V.K.: Partial Order Trace Analzyer (POTA),
  24. 24.
    Sen, A., Garg, V.K.: Detecting Temporal Logic Predicates on the Happened-Before Model. In: Proc. of the International Parallel and Distributed Processing Symposium (IPDPS), Fort Lauderdale, Florida (2002)Google Scholar
  25. 25.
    Sen, A., Garg, V.K.: Automatic Generation of Computation Slices for Detecting Temporal Logic Predicates. In: Papatriantafilou, M., Hunel, P. (eds.) OPODIS 2003. LNCS, vol. 3144, pp. 171–183. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  26. 26.
    Sen, A., Garg, V.K.: On Checking Whether a Predicate Definitely Holds. Technical Report TR-PDS-2003-003, PDSL, ECE Dept. Univ. of Texas at Austin (2003)Google Scholar
  27. 27.
    Sen, A., Garg, V.K.: Partial Order Trace Analyzer (POTA) for Distributed Programs. In: Runtime Verification 2003. ENTCS, vol. 89 (2003)Google Scholar
  28. 28.
    Tarafdar, A., Garg, V.K.: Predicate Control for Active Debugging of Distributed Programs. In: Proceedings of the 9th IEEE Symposium on Parallel and Distributed Processing (SPDP), Orlando, pp. 763–769 (1998)Google Scholar
  29. 29.
    Tarafdar, A., Garg, V.K.: Software Fault Tolerance of Concurrent Programs Using Controlled Re-execution. In: Jayanti, P. (ed.) DISC 1999. LNCS, vol. 1693, pp. 210–224. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  30. 30.
    Tomlinson, A.I., Garg, V.K.: Monitoring Functions on Global States of Distributed Programs. Journal of Parallel and Distributed Computing 41(2), 173–189 (1997)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Alper Sen
    • 1
  • Vijay K. Garg
    • 1
  1. 1.Dept. of Electrical and Computer EngineeringThe University of Texas at AustinAustinUSA

Personalised recommendations