Staroletov17mar26

Докладчик: Сергей Михайлович Старолетов (Институт Автоматики и Электрометрии и АлтГУ) Тема: Формальное моделирование различных архитектур графических конвейеров в SPIN Аннотация: В этом докладе представлена формальная модель графического конвейера GPU, реализованная на языке моделирования Promela, для возможной будущей верификации с помощью средства проверки моделей SPIN. Будет представлен анализ исторических графических архитектур. Модель осуществляет реальный 3D рендеринг в целочисленных координатах, абстрагирует ключевые этапы конвейера — выборку вершин, обработку шейдеров, растеризацию, текстурирование и пиксельные операции как параллельные процессы, синхронизированные через буферизованные каналы и семафоры. Модель может служить основой для сравнения графических архитектур, демонстрации в учебных целях и формальной проверки корректности конвейера.