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.

翻译：并行程序常被建模为依赖图或代价图，用于检测各类错误或直观展示代码的并行结构。然而，这类图仅反映单次特定执行，且通常采用事后构建方式。近期提出的图类型化方法可通过类型系统对程序进行静态赋值，并紧凑表征程序可能产生的所有图族。遗憾的是，先前工作在Future（一种日益普及且动态性极强的并行机制）处理上存在局限。简言之，每个Future实例必须与顶点名称静态配对，这导致Future无法被置于集合中或用于构建数据结构。这并非边缘性课题：此类结构构成了大量利用管线技术实现非Future不可达性能的算法基础。除最受限的少数案例外，这些算法实例均超出先前图类型系统的处理范围。本文提出一种允许Future与递归数据类型进行近乎任意组合的图类型系统。具体而言，我们通过类型级顶点结构（一种为数据结构中Future提供唯一顶点名称的余数据类型）对数据类型进行索引。在标注顶点结构及相关操作的并行核心演算中，我们证明了该系统的可靠性。尽管演算本身经过标注，这仅为定义类型系统提供便利。我们证明任意递归类型均可标注顶点结构，并借助原型推理引擎展示：对于多个复杂并行算法，这些标注可从类似OCaml的源码中自动推断得出。