使用 Promela 模型检测实现高性能程序自动调优

本文将传统上互不相交的研究方法相结合：1) 用于程序形式化验证的模型检测，以及 2) 高性能计算中常用的自动调优。自动调优框架通过为特定高性能架构和输入数据规模寻找性能关键参数（即所谓调优参数）的最优值来优化并行程序。由于影响程序性能的参数众多，即使对专家而言，寻找最优参数配置也是一项难以管理的任务。自动调优使该过程自动化，但往往耗时较长。我们应用模型检测，利用在程序最优性属性验证过程中构造的反例来加速自动调优。我们详细描述了针对用 OpenCL（编程现代高性能架构的标准）编写的程序所实现的方法，使用模型表示语言 Promela 和流行的 SPIN 验证工具，并报告了一个应用用例的实验结果。