Static Prediction of Parallel Computation Graphs
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.
In this paper, we introduce 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.
Wed 19 JanDisplayed time zone: Eastern Time (US & Canada) change
15:05 - 16:20
|Visibility Reasoning for Concurrent Snapshot AlgorithmsRemote|
Joakim Öhman IMDEA Software Institute; Universidad Politécnica de Madrid, Aleksandar Nanevski IMDEA Software InstituteDOI Media Attached
|Connectivity Graphs: A Method for Proving Deadlock Freedom Based on Separation LogicRemote|
Jules Jacobs Radboud University Nijmegen, Stephanie Balzer Carnegie Mellon University, Robbert Krebbers Radboud University NijmegenDOI Media Attached
|Static Prediction of Parallel Computation GraphsInPerson|
Stefan K. Muller Illinois Institute of TechnologyDOI Media Attached