Skip to content

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.

Contributions

All our patches are developed in public and reviewed by the MLIR community through LLVM pull requests.

Official LLVM mediums

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

Talks

Publications

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