Verifying parallel loops with separation logic

Stefan Blom, Saeed Darabi, Marieke Huisman

  • 1 Citations

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
StatePublished - 12 Apr 2014

Publication series

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

Fingerprint

Specifications
Synchronization

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. DOI: 10.4204/EPTCS.155.7

Blom, Stefan; Darabi, Saeed; Huisman, Marieke / Verifying parallel loops with separation logic.

Proceedings of the 7th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software (PLACES 2014). New York : Cornell University, 2014. p. 47-53 (EPTCS; Vol. 155, No. arXiv:1406.3313).

Research output: Scientific - peer-reviewConference contribution

@inbook{8f85311a0c844dbb8efbd5c3b71452c2,
title = "Verifying parallel loops with separation logic",
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.",
keywords = "EWI-24867, EC Grant Agreement nr.: FP7/2007-2013, METIS-305923, IR-91764, EC Grant Agreement nr.: FP7/287767",
author = "Stefan Blom and Saeed Darabi and Marieke Huisman",
note = "eemcs-eprint-24867",
year = "2014",
month = "4",
doi = "10.4204/EPTCS.155.7",
series = "EPTCS",
publisher = "Cornell University",
number = "arXiv:1406.3313",
pages = "47--53",
booktitle = "Proceedings of the 7th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software (PLACES 2014)",

}

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). EPTCS, no. arXiv:1406.3313, vol. 155, Cornell University, New York, pp. 47-53. DOI: 10.4204/EPTCS.155.7

Verifying parallel loops with separation logic. / Blom, Stefan; Darabi, Saeed; Huisman, Marieke.

Proceedings of the 7th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software (PLACES 2014). New York : Cornell University, 2014. p. 47-53 (EPTCS; Vol. 155, No. arXiv:1406.3313).

Research output: Scientific - peer-reviewConference contribution

TY - CHAP

T1 - Verifying parallel loops with separation logic

AU - Blom,Stefan

AU - Darabi,Saeed

AU - Huisman,Marieke

N1 - eemcs-eprint-24867

PY - 2014/4/12

Y1 - 2014/4/12

N2 - 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.

AB - 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.

KW - EWI-24867

KW - EC Grant Agreement nr.: FP7/2007-2013

KW - METIS-305923

KW - IR-91764

KW - EC Grant Agreement nr.: FP7/287767

U2 - 10.4204/EPTCS.155.7

DO - 10.4204/EPTCS.155.7

M3 - Conference contribution

T3 - EPTCS

SP - 47

EP - 53

BT - Proceedings of the 7th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software (PLACES 2014)

PB - Cornell University

ER -

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