• 6 Citations

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 Berlin Heidelberg
Pages202-217
Number of pages15
ISBN (Print)978-3-662-46674-2
DOIs
StatePublished - Apr 2015

Publication series

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

Fingerprint

Specifications
Synchronization

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 Berlin Heidelberg. DOI: 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). ed. / Alexander Egyed; Ina Schaefer. London : Springer Berlin Heidelberg, 2015. p. 202-217 (Lecture Notes in Computer Science; Vol. 9033).

Research output: Scientific - peer-reviewConference contribution

@inbook{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",
isbn = "978-3-662-46674-2",
series = "Lecture Notes in Computer Science",
publisher = "Springer Berlin Heidelberg",
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 Berlin Heidelberg, London, pp. 202-217. DOI: 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 Berlin Heidelberg, 2015. p. 202-217 (Lecture Notes in Computer Science; Vol. 9033).

Research output: Scientific - peer-reviewConference contribution

TY - CHAP

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)

PB - Springer Berlin Heidelberg

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 Berlin Heidelberg. 2015. p. 202-217. (Lecture Notes in Computer Science). Available from, DOI: 10.1007/978-3-662-46675-9_14