Abstract
A commonly used approach to develop parallel programs is to augment a sequential program with compiler directives that indicate which program blocks may potentially be executed in parallel. This paper develops a verification technique to prove correctness of compiler directives combined with functional correctness of the program. We propose syntax and semantics for a simple core language, capturing the main forms of deterministic parallel programs. This language distinguishes three kinds of basic blocks: parallel, vectorized and sequential blocks, which can be composed using three different composition operators: sequential, parallel and fusion composition. We show that it is sufficient to have contracts for the basic blocks to prove correctness of the compiler directives, and moreover that functional correctness of the sequential program implies correctness of the parallelized program. We formally prove correctness of our approach. In addition, we define a widely-used subset of OpenMP that can be encoded into our core language, thus effectively enabling the verification of OpenMP compiler directives, and we discuss automated tool support for this verification process.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
See the online version of the VerCors toolset at http://www.utwente.nl/vercors/.
References
Aviram, A., Ford, B.: Deterministic OpenMP for race-free parallelism. In: HotPar 2011, Berkeley, CA, USA, p. 4 (2011)
Barthe, G., Crespo, J.M., Gulwani, S., Kunz, C., Marron, M.: From relational verification to SIMD loop synthesis. In: ACM SIGPLAN Notices, vol. 48, pp. 123–134 (2013)
Berger, M.J., Aftosmis, M.J., Marshall, D.D., Murman, S.M.: Performance of a new CFD flow solver using a hybrid programming paradigm. J. Parallel Distrib. Comput. 65(4), 414–423 (2005)
Blom, S., Huisman, M.: The VerCors tool for verification of concurrent programs. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 127–131. Springer, Cham (2014). doi:10.1007/978-3-319-06410-9_9
Blom, S., Huisman, M., Mihelčić, M.: Specification and verification of GPGPU programs. Sci. Comput. Program. 95, 376–388 (2014)
Blom, S., Darabi, S., Huisman, M.: Verification of loop parallelisations. In: Egyed, A., Schaefer, I. (eds.) FASE 2015. LNCS, vol. 9033, pp. 202–217. Springer, Heidelberg (2015). doi:10.1007/978-3-662-46675-9_14
Bornat, R., Calcagno, C., O’Hearn, P., Parkinson, M.: Permission accounting in separation logic. In: POPL, pp. 259–270 (2005)
Botincan, M., Dodds, M., Jagannathan, S.: Resource-sensitive synchronization inference by abduction. In: POPL, pp. 309–322 (2012)
Botinčan, M., Dodds, M., Jagannathan, S.: Proof-directed parallelization synthesis by separation logic. ACM Trans. Program. Lang. Syst. 35, 1–60 (2013)
Boyland, J.: Checking interference with fractional permissions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 55–72. Springer, Heidelberg (2003). doi:10.1007/3-540-44898-5_4
Che, S., Boyer, M., Meng, J., Tarjan, D., Sheaffer, J.W., Lee, S.-H., Skadron, K.: Rodinia: a benchmark suite for heterogeneous computing. In: Workload Characterization, IISWC 2009, pp. 44–54 (2009)
Darabi, S., Blom, S.C.C., Huisman, M.: A verification technique for deterministic parallel programs (extended version). Technical report TR-CTIT-17-01, Centre for Telematics and Information Technology, University of Twente (2017)
Dodds, M., Jagannathan, S., Parkinson, M.J.: Modular reasoning for deterministic parallelism. In: ACM SIGPLAN Notices, pp. 259–270 (2011)
Hoare, C.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)
Hurlin, C.: Automatic parallelization and optimization of programs by proof rewriting. In: Palsberg, J., Su, Z. (eds.) SAS 2009. LNCS, vol. 5673, pp. 52–68. Springer, Heidelberg (2009). doi:10.1007/978-3-642-03237-0_6
**, H.-Q., Frumkin, M., Yan, J.: The OpenMP implementation of NAS parallel Benchmarks and its performance (1999)
O’Hearn, P.W.: Resources, concurrency and local reasoning. Theoret. Comput. Sci. 375(1–3), 271–307 (2007)
OpenMP Architecture Review Board: OpenMP API specification for parallel programming. http://openmp.org/wp/. Accessed 28 Nov 2016
LLNL OpenMP Benchmarks. https://asc.llnl.gov/CORAL-benchmarks/. Accessed 28 Nov 2016
Raychev, V., Vechev, M., Yahav, E.: Automatic synthesis of deterministic concurrency. In: Logozzo, F., Fähndrich, M. (eds.) SAS 2013. LNCS, vol. 7935, pp. 283–303. Springer, Heidelberg (2013). doi:10.1007/978-3-642-38856-9_16
Reynolds, J.: Separation logic: a logic for shared mutable data structures. In: Logic in Computer Science, pp. 55–74. IEEE Computer Society (2002)
Tuch, H., Klein, G., Norrish, M.: Types, bytes, and separation logic. In: Hofmann, M., Felleisen, M. (eds.) POPL, pp. 97–108. ACM (2007)
VerCors project homepage, 28 September 2016. http://www.utwente.nl/vercors/
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Darabi, S., Blom, S.C.C., Huisman, M. (2017). A Verification Technique for Deterministic Parallel Programs. In: Barrett, C., Davies, M., Kahsai, T. (eds) NASA Formal Methods. NFM 2017. Lecture Notes in Computer Science(), vol 10227. Springer, Cham. https://doi.org/10.1007/978-3-319-57288-8_17
Download citation
DOI: https://doi.org/10.1007/978-3-319-57288-8_17
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-57287-1
Online ISBN: 978-3-319-57288-8
eBook Packages: Computer ScienceComputer Science (R0)