Predicate Detection for Parallel Computations with Locking Constraints
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.
predicate detection
parallel computations
reachable global states
locking constraints
happened-before relation
17:1-17:17
Regular Paper
Yen-Jung
Chang
Yen-Jung Chang
Vijay K.
Garg
Vijay K. Garg
10.4230/LIPIcs.OPODIS.2016.17
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.
Yen-Jung Chang. Predicate detection for parallel computations. In PhD Dissertation, Department of Electrical and Computer Engineering, The University of Texas at Austin, 2016.
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.
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.
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.
R. Cooper and K. Marzullo. Consistent detection of global predicates. In Proceedings of the Workshop on Parallel and Distributed Debugging, pages 163-173, 1991.
B. A. Davey and H. A. Priestley. Introduction to lattices and order. In Cambridge University Press, Cambridge, UK, 1990.
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.
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.
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.
Bernhard Ganter. Two basic algorithms in concept analysis. In Proceedings of the International Conference on Formal Concept Analysis, pages 312-340, 2010.
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.
Vijay K. Garg. Introduction to Lattice Theory with Computer Science Applications. Wiley, 2015.
Vijay K. Garg and B. Waldecker. Detection of unstable predicates. In Proceedings of the Workshop on Parallel and Distributed Debugging, 1991.
Michel Habib, Raoul Medina, Lhouari Nourine, and George Steiner. Efficient algorithms on distributive lattices. Discrete Appl. Math., 110(2-3):169-187, 2001.
Maurice Herlihy and Nir Shavit. The Art of Multiprocessor Programming. Morgan Kaufmann, 2008.
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.
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.
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.
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.
Leslie Lamport. Time, clocks, and the ordering of events in a distributed system. Communications of the ACM, 21(7):558-565, 1978.
Y. Lei and R. H. Carver. Reachability testing of concurrent programs. IEEE Transactions on Software Engineering, 32(6):382-403, 2006.
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.
N. Mittal and V. K. Garg. Techniques and applications of computation slicing. Distributed Computing, 17(3):251-277, 2005.
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.
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.
Gara Pruesse and Frank Ruskey. Gray codes from antimatroids. Order 10, pages 239-252, 1993.
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.
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.
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.
Willem Visser, Klaus Havelund, Guillaume Brat, SeungJoon Park, and Flavio Lerda. Model checking programs. Automated Software Engineering Journal, 10(2):203-232, 2003.
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.
Chao Wang, Sudipta Kundu, Malay Ganai, and Aarti Gupta. Symbolic predictive analysis for concurrent programs. Formal Methods, 29:256-272, 2009.
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.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode