Document Open Access Logo

Predicate Detection for Parallel Computations with Locking Constraints

Authors Yen-Jung Chang, Vijay K. Garg

PDF
Thumbnail PDF

File

LIPIcs.OPODIS.2016.17.pdf
  • Filesize: 0.97 MB
  • 17 pages

Document Identifiers

Author Details

Yen-Jung Chang
Vijay K. Garg

Cite As Get BibTex

Yen-Jung Chang and Vijay K. Garg. Predicate Detection for Parallel Computations with Locking Constraints. In 20th International Conference on Principles of Distributed Systems (OPODIS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 70, pp. 17:1-17:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.OPODIS.2016.17

Abstract

The happened-before model (or the poset model) has been widely used for modeling the computations (execution traces) of parallel programs and detecting predicates (user-specified conditions). This model captures potential causality as well as locking constraints among the executed events of computations using Lamport's happened-before relation. The detection of a predicate in a computation is performed by checking if the predicate could become true in any reachable global state of the computation. In this paper, we argue that locking constraints are fundamentally different from potential causality. Hence, a poset is not an appropriate model for debugging purposes when the computations contain locking constraints. We present a model called Locking Poset, or a Loset, that generalizes the poset model for locking constraints. Just as a poset captures possibly an exponential number of total orders, a loset captures possibly an exponential number of posets. Therefore, detecting a predicate in a loset is equivalent to detecting the predicate in all corresponding posets. Since determining if a global state is reachable in a computation is a fundamental problem for detecting predicates, this paper first studies the reachability problem in the loset model. We show that the problem is NP-complete. Afterwards, we introduce a subset of reachable global states called lock-free feasible global states such that we can check whether a global state is lock-free feasible in polynomial time. Moreover, we show that lock-free feasible global states can act as "reset" points for reachability and be used to drastically reduce the time for determining the reachability of other global states. We also introduce strongly feasible global states that contain all reachable global states and show that the strong feasibility of a global state can be checked in polynomial time. We show that strong feasibility provides an effective approximation of reachability for many practical applications.

Subject Classification

Keywords
  • predicate detection
  • parallel computations
  • reachable global states
  • locking constraints
  • happened-before relation

Metrics

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

References

  1. 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
  2. Yen-Jung Chang. Predicate detection for parallel computations. In PhD Dissertation, Department of Electrical and Computer Engineering, The University of Texas at Austin, 2016. 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, pages 140-149, 2015. Google Scholar
  4. Yen-Jung Chang and Vijay K. Garg. Quicklex: A fast algorithm for consistent global states enumeration of distributed computations. In International Conference On Principles of Distributed Systems, 2015. Google Scholar
  5. 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
  6. R. Cooper and K. Marzullo. Consistent detection of global predicates. In Proceedings of the Workshop on Parallel and Distributed Debugging, pages 163-173, 1991. Google Scholar
  7. B. A. Davey and H. A. Priestley. Introduction to lattices and order. In Cambridge University Press, Cambridge, UK, 1990. Google Scholar
  8. 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
  9. 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
  10. 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
  11. Bernhard Ganter. Two basic algorithms in concept analysis. In Proceedings of the International Conference on Formal Concept Analysis, pages 312-340, 2010. Google Scholar
  12. 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
  13. Vijay K. Garg. Introduction to Lattice Theory with Computer Science Applications. Wiley, 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 Appl. Math., 110(2-3):169-187, 2001. Google Scholar
  16. Maurice Herlihy and Nir Shavit. The Art of Multiprocessor Programming. Morgan Kaufmann, 2008. Google Scholar
  17. 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
  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. Vineet Kahlon, Franjo Ivancic, and Aarti Gupta. Reasoning about threads communicating via locks. In Proceedings of International Conference on Computer Aided Verification, pages 505-518, 2005. Google Scholar
  20. Vineet Kahlon and Chao Wang. Universal causality graphs: A precise happens-before model for detecting bugs in concurrent programs. In Proceedings of International Conference on Computer Aided Verification, pages 434-449, 2010. Google Scholar
  21. Leslie Lamport. Time, clocks, and the ordering of events in a distributed system. Communications of the ACM, 21(7):558-565, 1978. Google Scholar
  22. Y. Lei and R. H. Carver. Reachability testing of concurrent programs. IEEE Transactions on Software Engineering, 32(6):382-403, 2006. Google Scholar
  23. 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
  24. N. Mittal and V. K. Garg. Techniques and applications of computation slicing. Distributed Computing, 17(3):251-277, 2005. Google Scholar
  25. Madanlal Musuvathi and Shaz Qadeer. Iterative context bounding for systematic testing of multithreaded programs. In Proceedings of ACM SIGPLAN conference on Programming language design and implementation, pages 446-455, 2007. Google Scholar
  26. Robert O'Callahan and Jong-Deok Choi. Hybrid dynamic data race detection. In Proceedings of the ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, pages 167-178, 2003. Google Scholar
  27. Gara Pruesse and Frank Ruskey. Gray codes from antimatroids. Order 10, pages 239-252, 1993. Google Scholar
  28. S. Savage, M. Burrows, G. Nelson, P. Sobalvarro, and T. Anderson. Eraser: a dynamic data race detector for multi-threaded programs. In Proceedings of the ACM Symposium on Operating System Principles, pages 27-37, 1997. Google Scholar
  29. 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
  30. Ashis Tarafdar. Software fault tolerance in distributed systems using controlled re-execution. In PhD Dissertation, Department of Electrical and Computer Engineering, The University of Texas at Austin, 2000. Google Scholar
  31. Willem Visser, Klaus Havelund, Guillaume Brat, SeungJoon Park, and Flavio Lerda. Model checking programs. Automated Software Engineering Journal, 10(2):203-232, 2003. Google Scholar
  32. 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
  33. Chao Wang, Sudipta Kundu, Malay Ganai, and Aarti Gupta. Symbolic predictive analysis for concurrent programs. Formal Methods, 29:256-272, 2009. Google Scholar
  34. Chao Wang, Rhishikesh Limaye, Malay Ganai, and Aarti Gupta. Trace-based symbolic analysis for atomicity violations. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 328-342, 2010. 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 About DROPS Imprint Privacy Contact