Static Prediction of Parallel Computation Graphs

on YouTube ↗24m

" summary

Claims a new static abstraction, graph types, that compactly represent all runtime computation graphs and supports a Hindley-Milner–style inference algorithm (drawing on affine logic and region systems). Implements inference over a subset of OCaml, automatically inferring vertex annotations for futures, emitting an ASCII graph type, a visualizer, and prototype analyses. Evaluation shows inference integrates into compilation, scales to realistic benchmarks, and a prototype deadlock detector finds deadlocks in adversarial cases and proves some programs deadlock-free when prior tools do not.

AI-written summary · about

" chapters (13)

1. 0:00Many static analyses of parallel programs are based on dependency graphs
2. 2:14Just getting information about graph requires advanced analysis
3. 5:24Back to Fibonacci
4. 6:40Normalizing a graph type gives the actual graphs it can represent
5. 8:03The graph type system assigns types and graph types to expressions
6. 10:12Soundness: The actual graph is in the normalization of the graph type
7. 10:35Types of futures are annotated with the last vertex in the future's graph
8. 15:27Recursive functions may need to generate new vertices
9. 16:20Full graph type syntax
10. 17:34Many analogies to region type systems
11. 18:45Implemented graph type inference and several use cases
12. 19:39Inspection of graph types can provide insight into a program
13. 20:37Future work