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)
    117 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 languageEnglish
    Title of host publicationProceedings of the 7th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software (PLACES 2014)
    Subtitle of host publicationGrenoble, France, 12 April 2014
    EditorsAlastair F. Donaldson, Vasco T. Vasconcelos
    Place of PublicationNew York
    PublisherCornell University
    Pages47-53
    Number of pages7
    DOIs
    Publication statusPublished - 12 Apr 2014
    Event7th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software, PLACES 2014 - Grenoble, France
    Duration: 12 Apr 201412 Apr 2014
    Conference number: 7

    Publication series

    NameElectronic Proceedings in Theoretical Computer Science
    PublisherCornell University
    Volume155
    ISSN (Electronic)2075-2180

    Workshop

    Workshop7th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software, PLACES 2014
    Abbreviated titlePLACES
    Country/TerritoryFrance
    CityGrenoble
    Period12/04/1412/04/14

    Keywords

    • EC Grant Agreement nr.: FP7/2007-2013
    • EC Grant Agreement nr.: FP7/287767

    Fingerprint

    Dive into the research topics of 'Verifying parallel loops with separation logic'. Together they form a unique fingerprint.

    Cite this