Verification of loop parallelisations
| Autor: | Blom, Stefan, Darabi, Saeed, Huisman, Marieke, Egyed, Alexander, Schaefer, Ina |
|---|---|
| Rok vydání: | 2015 |
| Předmět: |
For loop
Correctness LOOP (programming language) Programming language Computer science EWI-26136 020207 software engineering 02 engineering and technology Separation logic Permission EWI-26816 IR-99507 computer.software_genre EC Grant Agreement nr.: FP7/258405 020204 information systems 0202 electrical engineering electronic engineering information engineering Code (cryptography) IR-96982 EC Grant Agreement nr.: FP7/2007-2013 Loop interchange Compiler computer EC Grant Agreement nr.: FP7/287767 METIS-312667 |
| Zdroj: | Fundamental Approaches to Software Engineering ISBN: 9783662466742 FASE STARTPAGE=IPA;ENDPAGE=4;TITLE=ICT.OPEN 2015 Proceedings of the 18th International Conference on Fundamental Approaches to Software Engineering (FASE 2015), 202-217 STARTPAGE=202;ENDPAGE=217;TITLE=Proceedings of the 18th International Conference on Fundamental Approaches to Software Engineering (FASE 2015) University of Twente Research Information (Pure Portal) |
| ISSN: | 0302-9743 |
| DOI: | 10.1007/978-3-662-46675-9_14 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|