Autotuning parallel programs by model checking

N. O. Garanina ; S. P. Gorlatch

Modelirovanie i analiz informacionnyh sistem, Tome 28 (2021) no. 4, pp. 338-355.

Résumé

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.

Détail

Keywords: optimization problem, auto-tuning of parallel programs, parallel programs, GPU programming, model checking, counterexamples, OpenCL, SPIN
Mots-clés : Promela.

Bibliographie

[1] J. Ansel, S. Kamil, K. Veeramachaneni, et al., “OpenTuner: an extensible framework for program autotuning”, Proceedings of the 23rd international conference on parallel architectures and compilation, 2014, 303–316 | DOI

[2] J. Beckingsale, O. Pearce, I. Laguna, T. Gamblin, “Apollo: reusable models for fast, dynamic tuning of input-dependent code”, Proc. of 2017 IEEE international parallel and distributed processing symposium, IPDPS, IEEE, 2017, 385–392

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

[4] M. Christen, O. Schenk, H. Burkhart, “PATUS: a code generation and autotuning framework for parallel iterative stencil computations on modern microarchitectures”, Proc. of 2011 IEEE international parallel distributed processing symposium, IEEE, 2011, 385–392

[5] R. Whaley, J. Dongarra, “Automatically tuned linear algebra software”, Proc. of the ACM/IEEE conference on supercomputing, IEEE, 1998, 385–392

[6] M. Frigo, S. G. Johnson, “The design and implementation of FFTW3”, IEEE, 93:2 (2005), 187–195 | DOI

[7] G. Fursin, Y. Kashnikov, A. Memon, et al., “Milepost GCC: machine learning enabled self-tuning compiler”, Int J Parallel Prog, 39:3 (2011), 296–327 | DOI

[8] C. Nugteren, V. Codreanu, “CLTUne: a generic auto-tuner for OpenCL kernels”, Proc. of 9th international symposium on embedded multicore/many-core systems-on-chip, IEEE, 2015, 385–392

[9] A. Rasch, S. Gorlatch, “ATF: a generic, directive-based auto-tuning framework”, Concurrency and Computation: Practice and Experience, 31:5 (2018), 296–327

[10] C. Tapus, I. Chung, J. Hollingsworth, “Active harmony: towards automated performance tuning”, Proc. of 2002 ACM/IEEE conference on supercomputing, IEEE, 2002, 385–392

[11] R. Vuduc, J. W. Demmel, K. A. Yelick, “OSKI: a library of automatically tuned sparse matrix kernels”, Proc. of scientific discovery through advanced computing conference, IEEE, 2005, 385–392

[12] E. M. Clarke, T. A. Henzinger, H. Veith, R. Bloem, “Introduction to Model Checking”, Handbook of model checking, chapter 1, Springer International Publishing, 2018, 1–13

[13] T. C. Ruys, E. Brinksma, “Experience with literate programming in the modelling and validation of systems”, Proc. of the 4th int. conf. on tools and algorithms for the construction and analysis of systems, TACAS'98, Springer, 1998, 393–-408

[14] T. Ruys, “Optimal scheduling using branch and bound with SPIN 4.0”, Proc. of model checking software, SPIN 2003, Springer, 2003, 385–392

[15] E. Brinksma, A. Mader, A. Fehnker, “Verification and optimization of a PLC control schedule”, International Journal on Software Tools for Technology Transfer, 4 (2002), 21–33 | DOI

[16] A. Wijs, J. V. D. Pol, E. M. Bortnik, “Solving scheduling problems by untimed model checking: the clinical chemical analyser case study”, Proceedings of the 10th international workshop on formal methods for industrial critical systems, 2005, 54–61 | DOI

[17] R. Malik, P. Pena, “Optimal task scheduling in a flexible manufacturing system using model checking”, IFAC-PapersOnLine, 51:7 (2018), 230–235 | DOI

[18] 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 | Zbl

[21] M. Gaspari, G. Zavattaro, “An algebra of actors”, Proc. of formal methods for open object-based distributed systems, FMOODS 1999, Springer, 1999, 385–392

[22] A. Cimatti, S. Edelkamp, M. Fox, D. Magazzeni, E. Plaku, “Automated Planning and Model Checking (Dagstuhl Seminar 14482)”, Dagstuhl Reports, 4:11 (2015), 227–245 http://drops.dagstuhl.de/opus/volltexte/2015/4973 | DOI

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