Управляющие системы и машины, №4, 2018, статья 4
DOI: https://doi.org/10.15407/usim.2018.04.046
Погорілий С.Д., Кривий С.Л., Слинько М.С. Проектування та модельне обґрунтування застосувань на основі відеоадаптерів. Управляющие системы и машины. 2018. № 4. С. 46-56.
УДК 004.4
Погорелый Сергей Демьянович, доктор технических наук, профессор, заведующий кафедрой компьютерной инженерии факультета радиофизики, электроники и компьютерных систем Киевского национального университета имени Тараса Шевченко, E-mail: sdp@univ.net.ua, ORCID ID — http : //orcid.org/0000-0003-4231-0691,
Кривой Сергей Лукьянович, доктор физико-математических наук, профессор факультета компьютерных наук и кибернетики Киевского национального университета имени Тараса Шевченко, E-mail: sl.krivoi@gmail.com, ORCID ID — http://orcid.org/ 0000-0003-4231-0691,
Слинько Максим Сергеевич, аспирант 3-го года обучения факультета радиофизики, электроники и компьютерных систем Киевского национального университета имени Тараса Шевченко, E-mail: maxim.slinko@gmail.com, ORCID ID — http://orcid.org/0000 -0001-9667-8729.
Модельное обоснование приложений на основе видеоадаптеров
Введение. В настоящее время тенденции в области высокопроизводительных вычислений (HPC) смещаются от использования кластерных систем, состоящих из модулей общего назначения к более специализированным компонентам-акселераторам (GPU, FPGA и т.д.). Создание систем высокого уровня сложности с массовым параллелизмом на основе GPU-акселераторов требует разработки новых научно обоснованных методов проектирования и верификации приложений.
Цель. Презентация нового метода создания приложений с использованием видеоадаптеров, основанного на модельном проектировании.
Методы. Предложен метод проектирования и верификации приложений, который позволяет создавать абстракции различных уровней, используя аппарат размеченных транзиционных систем, композиции которых могут транслироваться в сети Петри и исследоваться средствами СП. Предложенный метод позволяет исследовать свойства системы, анализ которых в ручном режиме невозможен, так как количество потоков, выделяемых для решения задачи, измеряется сотнями тысяч (в архитектурах Pascal / Volta).
Результат. С помощью аппарата транзицийних систем удалось получить формализованную спецификацию анализируемой системы. Благодаря ее представлению сетью Петри проведен анализ модели на наличие дедлоков и ловушек, а также на отсутствие мертвых переходов и мест. Получены множества базисных и минимальных дедлоков и ловушек, показано, что каждый дедлок включает в себя по меньшей мере одну из ловушек, то есть полученная модель является живой.
Выводы. Предложенный метод позволяет формировать модели разного уровня абстракции и выполнять дальнейшую верификацию автоматизированными средствами. Представлены возможности исследования характеристик модели, созданной при помощи аппаратов транзиционных систем и сетей Петри. Созданный подход позволяет упростить и сократить процессы верификации и тестирования многопоточных приложений в компьютерных системах с видеоадаптерами.
Загрузитьполный текст в формате PDF (на украинском).
Ключевые слова: транзицийна система, Nvidia CUDA, сети Петри, модельное проектирования.
Поступила 26.11.2018
