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 language | English |
---|---|
Title of host publication | Proceedings of the 7th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software (PLACES 2014) |
Subtitle of host publication | Grenoble, France, 12 April 2014 |
Editors | Alastair F. Donaldson, Vasco T. Vasconcelos |
Place of Publication | New York |
Publisher | Cornell University |
Pages | 47-53 |
Number of pages | 7 |
DOIs | |
Publication status | Published - 12 Apr 2014 |
Event | 7th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software, PLACES 2014 - Grenoble, France Duration: 12 Apr 2014 → 12 Apr 2014 Conference number: 7 |
Publication series
Name | Electronic Proceedings in Theoretical Computer Science |
---|---|
Publisher | Cornell University |
Volume | 155 |
ISSN (Electronic) | 2075-2180 |
Workshop
Workshop | 7th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software, PLACES 2014 |
---|---|
Abbreviated title | PLACES |
Country/Territory | France |
City | Grenoble |
Period | 12/04/14 → 12/04/14 |
Keywords
- EC Grant Agreement nr.: FP7/2007-2013
- EC Grant Agreement nr.: FP7/287767