Preview

Моделирование и анализ информационных систем

Расширенный поиск

Подход к автонастройке параллельных программ методом проверки моделей

https://doi.org/10.18255/1818-1015-2021-4-338-355

Полный текст:

Аннотация

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


Рецензия

Для цитирования:


Гаранина Н.О., Горлач С.П. Подход к автонастройке параллельных программ методом проверки моделей. Моделирование и анализ информационных систем. 2021;28(4):338-355. https://doi.org/10.18255/1818-1015-2021-4-338-355

For citation:


Garanina N.O., Gorlatch S.P. Autotuning Parallel Programs by Model Checking. Modeling and Analysis of Information Systems. 2021;28(4):338-355. (In Russ.) https://doi.org/10.18255/1818-1015-2021-4-338-355

Просмотров: 92


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 1818-1015 (Print)
ISSN 2313-5417 (Online)