Disentanglement in Nested-Parallel Programs
Nested parallelism has proved to be a popular approach for programming the rapidly expanding range of multicore computers. It allows programmers to express parallelism at a high level and relies on a run-time system and a scheduler to deliver efficiency and scalability. As a result, many programming languages and extensions that support nested parallelism have been developed, including in C/C++, Java, Haskell, and ML. Yet, writing efficient and scalable nested parallel programs remains challenging, primarily due to difficult concurrency bugs arising from destructive updates or effects. For decades, researchers have argued that functional programming can simplify writing parallel programs by allowing more control over effects but functional programs continue to underperform in comparison to parallel programs written in lower-level languages. The fundamental difficulty with functional languages is that they have high demand for memory, and this demand only grows with parallelism.
In this paper, we identify a memory property, called disentanglement, of nested-parallel programs, and propose memory management techniques for improved efficiency and scalability. Disentanglement allows for (destructive) effects as long as concurrently executing threads do not gain knowledge of the memory objects allocated by each other. We formally define disentanglement by considering an ML-like higher-order language with mutable references and presenting a dynamic semantics for it that enables reasoning about computation graphs of nested parallel programs. Based on this graph semantics, we formalize a classic correctness property—determinacy race freedom—and prove that it implies disentanglement. This establishes that disentanglement applies to a relatively broad class of parallel programs. We then propose memory management techniques for nested-parallel programs that take advantage of disentanglement for improved efficiency and scalability. We show that these techniques are practical by extending the MLton compiler for Standard ML to support this form of nested parallelism. Our empirical evaluation shows that our techniques are efficient and scale well.
Fri 24 JanDisplayed time zone: Saskatchewan, Central America change
14:00 - 15:05
Language DesignResearch Papers at Ile de France III (IDF III)
Chair(s): Amin Timany imec-Distrinet KU-Leuven
|Stacked Borrows: An Aliasing Model for Rust|
Ralf Jung MPI-SWS, Hoang-Hai Dang MPI-SWS, Jeehoon Kang KAIST, Derek Dreyer MPI-SWSLink to publication DOI Media Attached File Attached
|Executable Formal Semantics for the POSIX Shell|
Michael Greenberg Pomona College, Austin J. Blatt Puppet LabsLink to publication DOI Media Attached File Attached
|Disentanglement in Nested-Parallel Programs|
Sam Westrick Carnegie Mellon University, Rohan Yadav Carnegie Mellon University, Matthew Fluet Rochester Institute of Technology, Umut A. Acar Carnegie Mellon UniversityLink to publication DOI Media Attached File Attached