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

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

2 2 Функциональные языки программирования –Язык программирования L называется функциональным, если любая программа p, написанная на L, является определением некоторой функции F p : X D, где X D. –Под программами можно понимать индуктивные (или рекуррентные) определения последовательностей элементов множества D.

3 3 Примеры функциональных программ D – множество натуральных чисел. Fact(0) = 1; Fact(1+n) = (1+n)*Fact(n); D – множество строк. Unary_Fact( ) = I; Unary_Fact(I n) = Mult(I n, Unary_Fact(n));

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

6 6 Специализация Специализатор x0x0 p(x,y) q(y) y Y. (q(y) = p(x 0, y)) (T(q,y) T(p, x 0, y))

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

8 8 Пример специализации p(x,n) = x n, = 3*3 14 = 3*9 7 = 3*(3*9 6 ) = 3*(3*81 3 ) = 3*(3*(81*81 2 )) = 3*(3*(81*6561)) = в прямом алгоритме 14 умножений; в данном алгоритме 6 умножений; p(x, n 0 ) = p(x,2), n 0 = 2; p(x, 0) = 1; p(x, 2*n+1) = x*p(x, 2*n); p(x, 2*n+2) = p(x*x, n+1); Остаточная программа: q(x) = x*x

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

10 10 Что такое суперкомпиляция? Суперкомпиляция это набор методов специализации программ написанных на функциональных языках программирования. –Суперкомпиляция не является компиляцией, также как многозначная функция не является функцией.

11 11 Что такое суперкомпиляция: Основная цель суперкомпиляции: – выполнить как можно больше действий параметризованного применения программы равномерно по значениям параметров previous node previous node

12 12 Пример дерева развёртки программы 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

13 13 Доказательство свойств программ Верифицированы параметризованные протоколы когерентности кэш-памяти (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. Верифицированы ряд модельных протоколов описанных в формализме сетей Петри.

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

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

16 16 Аппроксимация образа функции F(x,y) = g(h(x,y)), h(x,y) = x; F( x 0,y) = g( x 0 );.

17 17 Пример аппроксимации образа (вычисления выходного формата) S(n, I m) = I S(n, m); S(n, ) = n; S(I I I n, m) I k S(I I I n, m) I I I k

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

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

20 20 Достаточное условие тождественности 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( ) = После стирания всех метасимволов левые части равенств должны совпадать с правыми частями.

21 21 Частично рекурсивные мономы приписывания Определение. Пусть 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 ) О.Д.З. Здесь операция умножения – приписывание строк; возведение в степень относится к той же операции.

22 22 Примеры рекуррентных определений частичных мономов приписывания 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

23 23 Пример формального повышения местности Переменные x, y пробегают множество g( x, y) = g(x, y ); конечных строк символов; переменная g(, y) = y; пробегает множество символов. g 2,1 ( x 1, x 2, y) g 2,1 ( x, x, y) = g 2,1 (x, x, y ); g 2,1 (,, y) = y; g(x,y) = g 2,1 ( x, x, y)

24 24 Перестановка параметров в определении g 2,1 ( x 1, x 2, y) g 2,1 ( x, x, y) = g 2,1 (x, x, y ); g 2,1 (,, y) = y; (1) = 1, (2) = 3, (3) = 2 g 2,1 ( x, y, x) = g 2,1 (x, y, x); g 2,1 (, y, ) = y;

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

26 26 Пример Переменные x, y пробегают множество g( x, y) = g(x, y ); конечных строк символов; переменная g(, y) = y; пробегает множество символов. (1) = 1, (2) = 3, (3) = 2 g 2,1 ( x, y, x) = g 2,1 (x, y, x); g 2,1 (, y, ) = y; g(x,y) = g 2,1 (x, y, x) = x y x g 2,1 ( x, y, x) = g 2,1 (x, y, x); g 2,1 (, y, ) = y;

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

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

29 29 Применение Динамическая типизация данных. Задачи самоприменения: – холостые проходы функции подстановки и т.п. – пример (поиск вызова функции):

30 30 Приложения Верифицированы параметризованные протоколы когерентности кэш-памяти (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. Верифицированы ряд модельных протоколов описанных в формализме сетей Петри.

31 31 Основные результаты-I (из 2) Разработаны аппроксимирующие алгоритмы распознавания части- чно рекурсивных константных функций, частично рекурсивных фун- кций проекции. Разработан алгоритм построения выходных форматов подпрограм- мы F по ходу дела суперкомпиляции; что позволяет сразу исполь- зовать построенный формат для специализации по нему как других подпрограмм, вызывающих F, так и самой подпрограммы F. Показа- но, что на некоторых примерах этот алгоритм способен понижать временную сложность программы. Доказана теорема о достаточном условии частично рекурсивного монома конкатенации. Разработана стратегия выбора гипотезы мо- номиальности. Разработан алгоритм, распознающий частично рекур- сивные синтаксические мономы конкатенации.

32 32 Основные результаты-II (из 2) На основе полуавтоматических процедур обобщения параметризо- ванных конфигураций, представленных в работах В.Ф. Турчина, разработаны и реализованы алгоритмы обобщения параметризован- ных конфигураций. Улучшены качественные характеристики этих алгоритмов. Разработан и реализован экспериментальный автоматический суперкомпилятор SCP4, предметной областью которого является функциональный язык программирования РЕФАЛ-5. Демонстрация суперкомпилятора доступна на Web-странице в режиме online. Исследованы характеристики суперкомпилятора SCP4.

33 33 Публикации-I (из 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.

34 34 Публикации-II (из 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.

35 35 Спасибо!

36 36 Основные результаты-I (из 2) Разработаны аппроксимирующие алгоритмы распознавания части- чно рекурсивных константных функций, частично рекурсивных фун- кций проекции. Разработан алгоритм построения выходных форматов подпрограм- мы F по ходу дела суперкомпиляции; что позволяет сразу исполь- зовать построенный формат для специализации по нему как других подпрограмм, вызывающих F, так и самой подпрограммы F. Показа- но, что на некоторых примерах этот алгоритм способен понижать временную сложность программы. Доказана теорема о достаточном условии частично рекурсивного монома конкатенации. Разработана стратегия выбора гипотезы мо- номиальности. Разработан алгоритм, распознающий частично рекур- сивные синтаксические мономы конкатенации.

37 37 Основные результаты-II (из 2) На основе полуавтоматических процедур обобщения параметризо- ванных конфигураций, представленных в работах В.Ф. Турчина, разработаны и реализованы алгоритмы обобщения параметризован- ных конфигураций. Улучшены качественные характеристики этих алгоритмов. Разработан и реализован экспериментальный автоматический суперкомпилятор SCP4, предметной областью которого является функциональный язык программирования РЕФАЛ-5. Демонстрация суперкомпилятора доступна на Web-странице в режиме online. Исследованы характеристики суперкомпилятора SCP4.