一句话：提出支持 future 与递归数据类型近乎任意组合的图类型系统，可静态推断并证明可靠性。
并行程序常用依赖图或代价图建模，以检测缺陷或可视化并行结构，但此类图只反映单次执行且事后构造。图类型可静态赋予程序并紧凑表示所有可能图，然而先前工作对 future 限制严格：每个 future 实例须静态配唯一顶点名，故 future 不能放入集合或构建数据结构，难以覆盖大量流水线算法。本文提出支持 future 与递归数据类型近乎任意组合的图类型系统，用类型级 vertex structure（一种 codata 结构）索引数据类型，为其中的 future 提供唯一顶点名。作者在带 vertex structure 的并行核心演算中证明可靠性，证明任意递归类型均可如此标注，并用原型推断引擎从类 OCaml 源码为若干复杂并行算法推断标注。
Parallel programs are frequently modeled as dependency or cost graphs, which can be used to detect various bugs, or simply to visualize the parallel structure of the code. However, such graphs reflect just one particular execution and are typically constructed in a post-hoc manner. Graph types , which were introduced recently to mitigate this problem, can be assigned statically to a program by a type system and compactly represent the family of all graphs that could result from the program. Unfortunately, prior work is restricted in its treatment of futures , an increasingly common and especially dynamic form of parallelism. In short, each instance of a future must be statically paired with a vertex name. Previously, this led to the restriction that futures could not be placed in collections or be used to construct data structures. Doing so is not a niche exercise: such structures form the basis of numerous algorithms that use forms of pipelining to achieve performance not attainable without futures. All but the most limited of these examples are out of reach of prior graph type systems. In this paper, we propose a graph type system that allows for almost arbitrary combinations of futures and recursive data types. We do so by indexing datatypes with a type-level vertex structure , a codata structure that supplies unique vertex names to the futures in a data structure. We prove the soundness of the system in a parallel core calculus annotated with vertex structures and associated operations. Although the calculus is annotated, this is merely for convenience in defining the type system. We prove that it is possible to annotate arbitrary recursive types with vertex structures, and show using a prototype inference engine that these annotations can be inferred from OCaml-like source code for several complex parallel algorithms.
@article{paperbot2635,
title = {Pipelines and Beyond: Graph Types for ADTs with Futures},
author = {Francis Rinaldi and june wunder and Arthur Azevedo de Amorim and Stefan K. Muller},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {POPL},
year = {2024},
doi = {10.1145/3632859}
}