JetBrains Research — наука, меняющая мир

Семинар по насыщению равенствами

Оптимизирующий компилятор при обработке программы последовательно применяет десятки индивидуальных оптимизаций, при этом порядок их применения оказывает существенное влияние на результат компиляции. Некоторые оптимизации могут отменять улучшение от одних оптимизаций и делать невозможным применение других. В общем случае нет возможности найти порядок оптимизаций, который для любой программы гарантирует наилучший результат. Техника насыщения равенствами решает эту проблему за счет недеструктивного применения всех возможных оптимизаций до тех пор, пока не будет достигнуто насыщение: их применение перестанет давать новые результаты. Из всех возможных программ, полученных таким образом, при помощи решателя выбирается глобально оптимальный. Помимо оптимизаций насыщение равенствами также позволяет проверять корректность преобразований программ.

Материалы к докладу:

Ross Tate, Michael Stepp, Zachary Tatlock, and Sorin Lerner. Equality saturation: a new approach to optimization. SIGPLAN Not. 44, 1 (January 2009) (https://dl.acm.org/citation.cfm?id=1480915)

Гречаник С.А. Доказательство свойств функциональных программ методом насыщения равенствами. Диссерация на соискание степени к.ф-м.н., Институт прикладной математики им. Келдыша РАН (http://www.keldysh.ru/council/1/2017-grechanik/diss.pdf)

Докладчик: Екатерина Вербицкая

25.03.2019, 17:15.

Место: ауд. 3248, мат-мех. факультет СПбГУ, Старый Петергоф, Университетский пр-т, д. 28