一句话:提出图类型(graph types),静态推断并行程序所有可能的计算图,并用于死锁检测与开销分析。
许多并行程序分析(如死锁检测、数据竞争检测或执行代价计算)都基于捕获线程并行结构的计算图/依赖图模型。然而现代并行程序的计算图高度动态,强烈依赖输入与执行细节,导致多数分析要么是动态分析,要么是为特定目的收集依赖信息子集的专用静态分析。本文提出图类型(graph types),可紧凑地表示程序执行中可能出现的所有计算图。图类型通过图类型系统与推断算法从并行程序中推断得到,其设计借鉴了 Hindley-Milner 类型推断、仿射逻辑与区域类型系统的思想。作者在扩展了并行原语的 OCaml 子集上实现了该推断算法,并通过死锁检测与开销分析两个概念验证分析,展示了图类型如何加速新的基于图的静态分析开发。
Many algorithms for analyzing parallel programs, for example to detect deadlocks or data races or to calculate the execution cost, are based on a model variously known as a cost graph, computation graph or dependency graph, which captures the parallel structure of threads in a program. In modern parallel programs, computation graphs are highly dynamic and depend greatly on the program inputs and execution details. As such, most analyses that use these graphs are either dynamic analyses or are specialized static analyses that gather a subset of dependency information for a specific purpose. This paper introduces graph types, which compactly represent all of the graphs that could arise from program execution. Graph types are inferred from a parallel program using a graph type system and inference algorithm, which we present drawing on ideas from Hindley-Milner type inference, affine logic and region type systems. We have implemented the inference algorithm over a subset of OCaml, extended with parallelism primitives, and we demonstrate how graph types can be used to accelerate the development of new graph-based static analyses by presenting proof-of-concept analyses for deadlock detection and cost analysis.