Document Open Access Logo

QuickLex: A Fast Algorithm for Consistent Global States Enumeration of Distributed Computations

Authors Yen-Jung Chang, Vijay K. Garg

PDF
Thumbnail PDF

File

LIPIcs.OPODIS.2015.25.pdf
  • Filesize: 0.73 MB
  • 17 pages

Document Identifiers

Author Details

Yen-Jung Chang
Vijay K. Garg

Cite AsGet BibTex

Yen-Jung Chang and Vijay K. Garg. QuickLex: A Fast Algorithm for Consistent Global States Enumeration of Distributed Computations. In 19th International Conference on Principles of Distributed Systems (OPODIS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 46, pp. 25:1-25:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
https://doi.org/10.4230/LIPIcs.OPODIS.2015.25

Abstract

Verifying the correctness of executions of concurrent and distributed programs is difficult because they show nondeterministic behavior due to different process scheduling order. Predicate detection can alleviate this problem by predicting whether the user-specified condition (predicate) could have become true in any global state of the given concurrent or distributed computation. The method is predictive because it generates inferred global states from the observed execution path and then checks if those global states satisfy the predicate. An important part of the predicate detection method is global states enumeration, which generates the consistent global states, including the inferred ones, of the given computation. Cooper and Marzullo gave the first enumeration algorithm based on a breadth first strategy (BFS). Later, many algorithms have been proposed to improve the space and time complexity. Among the existing algorithms, the Tree algorithm due to Jegou et al. has the smallest time complexity and requires O(|P|) space, which is linear to the size of the computation P. In this paper, we present a fast algorithm, QuickLex, to enumerate global states in the lexical order. QuickLex requires much smaller space than O(|P|). From our experiments, the Tree algorithm requires 2-10 times more memory space than QuickLex. Moreover, QuickLex is 4 times faster than Tree even though the asymptotic time complexity of QuickLex is higher than that of Tree. The reason is that the worst case time complexity of QuickLex happens only in computations that are not common in practice. Moreover, Tree is built on linked-lists and QuickLex can be implemented using integer arrays. In comparison with the existing lexical algorithm (Lex), QuickLex is 7 times faster and uses almost the same amount of memory as Lex. Finally, we implement a parallel-and-online predicate detector for concurrent programs using QuickLex, which can detect data races and violation of invariants in the programs.
Keywords
  • consistent global state
  • algorithm
  • computation

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Sridhar Alagar and Subbarayan Venkatesan. Techniques to tackle state explosion in global predicate detection. IEEE Transactions on Software Engineering, 27:412-417, 2001. Google Scholar
  2. K. M. Chandy and L. Lamport. Distributed snapshots: Determining global states of distributed systems. ACM Transactions on Computer Systems, 3(1):63-75, February 1985. Google Scholar
  3. Yen-Jung Chang and Vijay K. Garg. A parallel algorithm for global states enumeration in concurrent systems. In ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, 2015. Google Scholar
  4. Feng Chen, Traian Florin Serbanuta, and Grigore Roşu. jPredictor: a predictive runtime analysis tool for java. In Proceedings of the International Conference on Software Engineering, pages 221-230, 2008. Google Scholar
  5. R. Cooper and K. Marzullo. Consistent detection of global predicates. In Proceedings of the ACM/ONR Workshop on Parallel and Distributed Debugging, pages 163-173, 1991. Google Scholar
  6. B. A. Davey and H. A. Priestley. Introduction to lattices and order. In Cambridge University Press, Cambridge, UK, 1990. Google Scholar
  7. E. Farchi, Y. Nir, and S. Ur. Concurrent bug patterns and how to test them. In Proceedings of the International Parallel and Distributed Processing Symposium, 2003. Google Scholar
  8. Colin J. Fidge. Timestamps in message-passing systems that preserve the partial ordering. In Proceedings of the Australian Computer Science Conference, pages 56-66, 1988. Google Scholar
  9. Cormac Flanagan and Stephen N. Freund. FastTrack: efficient and precise dynamic race detection. In Proceedings of ACM SIGPLAN the Conference on Programming Language Design and Implementation, pages 121-133, 2009. Google Scholar
  10. Bernhard Ganter. Two basic algorithms in concept analysis. In Proceedings of the International Conference on Formal Concept Analysis, pages 312-340, 2010. Google Scholar
  11. Vijay K. Garg. Enumerating global states of a distributed computation. In Proceedings of the International Conference on Parallel and Distributed Computing Systems, pages 134-139, 2003. Google Scholar
  12. Vijay K. Garg. Algorithmic combinatorics based on slicing posets. Theoretical Computer Science, 359(1-3):200-213, 2006. URL: http://dx.doi.org/10.1016/j.tcs.2006.03.005.
  13. Vijay K. Garg. Introduction to Lattice Theory with Computer Science Applications. John Wiley &Sons, Inc., 2015. Google Scholar
  14. Vijay K. Garg and B. Waldecker. Detection of unstable predicates. In Proceedings of the Workshop on Parallel and Distributed Debugging, 1991. Google Scholar
  15. Michel Habib, Raoul Medina, Lhouari Nourine, and George Steiner. Efficient algorithms on distributive lattices. Discrete Applied Mathematics, 110(2-3):169-187, 2001. Google Scholar
  16. Jeff Huang and Charles Zhang. Persuasive prediction of concurrency access anomalies. In Proceedings of the International Symposium on Software Testing and Analysis, pages 144-154, 2011. Google Scholar
  17. M. Hurfin, M. Mizuno, M. Raynal, and M. Singhal. Efficient distributed detection of conjunctions of local predicates. IEEE Transactions on Software Engineering, 24:664-677, 1998. Google Scholar
  18. Roland Jegou, Raoul Medina, and Lhouari Nourine. Linear space algorithm for on-line detection of global predicates. In Proceedings of the International Workshop on Structures in Concurrency Theory, pages 175-189, 1995. Google Scholar
  19. Leslie Lamport. Time, clocks, and the ordering of events in a distributed system. Communications of the ACM, 21(7):558-565, 1978. Google Scholar
  20. Y. Lei and R.H. Carver. Reachability testing of concurrent programs. IEEE Transactions on Software Engineering, 32(6):382-403, 2006. Google Scholar
  21. Shan Lu, Joseph Tucek, Feng Qin, and Yuanyuan Zhou. AVIO: detecting atomicity violations via access interleaving invariants. In Proceedings of the International Conference on Architectural Support for Programming Languages and Operating Systems, pages 37-48, 2006. Google Scholar
  22. Friedemann Mattern. Virtual time and global states of distributed systems. In Proceedings of the International Workshop on Parallel and Distributed Algorithms, pages 125-226, Chateau de Bonas, France, 1988. Google Scholar
  23. Vinit A. Ogale and Vijay K. Garg. Detecting temporal logic predicates on distributed computations. In Proceedings of International Symposium in Distributed Computing, pages 420-434, 2007. Google Scholar
  24. Soyeon Park, Shan Lu, and Yuanyuan Zhou. CTrigger: exposing atomicity violation bugs from their hiding places. In Proceedings of the International Conference on Architectural support for programming languages and operating systems, pages 25-36, 2009. Google Scholar
  25. Gara Pruesse and Frank Ruskey. Gray codes from antimatroids. Springer LNCS Order, 10:239-252, 1993. Google Scholar
  26. Francesco Sorrentino, Azadeh Farzan, and P. Madhusudan. PENELOPE: weaving threads to expose atomicity violations. In Proceedings of the ACM SIGSOFT International Symposium on Foundations of Software Engineering, pages 37-46, 2010. Google Scholar
  27. Matthew B. Squire. Enumerating the ideals of a poset. In PhD Dissertation, Department of Computer Science, North Carolina State University, 1995. Google Scholar
  28. George Steiner. An algorithm to generate the ideals of a partial order. Operations Research Letters, 5(6):317-320, 1986. Google Scholar
  29. Christoph von Praun and Thomas R. Gross. Object race detection. In Proceedings of the ACM SIGPLAN conference on Object-Oriented Programming, Systems, Languages, and Applications, pages 70-82, 2001. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact