Autotuning Parallel Programs by Model Checking

The paper presents a new approach to autotuning data-parallel programs. Autotuning is a search for optimal program settings which maximize its performance. The novelty of the approach lies in the use of the model checking method to find the optimal tuning parameters by the method of counterexamples. In our work, we abstract from specific programs and specific processors by defining their representative abstract patterns. Our method of counterexamples implements the following four steps. At the first step, an execution model of an abstract program on an abstract processor is described in the language of a model checking tool. At the second step, in the language of the model checking tool, we formulate the optimality property that depends on the constructed model. At the third step, we find the optimal values of the tuning parameters by using a counterexample constructed during the verification of the optimality property. In the fourth step, we extract the information about the tuning parameters from the counter-example for the optimal parameters. We apply this approach to autotuning parallel programs written in OpenCL, a popular modern language that extends the C language for programming both standard multi-core processors (CPUs) and massively parallel graphics processing units (GPUs). As a verification tool, we use the SPIN verifier and its model representation language Promela, whose formal semantics is good for modelling the execution of parallel programs on processors with different architectures.

optimization problem, auto-tuning of parallel programs, parallel programs, GPU programming, model checking, counterexamples, OpenCL, SPIN, Promela

1. J. Ansel, S. Kamil, K. Veeramachaneni, and et al., “OpenTuner: An extensible framework for program autotuning,” in Proceedings of the 23rd international conference on Parallel architectures and compilation, 2014, pp. 303-316.

2. J. Beckingsale, O. Pearce, I. Laguna, and T. Gamblin, “Apollo: Reusable models for fast, dynamic tuning of input-dependent code,” 2017.

3. C. Chen, J. Chame, and M. Hall, “CHILL: A framework for composing high-level loop transformations,” Technical Report 08-897. Los Angeles, CA, pp. 136-150, 2008.

4. M. Christen, O. Schenk, and H. Burkhart, “PATUS: A code generation and autotuning framework for parallel iterative stencil computations on modern microarchitectures,” 2011.

5. R. C. Whaley and J. J. Dongarra, “Automatically tuned linear algebra software,” 1998.

6. M. Frigo and S. G. Johnson, “The design and implementation of FFTW3,” IEEE, vol. 93(2), 2005.

7. G. Fursin, Y. Kashnikov, A. W. Memon, and et al., “Milepost GCC: machine learning enabled self-tuning compiler,” Int J Parallel Prog, vol. 39(3), pp. 296-327, 2011.

8. C. Nugteren and V. Codreanu, “CLTUne: A generic auto-tuner for OpenCL kernels,” 2015.

9. A. Rasch and S. Gorlatch, “ATF: A Generic, Directive-Based Auto-Tuning Framework,” Concurrency and Computation: Practice and Experience, vol. 31(5), 2018.

10. C. Tapus, I. H. Chung, and J. K. Hollingsworth, “Active harmony: towards automated performance tuning,” 2002.

11. R. Vuduc, J. W. Demmel, and K. A. Yelick, “OSKI: A library of automatically tuned sparse matrix kernels,” 2005.

12. E. M. Clarke, T. A. Henzinger, H. Veith, and R. Bloem, Handbook of Model Checking. Springer International Publishing, 2018, pp. 1-13.

13. T. C. Ruys and E. Brinksma, “Experience with Literate Programming in the Modelling and Validation of Systems,” in Proc. of the 4th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’98), 1998, pp. 393-408.

14. T. C. Ruys, “Optimal Scheduling Using Branch and Bound with SPIN 4.0,” 2003.

15. E. Brinksma, A. Mader, and A. Fehnker, “Verification and optimization of a PLC control schedule,” International Journal on Software Tools for Technology Transfer, vol. 4, pp. 21-33, 2002.

16. A. Wijs, J. V. D. Pol, and E. M. Bortnik, “Solving scheduling problems by untimed model checking: The clinical chemical analyser case study.,” in Proceedings of the 10th international workshop on Formal methods for industrial critical systems, 2005, pp. 54-61.

17. R. Malik and P. N. Pena, “Optimal Task Scheduling in a Flexible Manufacturing System using Model Checking,” IFAC-PapersOnLine, vol. 51, no. 7, pp. 230-235, 2018.

18. K. O. C. L. working group, The OpenCL Specification. Khronos OpenCL working group, 2021.

19. G. J. Holzmann, The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley Professional, 2003.

20. C. A. R. Hoare, Communicating sequential processes. Prentice-Hall, 1985.

21. M. Gaspari and G. Zavattaro, “An Algebra of Actors,” 1999.

22. A. Cimatti, S. Edelkamp, M. Fox, D. Magazzeni, and E. Plaku, “Automated Planning and Model Checking (Dagstuhl Seminar 14482),” Dagstuhl Reports, vol. 4, no. 11, pp. 227-245, 2015, doi: 10.4230/DagRep.4.11.227.

23. P. N. Glaskowsky, NVIDIA’s Fermi: The First Complete GPU Computing Architecture. NVIDIA Corporation, 2009.