Re: [mskhug:0] Сводка для группы mskhug@googlegroups.com - Сообщений: 1 в Тем: 1
3 views
Skip to first unread message
Serguey Zefirov
Jan 6, 2010, 7:48:22 PM1/6/10
to msk...@googlegroups.com
А где можно посмотреть на примеры суперкомпиляции императивных языков
программирования?
программирования?
7 января 2010 г. 2:36 пользователь <mskhug+...@googlegroups.com> написал:
> Сводка по сегодняшним темам
>
> Группа: http://groups.google.com/group/mskhug/topics
>
> "Реализация недетерминизма в проблемно-ориентированных языках через
> абстрактный синтаксис высшего порядка" [Обновлений: 1]
>
> Тема: "Реализация недетерминизма в проблемно-ориентированных языках через
> абстрактный синтаксис высшего порядка"
>
> Sergei Romanenko <sergei.r...@gmail.com> Jan 05 05:54PM -0800 ^
>
> Реализация недетерминизма в проблемно-ориентированных языках через
> абстрактный синтаксис высшего порядка
>
> http://metacomputation-ru.blogspot.com/2010/01/hoas-nondeterminism_4687.html
>
>
>
> --
> Данное сообщение отправлено Вам, так как Вы являетесь подписчиком группы
> "MskHUG" на группах Google.
> Для того, чтобы отправить сообщение в эту группу, пошлите его по адресу
> msk...@googlegroups.com
> Чтобы отменить подписку на эту группу, отправьте сообщение по адресу:
> mskhug-un...@googlegroups.com
>
Sergei Romanenko
Jan 7, 2010, 7:12:02 AM1/7/10
to MskHUG
On Jan 7, 3:48 am, Serguey Zefirov <sergu...@gmail.com> wrote:
> А где можно посмотреть на примеры суперкомпиляции императивных языков
> программирования?
Есть суперкомпилятор JScp для Явы. Он, правда, не очень могуч, но кое-
что делать всё же умеет. Например, использовался для верификации
протоколов "кеш-когерентности". Информацию можно найти здесь:
http://groups.google.ru/group/metacomputation-ru/msg/f30e1b1ddc4dd913
Проект JVer: Верификация программ на языке Java c помощью
суперкомпилятора JScp
http://pat.keldysh.ru/jver/
Там есть примеры программ, моделирующих поведение протоколов, и
результатов суперкомпиляции этих программ.
Сергей Романенко
Andrei Klimov
Jan 8, 2010, 4:49:45 PM1/8/10
to metacompu...@googlegroups.com, msk...@googlegroups.com, refal...@botik.ru, re...@botik.ru
Сергей (Зефиров), большое спасибо за интерес к суперкомпиляции императивных языков и вопросы, заданные в группе mskhug:
http://groups.google.ru/group/mskhug/browse_thread/thread/23bd4f015a9fa376
http://groups.google.ru/group/mskhug/browse_thread/thread/77e55d1ede215e5b
Они имеют прямое отношение к тематике группы metacomputation-ru, поэтому отвечаю сразу в обе группы, а также в списки рассылки refal...@botik.ru и re...@botik.ru.
From: "Serguey Zefirov"
Sent: 07 Jan 2010 03:48
>
> А где можно посмотреть на примеры суперкомпиляции императивных языков программирования?
Сергей Романенко немножко ответил:
http://groups.google.ru/group/mskhug/msg/fce99fe310bd34c7
а я продолжу подробнее.
Две последние статьи за 2009 год со страницы
http://pat.keldysh.ru/~anklimov/pub.html
посвящены двум приложениям Java-суперкомпилятора, целью которых является не оптимизация, а верификация программ и решение обратной задачи.
Сегодня я добавил туда pdf-файлы статей и презентаций.
Подобные приложения много раз делались на суперкомпиляторах функциональных языков, но здесь интересно, что используется объектно-ориентированных язык Java и суперкомпилятор для него.
1. Анд.В. Климов, Применение суперкомпилятора языка Java для решения обратных задач в стиле логического программирования. В сб.: Информационные и математические технологии в науке и управлении / Труды XIV Байкальской Всероссийской конференции "Информационные и математические технологии в науке и управлении", Иркутск - Байкал, 5-15 июля 2009 г. Часть III. Иркутск: ИСЭМ CO РАН, 2009. С. 165-172.
В качестве примера обратной задачи здесь разбирается классическая задача о расстановке N ферзей на доске N*N. На Java описывается предикат, проверяющий, правильно ли стоят ферзи на доске, представленной двумерным булевским массивом, и затем он суперкомпилируется при известных N от 1 до 9 (больше не получается за разумное время). В остаточной программе оказываются закодированы все решения. Тексты исходной и остаточной программы, выданной Java-суперкомпилятором, в статье приведены целиком и прокомментированы.
Здесь демонстрируется старый подход В.Ф. Турчина, с которого начались его работы по суперкомпиляции:
В.Ф. Турчин, Эквивалентные преобразования рекурсивных функций, описанных на языке РЕФАЛ. В сб.: Труды симпозиума "Теория языков и методы построения систем программирования'', Киев-Алушта: 1972. Стр. 31-42.
В.Ф. Турчин, Эквивалентные преобразования программ на РЕФАЛе. Автоматизированная система управления строительством. Труды ЦНИПИАСС, N 6. ЦНИПИАСС. Москва, 1974. Стр. 36-68.
В нашем случае интересно то, что используется не функциональный (или логический) язык, а императивный. Традиционно такие "фокусы" было принято делать на языках с "деревянистыми" неизменяемыми данными, а здесь показано, что можно использовать и "обычный" язык и изменяемые структуры данных типа массивов. Лишь бы язык был достаточно "хорошим", чтобы для него можно было реализовать суперкомпилятор. Java и C# для этого подходят, а С и C++ нет.
Кстати, эти статьи Турчина можно взять здесь:
http://pat.keldysh.ru/~roman/doc/Turchin/index.html
2. Andrei V. Klimov, A Java Supercompiler and its Application to Verification of Cache-Coherence Protocols. In: Perspectives of Systems Informatics (Proceedings of Seventh International Andrei Ershov Memorial Conference, PSI 2009, Novosibirsk, Russia, June 15-19, 2009). Novosibirsk: A.P. Ershov Institute of Informatics Systems, 2009. P. 141-149.
Эта задача и метод верификации с помощью суперкомпиляции также не новы. Здесь воспроизводятся на языке Java и на суперкомпиляторе JScp результаты по верификации автоматов некоторого класса (в которые вкладываются модели рассмотренных кеш-когерентных протоколов и некоторых других моделей), полученные Алексеем Лисицей и Андреем Немытых:
http://refal.botik.ru/protocols/
В статье обозревается часть методов, реализованных в JScp, которые вовлечены в решение данной задачи. Приводится шаблон кодирования моделей и проверяемого постусловия, пример одного протокола (MOESI) и условия его "безопасности", рисунок графа остаточной программы. Все выходы из остаточной программы имеют вид return True, то есть программа модели никогда не выдает False, что означает, что "опасные" состояния недостижимы.
Эта работа также интересна тем, что она демонстрирует, что турчинский метод доказательства теорем и верификации программ с использованием суперкомпиляции отнюдь не ограничен функциональными языками. Он хорошо работает и для объектно-ориентированных языков, лишь бы для них был реализован достаточно не трививальный суперкомпилятор.
Коллекция моделей с полными текстами исходных и остаточных программ на Java и изображениями остаточных графов собрана здесь:
http://pat.keldysh.ru/jver/
Страницы с текстами программ сгенерированы Doxigen'ом. Руками добавлены картинки остаточных графов, выданные суперкомпилятором JScp.
Там даны ссылки на сайты с экспериментами Андрея Немытых и Алексея Лисицы и ссылка на домашнюю страницу Андрея cо статьями по верификации. Описания моделей на нашем сайте умышленно оформлены так же, как на сайте Андрея Немытых, чтобы легче было находить глазом те же модели и сравнивать результаты на Рефале и на Java.
3. Ben Goertzel, Andrei Klimov, Arkady Klimov, Supercompiling Java Programs (white paper). April 2002. http://supercompilers.com/white_paper.shtml
Здесь приведены три маленьких примера на специализацию Java-программ с целью оптимизации и еще один на решение обратной задачи -- так называемой "головоломки Эйнштейна".
Сергей, Вы также спросили:
From: "Serguey Zefirov"
Sent: 08 Jan 2010 04:09
>
> А с открытым кодом нет?
Нет. Исполнимые бинарные файлы JScp выложены на сайте http://supercompilers.ru/ (правда, я давно их не обновлял), но исходные программы в открытый код мы не переводили. Кроме юридических "проблем", которые, думаю, можно было бы решить, мы это не делаем по содержательной причине: открытый код имеет смысл только если он приведен к хорошо читабельному виду, который можно дальше развивать независимо от авторов. Это очень хорошая цель, но чтобы ее достигнуть, надо вложить еще много труда, до которого руки не доходят, поскольку работы по Java-суперкомпилятору сейчас ведутся в "фоновом режиме" и пока он используется лишь в исследовательских целях.
Андрей
PS. Рассматривайте сие послание как частичное выполнение обещания по подготовке текстов по суперкомпиляции языка Java, данное в мае 2009:
http://groups.google.com/group/metacomputation-ru/browse_thread/thread/4235a88fc61fddbf
Его можно считать продолжением того треда, но я решил сменить сабж, поскольку прошло много времени.
http://groups.google.ru/group/mskhug/browse_thread/thread/23bd4f015a9fa376
http://groups.google.ru/group/mskhug/browse_thread/thread/77e55d1ede215e5b
Они имеют прямое отношение к тематике группы metacomputation-ru, поэтому отвечаю сразу в обе группы, а также в списки рассылки refal...@botik.ru и re...@botik.ru.
From: "Serguey Zefirov"
Sent: 07 Jan 2010 03:48
>
> А где можно посмотреть на примеры суперкомпиляции императивных языков программирования?
http://groups.google.ru/group/mskhug/msg/fce99fe310bd34c7
а я продолжу подробнее.
Две последние статьи за 2009 год со страницы
http://pat.keldysh.ru/~anklimov/pub.html
посвящены двум приложениям Java-суперкомпилятора, целью которых является не оптимизация, а верификация программ и решение обратной задачи.
Сегодня я добавил туда pdf-файлы статей и презентаций.
Подобные приложения много раз делались на суперкомпиляторах функциональных языков, но здесь интересно, что используется объектно-ориентированных язык Java и суперкомпилятор для него.
1. Анд.В. Климов, Применение суперкомпилятора языка Java для решения обратных задач в стиле логического программирования. В сб.: Информационные и математические технологии в науке и управлении / Труды XIV Байкальской Всероссийской конференции "Информационные и математические технологии в науке и управлении", Иркутск - Байкал, 5-15 июля 2009 г. Часть III. Иркутск: ИСЭМ CO РАН, 2009. С. 165-172.
В качестве примера обратной задачи здесь разбирается классическая задача о расстановке N ферзей на доске N*N. На Java описывается предикат, проверяющий, правильно ли стоят ферзи на доске, представленной двумерным булевским массивом, и затем он суперкомпилируется при известных N от 1 до 9 (больше не получается за разумное время). В остаточной программе оказываются закодированы все решения. Тексты исходной и остаточной программы, выданной Java-суперкомпилятором, в статье приведены целиком и прокомментированы.
Здесь демонстрируется старый подход В.Ф. Турчина, с которого начались его работы по суперкомпиляции:
В.Ф. Турчин, Эквивалентные преобразования рекурсивных функций, описанных на языке РЕФАЛ. В сб.: Труды симпозиума "Теория языков и методы построения систем программирования'', Киев-Алушта: 1972. Стр. 31-42.
В.Ф. Турчин, Эквивалентные преобразования программ на РЕФАЛе. Автоматизированная система управления строительством. Труды ЦНИПИАСС, N 6. ЦНИПИАСС. Москва, 1974. Стр. 36-68.
В нашем случае интересно то, что используется не функциональный (или логический) язык, а императивный. Традиционно такие "фокусы" было принято делать на языках с "деревянистыми" неизменяемыми данными, а здесь показано, что можно использовать и "обычный" язык и изменяемые структуры данных типа массивов. Лишь бы язык был достаточно "хорошим", чтобы для него можно было реализовать суперкомпилятор. Java и C# для этого подходят, а С и C++ нет.
Кстати, эти статьи Турчина можно взять здесь:
http://pat.keldysh.ru/~roman/doc/Turchin/index.html
2. Andrei V. Klimov, A Java Supercompiler and its Application to Verification of Cache-Coherence Protocols. In: Perspectives of Systems Informatics (Proceedings of Seventh International Andrei Ershov Memorial Conference, PSI 2009, Novosibirsk, Russia, June 15-19, 2009). Novosibirsk: A.P. Ershov Institute of Informatics Systems, 2009. P. 141-149.
Эта задача и метод верификации с помощью суперкомпиляции также не новы. Здесь воспроизводятся на языке Java и на суперкомпиляторе JScp результаты по верификации автоматов некоторого класса (в которые вкладываются модели рассмотренных кеш-когерентных протоколов и некоторых других моделей), полученные Алексеем Лисицей и Андреем Немытых:
http://refal.botik.ru/protocols/
В статье обозревается часть методов, реализованных в JScp, которые вовлечены в решение данной задачи. Приводится шаблон кодирования моделей и проверяемого постусловия, пример одного протокола (MOESI) и условия его "безопасности", рисунок графа остаточной программы. Все выходы из остаточной программы имеют вид return True, то есть программа модели никогда не выдает False, что означает, что "опасные" состояния недостижимы.
Эта работа также интересна тем, что она демонстрирует, что турчинский метод доказательства теорем и верификации программ с использованием суперкомпиляции отнюдь не ограничен функциональными языками. Он хорошо работает и для объектно-ориентированных языков, лишь бы для них был реализован достаточно не трививальный суперкомпилятор.
Коллекция моделей с полными текстами исходных и остаточных программ на Java и изображениями остаточных графов собрана здесь:
http://pat.keldysh.ru/jver/
Страницы с текстами программ сгенерированы Doxigen'ом. Руками добавлены картинки остаточных графов, выданные суперкомпилятором JScp.
Там даны ссылки на сайты с экспериментами Андрея Немытых и Алексея Лисицы и ссылка на домашнюю страницу Андрея cо статьями по верификации. Описания моделей на нашем сайте умышленно оформлены так же, как на сайте Андрея Немытых, чтобы легче было находить глазом те же модели и сравнивать результаты на Рефале и на Java.
3. Ben Goertzel, Andrei Klimov, Arkady Klimov, Supercompiling Java Programs (white paper). April 2002. http://supercompilers.com/white_paper.shtml
Здесь приведены три маленьких примера на специализацию Java-программ с целью оптимизации и еще один на решение обратной задачи -- так называемой "головоломки Эйнштейна".
Сергей, Вы также спросили:
From: "Serguey Zefirov"
Sent: 08 Jan 2010 04:09
>
> А с открытым кодом нет?
Нет. Исполнимые бинарные файлы JScp выложены на сайте http://supercompilers.ru/ (правда, я давно их не обновлял), но исходные программы в открытый код мы не переводили. Кроме юридических "проблем", которые, думаю, можно было бы решить, мы это не делаем по содержательной причине: открытый код имеет смысл только если он приведен к хорошо читабельному виду, который можно дальше развивать независимо от авторов. Это очень хорошая цель, но чтобы ее достигнуть, надо вложить еще много труда, до которого руки не доходят, поскольку работы по Java-суперкомпилятору сейчас ведутся в "фоновом режиме" и пока он используется лишь в исследовательских целях.
Андрей
PS. Рассматривайте сие послание как частичное выполнение обещания по подготовке текстов по суперкомпиляции языка Java, данное в мае 2009:
http://groups.google.com/group/metacomputation-ru/browse_thread/thread/4235a88fc61fddbf
Его можно считать продолжением того треда, но я решил сменить сабж, поскольку прошло много времени.
Reply all
Reply to author
Forward
0 new messages