Generating High Performance Code for Irregular Data Structures using Dependent Types
summary
Extends a data-parallel language with index-sequence types (nuts), a scoping primitive (lift_nut / lift_nuts) and dependent pairs so offsets and packed CSR arrays bundle safely; compiler derives closed-form flattening for indexing and emits OpenCL GPU code. Implements dense→CSR conversion and spMV (and BFS in paper), runs on an NVIDIA GTX1080 against cuSPARSE, reports typical speedups around 1.2–1.5× and competitive overall. Types drive fusion, index-simplification and loop-bounds inference rather than acting only as proofs.
AI-written summary · about
chapters (5)
- 0:00Start
- 23:29Question Does the compiler rely on or take advantage of types during optimisation, or are types only used for verification?
- 24:24Nice presentation is there any strong reason to have a nats type separate from arrays of indices? We were thinking of implementing something similar, but were planning to use arrays that are in scope as sources of sizes for other arrays.
- 25:39Could similarly fast code be written with data- parallel FP without dependent types, by implementing the code with "flat" arrays with manual offset computation i.e. presumably what your compiler itself ends up generating/?
- 27:52Does the type checker provide any guidance on when the compiler is able to turn indexing into closed forms?
related talks
19mCompiling Recurrences over Dense and Sparse Arrays
20mExploiting Sparsity and Redundancy
20mVectorizing Sparse Coiteration for Two-finger Loop Structure (Extended Abstract)
28mFunctional Sparse Tensor Compilation
19mCompiler Support for Sparse Tensor Convolutions
15mCompilation of Sparse Array Programming Models
11mExtending the Scope of the Array Abstraction beyond Sparsity
24mMapping Sparse Applications to Accelerated Computing Systems