RUS  ENG
Полная версия
ЖУРНАЛЫ // Моделирование и анализ информационных систем // Архив

Модел. и анализ информ. систем, 2021, том 28, номер 4, страницы 338–355 (Mi mais756)

Эта публикация цитируется в 1 статье

Theory of computing

Autotuning parallel programs by model checking

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

N. O. Garaninaab, S. P. Gorlatchc

a A.P. Ershov Institute of Informatics Systems (IIS), Siberian Branch of the Russian Academy of Sciences, 6 Acad. Lavrentjev pr., Novosibirsk 630090, Russia
b Institute of Automation and Electrometry SB RAS, 1, Academician Koptyug ave., Novosibirsk 630090, Russia
c University of Munster, 62 Einsteinstr, Muenster 48149, Germany

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

Ключевые слова: задача оптимизации, автонастройка параллельных программ, параллельные программы, программирование GPU, проверка моделей, контрпримеры, OpenCL, SPIN, Promela.

УДК: 004.822, 681.51

MSC: 68W10

Поступила в редакцию: 15.11.2021

Язык публикации: английский

DOI: 10.18255/1818-1015-2021-4-338-355



© МИАН, 2024