FPL: A Fast Presburger Library
Fast Presburger Library (FPL) is a new library for Presburger Arithmetic that attains high performance by optimizing for typical polyhedral workloads. In particular, FPL specializes for the small coefficients that typically arise in polyhedral compilation, uses cache optimized data structures and deploys vectorization. FPL is written in modern C++ and is available directly in MLIR.
Large parts of FPL have already been upstreamed into MLIR. Union, intersection, subtraction, complement, equality checks, and emptiness checks are already supported. We are currently working on upstreaming support for coalesce and lexicographic optimization, as well as our transprecision performance optimizations.
We created a benchmark for Presburger arithmetic as used in polyhedral workloads by running Polly, PPCG, and Pluto on Polybench and extracting the Presburger set operations that they performed. We compared the results against isl in two modes: isl (GMP), which performs all computations using arbitrary precision integers, and isl (element-TP), which uses 32-bit integers when possible and falls back to arbitrary precision when required to maintain correctness. We found that FPL is 5.4x times faster than isl (GMP) and 3.6x times faster than isl (element-TP).
FPL is being developed as part of the MLIR open-source project in close collaboration with the LLVM open-source community. All development is public and non-confidential to ensure broad community support.
All our source code is covered under the Apache License v2.0 with LLVM Exceptions.
All our patches are developed in public. As a result, we regularly take part in interactive patch review discussions with MLIR community members. We contribute changes several times a week to the MLIR repositories:
We regularly check MLIR discourse for any bugs/queries related to FPL. Feel free to start a dicussion there!
FPL: A Presburger Library in MLIR at LLVM Dev Meeting 2021
FPL: Fast Presburger Arithmetic through Transprecision at OOPSLA 2021
FPL: Fast Presburger arithmetic through transprecision
Arjun Pitchanathan, Christian Ulmann, Michel Weber, Torsten Hoefler, and Tobias Grosser
Fast linear programming through transprecision computing on small and sparse data
Tobias Grosser, Theodoros Theodoridis, Maximilian Falkenstein, Arjun Pitchanathan, Michael Kruse, Manuel Rigger, Zhendong Su, Torsten Hoefler
Our paper "Fast linear programming through transprecision computing on small and sparse data" won the 2021 HiPEAC Technology Transfer Award for developing the foundations of FPL and for working closely with the LLVM community to integrate our solver (and later FPL) into the LLVM compiler. The research on our Simplex solver was funded by ARM and Xilinx, in the context of Polly Labs. FPL is an ongoing research project at the University of Edinburgh that received industry funding for its development in the context of MLIR.
Our paper "FPL: Fast Presburger arithmetic through transprecision" won the OOPSLA 2021 Distinguished Paper Award.
- Arjun Pitchanathan
- Christian Ulmann
- Kunwar Shaanjeet Singh Grover
- Michel Weber
- Prashant Kumar
- Tobias Grosser
as well as our scientific collaborators Theodoros Theodoridis, Maximilian Falkenstein, Michael Kruse, Torsten Hoefler and Zhendong Su and many contributors from the MLIR community.