Tobias Grosser
ResearchTeamProjectsPublicationsEventsJoin Us!Contact

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.

FPL

Using The Library

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.

You can find the implementation in the main/mlir/include/mlir/Analysis/Presburger and main/mlir/lib/Analysis/Presburger directories in MLIR.

Performance

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).

Performance

Open Source Project and Development Model

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.

License and Patents

All our source code is covered under the Apache License v2.0 with LLVM Exceptions.

LLVM Patch reviews and commits

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:

Official LLVM mediums

We regularly check MLIR discourse for any bugs/queries related to FPL. Feel free to start a dicussion there!

Talks

Publications

FPL: Fast Presburger arithmetic through transprecision
Arjun Pitchanathan, Christian Ulmann, Michel Weber, Torsten Hoefler, and Tobias Grosser
OOPSLA 2021

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
OOPSLA 2020

Awards

HiPEAC Technology Transfer Award 2021

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.

OOPSLA 2021 Distinguished Paper Award

Our paper "FPL: Fast Presburger arithmetic through transprecision" won the OOPSLA 2021 Distinguished Paper Award.

Team

as well as our scientific collaborators Theodoros Theodoridis, Maximilian Falkenstein, Michael Kruse, Torsten Hoefler and Zhendong Su and many contributors from the MLIR community.