Метавычисления и системы с параллельной архитектурой (итоговый отчёт по НИР за гг.) Институт Программных Систем РАН Исследовательский Центр Мультипроцессорных Систем Лаборатория Автоматизации Программирования Научный руководитель НИР Сергей Михайлович Абрамов, Член-корреспондент РАН

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

3 Развитие технологий параллельного программирования суперкомпьютеров на основе языка Рефал Плюс (основные результаты - I) Предложены две модели параллельных вычислений на базе функционального языка РЕФАЛ Плюс: –первая основывается на понятии Т-функции без побочных эффектов, которая может вычисляться не на том вычислительном узле, где был произведён её вызов, и определяет во время исполнения программы гранулу параллелизма; –вторая представляет из себя детерминированную параллельную модель вычислений, расширяющую язык РЕФАЛ Плюс монотонными объектами. Она определяется как расширение функционального языка объектами классов, удовлетворяющих определенным ограничениям. Понятие монотонных объектов и классов определяется так, чтобы их использование из языка с параллельной операционной семантикой сохраняло детерминированность вычислений.

4 Развитие технологий параллельного программирования суперкомпьютеров на основе языка Рефал Плюс (основные результаты - II) На основе первой модели разработан и реализован прототип реализации параллельной версии языка РЕФАЛ Плюс для последовательных вычислительных машин (общедоступен через: ). Разработаны и реализованы эффективные средства параллельного программирования на языке Рефал Плюс при использовании компьютеров с распределенной памятью. Рефал-система реализована на нескольких платформах: C++, Java и OpenTS.

5 Развитие технологий параллельного программирования суперкомпьютеров на основе языка Рефал Плюс (основные результаты - III) Система программирования Рефал Плюс расширена средствами параллельного программирования, которые выполняются по схеме явного параллелизма: –для общей памяти в предположении, что на передачу данных от процесса к процессу требуется не больше времени, чем при простом вызове функций при последовательном программировании; –для распределенной памяти учитывают большую разницу времен доступа к локальной и чужой памяти. Разработаны методы и алгоритмы реализации коммуникационной сети на базе программируемых микросхем (ПЛИС), которые послужат основой для дальнейших работ по поддержке средств параллельного программирования на языках высокого уровня типа Рефала Плюс и других.

6 Развитие методов суперкомпиляции (основные результаты - I) Совместно с Институтом программирования Китайской академией наук разработан и реализован прототип суперкомпилятора для функционального типизированного языка программирования LFC. В рамках поддержки и развития суперкомпилятора SCP4 и системы программирования РЕФАЛ-5 осуществлён перенос РЕФАЛа-5 и SCP4 под операционную систему Windows Mobile Построена формальная модель, описывающая базовые инструменты суперкомпиляции. В рамках этой модели доказана теорема о возможности автоматического решения проблемы накрытия сети Петри.

7 Развитие методов суперкомпиляции (основные результаты - II) Показана возможность использования разработанных ранее методов для верификации новых классов параметризованных коммуникационных протоколов с условиями глобальной корректности. По разработанной схеме проведены автоматические доказательства корректности: –MOSI cache coherence протокола с условиями глобальной корректности; –моделей протоколов P/C, 2P/2C взаимодействия между потоками многопоточных/многонитевых (multithreaded) Java-программ. В результате полуавтоматического анализа неудачной попытки верификации одного из описаний протокола Inc/Dec модели многопоточных Java-программ с условием глобальной корректности, предъявлен тест, указывающий на некорректность данного описания.

8 Развитие методов суперкомпиляции (основные результаты - III) Разработан метод реверсного анализа программных моделей вычислительных систем. Показано, что он успешно работает при верификации некоторого класса параметризованных недетерминированных протоколов кэш когерентности и других параметризованных распределенных недетерминированных вычислительных систем, работающих бесконечное время. Разработано расширение метода частичных вычислений для специализации функциональных языков программирования на понятия, содержащееся в объектно-ориентированных языках: объекты, изменяемые во времени исполнения, классы, наследование классов, виртуальные вызовы методов. Разработанный метод поддерживает все основные конструкции объектно-ориентированных языков, таких как C# и Java.

9 Развитие методов суперкомпиляции (основные результаты - IV) Разработаны принципы построения графического трассировщика суперкомпилятора SCP4. Реализована первая версия графического трассировщика суперкомпилятора SCP4, в которой, в частности, решены задачи масштабирования больших графов и навигации по этим графам.

10 Структура доказательства корректности программной модели протокола Dragon (индукция по структуре данных)

11 Пример большого графа – результата суперкомпиляции (общий вид графической трассы)

12 Пример большого графа – результата суперкомпиляции (окно навигации)

13 Пример большого графа – результата суперкомпиляции (выделенный объект под увеличительным стеклом).

14 Развитие методов суперкомпиляции (основные результаты - V) Разработан метод суперкомпиляции функций высших порядков: –отличительной особенностью предложенного метода является работа со связанными переменными; –гомеоморфное вложение обобщено для выражений со связанными переменными; –алгоритм обобщения конфигураций расширен на случай выражений со связанными переменными; – доказаны завершаемость и корректность предложенного метода. Разработанный метод суперкомпиляции реализован в суперкомпиляторе HOSC, работающим с подмножеством функционального языка Haskell.

15 Развитие методов суперкомпиляции (основные результаты - VI) Разработаны методы многоуровневой и множественной суперкомпиляции. Исследована применимость суперкомпилятора HOSC на следующих задачах: –доказательство эквивалентности выражений языка с функциями высших порядков; –автоматическая генерация и доказательство лемм об эквивалентностях выражений при преобразованиях программ; –многоуровневая суперкомпиляция.

16 Развитие средств автоматизации символьных вычислений, поиска доказательств и анализа программ (основные результаты - I) Дальнейшее развитие получила система "Думатель" поиска доказательств свойств программ и доказательств в алгебре, в исчислении предикатов, основанная на методе вывода равенств пополнением и на способе рассуждения по индукции ( pre2/).

17 Развитие средств автоматизации символьных вычислений (основные результаты - II) Развитие системы "Думатель": –разработан и реализован алгоритм поиска гипотез-лемм при автоматическом поиске доказательств; разработана стратегия поиска лемм в системе за счет применения полиморфизма операторов-схем (2010); –разработана модель логической электронной схемы на основе теории равенства, в рамках которой автоматически проанализированы ряд свойств синхронных логических электронных схем; –разработана система полиморфных сортов и операторов в объектном языке этого prover-а; –реализована система анализа программ с явно заданным интерпретатором. Интерпретатор лямбда выражений задан в виде системы равенств; –реализована первая версия отождествления символьных выражений, основанная на унификации конечных множеств выражений (2010).

18 Публикации и доклады на конференциях 29 публикаций 16 докладов на конференциях

19 Организация научных мероприятий - I 1.Международный рабочий семинар: «First International Workshop on Metacomputation in Russia», Переславль- Залесский, 2-5 июля 2008 года. ( ) Опубликован сборник трудов: Proceedings of First International Workshop on Metacomputation in Russia, July 2-5, Pereslavl- Zalessky, Russia, Издательство Университет города Переславля, ISBN , 2008, 180 pages 2.Международный рабочий семинар: «Second International Workshop on Metacomputation in Russia», Переславль- Залесский, 1-5 июля 2010 года. ( ) Опубликован сборник трудов: Proceedings of Second International Workshop on Metacomputation in Russia, July , Pereslavl-Zalessky, Russia, Издательство Университет города Переславля, ISBN pages

20 Организация научных мероприятий - II 1.Российско-китайский рабочий семинар: «Development of supercompilation methods for a typed functional language», Переславль-Залесский, августа 2008 года. 2.Российско-китайский рабочий семинар: «Problems of verification of distributed computing systems», Переславль-Залесский, 31 марта -1 апреля 2009 года. 3.Стажировка китайской студентки Lili Zheng (Institute of Software, Chinese Academy of Sciences). Тема стажировки: «Development of supercompilation methods for a typed functional language», ИПС РАН, Переславль- Залесский, 25 ноября - 25 декабря 2009 года.

21 Спасибо! Вопросы?

22 Публикации - I [1] A.V. Klimov, A program specialization relation based on supercompilation and its properties In: Proceedings of First International Workshop on Metacomputation in Russia, Pereslavl-Zalessky, Russia, July 2-5, pp: 54-77, ISBN , [2] А.В. Климов, Применение суперкомпилятора языка Java для решения обратных задач в стиле логического программирования. // Информационные и математические технологии в науке и управлении / Труды XIV Байкальской Всероссийской конференции "Информационные и математические технологии в науке и управлении", Иркутск - Байкал, июля 2009 г. Часть III. Иркутск: ИСЭМ CO РАН, С ISBN [3] A.V. Klimov, A Java Supercompiler and its Application to Verification of Cache- Coherence Protocols. // 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, P [4] Yu.A. Klimov, An Approach to Polyvariant Binding Time Analysis for a Stack- Based Language. In: Proceedings of First International Workshop on Metacomputation in Russia, Pereslavl-Zalessky, Russia, July 2-5, pp: 78-84, ISBN , 2008.

23 Публикации - II [5] Климов Ю.А. Специализация программ на объектно-ориентированных языках методом частичных вычислений // Автореферат и диссертация на соискание ученой степени кандидата физико-математических наук. ИПМ им. М.В. Келдыша РАН, [6] Климов Ю.А. Метод частичных вычислений, позволяющий преобразовывать объектно-ориентированные программы в императивные // Научный сервис в сети Интернет: масштабируемость, параллельность, эффективность: Труды Всероссийской научной конференции (21-26 сентября 2009 г., г. Новороссийск). М.: Изд-во МГУ, С ISBN [7] Климов Ю.А. Специализатор CILPE: доказательство корректности // Препринты ИПМ им.М.В.Келдыша с. ISSN [8] Климов Ю.А. Преобразование объектно-ориентированных программ в императивные методом частичных вычислений // Программные продукты и системы (86). С ISSN X. [9] Климов Ю.А. Специализатор CILPE: генерация остаточной программы // Препринты ИПМ им.М.В.Келдыша с. ISSN [10] Климов Ю.А. Специализатор CILPE: анализ времен связывания // Препринты ИПМ им.М.В.Келдыша с. ISSN [11] Yu.A. Klimov, Anton Yu. Orlov, XSG: Fair Language with Built-in Equality. In: Proceedings of First International Workshop on Metacomputation in Russia, Pereslavl-Zalessky, Russia, July 2-5, pp: 85-93, ISBN , 2008.

24 Публикации - III [12] Ю.А. Климов, А.Ю. Орлов, С.А. Романенко, Рефал Плюс в среде Eclipse. Программные системы: теория и приложения (к пятнадцатилетию УГП им. А. К. Айламазяна) // Сборник трудов научно-практической совместной конференции студентов, аспирантов, преподавателей и научных сотрудников Института программных систем Российской академии наук и «Университета города Переславля» им. А.К. Айламазяна, г. Переславль- Залесский, апрель 2008 / Под редакцией С. М. Абрамова и С. В. Знаменского. В двух томах. Переславль-Залесский: Изд-во "Университет города Переславля", ISBN , (Т.1, с ) [13] Ilya Klyuchnikov and Sergei Romanenko. Proving the Equivalence of Higher- Order Terms by Means of Supercompilation // 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, P [14] Ilya Klyuchnikov and Sergei Romanenko. SPSC: a Simple Supercompiler in Scala // International Workshop on Program Understanding June, Altai Mountains, Russia. Novosibirsk: A.P. Ershov Institute of Informatics Systems, P [15] И.Г.Ключников, С.А.Романенко. SPSC: Суперкомпилятор на языке Scala. // Программные продукты и системы (86). С ISSN X.

25 Публикации - IV [16] Klyuchnikov I., Romanenko S. Towards Higher-Level Supercompilation // Proceedings of the second International Workshop on Metacomputation in Russia. Pereslavl-Zalessky, Russia, July 1-5, Pereslavl-Zalessky: Ailamazyan University of Pereslavl, Pp [17] A.P. Lisitsa, A.P. Nemytykh. Reachability Analysis in Verification via Supercompilation. (журнальный вариант статьи, ранее опубликованной в трудах международного семинара), International Journal of Foundations of Computer Science (IJFCS), Vol. 19, No. 4, pp: , August [18] A. Lisitsa, A.P. Nemytykh, Extracting Bugs from the Failed Proofs in Verification via Supercompilation, In: Bernhard Beckert, Reiner Hahnle (eds.), Tests and Proofs: Papers Presented at the Second International Conference TAP 2008, Prato, Italy, April 2008, Reports of the Faculty of Informatics, Univesitat Koblenz- Landau, No 5/2008, pp: 49-65, ISSN (print): , ISSN (Online): , [19] A. Lisitsa and A.P. Nemytykh. Verification as Specialization of Interpreters with Respect to Data. In: Proceedings of First International Workshop on Metacomputation in Russia, Pereslavl-Zalessky, Russia, July 2-5, pp: , ISBN , 2008.

26 Публикации - V [20] А.П. Лисица, А.П. Немытых. Об одном приложении вычислений с оракулом. // Труды международной конференции "Программные системы: теория и приложения", ИПС РАН, г. Переславль-Залесский, май 2009 / Под редакцией С.М. Абрамова и С.В. Знаменского. Изд-во "Университет города Переславля", Т. 1, стр ISBN [21] А.П. Лисица, А.П. Немытых. Об одном приложении вычислений с оракулом. (журнальный вариант статьи, ранее опубликованной в трудах конференции). // Журнал Программирование, Т. 36, 3, стр , [22] A. Lisitsa and A.P. Nemytykh. On One Application of Computations with Oracle, Programming and Computer Software, 2010, Vol. 36, No. 3, pp © Pleiades Publishing, Ltd., 2010, ISSN [23] S.D. Mechveliani. An Experience with Term Rewriting for Program Transformation. In: Proceedings of First International Workshop on Metacomputation in Russia, Pereslavl-Zalessky, Russia, July 2-5, pp: , ISBN , [24] A.P. Nemytykh, On the Place of Supercompilation inside Program Specialization. In: Proceedings of First International Workshop on Metacomputation in Russia, Pereslavl-Zalessky, Russia, July 2-5, pp: , ISBN , 2008.

27 Публикации - VI [25] A.P. Nemytykh (Editor). Proceedings of Second International Workshop on Metacomputation in Russia, July , Pereslavl-Zalessky, Russia, ISBN pages, // Издательство Университет города Переславля, г. Переславль-Залесский, [26] А.Ю. Орлов, Ю.А. Климов, Параллельное программирование на языке Рефал. В трудах Всероссийской научной конференции «Научный сервис в сети Интернет: решение больших задач», сентября 2008 г., г. Новороссийск. М.: Изд-во МГУ, C ISBN [27] А.Ю. Орлов, А.Б. Шворин: О реализации в ПЛИС маршрутизатора высокопроизводительной сети // Научный сервис в сети Интернет: масштабируемость, параллельность, эффективность: Труды Всероссийской научной конференции (21-26 сентября 2009 г., г. Новороссийск). М.: Изд-во МГУ, С ISBN [28] S.A. Romanenko, Higher-Order Functions as a Substitute for Partial Evaluation (A Tutorial). In: Proceedings of First International Workshop on Metacomputation in Russia, Pereslavl-Zalessky, Russia, July 2-5, pp: , ISBN , [29] A.P. Lisitsa, A.P. Nemytykh. Experiments on verification via supercompilation. Интернет-ресурс (Результаты тестирования разработанных методов верификации.)