Verifying parallel loops with separation logic

Stefan Blom, Saeed Darabi, Marieke Huisman

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

    1 Citation (Scopus)
    56 Downloads (Pure)

    Abstract

    This paper proposes a technique to specify and verify whether a loop can be parallelised. Our approach can be used as an additional step in a parallelising compiler to verify user annotations about loop dependences. Essentially, our technique requires each loop iteration to be specified with the locations it will read and write. From the loop iteration specifications, the loop (in)dependences can be derived. Moreover, the loop iteration specifications also reveal where synchronisation is needed in the parallelised program. The loop iteration specifications can be verified using permission-based separation logic.
    Original languageUndefined
    Title of host publicationProceedings of the 7th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software (PLACES 2014)
    Place of PublicationNew York
    PublisherCornell University
    Pages47-53
    Number of pages7
    DOIs
    Publication statusPublished - 12 Apr 2014

    Publication series

    NameEPTCS
    PublisherCornell University
    NumberarXiv:1406.3313
    Volume155
    ISSN (Print)2075-2180
    ISSN (Electronic)2075-2180

    Keywords

    • EWI-24867
    • EC Grant Agreement nr.: FP7/2007-2013
    • METIS-305923
    • IR-91764
    • EC Grant Agreement nr.: FP7/287767

    Cite this

    Blom, S., Darabi, S., & Huisman, M. (2014). Verifying parallel loops with separation logic. In Proceedings of the 7th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software (PLACES 2014) (pp. 47-53). (EPTCS; Vol. 155, No. arXiv:1406.3313). New York: Cornell University. https://doi.org/10.4204/EPTCS.155.7