Суперкомпиляция: современное состояние

[ushastyi]

Неожиданно, комментируя статью _darkus_ по архитектуре СППР, посмотрел другие материалы "Записок программиста" и увидел подкаст с Ильей Ключниковым о суперкомпиляции. Несколько лет назад я вкратце рассказывал, что это такое. Но в подкасте Илья это раскрывает все гораздо более подробно, включая основные направления исследований, результаты и приложения

Comments

[igor_abramov]

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

Я такую штуку для Борланда лет 10 назад ваял, на уровне proof-of-concept оно вполне лихо работало, как раз для Java.

[ushastyi]

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

"Функциональные игрища" -- это не самоцель, а средство. Структура функциональных программ позволяет их анализировать проще, чем императивные и пр.

А как это делается через SSA, объясните поподробнее?

Кстати, если верить википедии, то в HotSpot используется SSA. А ему больше 10 лет.

[igor_abramov]

Некотором смысле анализ потоков данных тоже может находить много чего. Это, собственно, основная техника, лежащая в современных оптимизаторах и статических анализаторах кода

[ushastyi]

А под "мы определяем некую решетку" -- кто имеется ввиду под "мы"?

В суперкомпиляции, насколько я понимаю, никто ничего не определяет. Прогонка происходят на всех возможных значениях данных. Если есть некоторые свойства, те же инварианты, то они получаются "как бы" автоматически (ну или доказываются).

Но возможно, я недостаточно это все понимаю. Попробуйте спросить Илью на eax.me. Он отвечал там на вопросы. Регистрация простая.

[igor_abramov]

Решетку приходится определять под конкретную задачу.

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

1) маски битов, которые точно 0 и точно 1,
2) верхнюю и нижнюю оценки на значение величины

Если же анализатор предназначен, например, для нахождения проблем в драйверах Линукса, то там анализируется, в частности, тип адреса (на какое адресное пространство он указывает - пользовательское или системное), или значение такого неявного параметра кмк текущий уровень прерываний (позволяет находить ситуации, когда при возникновении ошибки устройства драйвер не восстанавливает исходный уровень прерываний).

То есть, надеяться, что такие штуки будут вычисляться "сами" как-то не приходится.

[ushastyi]

И тем не менее, некоторые штуки могут сами вычисляться. Суперкомпиляция теоретически позволяет "проверить" программу на всех возможных входных данных. Никакой тест это не покроет. В подкасте, кстати, есть про использование суперкомпиляции для верификации протоколов. Что уже недалеко от драйверов.

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

А вы сейчас где работаете и чем занимаетесь?

[igor_abramov]

>>> Суперкомпиляция теоретически позволяет "проверить" программу на всех возможных входных данных

[ushastyi]

>>> >>> Суперкомпиляция теоретически позволяет "проверить" программу на всех возможных входных данных