The paper combines research approaches that traditionally have been disjoint: 1) model checking as used in formal verification of programs, and 2) auto-tuning as often used in high-performance computing. Auto-tuning frameworks optimize parallel programs by finding the optimal values of the performance-critical parameters -- so-called tuning parameters -- for a particular high-performance architecture and input data size. As there are many parameters influencing program's performance, finding the optimal parameter configuration is a hardly manageable task even for experts. Auto-tuning automates this process, but it is often time-consuming. We apply model checking for accelerating auto-tuning by using a counterexample constructed during the verification of the optimality property of the program. We describe in detail an implementation of our approach for programs written in OpenCL -- the standard for programming modern high-performance architectures -- using the model representation language Promela and the popular SPIN verification tool, and we report experimental results for an application use case.
@article{arxiv.2305.09130,
title = {Auto-Tuning High-Performance Programs Using Model Checking in Promela},
author = {Natalia Garanina and Sergey Staroletov and Sergei Gorlatch},
journal= {arXiv preprint arXiv:2305.09130},
year = {2023}
}