一句话:为基于区域推断的编译器设计 fork-join 并行构造,并给出类型规则、动态语义、类型可靠性及效应推断算法。
区域推断是一种基于类型的内存管理分析,可将未标注程序转换为显式使用区域栈进行分配与释放的程序;区域内存管理在并行执行中已有优势,但与高阶并行编程的结合尚未研究。本文面向基于区域推断的编译器实现 fork-join 并行构造,给出包含该构造的最小高阶语言的类型规则与动态语义,证明类型可靠性,并提出一种新的基于效应的区域保护推断算法。作者将该方法高效嵌入 MLKit Standard ML 编译器,使用一组并行基准进行评估,结果表明该技术能在高阶函数式环境中有效利用多核架构。
Region inference is a type-based program analysis that takes a non-annotated program as input and constructs a program that explicitly manages memory allocation and deallocation by dividing the heap into a stack of regions, each of which can grow and shrink independently from other regions, using constant-time operations.Whereas region-based memory management has shown useful in the contexts of explicit region-based memory management, and in particular, in combination with parallel execution of code, combining region inference with techniques for higher-order parallel programming has not been investigated.In this paper, we present an implementation of a fork-join parallel construct suitable for a compiler based on region inference. We present a minimal higher-order language incorporating the parallel construct, including typing rules and a dynamic semantics for the language, and demonstrate type soundness. We present a novel effect-based region-protection inference algorithm and discuss benefits and shortcomings of the approach. We also describe an efficient implementation embedded in the MLKit Standard ML compiler. Finally, we evaluate the approach and the implementation based on a number of parallel benchmarks, and thereby demonstrate that the technique effectively utilises multi-core architectures in a higher-order functional setting.