Static Prediction of Parallel Computation GraphsInPerson
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 | |||
15:05 25mResearch paper | Visibility Reasoning for Concurrent Snapshot AlgorithmsRemote POPL Joakim Öhman IMDEA Software Institute; Universidad Politécnica de Madrid, Aleksandar Nanevski IMDEA Software Institute DOI Media Attached | ||
15:30 25mResearch paper | Connectivity Graphs: A Method for Proving Deadlock Freedom Based on Separation LogicRemote POPL Jules Jacobs Radboud University Nijmegen, Stephanie Balzer Carnegie Mellon University, Robbert Krebbers Radboud University Nijmegen DOI Media Attached | ||
15:55 25mResearch paper | Static Prediction of Parallel Computation GraphsInPerson POPL Stefan K. Muller Illinois Institute of Technology DOI Media Attached |