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

    Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

    182 Downloads (Pure)


    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
    Publication statusPublished - 2011
    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

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

    Cite this