Fri 22 Oct 2021 19:20 - 19:35 at Zurich C - Algorithms, Libraries and Databases - mirror Chair(s): Fabian Muehlboeck
Presburger arithmetic provides the mathematical core for the polyhedral compilation techniques that drive analytical cache models, loop optimization for ML and HPC, formal verification, and even hardware design. Polyhedral compilation is widely regarded as being slow due to the potentially high computational cost of the underlying Presburger libraries. Researchers typically use these libraries as powerful black-box tools, but the perceived internal complexity of these libraries, caused by the use of C as the implementation language and a focus on end-user-facing documentation, holds back broader performance-optimization efforts. With FPL, we introduce a new library for Presburger arithmetic built from the ground up in modern C++. We carefully document its internal algorithmic foundations, use lightweight C++ data structures to minimize memory management costs, and deploy transprecision computing across the entire library to effectively exploit machine integers and vector instructions. On a newly-developed comprehensive benchmark suite for Presburger arithmetic, we show a 5.4x speedup in total runtime over the state-of-the-art library isl in its default configuration and 3.6x over a variant of isl optimized with element-wise transprecision computing. We expect that the availability of a well-documented and fast Presburger library will accelerate the adoption of polyhedral compilation techniques in production compilers.
Fri 22 OctDisplayed time zone: Central Time (US & Canada) change
10:50 - 12:10 | |||
10:50 15mTalk | UDF to SQL Translation through Compositional Lazy Inductive SynthesisVirtual OOPSLA Guoqiang Zhang North Carolina State University; Facebook, Yuanchao Xu North Carolina State University, Xipeng Shen North Carolina State University; Facebook, Işıl Dillig University of Texas at Austin DOI | ||
11:05 15mTalk | LXM: Better Splittable Pseudorandom Number Generators (and Almost as Fast)Virtual OOPSLA DOI | ||
11:20 15mTalk | FPL: Fast Presburger Arithmetic through TransprecisionIn-Person OOPSLA Arjun Pitchanathan IIIT Hyderabad, Christian Ulmann ETH Zurich, Michel Weber ETH Zurich, Torsten Hoefler ETH Zurich, Tobias Grosser University of Edinburgh DOI | ||
11:35 15mTalk | Verifying Concurrent Multicopy Search StructuresIn-Person OOPSLA Nisarg Patel New York University, Siddharth Krishna Microsoft Research, Dennis Shasha New York University, Thomas Wies New York University DOI | ||
11:50 20mLive Q&A | Discussion, Questions and Answers OOPSLA |