Advertisement

Mostly Automated Formal Verification of Loop Dependencies with Applications to Distributed Stencil Algorithms

Article
  • 11 Downloads

Abstract

The class of stencil programs involves repeatedly updating elements of arrays according to fixed patterns, referred to as stencils. Stencil problems are ubiquitous in scientific computing and are used as an ingredient to solve more involved problems. Their high regularity allows massive parallelization. Two important challenges in designing such algorithms are cache efficiency and minimizing the number of communication steps between nodes. In this paper, we introduce a mathematical framework for a crucial aspect of formal verification of both sequential and distributed stencil algorithms, and we describe its Coq implementation. We present a domain-specific embedded programming language with support for automating the most tedious steps of proofs that nested loops respect dependencies, applicable to sequential and distributed examples. Finally, we evaluate the robustness of our library by proving the dependency-correctness of some real-world stencil algorithms, including a state-of-the-art cache-oblivious sequential algorithm, as well as two optimized distributed kernels.

Keywords

Formal software verification Automated software verification Stencil algorithm Distributed stencil algorithms Loop dependencies 

Notes

Acknowledgements

This work was supported in part by the U.S. Department of Energy, Office of Science, Advanced Scientific Computing Research Program, under Award Number DE-SC0008923; and by National Science Foundation Grant CCF-1253229. We also thank Shoaib Kamil for feedback on this paper.

References

  1. 1.
    Betts, A., Chong, N., Donaldson, A., Qadeer, S., Thomson, P.: GPUVerify: a verifier for GPU kernels. In: Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications, pp. 113–132. ACM (2012)Google Scholar
  2. 2.
    Boldo, S., Clément, F., Filliâtre, J.C., Mayero, M., Melquiond, G., Weis, P.: Formal proof of a wave equation resolution scheme: the method error. In: Interactive Theorem Proving, pp. 147–162. Springer (2010)Google Scholar
  3. 3.
    Boldo, S., Clément, F., Filliâtre, J.C., Mayero, M., Melquiond, G., Weis, P.: Wave equation numerical resolution: a comprehensive mechanized proof of a C program. J. Autom. Reason. 50(4), 423–456 (2013)MathSciNetCrossRefMATHGoogle Scholar
  4. 4.
    Cachera, D., Pichardie, D.: Embedding of systems of affine recurrence equations in Coq. In: TPHOLs, pp. 155–170. Springer (2003)Google Scholar
  5. 5.
    Epperson, J.F.: An Introduction to Numerical Methods and Analysis. Wiley, Hoboken (2014)MATHGoogle Scholar
  6. 6.
    Feautrier, P.: Automatic parallelization in the polytope model. In: Perrin, G.-R., Darte, A. (eds.) The Data Parallel Programming Model, pp. 79–103. Springer, Berlin (1996)CrossRefGoogle Scholar
  7. 7.
    Frigo, M., Strumpen, V.: Cache oblivious stencil computations. In: Proceedings of the 19th Annual International Conference on Supercomputing, pp. 361–366. ACM (2005)Google Scholar
  8. 8.
    Frigo, M., Strumpen, V.: The cache complexity of multithreaded cache oblivious algorithms. Theory Comput. Syst. 45(2), 203–233 (2009)MathSciNetCrossRefMATHGoogle Scholar
  9. 9.
    Gardner, M.: Mathematical games—the fantastic combinations of John Conway’s new solitaire game “Life”. Sci. Am. 223(4), 120–123 (1970)CrossRefGoogle Scholar
  10. 10.
    Grégoire, T., Chlipala, A.: Mostly automated formal verification of loop dependencies with applications to distributed stencil algorithms. In: International Conference on Interactive Theorem Proving, pp. 167–183. Springer (2016)Google Scholar
  11. 11.
    Immler, F., Hölzl, J.: Numerical analysis of ordinary differential equations in Isabelle/HOL. In: Beringer, L., Felty, A. (eds.) Interactive Theorem Proving, pp. 377–392. Springer, Berlin (2012)CrossRefGoogle Scholar
  12. 12.
    Kelly, W., Pugh, W.: Unifying framework for iteration reordering transformations. In: Proceedings of IEEE First International Conference on Algorithms and Architectures for Parallel Processing, vol. 1, pp. 153–162 (1995)Google Scholar
  13. 13.
    LeVeque, R.J.: Finite Difference Methods for Ordinary and Partial Differential Equations: Steady-State and Time-Dependent Problems, vol. 98. SIAM, Philadelphia (2007)CrossRefMATHGoogle Scholar
  14. 14.
    Li, G., Gopalakrishnan, G.: Scalable SMT-based verification of GPU kernel functions. In: Proceedings of the Eighteenth ACM SIGSOFT International Symposium on Foundations of Software Engineering, pp. 187–196. ACM (2010)Google Scholar
  15. 15.
    Li, G., Li, P., Sawaya, G., Gopalakrishnan, G., Ghosh, I., Rajan, S.P.: GKLEE: concolic verification and test generation for GPUs. In: PPOPP, pp. 215–224 (2012)Google Scholar
  16. 16.
    Loechner, V.: PolyLib: A library for manipulating parameterized polyhedra. http://camlunity.ru/swap/Library/Conflux/Techniques%20-%20Code%20Analysis%20and%20Transformations%20(Polyhedral)/Free%20Libraries/polylib.ps. Accessed 10 Feb 2018.
  17. 17.
    Maydan, D., Hennessy, J., Lam, M.: Efficient and exact data dependence analysis. In: Proceedings of the ACM SIGPLAN’91 Conference on Programming Language Design and Implementation (1991)Google Scholar
  18. 18.
    Orchard, D., Mycroft, A.: Efficient and correct stencil computation via pattern matching and static typing. arXiv preprint: arXiv:1109.0777 (2011)
  19. 19.
    Pugh, W.: The Omega test: a fast and practical integer programming algorithm for dependence analysis. In: Proceedings of the 1991 ACM/IEEE Conference on Supercomputing, pp. 4–13. ACM (1991)Google Scholar
  20. 20.
    Solar-Lezama, A., Arnold, G., Tancau, L., Bodik, R., Saraswat, V., Seshia, S.: Sketching stencils. In: Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 167–178. ACM (2007)Google Scholar
  21. 21.
    Tang, Y., Chowdhury, R.A., Kuszmaul, B.C., Luk, C.K., Leiserson, C.E.: The Pochoir stencil compiler. In: Proceedings of the Twenty-Third Annual ACM Symposium on Parallelism in Algorithms and Architectures, pp. 117–128. ACM (2011)Google Scholar
  22. 22.
    Valiant, L.G.: A bridging model for parallel computation. Commun. ACM 33(8), 103–111 (1990)CrossRefGoogle Scholar
  23. 23.
    Xu, Z., Kamil, S., Solar-Lezama, A.: MSL: a synthesis enabled language for distributed implementations. In: Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis, pp. 311–322. IEEE Press (2014)Google Scholar

Copyright information

© Springer Science+Business Media B.V., part of Springer Nature 2018

Authors and Affiliations

  1. 1.ÉNS LyonLyonFrance
  2. 2.MIT CSAILCambridgeUSA

Personalised recommendations