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

2Актуальность Суперкомпиляция автоматическое преобразование программ с целью их оптимизации: –Автоматизации программирования –Исследований и автоматического доказательства различных свойств программ –Автоматического доказательства свойств формальных систем (верификация программ, верификация протоколов и т.п.) Все данные задачи являются актуальными для развития теории и практики IT

3 Цели и задачи исследования Цель: Развитее теории и практики оптимизации и специализации функциональных программ методами суперкомпиляции Задачи исследования: Развитие методов работы суперкомпилятора с деревом конфигураций: –факторизация дерева (обобщение конфигураций, распознание зацикливания дерева) алгоритмы и их обоснование –распознание в остаточной программе подфункций, допускающих радикальное улучшение эффективности их реализации (частично рекурсивные тождественные, проекции, мономы конкатенации) –вычисление выходных форматов подфункций и использование данной информации для оптимизации остаточной программы Реализация автоматического суперкомпилятора для Рефала-5 Исследование методов применения суперкомпиляции на практике –В том числе для верификации протоколов (доказательства теорем о свойстве протоколов)

4 Реализация функционального языка Определение 1. Реализацией функционального языка программирования R назовём четвёрку, где множество P называется множеством R-программ, множество D называется множеством R-данных; частично рекурсивные функции U: P D D и T: P D N называются соответственно универсальной функцией (или семантикой) и сигнализирующей функцией времени языка R. Здесь N – множество натуральных чисел. Рассмотрим реализацию функционального языка программирования R = где D = n N M n для некоторого непустого множества M.

5 Задача специализации Пусть программа p(x,y) из P, определяет функцию F(x,y): X Y D, где X D, Y D. Зафиксируем значение первого аргумента этой функции x 0 X. В задаче специализации требуется построить другую программу q p (y) P такую, что y Y. (q p (y) = p(x 0, y)) (T(q p,y) T(p,x 0, y)). Таким образом, программа q p определяет некоторое продолжение функции F(x 0,y) по второй компоненте. Программу q p называют остаточной программой.

6 Пример специализации Специализатор n 0 =10 p(n,m) q p (m) p(n,m) -- умножение натуральных чисел q p (m) = p(10,m) = m0

7 История вопроса 70-е годы XX века –А.П. Ершов (смешанные вычисления). –В.Ф. Турчин (суперкомпиляция). –Y. Futamura (generalized partial computation). 80-е годы XX века –N.D. Jones (частичные вычисления)

8Суперкомпиляция Основная цель суперкомпиляции: – выполнить как можно больше действий параметризованного применения программы равномерно по значениям параметров предыдущий узел...

9 Пример дерева развёртки программы (дерева конфигураций) S( n, 1+m) = 1+S( n, m ); S( n, 0 ) = n; S(n,m)1+S(n,m-1) m > 0 m =? 0 n 1+(1+S(n,m-2)) m-1 > 0 m-2 > 0..… m-1 =? 0 m-2 =? 0 1+n 2+n

10 Сужение области определения и сужение образа программы сужение области определения функции (например, до пустой) аппроксимация образа функции (построение выходных форматов) частично рекурсивные константы частично рекурсивные тождественные функции частично рекурсивные мономы конкатенации

11 Аппроксимация образа функции вычисление выходных форматов функций F(x,y) = g(h(x,y)), h(x,y) = x; F( x 0,y) = g( x 0 );.

12 Частично рекурсивные тождественные функции Частично рекурсивная функция F(x): D D тождественная на её области определения: x О.Д.З. F(x) = x

13 Достаточное условие тождественности F:, - множество пропозициональных формул. F( x ) = F(F( x )); F( x y ) = F( x ) F( F( y )); F( x y ) = F(F( F( x ))) F( y ); F( x y ) = F(F( x )) F(F( F( F( y )))); F( ) = ; После стирания всех метасимволов левые части равенств должны совпадать с правыми частями. Здесь переменные x, y пробегают множество пропозицио- нальных формул; переменная пробегает множество про- позициональных переменных.

14 Частично рекурсивные мономы приписывания Определение. Пусть D – множество конечных последова- тельностей символов (конечных строк символов). Частично рекурсивную функцию F:D n D назовём частичным моно- мом приписывания, если k 1, k 2,…, k m и j 1, j 2,…, j m такие, что k i N, s. j s N, n j s > 0 и (x 1, x 2,…, x n ) О.Д.З. Здесь операция умножения – приписывание строк; возведение в степень относится к той же операции.

15 Примеры рекуррентных определений частичных мономов приписывания F(x) = g(x, ); g( x, y) = g(x, y ); g(, y) = y; Здесь переменные x, y пробегают множество конечных строк символов; переменная пробегает множество символов. F(x) = x x g(x,y) = x y x

16 Достаточное условие мономиальности Теорема. Пусть D – множество конечных строк символов. Пусть дано рекуррентное определение P частично рекурси- вной функции F:D n D. Предположим, что k 1, k 2,…, k m такие, что k i N и перестановка параметров определе- ния такая, что определение (программа) Q, полу- ченная из формальным стиранием запятых раз- деляющих аргументы, определяет частично рекурсивную тождественную функцию, тогда определение P определят частично рекурсивный моном приписывания.

17 Стратегия выбора гипотезы мономиальности На основании пассивных правых частей: они являются базисными случаями выхода из рекурсии. Пассивные правые части не меняются при определённых ранее преобразованиях. В g (пример на пред. слайде) существует бесконечно много гипотез вида: x k y x m

18 Достаточное условие конечности числа гипотез Утверждение. Пусть в программе g существует хотя бы одно предложение g(p 1,..., p n ) =... такое, что правая часть не содержит g(...) и для всех k p k отличны от пустых строк. Тогда может существовать лишь конечное число гипотез, которые можно построить в рамках описанной выше стратегии.

19 Суперкомпилятор SCP4 для Рефала-5 Разработан и реализован суперкомпилятор SCP4 для языка программирования РЕФАЛ-5 –Основан на описанных выше методах и алгоритмах обобщение конфигураций и факторизация дерева конфигураций построение выходных форматов функций распознание и оптимизация частично рекурсивных тождественных функций, функций-проекций, функций-мономов конкатенации –Полностью автоматический суперкомпилятор –Допускает на входе реальные программы Рефал-5 «как они есть», без упрощения и ограничения входного языка –Демонстрация суперкомпилятора доступна на Web- странице в режиме online Исследованы характеристики SCP4 Показана эффективность использования SCP4 для верификации программ и протоколов

20 Приложения. Доказательство свойств программ Верифицированы параметризованные протоколы когерентности кэш-памяти (cache coherence): –IEEE Futurebus+, MOESI, MESI, MSI, The University of Illinois, DEC Firefly, Berkeley, Xerox PARC Dragon. Верифицированы протоколы: –Java Meta-Locking Algorithm, Reader-Writer protocol, Steve German's directory-based consistency protocol. Верифицированы ряд модельных протоколов описанных в формализме сетей Петри.

21 Структура доказательства корректности протокола MOESI (индукция по структуре данных) Theorem 1 Theorem 2 True2 Lemma $# # # $ $ $$$ True

22 Основные результаты-1 (из 2) Разработаны методы и реализованы алгоритмы обобщения конфигураций и факторизации дерева конфигураций. –Развивают идеи полуавтоматических процедур обобщения конфигураций В.Ф. Турчина –Имеют существенно лучшие качественные характеристики, чем эти процедуры Исследованы критерии, достаточные условия и разработаны алгоритмы распознавания некото- рых классов частично рекурсивных функций тождественные функции, проекции, мономы конкатенации, разработаны алгоритмы радикального улучшения эффективности реализации таких функций.

23 Основные результаты-2 (из 2) Предложены методы и разработан алгоритм построения во время суперкомпиляции выходных форматов подпрограмм в дереве конфигураций. Показано, что в ряде случаев этот алгоритм понижает порядок временной сложности программы Разработан и реализован автоматический суперкомпилятор SCP4 для языка программиро- вания РЕФАЛ-5, исследованы его характеристи- ки, показана эффективность его использования для верификации программ и протоколов.

24 Публикации-1 (из 2) [1] Немытых А.П., Суперкомпилятор SCP4: Общая структура. Монография. Издательство УРСС, стр. [2] Лисица А.П. и Немытых А.П., Верификация как параметризованное тестирование (Эксперименты с суперкомпилятором SCP4). ЖурналПрограммирование, 1, [3] Korlyukov A.V. and Nemytykh A.P., Supercompilation of Double Interpretation. (How One Hour of the Machines Time Can Be Turned to One Second). Вестник национального технического университета Харьковского политехнического института, Том 1, стр , [4] Lisitsa A. P., and Nemytykh A.P., Verification of parameterized systems using supercompilation. In Proc. of the APPSEM05, Fraunchiemsee, Germany, [5] Lisitsa A.P. and Nemytykh A.P., Towards verification via supercompilation. In Proc. of the COMPSAC2005, [6] Лисица А.П. и Немытых А.П., Работа над ошибками, Программные системы: теория и приложения, Физматлит, Том 1, стр , 2006.

25 Публикации-2 (из 2) [7] Lisitsa A.P. and Nemytykh A.P., Reachability Analysis in Verification via Supercompilation, The Proc. of the Satellite Workshops of DTL 2007 / TUCS General Publication, No. 45, Part 2, pp Turku, Finland [8] Lisitsa A.P., and Nemytykh A.P., A Note on Specialization of Interpreters, LNCS, Vol. 4649, pp , The Proc. of CSR [9] Nemytykh A.P., Supercompiler SCP4: Use of quasi-distributive laws in program transformation, Wuhan University Journal of Natural Sciences, Vol. 95(1-2), pp , [10] Nemytykh A.P., A Note on Elimination of Simplest Recursions, The Proc. of Asia- PEPM02, pp ACM Press. Aizu, Japan [11] Nemytykh A.P., The Supercompiler SCP4: General Structure (extended abstract), LNCS, Vol. 2890, pp , The Proc. of the Perspectives of System Informatics [12] Nemytykh A.P., Playing on REFAL / The Proc. of the International Workshop on Program Understanding, pp Novosibirsk - Altai Mountains, [13] Nemytykh A.P., The Supercompiler SCP4: General Structure, Программные системы: теория и приложения, Физматлит, Том 1, стр , [14] Nemytykh A.P. and Turchin V.F., The Supercompiler SCP4: sources, on-line demonstration, [15] Turchin V.F. and Nemytykh A.P., Metavariables: Their implementation and use in Program Transformation // Technical Report CSc. TR , City College of the City University of New York, 1995.

26 Готов ответить на вопросы

27 Основные результаты Методы и алгоритмы обобщения конфигураций, улучшение качественных характеристик этих процедур. Достаточные условия и алгоритмы распознавания частично рекурсивных тождественных функций, функций- проекций, функций-мономов конкатенации. Алгоритмы радикального улучшения эффективности реализации таких функций Методы и алгоритм построения во время суперкомпи- ляции выходных форматов подпрограмм в дереве конфигураций (в ряде случаев этот алгоритм понижает порядок временной сложности программы) Автоматический суперкомпилятор SCP4 для языка программирования РЕФАЛ-5; исследованы его характеристики, показана эффективность его использования для верификации программ и протоколов