Rank-Polymorphism for Shape-Guided Blocking
summary
Claims a method to express arbitrary levels of cache blocking by encoding block depth and sizes in rank-polymorphic arrays, with reshaping switching between blocked and flat views and combinators avoiding explicit loops or index math. A dependently-typed Agda framework proves out-of-bounds safety and that all blocked variants equal the canonical multiply. Implementation targets SaC, generates C, and on a 32-core machine beats OpenBLAS by 7% and MKL by 3% in reported experiments.
AI-written summary · about
chapters (8)
- 0:00Rank-polymorphism intro
- 3:15Recursive blocking in matrix multiply
- 7:34Rank polymorphism for recursion
- 10:05Formal verification in Agda
- 16:37Blocked matrix spec
- 21:34Proving blocked algorithm
- 26:16Key insights and future
- 28:13Q&A on floating-point
related talks
20mAUTOMAP: Inferring Rank-Polymorphic Function Applications with Integer Linear Programming
30mLayout Polymorphism: Using static computation to allow efficient polymorphism over...
25mAUTOMAP: Inferring Rank-Polymorphic Function Applications with Integer Linear Programming
21mSeamless Scope-Safe Metaprogramming Through Polymorphic Subtype Inference (Short Paper)
14mMicroKanren in J
19mPanel: Compilation Frameworks
18mA Simple and Efficient Implementation of Strong Call by Need by an Abstract Ma…
14mThe Simple Essence of Monomorphization