An approach to multicore parallelism using functional programming: A case study based on Presburger Arithmetic

Research output: Contribution to journalJournal articleResearchpeer-review


In this paper we investigate multicore parallelism in the context of functional programming by means of two quantifier-elimination procedures for Presburger Arithmetic: one is based on Cooper’s algorithm and the other is based on the Omega Test.

We first develop correct-by-construction prototype implementations in a functional programming language. Thereafter, the parallelism inherent in the decision procedures is analyzed using the Directed Acyclic Graph (DAG) model of multicore parallelism. In the step from a DAG model to a parallel implementation, the parallel implementation is optimized taking into account negative factors such as cache misses, garbage collection and overhead due to task creations, because such factors may introduce sequential bottlenecks with severe consequences for the parallel efficiency.

The experiments were conducted using the functional programming language F# and .NET platform executing on an 8-core machine. A speedup of approximately 4 was obtained for Cooper’s algorithm and a speedup of approximately 6 was obtained for the exact-shadow part of the Omega Test.

The considered procedures are complex, memory-intense algorithms on huge formula trees and the case study reveals more general applicable techniques and guideline for deriving parallel algorithms from sequential ones in the context of data-intensive tree algorithms. The obtained insights should apply for any strict and impure functional programming language.

Furthermore, the results obtained for the exact-shadow elimination procedure have a wider applicability because they can directly be transferred to the Fourier–Motzkinelimination method.
Original languageEnglish
JournalJournal of Logic and Algebraic Programming
Issue number1
Pages (from-to)2–18
Number of pages17
Publication statusPublished - 2015
Event23rd Nordic Workshop on Programming Theory - Västerås, Sweden
Duration: 26 Oct 201128 Oct 2011
Conference number: 23


Conference23rd Nordic Workshop on Programming Theory
Internet address


  • Multicore
  • Parallelism
  • Functional programming
  • Presburger Arithmetic
  • Decision procedure

Fingerprint Dive into the research topics of 'An approach to multicore parallelism using functional programming: A case study based on Presburger Arithmetic'. Together they form a unique fingerprint.

Cite this