一句话：提出嵌套并行程序的内存性质“解纠缠”，并据此设计内存管理技术以提升效率与可扩展性。
嵌套并行广泛用于多核编程，但破坏性更新带来的并发缺陷使高效可扩展的实现困难，函数式语言又因内存需求随并行度增长而性能受限。本文识别出嵌套并行程序的一种内存性质——解纠缠（disentanglement）：只要并发线程不获取彼此分配的内存对象的知识，就允许破坏性效应。作者用带可变引用的 ML 类高阶语言给出动态语义，基于计算图形式化解纠缠，并证明经典正确性性质“确定性竞争自由”蕴含解纠缠，表明该性质适用于较广的并行程序类。随后提出利用解纠缠的内存管理技术，并扩展 Standard ML 的 MLton 编译器予以支持；实验表明这些技术高效且扩展良好。
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.
@article{paperbot513,
title = {Disentanglement in nested-parallel programs},
author = {Sam Westrick and Rohan Yadav and Matthew Fluet and Umut A. Acar},
journal = {Proceedings of the ACM on Programming Languages},
volume = {4},
number = {POPL},
year = {2019},
doi = {10.1145/3371115}
}