Deadlock Avoidance in Parallel Programs with Futures: Why Parallel Tasks Should Not Wait for Strangers
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.
Fri 27 OctDisplayed time zone: Tijuana, Baja California change
13:30 - 15:00 | |||
13:30 22mTalk | Deadlock Avoidance in Parallel Programs with Futures: Why Parallel Tasks Should Not Wait for Strangers OOPSLA Tiago Cogumbreiro Rice University, Rishi Surendran Rice University, USA, Francisco Martins LaSIGE, University of Lisbon, Vivek Sarkar Rice University, USA, Vasco T. Vasconcelos University of Lisbon, Portugal, Max Grossman Rice University, USA DOI | ||
13:52 22mTalk | Detecting Argument Selection Defects OOPSLA Andrew Rice University of Cambridge, UK, Eddie Aftandilian Google, Ciera Jaspan Google, Emily Johnston Google, Michael Pradel TU Darmstadt, Yulissa Arroyo-Paredes Columbia University, USA DOI | ||
14:15 22mTalk | How Type Errors Were Fixed and What Students Did? OOPSLA DOI | ||
14:37 22mTalk | Learning User Friendly Type-Error Messages OOPSLA Baijun Wu University of Louisiana at Lafayette, USA, John Peter Campora ULL Lafayette, Sheng Chen ULL Lafayette DOI |