From functional programming to multicore parallelism: A case study based on Presburger Arithmetic

The overall goal of this work is studying parallelization of functional programs with the specific case study of decision procedures for Presburger Arithmetic (PA). PA is a first order theory of integers accepting addition as its only operation. Whereas it has wide applications in different areas, we are interested in using PA in connection with the Duration Calculus Model Checker (DCMC) [5].

There are effective decision procedures for PA including Cooper’s algorithm and the Omega Test; however, their complexity is extremely high with doubly exponential lower bound and triply exponential upper bound [7]. We investigate these decision procedures in the context of multicore parallelism with the hope of exploiting multicore powers.

Unfortunately, we are not aware of any prior parallelism research related to decision procedures for PA. The closest work is the preliminary results on parallelism in the SMT-solver Z3 [8] which has the capability of solving Presburger formulas. Functional programming is well-suited for the domain of decision procedures, and its immutability feature helps to reduce parallelization effort.

While Haskell has progressed with a lot of parallelismrelated research [6], we choose F# to be able to have explicit control over parallelism on the .NET framework and utilize its option to resort to mutation when optimizing performance.