paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Static prediction of parallel computation graphs

并行计算图的静态预测
POPL 6(POPL)2022匹配度 4/10 · 论文提出用于静态推断并行程序计算图的类型系统与推理算法,并实现于 OCaml,属于理论形式化与工程实现兼具的 PL/静态分析工作,与用户对静态分析、类型系统的研究方法有部分交集。但其核心是传统并行程序分析,不涉及 LLM/Agent、浮点程序分析或贝叶斯程序分析,与画像中正在追踪的交叉方向匹配度较低。引用 4 inbox
Stefan K. Muller
crossref: 2026-09-10

AI 速览

一句话:提出图类型(graph types),静态推断并行程序所有可能的计算图,并用于死锁检测与开销分析。

许多并行程序分析(如死锁检测、数据竞争检测或执行代价计算)都基于捕获线程并行结构的计算图/依赖图模型。然而现代并行程序的计算图高度动态,强烈依赖输入与执行细节,导致多数分析要么是动态分析,要么是为特定目的收集依赖信息子集的专用静态分析。本文提出图类型(graph types),可紧凑地表示程序执行中可能出现的所有计算图。图类型通过图类型系统与推断算法从并行程序中推断得到,其设计借鉴了 Hindley-Milner 类型推断、仿射逻辑与区域类型系统的思想。作者在扩展了并行原语的 OCaml 子集上实现了该推断算法,并通过死锁检测与开销分析两个概念验证分析,展示了图类型如何加速新的基于图的静态分析开发。

问题
如何静态地刻画并行程序运行时可能产生的动态计算图,以支持通用而非专用的并行程序分析。
方法
提出图类型(graph types)紧凑表示所有可能的计算图,设计图类型系统与推断算法,借鉴 Hindley-Milner 类型推断、仿射逻辑和区域类型系统的思想。
评估
在扩展并行原语的 OCaml 子集上实现推断算法,并实现死锁检测与开销分析两个概念验证静态分析以展示图类型的用途。
原文摘要(Abstract)

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.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot1549,
  title = {Static prediction of parallel computation graphs},
  author = {Stefan K. Muller},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {6},
  number = {POPL},
  year = {2022},
  doi = {10.1145/3498708}
}