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.

翻译：本文融合了传统上彼此独立的两类研究方法：1）程序形式化验证中的模型检验，以及2）高性能计算中常用的自动调优技术。自动调优框架通过为特定高性能架构和输入数据规模寻找影响性能的关键参数（即调优参数）的最优值来优化并行程序。由于影响程序性能的参数众多，即使对专家而言，寻找最优参数配置也是一项艰巨任务。自动调优虽能自动化这一过程，但往往耗时较长。我们利用模型检验技术加速自动调优，具体通过验证程序最优性属性过程中构造的反例来实现。详细阐述了该方法在OpenCL（现代高性能架构的标准编程语言）程序中的实现流程——采用模型描述语言Promela及广泛使用的SPIN验证工具，并报告了一个应用案例的实验结果。