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

Publication: Research - peer-reviewArticle in proceedings – Annual report year: 2011


View graph of relations

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.
Original languageEnglish
Title of host publicationProceedings of the 23rd Nordic Workshop Programming Theory
Publication date2011


Conference23rd Nordic Workshop on Programming Theory
Internet address
Download as:
Download as PDF
Select render style:
Download as HTML
Select render style:
Download as Word
Select render style:

Download statistics

No data available

ID: 6373685