Skip to main content
SpringerLink
Log in
Book cover

International Workshop on Formal Approaches to Software Testing

FATES 2003: Formal Approaches to Software Testing pp 15–29Cite as

On Checking Whether a Predicate Definitely Holds

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2931))

Abstract

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].

supported in part by the NSF Grants ECS-9907213, CCR-9988225, Texas Education Board Grant ARP-320, an Engineering Foundation Fellowship, and an IBM grant.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  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)

    Article  Google Scholar 

  2. Chase, C., Garg, V.K.: Detection of Global Predicates: Techniques and their Limitations. Distributed Computing 11(4), 191–201 (1998)

    Article  Google Scholar 

  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. 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. Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order. Cambridge University Press, Cambridge (1990)

    MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  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. Garg, V.K.: Elements of Distributed Computing. John Wiley & Sons, Chichester (2002)

    Google Scholar 

  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. 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)

    Article  Google Scholar 

  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. Havelund, K., Rosu, G.: Monitoring Java Programs with Java PathExplorer. In: Runtime Verification 2001. ENTCS, vol. 55 (2001)

    Google Scholar 

  13. Holzmann, G.J.: The Model Checker Spin. IEEE Trans. on Software Engineering 23(5), 279–295 (1997)

    Article  MathSciNet  Google Scholar 

  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. 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)

    Article  Google Scholar 

  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)

    Article  MATH  Google Scholar 

  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. Lamport, L.: Time, Clocks, and the Ordering of Events in a Distributed System. Communications of the ACM (CACM) 21(7), 558–565 (1978)

    Article  MATH  Google Scholar 

  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. 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)

    Chapter  Google Scholar 

  21. Preusse, G., Ruskey, F.: Generating Linear Extensions Fast. SIAM J. Comput. 23, 373–386 (1994)

    Article  MathSciNet  Google Scholar 

  22. Schwartz, R., Mattern, F.: Detecting Causal Relationships in Distributed Computations: In Search of the Holy Grail. Distributed Computing 7(3), 149–174 (1994)

    Article  Google Scholar 

  23. Sen, A., Garg, V.K.: Partial Order Trace Analzyer (POTA), http://maple.ece.utexas.edu/~sen/POTA.html

  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. 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)

    Chapter  Google Scholar 

  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. Sen, A., Garg, V.K.: Partial Order Trace Analyzer (POTA) for Distributed Programs. In: Runtime Verification 2003. ENTCS, vol. 89 (2003)

    Google Scholar 

  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. 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)

    Chapter  Google Scholar 

  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)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dept. of Electrical and Computer Engineering, The University of Texas at Austin, Austin, TX, 78712, USA

    Alper Sen & Vijay K. Garg

Authors
  1. Alper Sen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Vijay K. Garg
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. CRIM, Canada

    Alexandre Petrenko

  2. Siemens AG, Corporate Research & Technologies CT SE 1, Otto-Hahn-Ring 6, 81730, Munich, Germany

    Andreas Ulrich

Rights and permissions

Reprints and permissions

Copyright information

© 2004 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Sen, A., Garg, V.K. (2004). On Checking Whether a Predicate Definitely Holds. In: Petrenko, A., Ulrich, A. (eds) Formal Approaches to Software Testing. FATES 2003. Lecture Notes in Computer Science, vol 2931. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24617-6_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-24617-6_2

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-20894-5

  • Online ISBN: 978-3-540-24617-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation