Суперкомпиляция: современное состояние
Sep. 30th, 2014 06:22 pm![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
kaipaНеожиданно, комментируя статью ![[livejournal.com profile]](https://www.dreamwidth.org/img/external/lj-userinfo.gif)
_darkus_ по архитектуре СППР, посмотрел другие материалы "Записок программиста" и увидел подкаст с Ильей Ключниковым о суперкомпиляции. Несколько лет назад я вкратце рассказывал, что это такое. Но в подкасте Илья это раскрывает все гораздо более подробно, включая основные направления исследований, результаты и приложения.
Любопытно, что подкаст опубликован 12го сентября, примерно в то же время, когда мы с ним сидели на одном пляже на Майорке, но там поговорить о суперкомпиляции получилось от силы минут пять.
_darkus_ по архитектуре СППР, посмотрел другие материалы "Записок программиста" и увидел подкаст с Ильей Ключниковым о суперкомпиляции. Несколько лет назад я вкратце рассказывал, что это такое. Но в подкасте Илья это раскрывает все гораздо более подробно, включая основные направления исследований, результаты и приложения. Любопытно, что подкаст опубликован 12го сентября, примерно в то же время, когда мы с ним сидели на одном пляже на Майорке, но там поговорить о суперкомпиляции получилось от силы минут пять.
![[identity profile]](https://www.dreamwidth.org/img/silk/identity/openid.png){kind=small}
no subject
Date: 2014-09-30 07:14 pm (UTC)Я такую штуку для Борланда лет 10 назад ваял, на уровне proof-of-concept оно вполне лихо работало, как раз для Java.
no subject
Date: 2014-09-30 08:22 pm (UTC)"Функциональные игрища" -- это не самоцель, а средство. Структура функциональных программ позволяет их анализировать проще, чем императивные и пр.
А как это делается через SSA, объясните поподробнее?
Кстати, если верить википедии, то в HotSpot используется SSA. А ему больше 10 лет.
no subject
Date: 2014-09-30 08:51 pm (UTC)Подход элементарный, на базовом уровне внятно описан в Книге Дракона. Строим ориентированный граф, вершины его аргументы и результат[ы] операторов программы. Стрелка идет либо от определения к использованию (прямой анализ) либо наоборот (обратный). Далее, мы определяем некую решетку (часто и полурешетки хватает) которая описывает наши знания о данных (может варьироваться от простой булевой решетки описывающей состояния конечного множества до весьма изощренных структур). Для ситуации когда две стрелки сходятся в одной точки оцениваем значения максимальным/минимальным элементов.
Операторы у нас описываются в терминах перобразования значений.
В итоге получается система уравнений, которую, можно решить. Если повезет, за приемлемое время. Любымый способ --- метод итераций, а SSA/SSI очень хорошо влияет на сходимость.
Этим техникам уже много лет, они неплохо развились и давно и активно используются на практике. У нас подобные вещи относили к "Теории схем программ", но там теория чуть более отвлеченная от практики.
no subject
Date: 2014-09-30 09:22 pm (UTC)В суперкомпиляции, насколько я понимаю, никто ничего не определяет. Прогонка происходят на всех возможных значениях данных. Если есть некоторые свойства, те же инварианты, то они получаются "как бы" автоматически (ну или доказываются).
Но возможно, я недостаточно это все понимаю. Попробуйте спросить Илью на eax.me. Он отвечал там на вопросы. Регистрация простая.
no subject
Date: 2014-10-01 06:19 am (UTC)В простом случае, например, при анализе в целях дальнейшей оптимизации кода, мы используем что-то навроде следующего набора признаков:
1) маски битов, которые точно 0 и точно 1,
2) верхнюю и нижнюю оценки на значение величины
Если же анализатор предназначен, например, для нахождения проблем в драйверах Линукса, то там анализируется, в частности, тип адреса (на какое адресное пространство он указывает - пользовательское или системное), или значение такого неявного параметра кмк текущий уровень прерываний (позволяет находить ситуации, когда при возникновении ошибки устройства драйвер не восстанавливает исходный уровень прерываний).
То есть, надеяться, что такие штуки будут вычисляться "сами" как-то не приходится.
no subject
Date: 2014-10-01 10:25 am (UTC)Формальная верификация программ тоже теоретически возможна, и проблема, насколько я понимаю, состоит во-первых, в сложности, а во-вторых, что нужно на чем-нибудь описать как программа должна работать правильно, а это порой так же сложно, как написать саму программу.
А вы сейчас где работаете и чем занимаетесь?
no subject
Date: 2014-10-01 11:49 am (UTC)Наверное, это слишком сильное утверждение, тем более для слова "теоретически". Как раз теоретически достижимость некого участка программы можно свести к проблеме останова, которая алгоритмически неразрешима.
На самом деле, если модель множества возможных значений некой переменной точная (может представить любое множество значений), такие вычисления (любым методом) потребуют нереальных ресурсов (просто из соображений необходимых объемов данных). Поэтому, представление множеств приходится сильно загрублять, притом под конкретную задачу.
Так что, осмелюсь наивно предположить, что реальные суперкомпиляторы тоже весьма компромиссны в этом смысле.
>>> Суперкомпиляция теоретически позволяет "проверить" программу на всех возможных входных данных. Никакой тест это не покроет.
Статические анализаторы присутствуют на рынке уже лет 20 минимум и решают именно эту задачу. Насколько я знаю, решают методами анализа потока данных (конечно, они находят еще множество мелких несообразностей в коде более простыми способами).
>>> Формальная верификация программ тоже теоретически возможна,
опять же с неслабыми оговорками, но да, основная проблема в спецификации. Ее сложно писать, непонятно как отлаживать и верифицировать саму спецификацию. Так что не панацея.
В ИСП РАН этим занимались и даже применяли для практических промышленных систем.
>>> А вы сейчас где работаете и чем занимаетесь?
анализаторами кода не занимаюсь, спрос в промышленности невелик на самом деле.
А занимаюсь двумя вещами: эмуляторами устаревающих систем (в том числе, динамической бинарной трансляцией) для Stromasys, и системой торговли в реальном времени на бирже рекламных объявлений (стартап, пока undisclosed).
no subject
Date: 2014-10-02 02:12 pm (UTC)>>> Наверное, это слишком сильное утверждение, тем более для слова "теоретически". Как раз теоретически достижимость некого участка программы можно свести к проблеме останова, которая алгоритмически неразрешима.
Да, это одна из проблем, которые существуют при суперкомпиляции, В процессе построения модели программы (граф с циклами), существуют специальные ухищрения и алгоритмы для распознавания циклов (см, например, тут: http://window.edu.ru/library/pdf2txt/721/41721/18879/page2)
В любом случае, прогонка на данных производится после этапа преобразования программы во внутреннее мета-представление. То есть проблема останова обходится до проверки программы на данных.
Но это все теория, "реальные суперкомпиляторы" пока что по большей части модельные примеры, чем что-то реально рабочее.
Статический анализ кода, насколько я понимаю, решает все же несколько другую задачу.
Давайте я повторюсь, может быть. Я не специалист по суперкомпиляции, такие вопросы лучше Илье задавать. Но из того, что я понимаю, это метод, который позволяет общим образом решить разные задачи, в том числе те, которые могут быть, и решаются сейчас другими узкоспециализированными способами.
> и системой торговли в реальном времени на бирже рекламных объявлений (стартап, пока undisclosed).
А, RTB… Мы тоже этим занимаемся. Деньги из воздуха.
no subject
Date: 2014-10-02 03:19 pm (UTC)Да именно ту же самую. И теория этого анализа формулируется именно в терминах абстрактного исполнения схемы программ. И циклы там теми же способами выявляются, что неудивительно. Просто разработчики статических анализаторов идут от продукта и более скромны в своих мечтаниях :). Вообще, меня начинают терзать смутные сомнения что, по-существу, это один и тот же аппарат, только терминология немного разная.
Лет 25 с лишним назад, на мехматовском семинаре выступал Романенко и его там немного и по-дружески троллили, в основном за оптимизм. Ну а я столкнулся с этой тематикой лет 10 назад, когда делал анализатор для Борланда.
>>> А, RTB… Мы тоже этим занимаемся. Деньги из воздуха.
Тесен мир. Деньги-то из воздуха, а вот математика хорошая, пришлось вспомнить даже то, чего не изучал :) Ну и попрограммировать есть чего.
no subject
Date: 2014-10-02 03:31 pm (UTC)Лет 25 назад может быть. Судя по всему существенный прогресс пошел в последние лет десять, причем не последнюю роль сыграло в этом второе пришествие функциональных языков, с которыми легко работать. Поживем-увидим ,)
В самом RTB математики, по-моему, нет :) То есть она есть, но в рекламе объявлений вообще, система реального времени добавляет технологические сложности. Впрочем, может это в нашей компании так получилось, потому что сначала мы построили рекламную сеть, в которой решаются похожие задачи и там как раз вся математика, а уже потом пошли в RTB.
no subject
Date: 2014-10-02 04:29 pm (UTC)Пожалуй, почти что так. Тем не менее есть, интересный нетехнологический фрагмент, специфический для RTB, --- собственно стратегия игры на аукционе.
А так да, самый-то содержательный код решает те же задачи, что и просто рекламная сеть. Хотя, признаться. я не задумывался над этим.
А у вас Pay-per-action, или, хотя бы pay-per-click поддерживаются?
no subject
Date: 2014-10-02 06:13 pm (UTC)Конечно. http://www.lifestreetmedia.com/mobile/performance/
Отсюда задачи прогнозирования и оценки рисков.
no subject
Date: 2014-10-02 06:24 pm (UTC)Вот-вот. Именно.
Спасибо