Using the Spin Model Checker for Auto-Tuning High-Performance Programs

The paper bridges two traditionally separate research directions: (1) model checking, commonly used in the formal verification of programs, and (2) auto-tuning, frequently applied in high-performance computing. Auto-tuning frameworks optimize parallel programs by identifying the optimal values of performance-critical parameters—known as tuning parameters—for specific high-performance architectures and data sizes. Given the large number of parameters affecting a program’s performance, determining the optimal configuration is a challenging task, even for experts. Although auto-tuning automates this process, it is often time-intensive. We accelerate auto-tuning by applying model checking, utilizing a counterexample generated during the verification of the program’s optimality property. This paper provides a detailed implementation of our approach for OpenCL programs—a standard for programming modern high-performance architectures—using the Promela modeling language and the SPIN verification tool, along with a report on our experimental results.