VSL Publications

Towards Self-Verification in Finite Difference Code Generation

Hückelheim, Ziqing Luo, Fabio Luporini, Navjot Kukreja, Michael Lange, Gerard Gorman, Stephen Siegel, Matthew Dwyer, and Paul Hovland. In Proceedings of the First International Workshop on Software Correctness for HPC Applications (Correctness'17) ACM, New York, NY, USA, 42-49. DOI
Code generation from domain-specific languages is becoming increasingly popular as a method to obtain optimised low-level code that performs well on a given platform and for a given problem instance. Ensuring the correctness of generated codes is crucial. At the same time, testing or manual inspection of the code is problematic, as the generated code can be complex and hard to read. Moreover, the generated code may change depending on the problem type, domain size, or target platform, making conventional code review or testing methods impractical. As a solution, we propose the integration of formal verification tools into the code generation process. We present a case study in which the CIVL verification tool is combined with the Devito finite difference framework that generates optimised stencil code for PDE solvers from symbolic equations. We show a selection of properties of the generated code that can be automatically specified and verified during the code generation process. Our approach allowed us to detect a previously unknown bug in the Devito code generation tool.
  1. Download from ACM library
Related Links
  1. Github page
 author = {Hückelheim, Jan and Luo, Ziqing and Luporini, Fabio and Kukreja, Navjot and Lange, Michael and Gorman, Gerard and Siegel, Stephen and Dwyer, Matthew and Hovland, Paul},
 title = {{T}owards {S}elf-{V}erification in {F}inite {D}ifference {C}ode {G}eneration},
 booktitle = {Proceedings of the First International Workshop on Software Correctness for HPC Applications},
 series = {Correctness'17},
 year = {2017},
 isbn = {978-1-4503-5127-0},
 location = {Denver, CO, USA},
 pages = {42--49},
 numpages = {8},
 url = {http://doi.acm.org/10.1145/3145344.3145488},
 doi = {10.1145/3145344.3145488},
 acmid = {3145488},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {Code generation, Equivalence checking, Formal methods, HPC, Specification, Symbolic execution, Verification},

VSL | Publications