Transitive Joins: A Sound and Efficient Online Deadlock-Avoidance Policy
We introduce a new online deadlock-avoidance policy, Transitive Joins (TJ), that targets programs with dynamic task parallelism and arbitrary join operations. In this model, a computation task can asynchronously spawn new tasks and selectively join (block) on any task for which it has a handle. We prove that TJ soundly guarantees the absence of deadlock cycles among the blocking join operations. We present an algorithm for dynamically verifying TJ and show that TJ results in fewer false positives than the state-of-the-art policy, Known Joins (KJ). We evaluate an implementation of our verifier in comparison to prior work. The evaluation results show that instrumenting a program with a TJ verifier incurs geometric mean overheads of only 1.06$\times$ in execution time and 1.09$\times$ in memory usage, which is better overall than existing KJ verifiers. TJ is a practical online deadlock-avoidance policy that is applicable to a wide range of parallel programming models.
Wed 20 FebDisplayed time zone: Guadalajara, Mexico City, Monterrey change
11:20 - 12:35 | Session 10: VerificationMain Conference at Salon 12/13 Chair(s): Michael Lam James Madison University | ||
11:20 25mTalk | Verifying C11 Programs Operationally Main Conference Simon Doherty University of Sheffield, Brijesh Dongol University of Surrey, Heike Wehrheim Paderborn University, John Derrick University of Sheffield DOI | ||
11:45 25mTalk | Checking Linearizability Using Hitting Families Main Conference Burcu Kulahcioglu Ozkan MPI-SWS, Germany, Rupak Majumdar MPI-SWS, Germany, Filip Niksic University of Pennsylvania DOI | ||
12:10 25mTalk | Transitive Joins: A Sound and Efficient Online Deadlock-Avoidance Policy Main Conference Caleb Voss Georgia Institute of Technology, Tiago Cogumbreiro University of Massachusetts Boston, Vivek Sarkar Rice University, USA DOI |