Verification of loop parallelisations

Stefan Blom, Saeed Darabi, Marieke Huisman

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

9 Citations (Scopus)
58 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
Blom, Stefan ; Darabi, Saeed ; Huisman, Marieke. / Verification of loop parallelisations. Proceedings of the 18th International Conference on Fundamental Approaches to Software Engineering (FASE 2015). editor / Alexander Egyed ; Ina Schaefer. London : Springer, 2015. pp. 202-217 (Lecture Notes in Computer Science).
@inproceedings{443b6e5256ca41a3a2d9652a1bc0221d,
title = "Verification of loop parallelisations",
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.",
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",
author = "Stefan Blom and Saeed Darabi and Marieke Huisman",
note = "eemcs-eprint-26136",
year = "2015",
month = "4",
doi = "10.1007/978-3-662-46675-9_14",
language = "Undefined",
isbn = "978-3-662-46674-2",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "202--217",
editor = "Alexander Egyed and Ina Schaefer",
booktitle = "Proceedings of the 18th International Conference on Fundamental Approaches to Software Engineering (FASE 2015)",

}

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). Lecture Notes in Computer Science, vol. 9033, Springer, London, pp. 202-217. https://doi.org/10.1007/978-3-662-46675-9_14

Verification of loop parallelisations. / Blom, Stefan; Darabi, Saeed; Huisman, Marieke.

Proceedings of the 18th International Conference on Fundamental Approaches to Software Engineering (FASE 2015). ed. / Alexander Egyed; Ina Schaefer. London : Springer, 2015. p. 202-217 (Lecture Notes in Computer Science; Vol. 9033).

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

TY - GEN

T1 - Verification of loop parallelisations

AU - Blom, Stefan

AU - Darabi, Saeed

AU - Huisman, Marieke

N1 - eemcs-eprint-26136

PY - 2015/4

Y1 - 2015/4

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

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

KW - EC Grant Agreement nr.: FP7/287767

KW - EWI-26136

KW - METIS-312667

KW - EC Grant Agreement nr.: FP7/258405

KW - IR-96982

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

U2 - 10.1007/978-3-662-46675-9_14

DO - 10.1007/978-3-662-46675-9_14

M3 - Conference contribution

SN - 978-3-662-46674-2

T3 - Lecture Notes in Computer Science

SP - 202

EP - 217

BT - Proceedings of the 18th International Conference on Fundamental Approaches to Software Engineering (FASE 2015)

A2 - Egyed, Alexander

A2 - Schaefer, Ina

PB - Springer

CY - London

ER -

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