Journal of Automated Reasoning

, Volume 60, Issue 3, pp 279–298 | Cite as

Automated Verification of Functional Correctness of Race-Free GPU Programs

  • Kensuke Kojima
  • Akifumi Imanishi
  • Atsushi Igarashi
Article
  • 49 Downloads

Abstract

We study an automated verification method for functional correctness of parallel programs running on graphics processing units (GPUs). Our method is based on Kojima and Igarashi’s Hoare logic for GPU programs. Our algorithm generates verification conditions (VCs) from a program annotated by specifications and loop invariants, and passes them to off-the-shelf SMT solvers. It is often impossible, however, to solve naively generated VCs in reasonable time. A main difficulty stems from quantifiers over threads due to the parallel nature of GPU programs. To overcome this difficulty, we additionally apply several transformations to simplify VCs before calling SMT solvers. Our implementation successfully verifies correctness of several GPU programs, including matrix multiplication optimized by using shared memory. In contrast to many existing verification tools for GPU programs, our verifier succeeds in verifying fully parameterized programs: parameters such as the number of threads and the sizes of matrices are all symbolic. We empirically confirm that our simplification heuristics is highly effective for improving efficiency of the verification procedure.

Keywords

Program verification GPGPU SMT Symbolic execution 

Notes

Acknowledgements

We thank anonymous reviewers for their valuable comments.

References

  1. 1.
    Asakura, I., Masuhara, H., Aotani, T.: Proof of soundness of concurrent separation logic for GPGPU in Coq. J. Inf. Process. 24(1), 132–140 (2016)Google Scholar
  2. 2.
    Betts, A., Chong, N., Donaldson, A.F., Ketema, J., Qadeer, S., Thomson, P., Wickerson, J.: The design and implementation of a verification technique for GPU kernels. ACM Trans. Program. Lang. Syst. 37(3), 10:1–10:49 (2015). doi: 10.1145/2743017 CrossRefGoogle Scholar
  3. 3.
    Blom, S., Huisman, M., Mihelčić, M.: Specification and verification of GPGPU programs. Sci. Comput. Programm. 95(3), 376–388 (2014)CrossRefGoogle Scholar
  4. 4.
    Bobot, F., Filliâtre, J.C., Marché, C., Paskevich, A.: Why3: Shepherd Your Herd of Provers. In: Boogie 2011: 1st International Workshop on Intermediate Verification Languages, pp. 53–64. Wroclaw, Poland (2011). URL https://hal.inria.fr/hal-00790310
  5. 5.
    Bozga, M., Iosif, R.: On decidability within the arithmetic of addition and divisibility. In: Sassone, V. (ed.) Proceedings of FOSSACS 2005, Springer LNCS, vol. 3441, pp. 425–439. (2005). doi: 10.1007/978-3-540-31982-5_27
  6. 6.
    Cachera, D., Jensen, T.P., Jobin, A., Kirchner, F.: Inference of polynomial invariants for imperative programs: A farewell to Gröbner bases. Sci. Comput. Program. 93, 89–109 (2014). doi: 10.1016/j.scico.2014.02.028 CrossRefGoogle Scholar
  7. 7.
    Collingbourne, P., Cadar, C., Kelly, P.H.: Symbolic testing of OpenCL code. In: Eder, K., Lourenço, J.A., Shehory, O. (eds.) Proceedings of Hardware and Software: Verification and Testing, Springer LNCS, vol. 7261, pp. 203–218. Springer Verlag (2012). doi: 10.1007/978-3-642-34188-5_18
  8. 8.
    Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM 52(3), 365–473 (2005). doi: 10.1145/1066100.1066102 MathSciNetCrossRefMATHGoogle Scholar
  9. 9.
    Ernst, M.D., Perkins, J.H., Guo, P.J., McCamant, S., Pacheco, C., Tschantz, M.S., Xiao, C.: The daikon system for dynamic detection of likely invariants. Sci. Comput. Program. 69(1–3), 35–45 (2007). doi: 10.1016/j.scico.2007.01.015 MathSciNetCrossRefMATHGoogle Scholar
  10. 10.
    Flanagan, C., Leino, K.R.M.: Houdini, an annotation assistant for ESC/Java. In: Oliveira, J.N., Zave, P. (eds.) Proceedings of International Symposium of Formal Methods Europe (FME 2001), Springer LNCS, vol. 2021, pp. 500–517. Springer (2001). doi: 10.1007/3-540-45251-6_29
  11. 11.
    Flanagan, C., Saxe, J.B.: Avoiding exponential explosion: Generating compact verification conditions. In: Proceedings of ACM POPL, POPL ’01, pp. 193–205. ACM, New York, NY, USA (2001). doi: 10.1145/360204.360220
  12. 12.
    Garg, P., Löding, C., Madhusudan, P., Neider, D.: ICE: A robust framework for learning invariants. In: Biere, A., Bloem, R. (eds.) Proceedings of 26th International Conference on Computer Aided Verification (CAV 2014), Springer LNCS, vol. 8559, pp. 69–87. Springer (2014). doi: 10.1007/978-3-319-08867-9_5
  13. 13.
    King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385–394 (1976). doi: 10.1145/360248.360252 MathSciNetCrossRefMATHGoogle Scholar
  14. 14.
    Kojima, K., Igarashi, A.: A Hoare Logic for SIMT programs. In: Chieh Shan, C. (ed.) Proceedings of Asian Symposium on Programming Languages and Systems (APLAS 2013), Springer LNCS, vol. 8301, pp. 58–73 (2013)Google Scholar
  15. 15.
    Kojima, K., Igarashi, A.: A Hoare logic for GPU kernels. ACM Transactions on Computational Logic (2016). To appear. A revised and extended version of [14]Google Scholar
  16. 16.
    Kojima, K., Imanishi, A., Igarashi, A.: Automated verification of functional correctness of race-free GPU programs. In: Blazy, S., Chechik, M. (eds.) Verified Software. Theories, Tools, and Experiments–8th International Conference, VSTTE 2016, Toronto, ON, Canada, July 17-18, 2016, Revised Selected Papers, Lecture Notes in Computer Science, vol. 9971, pp. 90–106 (2016). doi: 10.1007/978-3-319-48869-1_7
  17. 17.
    Komuravelli, A., Bjørner, N., Gurfinkel, A., McMillan, K.L.: Compositional verification of procedural programs using Horn clauses over integers and arrays. In: Kaivola, R., Wahl, T. (eds.) Formal Methods in Computer-Aided Design, FMCAD 2015, Austin, Texas, USA, September 27-30, 2015, pp. 89–96. IEEE (2015)Google Scholar
  18. 18.
    Kovács, L., Voronkov, A.: Finding loop invariants for programs over arrays using a theorem prover. In: Chechik, M., Wirsing, M. (eds.) Fundamental Approaches to Software Engineering, Springer LNCS, vol. 5503, pp. 470–485. Springer Berlin Heidelberg (2009). doi: 10.1007/978-3-642-00593-0_33
  19. 19.
    Lechner, A., Ouaknine, J., Worrell, J.: On the complexity of linear arithmetic with divisibility. In: Proceedings of 30th Annual ACM/IEEE Symposium on Logic in Computer Science, (LICS 2015), pp. 667–676. IEEE (2015). doi: 10.1109/LICS.2015.67
  20. 20.
    Li, G., Gopalakrishnan, G.: Scalable SMT-based verification of GPU kernel functions. In: Proceedings of the 18th ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE’10), pp. 187–196. ACM (2010). doi: 10.1145/1882291.1882320
  21. 21.
    Li, G., Gopalakrishnan, G.: Parameterized verification of GPU kernel programs. In: IPDPS Workshop on Multicore and GPU Programming Models, Languages and Compilers Wokshop, pp. 2450–2459. IEEE (2012)Google Scholar
  22. 22.
    Li, G., Li, P., Sawaya, G., Gopalakrishnan, G., Ghosh, I., Rajan, S.P.: GKLEE: concolic verification and test generation for GPUs. In: Ramanujam, J., Sadayappan, P. (eds.) Proc. of ACM PPoPP, pp. 215–224. ACM (2012). doi: 10.1145/2145816.2145844
  23. 23.
    Li, P., Li, G., Gopalakrishnan, G.: Parametric flows: automated behavior equivalencing for symbolic analysis of races in CUDA programs. In: Proceedings of the International Conference on High Performance Computing, Networking, Storage and Analysis (SC’12). IEEE Computer Society Press (2012)Google Scholar
  24. 24.
    Li, P., Li, G., Gopalakrishnan, G.: Practical symbolic race checking of GPU programs. In: T. Damkroger, J. Dongarra (eds.) Proceedings of International Conference for High Performance Computing, Networking, Storage and Analysis (SC 2014), pp. 179–190. IEEE (2014). doi: 10.1109/SC.2014.20
  25. 25.
    McMillan, K.: Quantified invariant generation using an interpolating saturation prover. In: Ramakrishnan, C., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, Springer LNCS, vol. 4963, pp. 413–427. Springer Berlin Heidelberg (2008). doi: 10.1007/978-3-540-78800-3_31
  26. 26.
    Necula, G.C., McPeak, S., Rahul, S.P., Weimer, W.: CIL: intermediate language and tools for analysis and transformation of C programs. In: Proceedings of 11th International Conference on Compiler Construction (CC 2002), Springer LNCS, vol. 2304, pp. 213–228 (2002). doi: 10.1007/3-540-45937-5_16
  27. 27.
    Nguyen, H.: GPU Gems 3, first edn. Addison-Wesley Professional (2007). http://developer.nvidia.com/object/gpu-gems-3.html
  28. 28.
    NVIDIA: NVIDIA CUDA C Programming Guide (2014). URL http://docs.nvidia.com/cuda/cuda-c-programming-guide/index.html

Copyright information

© Springer Science+Business Media B.V. 2017

Authors and Affiliations

  1. 1.Graduate School of InformaticsKyoto UniversityKyotoJapan

Personalised recommendations