PPoPP 2019
Sat 16 - Wed 20 February 2019 Washington, DC, United States
Wed 20 Feb 2019 12:10 - 12:35 at Salon 12/13 - Session 10: Verification Chair(s): Michael Lam

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 Feb

11:20 - 12:35: Main Conference - Session 10: Verification at Salon 12/13
Chair(s): Michael LamJames Madison University
PPoPP-2019-papers11:20 - 11:45
Simon DohertyUniversity of Sheffield, Brijesh DongolUniversity of Surrey, Heike WehrheimPaderborn University, John DerrickUniversity of Sheffield
PPoPP-2019-papers11:45 - 12:10
Burcu Kulahcioglu OzkanMPI-SWS, Germany, Rupak MajumdarMPI-SWS, Germany, Filip NiksicUniversity of Pennsylvania
PPoPP-2019-papers12:10 - 12:35
Caleb VossGeorgia Institute of Technology, Tiago CogumbreiroUniversity of Massachusetts Boston, Vivek SarkarRice University, USA