Towards Self-Verification in Finite Difference Code
Generation
Author/Presenters
Event Type
Workshop
Applications
Correctness
Debugging
Reliability
SIGHPC Workshop
Verification
TimeSunday, November 12th12:12pm -
12:29pm
Location501
DescriptionCode 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.
Author/Presenters
