Write a Blog >>
Sun 22 - Fri 27 October 2017 Vancouver, Canada
Fri 27 Oct 2017 13:30 - 13:52 at Regency A - Usability and Deadlock Chair(s): Jonathan Aldrich

Futures represent an elegant approach to express parallelism in functional programs. Combining futures with imperative programming can lead to pernicious bugs in the form of data races and deadlocks, as a consequence of uncontrolled information flow through mutable shared memory. In this paper, we formalize a new Known Joins (KJ) property for parallel programs with future tasks, and relate it to the Deadlock Freedom (DF) and Data-Race Freedom (DRF) properties. Our paper offers two key theoretical results: 1) DRF ⇒ KJ, and 2) KJ ⇒ DF. These results show that data-race freedom is sufficient to guarantee deadlock freedom. To the best of our knowledge, these are the first theoretical results to establish sufficient conditions for deadlock freedom in imperative parallel programs with future tasks, and to characterize the subset of data races that can trigger deadlocks (those that violate the KJ property). From result KJ ⇒ DF, we developed a tool that avoids deadlocks in linear time and space when KJ holds, i.e., no data-races are found in references to futures. When KJ fails, the tool reports the data-race and falls back to a standard cycle detection algorithm. The performance results obtained from our tool are very encouraging: a maximum slowdown of 1.08× on a 16-core machine, always outperforming deadlock avoidance via cycle-detection. Proofs of all results were formalized using the Coq proof assistant.