Abstract
We propose a specification and verification technique based on separation logic to reason about data race freedom and functional correctness of GPU kernels that use atomic operations as synchronisation mechanism. Our approach exploits the notion of resource invariant from Concurrent Separation Logic (CSL) to capture the behaviour of atomic operations. However, because of the different memory levels in the GPU architecture, we adapt this notion of resource invariant to these memory levels, i.e., group resource invariants capture the behaviour of atomic operations that access locations in local memory, while kernel resource invariants capture the behaviour of atomic operations that access locations in global memory. We show soundness of our approach and we provide tool support that enables us to verify kernels from standard benchmarks suites.
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
Notes
- 1.
To be precise, the GPU execution model is Single Instruction Multiple Thread (SIMT), which extends SIMD with more flexibility in the control flow.
- 2.
Our implementation supports the OpenCL programming language, but can easily be extended to other GPGPU programming languages such as CUDA and C++ AMP.
- 3.
In our specification language we use ** for star conjunction because of the syntactic overlap with multiplication.
- 4.
The number of work groups is determined in the host code before launching the kernel.
- 5.
A ghost variable (a.k.a. as auxiliary variable) is a specification-only variable, which does not change the control flow of the program and is used only for verification.
- 6.
This is syntactic sugar for universal quantification of the permissions over all the indices of cont[].
- 7.
\(L[e]\) denotes the value stored at location \(e\) in the local memory array, and substitution is as usually defined for arrays, cf. [1]:
$$ L [ e ] [ L [ e_1 ] := e_2 ] = (e=e_1)?e_2:L[e]. $$ - 8.
References
Apt, K.R.: Ten years of Hoare’s logic: A survey \(-\) Part I. ACM Trans. Program. Lang. Syst. 3, 431–483 (1981)
Bardsley, E., Donaldson, A.F.: Warps and atomics: Beyond barrier synchronization in the verification of GPU kernels. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2014. LNCS, vol. 8430, pp. 230–245. Springer, Heidelberg (2014)
Betts, A., Chong, N., Donaldson, A., Qadeer, S., Thomson, P.: GPUVerify: a verifier for GPU kernels. In: OOPSLA 2012, pp. 113–132. ACM (2012)
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, Heidelberg (2014)
Blom, S., Huisman, M., Mihelčić, M.: Specification and verification of GPGPU programs. Sci. Comput. Program. 95(3), 376–388 (2014)
Bornat, R., Calcagno, C., O’Hearn, P., Parkinson, M.: Permission accounting in separation logic. In: POPL 2005, 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)
Hobor, A., Gherghina, C.: Barriers in concurrent separation logic. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 276–296. Springer, Heidelberg (2011)
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)
Li, G., Gopalakrishnan, G.: Scalable SMT-based verification of GPU kernel functions. In: SIGSOFT FSE 2010, pp. 187–196. ACM (2010)
NVIDIA Corporation, CUDA C programming guide, version 5.5 (2013)
O’Hearn, P.W.: Resources, concurrency and local reasoning. Theoret. Comput. Sci. 375, 271–307 (2007)
Reynolds, J.: Separation logic: A logic for shared mutable data structures. In: Logic in Computer Science, pp. 55–74. IEEE Computer Society (2002)
Smans, J., Jacobs, B., Piessens, F.: Implicit dynamic frames. ACM Trans. Program. Lang. Syst. 34(1), 2:1–2:58 (2012)
Stratton, J.A., Rodrigues, C., Sung, I.-J., Obeid, N., Chang, L.-W., Anssari, N., Liu, G.D., Hwu, W.-M.: Parboil: A revised benchmark suite for scientific and commercial throughput computing, Center for Reliable and High-Performance Computing (2012)
Vafeiadis, V.: Concurrent separation logic and operational semantics. Electr. Notes Theor. Comput. Sci. 276, 335–351 (2011)
Acknowledgement
This work is supported by the ERC 258405 VerCors project and by the EU FP7 STREP 287767 project CARP.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Amighi, A., Darabi, S., Blom, S., Huisman, M. (2015). Specification and Verification of Atomic Operations in GPGPU Programs. In: Calinescu, R., Rumpe, B. (eds) Software Engineering and Formal Methods. SEFM 2015. Lecture Notes in Computer Science(), vol 9276. Springer, Cham. https://doi.org/10.1007/978-3-319-22969-0_5
Download citation
DOI: https://doi.org/10.1007/978-3-319-22969-0_5
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-22968-3
Online ISBN: 978-3-319-22969-0
eBook Packages: Computer ScienceComputer Science (R0)