EaxCast S02E09 — Илья Ключников о суперкомпиляции, ее использовании в IntelliJ IDEA, а также Agda и Coq

12 сентября 2014

Темы выпуска: суперкомпиляция и её приложения, model checking, верификация. Предыдущие выпуски: пятнадцатый, четырнадцатый, тринадцатый, двенадцатый.

Слушать онлайн:
http://eaxcast.podfm.ru/_eaxcast/16/

Скачать файл:
http://eaxcast.podfm.ru/_eaxcast/16/file/podfm_eaxcast__eaxcast_209.mp3

Шоу нотес:

Голоса выпуска: Илья @lambdamix Ключников, Валерий @sum3rman Мелешкин, Александр @afiskon Алексеев

Фоновая музыка: Diablo Swing Orchestra: Balrog Boogie (8-bit version)

 

Валерий: Всем привет! С вами EaxCast, 2-ой сезон 9-ый выпуск. Я Валерий @sum3rman. Здесь с нами также Саша @afiskon и Илья @lambdamix Ключников. У нас тут произошли некоторые изменения. Теперь EaxCast в большей степени мой проект, а у Саши…Саше слово!

Александр: Да, Саша здесь стоит для мебели и дает погонять свой бложик для публикации подкаста. На самом деле я обнаружил, что мне уже не так интересно заниматься EaxCast, главным образом потому, что это отнимает у меня слишком много времени, то есть реально прямо все выходные уходят! Поэтому EaxCast – это теперь исключительно Валерин проект, а у меня в блоге он просто публикуется. Также есть теперь еще один подкаст. Он называется DevZen подкаст ссылка будет в Шоу нотес, если вы его еще не слушали, обязательно ознакомьтесь. Я обнаружил, что для меня такой формат более удобен, меньше времени тратится на обработку и, если называть вещи своими именами, то это такой радио IT, в котором каждый выпуск гиковый. Если вам это интересно, то подпишитесь, я, думаю, вам понравится.

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

Илья: Зовут меня Илья Ключников. Я сейчас работаю в JetBrains, в проекте IntelliJ IDEA, где в районе последних 7-8 месяцев я занимался для идей-ного анализа суперкомпиляцией и совсем скоро уже выйдет EP следующей идеи и там будет анализ байт-кода, который под капотом использует суперкомпиляцию. До этого работал в разных конторах, в частности предыдущее место работы было Huawei Research в Москве. Про суперкомпиляцию у меня диссертация есть, которую я защитил в ИПМ имени Келдыша Российской Академии Наук. Вот все, наверное, что интересного про краткую биографию.

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

И: Это получилось, таким образом, что… Как бы такой интересный жизненный сюжет возник. Я, начиная со 2-го или 3-го курса работал в одной конторе тестером, где одним из административных людей этой конторы был мой учитель, по информатике из ВУЗа, из МПТИ. Когда пришла пора армии и всего такого, одним из вариантов откосить от нее, было пойти в аспирантуру, и, поскольку в этой конторе все получалось хорошо, меня этот человек привел к своим друзьям в ИПМ Келдыша. Сам он был, из, что называется, из команды Турчина, из турчинской тусовки. В общем, меня привели в ИПМ имени Келдыша, в такую рефальскую тусовку, и так получилось, что мы все сошлись характерами. У меня научным руководителем стал Сергей Романенко, широко известный в русских кругах как специалист по суперкомпиляциям, по частичным вычислениям, человек. Мне это стало очень интересно, занялся и сделал диссертацию. Вот, как-то так!

В: Признаться, довольно необычно! Обычно сначала находят какую-то суперинтересную тему, а потом не могут найти, кто бы ею занимался и взял тебя в … Хотя, взять не сложно, трудно просто найти, кто бы занимался, если такая редкая тема. Вот сейчас ты сказал, что JetBrains где-то применяет суперкомпиляцию при том, что, в общем-то, вещь эта не беспроблемная. Вот что сейчас мотивирует лично тебя, что подпитывает твои последние работы, которые были уже, видимо, после аспирантуры, после того, как отпала необходимость откашивать от армии. Что подпитывает твой интерес заниматься этим сейчас?

А: Я дополню своего рода вопрос, если позволите! Было бы неплохо, я думаю, рассказать слушателям, что такое суперкомпиляция.

И: Ну, в подкасте это, наверное, рассказать в двух словах не удастся, но, если попытаться рассказать об этом очень-очень просто, то, во-первых, суперкомпиляция – это не какая-то техника и не какой-то алгоритм, а это некоторый метод работы с программами, который в каждом конкретном случае может быть очень-очень разным. Практически никогда речь не идет о конкретном суперкомпиляторе, потому, что конкретный суперкомпилятор – это нечто большее, чем просто применение метода суперкомпиляции. Это может быть применение других методов, трюков и хаков… А так, суперкомпиляция – это некоторый такой метод работы с программами. Если совсем уж говорить про computer science, то есть такое большое направление, которое по-английски называется Semantic based program transformation, а по-русски – преобразование программ, основанное на их семантике, на их смысле.

Суперкомпиляция – это такой метод, который был придуман русским ученым Турчиным, который впоследствии уехал в Америку. Он был придуман в 70-ых годах 20-го столетия. Изначально он был придуман в контексте языка РЕФАЛ, который также был им придуман. Метод весьма удачно и весьма широко применялся. Метод такой, что, допустим, у нас есть некая программа и мы хотим с ней что-либо сделать. Допустим, мы хотим ее проанализировать или прооптимизировать. Есть различные методы оптимизации программ, основанные на том, что мы смотрим на синтаксис и применяем какие-то преобразования, допустим, на AST над синтаксисом программы. Это обычно выражается в серии небольших, маленьких шажков по переписыванию программы, а суперкомпиляция – это, в некотором смысле, диаметрально противоположное. У вас есть программа и у вас есть некоторая точка входа в эту программу. Вы хотите эту программу оптимизировать и начинаете делать следующие вещи: вы пытаетесь повторить, воспроизвести работу этой программы на любых входных данных, а то, что вы это делаете на основе семантики программы, вы как бы пытаетесь её выполнять над обобщенными данными. Когда в вашей программе получается некая развилка, вы пытаетесь исследовать все возможные пути исполнения этой программы, потому что она может пойти и влево и вправо.

Понятно, что в общем случае попытка такого вот абстрактного исполнения программы будет бесконечной, потому, что вы будете строить такое дерево вычислений. Оно в общем случае у вас будет бесконечным. Такой подход, что вы начинаете рассматривать программу: что будет, если пойти налево, что будет, если пойти направо, применяется очень часто в анализе программы, но, как правило, это когда-нибудь останавливается. Суперкомпиляция к этому делу подходит таким образом, что она пытается это дерево всевозможного исполнения программы превратить в некий конечный объект, в некоторые графы конфигурации. Это самая нетривиальная часть суперкомпиляции. Когда вы эти графы конфигурации получили, вы с ней может делать все, что хотите, но если речь идет об оптимизации программы, то вы из этих граф конструируете некую новую программу. Если же речь идет об анализе программ, то вы можете новую программу не конструировать, а просто использовать этот граф для изучения некоторых свойств или спецификаций программы. А если речь идет об оптимизации, то это получается такое преобразование из исходников в исходники.

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

А: Ну, на пальцах понятно, а вот на примере. В «Идее» где это используется?

И: В «Идее» это используется немного для другого. В «Идее», 12 числа сентября будет превью новой «Идеи» и там это используется для автоматического вывода по байт-коду некоторых контрактов. В мире Java идея поддерживать такого рода контракты, как nullable, not null, аннотацию contracts; но, если кратко говорить, то вы можете проаннотировать параметр как not null. Это значит, что вы не ожидаете, что кто-то сюда сунет null в качестве аргумента. Или, если вы аннотируете метод как nullable, то вполне можете ожидать, что данный метод сможет вернуть null результат и ожидаете, что клиент к этому должен быть готов и перед тем как попытаться у возвращаемого значения, допустим, вызвать метод, в общем случае нужно это проверить это на null. «Идея» поддерживает аннотирование библиотек как бы ручками, таким образом, что вы берете некоторый метод и говорите: хочу его проаннотировать и там записываете в некоторый xml-файл. Это помогает потом, когда вы используете метод библиотек, помогает идеевскому анализу, чтобы он был более глубоким и больше понимал семантику библиотеки.

В общем случае, аннотировать такие библиотеки ручками – не очень приятное занятие и то, чем я занимался последние несколько месяцев – это автоматический вывод таких аннотаций просто по байт-коду. Вы подключаете библиотеку, она индексируется и у вас достаточно большое количество таких аннотаций появляется в редакторе автоматически, где он их понимает и использует при анализе кода. Внутри это происходит таким образом, что есть некоторый метод, которым нужно проаннотировать и я его как бы суперкомпилирую, но суперкомпилирую с целью анализа этого байт-кода. У меня внутри некоторые такие значения, которые, грубо говоря, делят объект на null, not null, nullable и так далее, строятся графы конфигурации, а потом из этих графов конфигураций вытаскиваются эти аннотации. Вот это примеры суперкомпиляций для анализа программ. На ближайшем превью «Идеи» это можно будет посмотреть.

А: Звучит очень круто, я думаю, ты своим ответом уже дал ответ на вопрос Валеры про мотивацию и все такое.

В: Ну, все-таки, мотивация с «Идеей» это понятно – мотивация с анализом программ. У тебя, я смотрел на твоей страничке, у тебя последние работы про суперкомпиляцию для теории типов Мартина Лефа и я не могу даже представить себе, что это такое, но, я думаю, мы к этому еще вернемся. Я хотел еще добавить, что… вот Саша запросил про конкретный пример, на самом деле, у нашего гостя есть статья в крайнем выпуске «Практики функционального программирования», которая так и называется «Суперкомпиляция», или как-то так… «Методы суперкомпиляции на примерах», вот! Она, в общем-то, с примерами на простом языке, с простой семантикой и один из вопросов, которые я хотел тебе задать. У тебя в статье разбирается язык с простой семантикой, где семантика так подогнана, чтобы было удобно суперкомпилировать, то есть Call by name, то есть нормальная, не помню как свойство называется, когда возможность композици… что eval части можно подставить вместо самой части. Как с этим вообще живут в реальном мире, там, где применяется суперкомпиляция?

И: Живут следующим образом. На самом деле, вначале, когда Турчин суперкомпиляцию придумывал, там происходило так. Дело в том, что РЕФАЛ – язык со строгой семантикой, то есть вычисления происходят с call by value. Аргументы вычисляются вызов по значению, тем не менее, суперкомпиляция там происходит точно также, как написано в статье call by value. Классический рефальский суперкомпилятор, он способен изменять семантику программы в таком смысле, что в том случае, если у тебя исходная программа на каких-то данных могла, допустим, привести к ошибке, то суперкомпилированная программа могла выдавать некоторый результат. Точно также, если исходная программа могла зациклиться на каких-то входных данных, а суперкомпилирвоанная программа могла на этих данных выдавать некоторый ответ. С точки зрения Турчина это считалось нормальным. Как бы принесение таких тонких мест в жертву оптимизации. Но в последнее время появились работы, которые адаптируют такую классическую суперкомпиляцию Call by name к семантике Call by need и к семантике call by value.

Здесь можно привести в пример работы шведа по имени Питер Джонсон, в Швеции недавно защитил диссертацию на эту тему. Там как раз основной момент диссертации – адаптация. Природа суперкомпиляции такова, что она все пытается сделать с Call by name к языку с семантикой call by value. Там язык очень похожий на Haskell, только семантика call by value. И там основная проблема получается то, что называется по-английски strictntess analysis, то есть для некоторых функций нужно произвести анализ, который говорит о том, что параметры этой функции они на самом деле внутри функции… то есть в них кто-то залезет внутрь. Что Call by name, что call by value, исполнение будет идентично. Поэтому у него адаптация происходит следующим образом: проводится дополнительный анализ, если дополнительный анализ говорит, что на каком-то участке абстрактного исполнения call by value оно будет давать те же результаты, что и Call by name, тогда делается то, что происходит в классике. Если нет, то там делаются специальные трюки, которые как бы форсируют call by value и потом опять это продолжается.

Если говорить про Call by need, то этим занимался Саймон Пейтон Джонс (SPJ) со своим аспирантом Максом Болингброуком. Там, на самом деле, похожие вещи, когда делаются абстрактные вычисления, делаются с более сложными конфигурациями внутри, в них есть понятие хипа, понятие стека и эти конфигурации знают, кто что заленивил, кто что форсировал и может следить, что семантика Call by need сохраняется. Получается так, что в семантике Call by name суперкомпиляция более гармонично и органично смотрятся, а для других семантик она адаптируется, но получаются лишние шаги, которые следят за тем, чтобы у нас сохранилась семантика. Вот так происходит.

В: У тебя в статье, кстати, были два упражнения: попробуйте реализовать Call by value, попробуйте реализовать Call by need. Учитывая, что ты сейчас говоришь, что это прямо диссертации чьи-то, то это был легкий троллинг или эта правда просто делается для того суперкомпилятора, который там у тебя в примере?

И: Ну, не то, чтобы легкий троллинг. Это, может быть, такое просто упражнение немножко на сложность, когда начинаешь его делать, то возникает понимание того, что, в общем, звучит не так тривиально. Одно из возможных решений – это просто придумать некоторые достаточные условия, когда обычные методы суперкомпиляции они будут давать те же самые корректные результаты, потому что в общем случае задача алгоритмически не разрешима. Например, провести strictntess analysis и понять, что call by value и call by name дадут один и тот же результат, поэтому, как и везде, люди придумывают различные условия и потом на практике проверяют, что они дают нормальный практически результат. Поэтому, я бы удовлетворился, если бы человек придумал некое достаточное условие, которое показывало бы на данном конкретном примере, что условие срабатывает и корректность гарантирована.

В: Ok, а как живут с тем, что композиция эта не всегда хорошо и правильно, потому, что побочные эффекты: объектно-ориентированная фигня и прочая Callback-лапша или с этим просто не живут?

И: Нет, с этим живут. То, что я говорил про call by value и call by need семантику — это было применительно чисто к языкам. Haskell и, соответственно, то, чем занимался Питер Джонсон, там язык Timber для встроенных систем. Он тоже такой чистый, эффекты там заворачивались в некоторое подобие IO-монады. Если же говорить про нечистые языки, типа Java, то есть суперкомпилятор для Java JCP. Его делает и делал мой коллега из ИПМ Андрей Климов со своими коллегами. Сейчас этот проект не в очень живом состоянии, но, тем не менее, для него тоже есть некоторые интересные задачи, допустим анализа программы. Как живут с нечистотой? Живут с нечистотой очень просто. Практически также, как и во всех анализах. Ее пытаются загнать в специальный загончик. Производится отдельный анализ, который говорит, что вот этот вот код чистый, а этот нечистый и, когда суперкомпиляция доходит до символьного исполнения нечистого кода, она делает очень простую вещь, она оставляет его так, как есть. Когда компилятор делает какие-то оптимизации или анализ программ делает какие-то оптимизации, если что-то он не может гарантировано корректно сделать, то он просто оставляет это так как есть. Вот такое самое простое рабочее решение, если мы не уверены в том, что этот код чистый, то мы просто оставляем его как есть.

В: А вот расскажи, у тебя последние работы были про суперкомпиляцию для теории Мартина Лефа. Это вообще как?

И: Ну я немножко уточню, на самом деле у меня последние работы были про то, как сделана суперкомпиляция… анализ байт-кода в «Идее», потом пришлю ссылки, а этот можно так сказать, предпоследняя работа по теории суперкомпиляции Мартина Лефа, там основная мотивация была такая, что никто в мире суперкомпиляции, я скажу больше, в менее мощном методе, который известен как частичные вычисления, не сделал такую простую, очевидную вещь. Некоторые преобразование программ можно проверить на предмет того, что они корректно. Дело в том, что такие нетривиальные преобразователи программ, типа частичных вычислителей или суперкомпилятора они могут выдавать некоторые нетривиальные результаты, но как проверить, что эти результаты корректны?! Есть несколько подходов.

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

Другой возможный способ, как это можно сделать – это закодировать суперкомпилятор на некотором языке, типа Agda или Coq, который поддерживает автоматическую верификацию свойств вашей программы, но для этого нужно будет еще ручками написать доказательства этой корректности. Тут перед вами встают такие преграды, заключающиеся в том, что языки типа Agda, Coq или Idris, поскольку они такие навороченные с зависимыми типами, в качестве доказательств они более строгие по отношению к тому, как вы пишите код, что вы можете написать в этом коде, поэтому написание суперкомпиляторов на таких языках оно становится весьма и весьма нетривиальной технической проблемой. Мой коллега из Болгарии Димитур Крусев, он такими вещами занимается, у него есть статьи с примерами на Coq, как можно написать суперкомпилятор для простого языка, который будет гарантировано корректным. Эти статьи показывают, что даже для очень-очень простого даже тьюринг-неполного языка это написать непросто.

То, что я с Сергеем Романенко сделал – это немножко другая тема. Предположим, что у нас есть язык, типа Agda или Coq. Мы для него написали суперкомпиляцию и можем доказать, что конкретно вот это преобразование, которое мы сделали над программой, конкретно это преобразование оно корректно сохраняет семантику. Язык c зависимыми типами позволяют такие утверждения сделать и это утверждение доказать. Суть этой работы заключалась в том, что был написан простенький суперкомпилятор для большого языка на основе теории типов, который, помимо того, что преобразовывал программу, выдавал на том же самом языке доказательства того, что преобразованная программа есть то же самое. Доказательства эти можно механически проверифицировать. Там эти доказательства можно экспортировать в Agda или в Coq. Вот как бы суть этой работы и на самом деле такие подходы сейчас есть и в других областях тоже. Они известны под названием Certifying compilation. Когда у вас есть не компилятор, который вы проверили, что он будет удовлетворять некоторым свойствам, он может быть внутри написан как угодно, но вот он, помимо того, что он выдает скомпилирвоанную программу, то он еще выдает некоторые доказательства того, что скомпилированная версия отвечает всем требованиям и это доказательство может быть механическим образом проверено. Вот так вот.

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

И: Это утверждение, это доказательство, оно говорит о том, что скомпилирвоанная программа семантически эквивалентна исходной программе и типам, там такие утверждения прямо встроены в язык, то есть там есть такой тип, который говорит, что выражение A оно эквивалентно выражению B.

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

И: Суперкомпилятор можно рассматривать как черный ящик. Он экспортирует доказательства в Coq. Он экспортирует в Coq следующие вещи: исходную программу, на моем язычке, которая переводится в некоторую исходную программу на языке системы Coq. Также экспортируется суперкомпилированная программа и экспортируются доказательства о том, что исходная программа, теперь уже на языке Coq, она эквивалентна суперкомпилированной программе, опять-таки, уже на языке Coq. Вот, поэтому тут такого расхождения нет, потому, что, если верифицировать это в Coq, если исходный в Coq и остаточный суперкомпилирвоанный терм в Коке, то это есть доказательство, которое тоже уже в Coq.

В: Ну, допустим, я готов поверить, что с твоим, конкретно с твоим, суперкомипилятором все в порядке, но ты ведь говоришь, что подход сертифицирующей компиляции… Если сертифицирующий компилятор генерирует не что-то, что можно заимпортировать в Coq, а просто какой-то байт-код, то где гарантия, что байт-код без опечатки? То есть байт-код – это тот объект, про который написано доказательство?

И: Потому, что сам этот байт-код он объект этого доказательства, сам этот байт-код он сидит внутри доказательства и оно конкретно говорит, что вот этот байт-код, допустим, последовательность просто байт, она вот обладает такими-то и такими-то свойствами.

В: Ok, я видимо, недостаточно хорошо разбираюсь в предмете, чтобы понять, что это правда. И еще один вопрос про применение суперкомпиляций в реальном мире. Если я правильно понимаю, поправь меня, если это не так, суперкомпилятор… при прогонке необходимо построить более-менее все дерево состояний с точностью до сверток. Насколько это проблема при анализе программ реального мира? Я, конечно, понимаю, что там есть свисток, который говорит, что порог глубины пройден и дальше мы не разворачиваем и так далее, но все равно, даже при наличии свистка, мне кажется, для реальной программы дерево состояний будет огромным. Как с этим борются в реальном мире?

И: Можно сказать, что сейчас это большое поле для исследований, потому, что суперкомпиляция как метод появилась в 70-ых годах. Турчин и его коллеги они трудились над продуктизацией в терминах Рефала методов и до 90-ых годов просто многих технических моментов, даже, если мы компилировали маленькую программу, они были не понятны. Поэтому 20 лет ушли на то, чтобы в итоге появилось понимание, что там происходит и как даже на небольших программах. Потом, когда этот этап был пройден, возник следующий этап, основные действия на котором заключались в том, что эти методы стали переносить на другие языки. Не то чтобы переноситься, а адаптироваться, так как возникло понимание как это работает в Рефал и как это работает в других модельных языках, на каком-нибудь упрощенном Haskell. На Haskell call by value. Относительно недавно, в 2010-ых годах SPJ и еще несколько людей стали делать более интересные и мощные суперкомпиляторы для Haskell, которые стали показывать на очень простых бенчмарках то, что суперкомпиляция очень хорошо подходит для оптимизации небольших программ.

Если говорить про суперкомпиляции больших программ, то тут пока это остается открытым вопросом, потому что непонятно как это можно сделать так, чтобы пользователь был удовлетворен. Есть, грубо говоря, два подхода и оба они до конца не исследованы. Первый подход заключается в следующем: на самом деле, суперкомпиляция – достаточно мощный метод. Как любой достаточно мощный, нетривиальный метод, он непредсказуемый. Поэтому, когда мы строим бесконечное дерево прогонки и хотим, чтобы суперкомпиляция была предсказуемой, работала за некое разумное время, нам нужно распределять ресурс и это то, чем занимался SPJ со своим аспирантом последнее время, насколько я знаю, эта работа не опубликована, она очень интересная и там, насколько я знаю, ответов пока на этот вопрос нет. Предложен такой способ решения проблемы, когда у вас есть некоторые ресурсы, какое-то время и… сделать хоть что-нибудь.

Второй подход – это попытаться сделать суперкомпиляцию модульной, чтобы она могла делать не глобальный анализ, не строить дерево граф конфигураций для всей программы, а анализировать её по частям, а потом склеивать результат. Это большое поле для исследования и пока что на эти вопросы ответа нет. На эти вопросы частично ответ есть в области применения суперкомпиляций для анализа программ. Там такие вещи можно делать, можно суперкомпилировать, анализировать не программу целиком, а по частям. Если говорить про оптимизацию – то это большой открытый вопрос и ответить на него смогут только исследователи.

В: Ok, здорово! Обсуждение за размер графы программы и обсуждение, что ты упомянул, применение суперкомпиляции для анализа, подводит на самом деле нас к следующей теме разговора, а именно к применению суперкомпиляции для анализа. Мне это напомнило схожие проблемы в model checking, когда тоже необходимо построить множество состояний всех и проверить, что на всех состояниях все выполняется. Там до сих пор для больших программ нетривиальные не решены проблемы. Когда я смотрел на суперкомпиляцию и смотрел на module checking, я нашел очень много для себя схожего. Может ли суперкомпилятор взять какое-то свойство, записанное на языке темпоральной логики какой-нибудь и проверить на графе?

И: Теоретически, может, да, смотря какое свойство. Если взять язык Haskell, где такое свойство можно попытаться записать на самом Haskell, суперкомпилирвоать и посмотреть как это свойство выполняется. Вот таким образом это можно сделать. На самом деле, такие вещи, ими занимался Андрей Немытых и у него есть очень хорошая статья по применению суперкомпилятора Рефал для верификации протокола. Есть такая большая тема – это кэш-клиент для протокола, который используется в операционных системах, в различных устройствах, которые работают с памятью, сбрасывают на диски что-то и там есть некоторые протоколы и условия того, что этот протокол корректен. Условия могут выражаться в том, что то значение, которое находится в кэше, оно совпадает с неким реальным значением, никогда не затирается. Эти протоколы достаточно просты и если написать на каком-нибудь языке программирования типа Haskell или Рефал, но их верификация зачастую бывает достаточно нетривиальна.

Одним из подходов к верификации протоколов, в том числе, является model checking с помощью практических инструментов. Вот Андрей Немытых показал, что суперкомпиляция здесь также работает, но для того, чтобы показать, что этот протокол корректен, нужно сделать некоторые дополнительные движения. Каким образом это происходит? На самом деле корректность такого протокола может быть проверена простым юнит-тестированием. Вы совершаете некие действия и смотрите, что пред- и пост-условия выполняются.

Проблема юнит-тестирования заключается в том, что оно происходит на конкретных данных и вы не покрываете все пространство состояний. Если вы пишете некий абстрактный тест, который говорит, что для любого входного значения, если выполняется такое-то условие, то и выполняется такое-то условие, если выполняется такое-то предусловие, то и выполняется такое-то постусловие. Что делал Андрей Немытых, он говорил: давайте теперь эту программу отсуперкомпилируем. Если у нас получится, что суперкомпилирвоанная версия просто сведется к тому, что программа выдает TRUE, то тогда, при условии, что суперкомпилятор корректен, мы получим некое такое доказательство того, что этот протокол корректен и удовлетворяет некоторым свойствам. В данном случае получается, что если вы используете некий инструмент, который основан на суперкомпиляции, первый нетривиальный шаг – это попытаться вот в таком виде сформулировать условия корректности.

Суперкомпиляция с этой точки зрения похожа на обобщенное тестирование. Чем занимается тестирование? Вот вы написали некоторое условие и тестирование проверяет, что у вас эти условия выполняются на некоторых конкретных данных или инструменты типа quick check, scala check, они условия генерируют и проверяют, что они выполняются на некоем множестве или подмножестве. Суперкомпиляция, поскольку она потенциально может исследовать все пространство состояний, может оказаться, что она преобразует программу к такому виду, что станет очевидным, что некоторые условия корректности соблюдаются.

Одной из моих работ была работа на основе работ Андрея Немытыха. Мы с Сергеем Романенко это повторили, только мы сделали это таким образом, что делается эта суперкомпиляция над протоколами, строятся графы конфигурации, а потом просто вынимается доказательство и экспортируется в некий язык, на котором можно проверить, что оно корректно. По-моему, оно экспортировалось в Isabelle. Брался тот же самый протокол, экспортировался в Isabelle, также экспортировались доказательства того, что этот протокол удовлетворяет таким-то и таким-то свойствам. Это на самом деле весьма похоже на model checking в этом смысле. Другое дело, что moduel checking… сейчас все основные инструменты, не способны выдать доказательства, которые могли бы быть проверены независимо.

В: А, можно еще провести такую аналогию, что суперкомпиляция – это такой quick check, который бьет строго по граничным условиям, по граничным случаям?

И: Если только очень грубую. Потому, что …

В: Да, само собой!

И: Что такое граничные случаи у автора библиотеки может быть иное мнение, чем у суперкомпилятора. Но, можно сказать так, что, если скомпилировать некоторый тест, то суперкомпилятор он пытается происследовать все возможные способы и пути исполнения этого теста. Понятно, что в большинстве случаев это не всегда удается, делаются обобщения, но в общем случае именно так и происходит. Есть такой на основе quick check… автор quick check сделал такой hip-spec (?), очень похожие вещи. Там даже некоторое подобие суперкомпиляции применяется.

Берется программа и hip-spec пытается вывести некоторые свойства этой программы. Там есть некоторый инструмент, который берет и пытается с потолка эти свойства генерировать и потом запускается quick check, который пытается эти свойства сфальсифицировать на каких-то данных. Если ему эти свойства сфальсифицировать не удалось, то тогда запускается более интересный инструмент, который пытается эти свойства доказать. Если ему удается эти свойства доказать, они добавляются в копилку знаний и потом, на следующем раунде, используются. В мире Haskell на самом деле такие инструменты появляются и, по крайне мере, показывают, что такие вещи можно делать. На самом деле это тоже интересный момент по суперкомпиляции.

Одно из применений суперкомпиляции в качестве метода трансформации программы для более надежного тестирования, потому, что суперкомпилятор может весьма интересные и хитрые пограничные случаи распознавать. Ну, вот так близко из практиков еще никто не занимался, хотя у Сергея Абрамова есть очень интересная работа про… в близкой области, про гарантированность теста.

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

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

Сейчас и другие есть интересные работы на примере суперкомиляции для параллельного программирования. Это ирландцы: Гамильтон и его ученики делали такие работы. Суть там заключается в том, что вы пишите некую работу, грубо говоря, на Haskell, автоматически эта программа, в том числе с помощью метода суперкомпиляции, превращается в набор некоторых комбинаторов: map, reduce, fold и так далее. Основное достижение заключается в том, что суперкомпиляция может помочь (программа написана на обычном языке) свести вот к таким комбинаторам для параллельного программирования.

Если говорить про конкурентное программирование, где есть всякие локи, мьютексы и так далее, то этим никто не занимался, но здесь может быть два направления. Первое – это применить суперкомпиляцию для анализа таких программ и изучения их свойств. Если говорить про попытки оптимизации, то здесь… никто этим не занимался и даже сама постановка задачи может быть очень-очень интересной. Просто не понятно, что там делать: пытаться от чего избавиться, что устранить: избыточную синхронизацию локов, или тот код, который между локами устанавливается? В зависимости от задачи могут быть разные решения этого вопроса!

В: Ну, вот тут, кстати, у model checking, как средства анализа есть небольшое преимущество, потому, что там, где он применяется – он неплохо применяется для проверки конкурентных программ, и в это смысле, видимо, пока суперкомпиляция не имеет чего предложить, к сожалению. Хотя, это было бы, наверное, интересно.

И: Ну, если говорить про model checking, то он работает не с программой напрямую,…

В: Да, конечно!

И: А он работает с некоторой моделью программы. И…

В: Извини, есть Erlang, для которого model checking практически как есть, потому, что Erlang сам по себе достаточно ограниченный, чтобы некоторые программы на нем можно было промоделировать нормально.

И: Я, к сожалению, с этим инструментом не знаком, я на него посмотрю! В большинстве случаев самый нетривиальный шаг сводится к тому, что составляется некая конкретная модель и все эти преобразования происходят не с реальной программой, а с её моделью. В большинстве случаев модель строится все же ручками.

В: Ну, да, собственно! Кстати, вот интересная постановка: можно ли применить суперкомпилятор для построения модели программы?

И: Я думаю да. Сама задача интересная, думаю, да!

В: Например амазоновцы, в прошлом выпуске я упоминал, публиковали whitepapper, как они успешно пишут модели руками на ТLA+. Я думаю, что на этом можно закончить выпуск. У меня к тебе еще один вопрос, но, видимо, как-нибудь уже в следующий раз. Всем спасибо большое, спасибо, Илья, за крайне интересную беседу.

А: И за твое время, Илья!

И: Вам тоже спасибо, что пригласили.

В: Я думаю, мы еще тебя позовем вместе с кем-нибудь, потому, что я бы хотел с кем-нибудь устроить холивор о зависимых типах. Я думаю, что здесь интересно было бы послушать несколько человек. У меня есть небольшое объявление под конец выпуска. Компания Exante, в которой я работаю, ищет Erlang-программиста, поэтому, если вы вдруг пишите на Erlang и почему-то ищите работу, то шлите ваше резюме нам. На этом я завершаю выпуск. Еще раз спасибо.

А: Ссылка на вакансию наверняка будет в шоу нотах!

В: Да, конечно же! Всем спасибо, лайкайте, шарте, слушайте, пишите комментарии. Всем пока!

И: Пока.

А: Всем пока!

Дополнение: EaxCast S02E10 — Интервью с Евгением Бурмако о Scala, макросах и академической карьере

Метки: .


Вы можете прислать свой комментарий мне на почту, или воспользоваться комментариями в Telegram-группе.

Копирование материалов данного сайта не возбраняется при условии
указания ссылки на первоисточник. © 2009–2024 Записки программиста