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.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Baghdadi, R., Cohen, A., Guelton, S., Verdoolaege, S., Inoue, J., Grosser, T., Kouveli, G., Kravets, A., Lokhmotov, A., Nugteren, C., Waters, F., Donaldson, A.F.: PENCIL: Towards a Platform-Neutral Compute Intermediate Language for DSLs. CoRR, abs/1302.5586 (2013)
Barthe, G., Crespo, J.M., Gulwani, S., Kunz, C., Marron, M.: From relational verification to SIMD loop synthesis. In: PPoPP, pp. 123–134 (2013)
Blom, S., Darabi, S., Huisman, M.: Verifying parallel loops with separation logic. In: PLACES, pp. 47–53 (2014)
Blom, S., Huisman, M., Mihelčić, M.: Specification and verification of GPGPU programs. In: Science of Computer Programming (2014)
Bornat, R., Calcagno, C., O’Hearn, P., Parkinson, M.: Permission accounting in separation logic. In: Palsberg, J., Abadi, M. (eds.) POPL, pp. 259–270. ACM (2005)
Boyland, J.: Checking interference with fractional permissions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 55–72. Springer, Heidelberg (2003)
Dagum, L., Menon, R.: OpenMP: an industry standard API for shared-memory programming. IEEE Computational Science & Engineering 5(1), 46–55 (1998)
Gedell, T., Hähnle, R.: Automating verification of loops by parallelization. In: LPAR, pp. 332–346 (2006)
Haack, C., Huisman, M., Hurlin, C.: Reasoning about java’s reentrant locks. In: Ramalingam, G. (ed.) APLAS 2008. LNCS, vol. 5356, pp. 171–187. Springer, Heidelberg (2008)
Hehner, E.: Specified blocks. In: Meyer, B., Woodcock, J. (eds.) VSTTE 2005. LNCS, vol. 4171, pp. 384–391. Springer, Heidelberg (2008)
Hoare, C.: An axiomatic basis for computer programming. Communications of the ACM 12(10), 576–580 (1969)
Juhasz, U., Kassios, I.T., Müller, P., Novacek, M., Schwerhoff, M., Summers, A.J.: Viper: A verification infrastructure for permission-based reasoning. Technical report, ETH Zurich (2014)
Microsoft TPL, http://msdn.microsoft.com/enus/library/dd460717.aspx
Oancea, C.E., Rauchwerger, L.: Logical inference techniques for loop parallelization. SIGPLAN Not 47(6), 509–520 (2012)
O’Hearn, P.W.: Resources, concurrency and local reasoning. Theoretical Computer Science 375(1–3), 271–307 (2007)
Radoi, C., Dig, D.: Practical static race detection for java parallel loops. In: ISSTA, pp. 178–190 (2013)
Reynolds, J.: Separation logic: A logic for shared mutable data structures. In: Logic in Computer Science, pp. 55–74. IEEE Computer Society (2002)
Rus, S., Pennings, M., Rauchwerger, L.: Sensitivity analysis for automatic parallelization on multi-cores. In: Proceedings of the 21st Annual International Conference on Supercomputing, ICS, pp. 263–273. ACM (2007)
Salamanca, J., Mattos, L., Araujo, G.: Loop-carried dependence verification in openMP. In: DeRose, L., de Supinski, B.R., Olivier, S.L., Chapman, B.M., Müller, M.S. (eds.) IWOMP 2014. LNCS, vol. 8766, pp. 87–102. Springer, Heidelberg (2014)
State of the Lambda: Libraries Edition, http://cr.openjdk.java.net/~briangoetz/lambda/lambda-libraries-final.html
Threading Building Blocks, http://threadingbuildingblocks.org
Tuch, H., Klein, G., Norrish, M.: Types, bytes, and separation logic. In: Hofmann, M., Felleisen, M. (eds.) POPL, pp. 97–108. ACM (2007)
Viper project website, http://www.pm.inf.ethz.ch/research/viper
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Blom, S., Darabi, S., Huisman, M. (2015). Verification of Loop Parallelisations. In: Egyed, A., Schaefer, I. (eds) Fundamental Approaches to Software Engineering. FASE 2015. Lecture Notes in Computer Science(), vol 9033. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-46675-9_14
Download citation
DOI: https://doi.org/10.1007/978-3-662-46675-9_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-46674-2
Online ISBN: 978-3-662-46675-9
eBook Packages: Computer ScienceComputer Science (R0)