maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2021-4-338-355mais-1564Research ArticleTheory of ComputingПодход к автонастройке параллельных программ методом проверки моделейAutotuning Parallel Programs by Model Checkinghttps://orcid.org/0000-0001-9734-3808ГаранинаНаталья ОлеговнаGaraninaNatalia Olegovnagaranina@iis.nsk.suhttps://orcid.org/0000-0003-3857-9380ГорлачСергей ПетровичGorlatchSergei Petrovichgorlatch@uni-muenster.deИнститут систем информатики имени А. П. Ершова СО РАН;Институт автоматики и электрометрии СО РАНРоссияA.P. Ershov Institute of Informatics Systems (IIS), Siberian Branch of the Russian Academy of Sciences;Institute of Automation and Electrometry SB RASRussian FederationУниверситет МюнстераРоссияUniversity of MunsterRussian Federation202118122021284338355Copyright © Гаранина Н.О., Горлач С.П., 20212021Гаранина Н.О., Горлач С.П.Garanina N.O., Gorlatch S.P.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.mais-journal.ru/jour/article/view/1564

В этой статье представлен новый подход к автонастройке программ, параллельных по данным. Автонастройка -- это поиск оптимальных параметров настройки программы, при которых её производительность оказывается максимальной. Новизна подхода состоит в использовании метода проверки моделей для поиска оптимальных параметров настройки методом контрпримеров. В нашей работе мы абстрагируемся от конкретных программ и конкретных процессоров, задавая их представительные абстрактные шаблоны. Наш метод контрпримеров состоит в реализации следующих четырёх шагов. На первом шаге на языке инструмента проверки моделей задаётся модель исполнения абстрактной программы на абстрактном процессоре. На втором шаге на языке инструмента проверки моделей формулируем свойство оптимальности, зависящее от построенной модели. На третьем шаге подбираем оптимальные значения параметров настройки посредством использования контрпримеров, построенных в ходе верификации свойства оптимальности. На четвёртом шаге извлекаем информацию о параметрах настройки из контрпримера для оптимальных параметров. Мы применяем этот подход к автонастройке параллельных программ, написанных на языке OpenCL -- современном популярном языке, который расширяет язык C для программирования как обычных многоядерных процессоров (CPU), так и массивно-параллельных графических процессоров (GPU). В качестве инструмента верификации мы используем верификатор SPIN и его язык представления моделей Promela, формальная семантика которого позволяет моделировать исполнение параллельных программ на процессорах с различной архитектурой.

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.

задача оптимизацииавтонастройка параллельных программпараллельные программыпрограммирование GPUпроверка моделейконтрпримерыOpenCLSPINPromelaoptimization problemauto-tuning of parallel programsparallel programsGPU programmingmodel checkingcounterexamplesOpenCLSPINPromelaReferencesJ. 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.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.J. Beckingsale, O. Pearce, I. Laguna, and T. Gamblin, “Apollo: Reusable models for fast, dynamic tuning of input-dependent code,” 2017.J. Beckingsale, O. Pearce, I. Laguna, and T. Gamblin, “Apollo: Reusable models for fast, dynamic tuning of input-dependent code,” 2017.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.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.M. Christen, O. Schenk, and H. Burkhart, “PATUS: A code generation and autotuning framework for parallel iterative stencil computations on modern microarchitectures,” 2011.M. Christen, O. Schenk, and H. Burkhart, “PATUS: A code generation and autotuning framework for parallel iterative stencil computations on modern microarchitectures,” 2011.R. C. Whaley and J. J. Dongarra, “Automatically tuned linear algebra software,” 1998.R. C. Whaley and J. J. Dongarra, “Automatically tuned linear algebra software,” 1998.M. Frigo and S. G. Johnson, “The design and implementation of FFTW3,” IEEE, vol. 93(2), 2005.M. Frigo and S. G. Johnson, “The design and implementation of FFTW3,” IEEE, vol. 93(2), 2005.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.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.C. Nugteren and V. Codreanu, “CLTUne: A generic auto-tuner for OpenCL kernels,” 2015.C. Nugteren and V. Codreanu, “CLTUne: A generic auto-tuner for OpenCL kernels,” 2015.A. Rasch and S. Gorlatch, “ATF: A Generic, Directive-Based Auto-Tuning Framework,” Concurrency and Computation: Practice and Experience, vol. 31(5), 2018.A. Rasch and S. Gorlatch, “ATF: A Generic, Directive-Based Auto-Tuning Framework,” Concurrency and Computation: Practice and Experience, vol. 31(5), 2018.C. Tapus, I. H. Chung, and J. K. Hollingsworth, “Active harmony: towards automated performance tuning,” 2002.C. Tapus, I. H. Chung, and J. K. Hollingsworth, “Active harmony: towards automated performance tuning,” 2002.R. Vuduc, J. W. Demmel, and K. A. Yelick, “OSKI: A library of automatically tuned sparse matrix kernels,” 2005.R. Vuduc, J. W. Demmel, and K. A. Yelick, “OSKI: A library of automatically tuned sparse matrix kernels,” 2005.E. M. Clarke, T. A. Henzinger, H. Veith, and R. Bloem, Handbook of Model Checking. Springer International Publishing, 2018, pp. 1-13.E. M. Clarke, T. A. Henzinger, H. Veith, and R. Bloem, Handbook of Model Checking. Springer International Publishing, 2018, pp. 1-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.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.T. C. Ruys, “Optimal Scheduling Using Branch and Bound with SPIN 4.0,” 2003.T. C. Ruys, “Optimal Scheduling Using Branch and Bound with SPIN 4.0,” 2003.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.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.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.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.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.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.K. O. C. L. working group, The OpenCL Specification. Khronos OpenCL working group, 2021.K. O. C. L. working group, The OpenCL Specification. Khronos OpenCL working group, 2021.G. J. Holzmann, The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley Professional, 2003.G. J. Holzmann, The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley Professional, 2003.C. A. R. Hoare, Communicating sequential processes. Prentice-Hall, 1985.C. A. R. Hoare, Communicating sequential processes. Prentice-Hall, 1985.M. Gaspari and G. Zavattaro, “An Algebra of Actors,” 1999.M. Gaspari and G. Zavattaro, “An Algebra of Actors,” 1999.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.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.P. N. Glaskowsky, NVIDIA’s Fermi: The First Complete GPU Computing Architecture. NVIDIA Corporation, 2009.P. N. Glaskowsky, NVIDIA’s Fermi: The First Complete GPU Computing Architecture. NVIDIA Corporation, 2009.

The authors declare that there are no conflicts of interest present.