Towards Self-Verification in Finite Difference Code Generation

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.

@inproceedings{Huckelheim:2017:TSF:3145344.3145488,
 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},
}