Joint Department with the RAS Institute for System Programming

Regular version of the site

Publications

Book

ECPPM 2021 – eWork and eBusiness in Architecture, Engineering and Construction

Edited by: Vitaly Semenov, R. J. Scherer.

CRC Press, 2021.

Article

Equivalence checking and intersection of deterministic timed finite state machines

Bresolin D., El-Fakih K., Villa T. et al.

Formal Methods in System Design. 2022.

Book chapter

City and building information modelling using IFC standard

Shutkin V., Morozkin N., Zolotov V. et al.

In bk.: ECPPM 2021 – eWork and eBusiness in Architecture, Engineering and Construction. CRC Press, 2021. P. 406-413.

Working paper

Preventive Model-based Verification and Repairing for SDN Requests

Burdonov I., Kossachev A., Nina Yevtushenko et al.

arxiv.org. Computer Science. Cornell University, 2020

All publications

Delivered by:: Joint Department with the RAS Institute for System Programming

Type:: Elective course

When:: 3 year, 3, 4 module

Instructors

Gaysaryan, Sergey S.

Мельник Дмитрий Михайлович

Полная версия программы учебной дисциплины

Аннотация

В результате освоения дисциплины студенты изучат основы построения оптимизирующих статических и динамических компиляторов современных языков программирования, учитывающих особенности архитектур современных компьютеров, ознакомятся с предметом и основными подходами к формальной спецификации и верификации программ.

Цель освоения дисциплины

освоение студентами базовых знаний в области оптимизирующей компиляции программ
приобретение теоретических знаний в области теории графов, теории решеток, методов сбора статистики, используемых при разработке методов анализа и трансформации программ
оказание консультаций и помощи студентам в проведении собственных исследований и разработок в областях, использующих компиляторные технологии
приобретение навыков работы на современных неоднородных распределенных компьютерных системах
освоение студентами базовых современных достижений формальных методов в разработке программного обеспечения для критических по безопасности систем
формирование практических навыков применения формальных методов при проектировании и разработке программного обеспечения

Содержание учебной дисциплины

Структура оптимизирующего компилятора. Промежуточные представления компилируемой программы. Локальная оптимизация. Метод нумерации значений.
Вычисление достигающих определений и живых переменных с помощью анализа потока данных по графу потока управления
Доказательство сходимости итерационных методов анализа потока управления.
Простейшие методы глобальной оптимизации процедуры: сворачивание констант, распространение копий, обнаружение недостижимого кода и т.п.
Методы оптимизации циклов и гнезд циклов: выявление естественных циклов, вынесение в предзаголовок цикла инвариантных вычислений, анализ индуктивных переменных
Распространение констант
Построение частично-усеченной SSA-формы
Выделение областей в ГПУ. Передаточные функции областей.
Открытая вставка процедур и межпроцедурный анализ (обзор)
Введение в теорию решеток. Построение полурешеток для различных видов анализа потока данных. Понятие передаточной функции. Монотонные и дистрибутивные передаточные функции и их свойства.
Генерация низкоуровневого кода методом переписывания дерева.
Распределение регистров
Планирование кода
Обеспечение локальности данных и оптимизация передач управления
Конвейеризация циклов
Параллельное выполнение циклов.

Элементы контроля

Контрольные работы
Экзамен

Промежуточная аттестация

2021/2022 учебный год 4 модуль
Итог = По модулю 10 ( Среднее (КР) + Экзамен)

Contacts

Compiler Technology

Instructors

Программа дисциплины

Аннотация

Цель освоения дисциплины

Содержание учебной дисциплины

Элементы контроля

Промежуточная аттестация

Список литературы

Рекомендуемая основная литература