Verification of loop parallelisations

Stefan Blom, Saeed Darabi, Marieke Huisman

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    11 Citations (Scopus)
    75 Downloads (Pure)

    Abstract

    Writing correct parallel programs becomes more and more difficult as the complexity and heterogeneity of processors increase. This issue is addressed by parallelising compilers. Various compiler directives can be used to tell these compilers where to parallelise. This paper addresses the correctness of such compiler directives for loop parallelisation. Specifically, we propose a technique based on separation logic to verify whether a loop can be parallelised. Our approach requires each loop iteration to be specified with the locations that are read and written in this iteration. If the specifications are correct, they can be used to draw conclusions about loop (in)dependences. Moreover, they also reveal where synchronisation is needed in the parallelised program. The loop iteration specifications can be verified using permission-based separation logic and seamlessly integrate with functional behaviour specifications. We formally prove the correctness of our approach and we discuss automated tool support for our technique. Additionally, we also discuss how the loop iteration contracts can be compiled into specifications for the code coming out of the parallelising compiler.
    Original languageUndefined
    Title of host publicationProceedings of the 18th International Conference on Fundamental Approaches to Software Engineering (FASE 2015)
    EditorsAlexander Egyed, Ina Schaefer
    Place of PublicationLondon
    PublisherSpringer
    Pages202-217
    Number of pages15
    ISBN (Print)978-3-662-46674-2
    DOIs
    Publication statusPublished - Apr 2015

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer Berlin Heidelberg
    Volume9033
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Keywords

    • EC Grant Agreement nr.: FP7/287767
    • EWI-26136
    • METIS-312667
    • EC Grant Agreement nr.: FP7/258405
    • IR-96982
    • EC Grant Agreement nr.: FP7/2007-2013

    Cite this

    Blom, S., Darabi, S., & Huisman, M. (2015). Verification of loop parallelisations. In A. Egyed, & I. Schaefer (Eds.), Proceedings of the 18th International Conference on Fundamental Approaches to Software Engineering (FASE 2015) (pp. 202-217). (Lecture Notes in Computer Science; Vol. 9033). London: Springer. https://doi.org/10.1007/978-3-662-46675-9_14