Верификация как параметрическое тестирование. (Эксперименты с суперкомпилятором SCP4.) Алексей Лисица The University of Liverpool, Андрей П. Немытых Институт программных систем РАН.

Суперкомпилятор SCP4 - экспериментальный специализатор функционального языка программирования РЕФАЛ-5. Реализован также на РЕФАЛе-5. Исходные тексты суперкомпилятора, исполняемые модули и исходные тексты РЕФАЛа-5 свободно распространяются: (Андрей П. Немытых и Валентин Ф. Турчин) Windows 98, Windows NT/2000/XP, Linux (Intel)

Верификация параметризованных систем суперкомпилятором SCP4. ( ) Удачные эксперименты по верификации cache coherence протоколов с глобальными свойствами: –IEEE Futurebus+, MOESI, MESI, MSI, The University of Illinois, DEC Firefly, Berkeley, Xerox PARC Dragon. А также параметризованных протоколов: –Java Meta-Locking Algorithm, Reader-Writer protocol.

Тестирование. Пусть дана общерекурсивная функция f: D M, Im(f) является подмножеством множества истинности общерекурсивного предиката. Пусть P – программа, реализующая ; P f – программа, d 0 D завершающая исполнение вызова P f (d 0 ) в конечное время, и о которой предполагается что она реализует f. Тестированием P f по постусловию назовём программу T: D {True, False}, реализующую композицию P P f. d 0 D результат вычисления T(d 0 ) = True подтверждает корректность P f на d 0, а T(d 0 ) = False даёт тест d 0, на котором корректность нарушается.

Верификация. Перебор всего множества D с корректным результатом тестирования верифицирует P f по постусловию. Пусть – оптимизирующая программа, результат вычисления которой ( P P f,d) есть программа, обладающая простым синтаксическим свойством, позволяющим утверждать, что Im( ) = {True}. Пусть результат оптимизации, по определению, всегда реализует некоторое расширение частичной функции, которая реализована преобразуемой программой (в нашем случае P P f ). В таком случае получаем верификацию P f по постусловию.

Суперкомпилятор SCP4 - экспериментальный специализатор функционального языка программирования РЕФАЛ-5. Реализован также на РЕФАЛе-5. Исходные тексты суперкомпилятора, исполняемые модули и исходные тексты РЕФАЛа-5 свободно распространяются: (Андрей П. Немытых и Валентин Ф. Турчин) Windows 98, Windows NT/2000/XP, Linux (Intel)

Кодировка некоторого класса cache coherence протоколов Эволюция состояний мультипроцессорной системы представляет собой недетерминированную динамическую систему с дискретным временем time. Пусть Int(time,InitConfig) – интерпретатор этой системы, который по данной начальной конфигурации InitConfig системы выдаёт конфигурацию Config системы через время time. Мы моделируем недетерминированность, помечая такты времени случайными действиями, которые будут происходить в системе. Корректность протоколов выражается в недостижимости конфигураций определённого вида и проверяется предикатом- программой (Config). Задача для суперкомпилятора: проспециализировать композицию Int(time,InitConfig 0 )

Cache coherence протокол MOESI. ( Структура доказательства корректности построенного SCP4 ) Theorem 1 Theorem 2 True2 Lemma $# # # $ $ $$$ True

Верификация cache coherence протокола Xerox PARC Dragon. В результате анализа остаточной программы – результата суперкомпиляции обнаружена ошибка в описании протокола данном в: –G. Delzanno, Automatic Verification of Parameterized Cache Coherence Protocols. и построен тест, на котором нарушается корректность протокола. Удачно верифицировано уточнённое описание этого протокола: –

Суперкомпиляция Supercompilation (от supervised compilation) есть техника специализации функциональных программ. В 70-х годах В.Ф. Турчин предложил ряд идей по автоматическому преобразованию программ, которые неудачно назвал суперкомпиляцией. Он поставил задачу создать инструменты для наблюдения за операционной семантикой программы, когда фиксирована функция F, вычисляемая этой программой. Результатом таких наблюдений должно стать новое алгоритмическое определение некоторого продолжения функции F. Новый алгоритм строится с целью более быстрого вычисления F на конкретных аргументах. Главная цель суперкомпилятора: исполнить максимальное число действий некоторого параметризованного применения программы равномерно по значениям параметров.

Общая структура РЕФАЛ интерпретатора. Refal-5 task final inp.-prog. result := ; /* undefined */ do { Refal-step; } while( the task is not solved ) /* still is not completely evaluated */ if( the task is determined ) { result := task; } Entry config. Source prog. Internal language Refal-5 Result

Общая структура SCP4 residual := ; /* empty */ do { current-task := head(tasks); driving; folding; if( the current-task is solved ) { global-analysis; /* folded */ specialization w.r.t the global properties; propagation of the global inf. over the tasks; if( the current-task is not empty ) { residual := residual current-task; } tasks := tail(tasks); } } while( tasks ) dead-code-analysis; Refal -5 Intern. language Parameterized entry config.-s Source program tasks final input program Refal -5 parameterized entry points, residual program C

Прогонка Прогонка есть расширение интерпретации одного шага REFAL-graph машины на параметризованное множество входных конфигураций. a x + b = 0 driving a x + b = 0 x = -b/a; a 0 b = 0 any x Ø a =? 0 a ? 0 b =? 0 b ? 0 Школьная прогонка:

Свёртка Свёртка сворачивает мета-дерево возможных вычислений в конечный граф и вызывается сразу после прогонки. Т.е. она пробует свернуть часть пути (который не свёрнут к данному моменту) от корня мета-дерева к текущему в текущей грозди, построенной прогонкой. Алгоритм состоит из двух логически замкнутых инструментов: сведения и обобщения. Оба эти инструмента как синтаксические так и семантические свойства функционального стека. преобразуемой программы current node previous node

Глобальный анализ (построение выходных форматов) Построение выходных форматов компонент факторизации критично, когда длина стека вызовов функций преобразуемой программы не является равномерно ограниченной по входным данным. После построения очередного выходного формата мета-граф специализируется по этому формату (без дополнительных развёрток в мета-дереве). Без построения выходных форматов интересных преобразований не происходит, за редким исключением.

Введение в РЕФАЛ (данные) РЕФАЛ (В.Ф. Турчин) строгий функциональный язык первого порядка, в котором конкатенация ассоциативна. Имеется также унарный конструктор для построения структура дерева. Семантика языка базируется на отождествлении по образцу и модели вычислений – алгорифмах Маркова. Данные РЕФАЛа определяются следующей грамматикой: d ::= (d 1 ) | d 1 d 2 | SYMBOL | empty empty ::= /* nothing */ Example:(A + B) * (C – D) * +-ABCD

Введение в РЕФАЛ (ассоциативность конкатенации) Palindrome { = True; s.1 = True; -- application constr. s.1 e.2 s.1 = ; e.1 = False; } * The palindrome predicate: Example 1: Example 2: (Refal style reversing) * Reversing a list of terms: rev { t.x e.ys = t.x; = ; -- empty expression } -- on the both sides. /* Reversing a list of terms: we may concatenate a term taken by the variable t.x right on the end of the list. The blank is used to denote the concatenation. */ /* Pattern may be split from both sides: a symbol-variable s.1 is split from the left and right sides. */

Cache coherence протокол MOESI. ( Структура доказательства корректности построенного SCP4 ) Theorem 1 Theorem 2 True2 Lemma $# # # $ $ $$$ True

Языковая зависимость (протокол MOESI) RandomAction { … … = (invalid e.x1) (modified ) (shared I e.x3 e.x4) (exclusive )(owned e.x2 e.x5); … } Append { () (e.y) = e.y; (s.z e.x) (e.y) = s.z ; } RandomAction { … … = (invalid e.x1) (modified ) (shared I ) (exclusive )(owned ); … }

SCP4 as a simple theorem prover. The task: $ENTRY Go { e.ls = >; } palindrome { = True; s.x = True; s.x e.ls s.x = ; s.x e.ls s.y = False; } rev { = ; t.x e.ls = t.x; } The result of specialization: A simple theorem has been proven. $ENTRY Go { = True ; s.102 e.41 = True ; }

Использование SCP4 для упрощения определений. Задача: Решить уравнение 'a' X = X 'a', где область допустимых значений переменной X есть множество конечных строк. $ENTRY Go { e.x = ; } Eq { (s.1 e.x) (s.1 e.y) = ; ((e.1) e.x) ((e.2) e.y) = ; () () = True; (e.x) (e.y) = False; } Упрощённое определение: построенное SCP4. Доказана простая теорема. $ENTRY Go { e.41 = ; } F7 { 'a' e.41 = ; = True ; e.41 = False ; }

SCP4 as a simple theorem prover (идея Александра Корлюкова) Задача (по мотивам Л. Ф. Магнитцкого): Летит стая гусей. Навстречу ей гусь: Привет сотня гусей!. Вожак отвечает: Нас не сотня. Если всех нас сосчитать и прибавить ещё столько же, и пол-столько, и четверть-столько, да ещё и тебя, Гусь, тогда получится сотня. Вопрос: Сколько гусей в стае? $ENTRY Go { e.n = ) ( )>; } Eq { ( ) ( ) = TRUE; ('g' e.xs) ('g' e.ys) = ; (e.xs) (e.ys) = FALSE; } Hundred { = 'gggggggggggggggggggggggggggggggggggggggggggggggggg' 'gggggggggggggggggggggggggggggggggggggggggggggggggg' ; } Counter { 'gggg' e.n = 'gggg' 'gggg' 'gg' 'g' ; = 'g'; } Здесь 'gg' := 'g' 'g'

Вопрос: Сколько гусей в стае? Ответ данный суперкомпилятором SCP4: $ENTRY Go { 'gggggggggggggggggggggggggggggggggggggggg' e.n = FALSE ; * The following string has 36 of 'g' (of geese). 'gggggggggggggggggggggggggggggggggggg' = TRUE ; 'gggggggggggggggggggggggggggggggg' = FALSE ; * The length of the (n+3)-th left side is 36-4(n+1), * while the right side is FALSE.... = FALSE ; } Мы не только ответили на поставленный вопрос, но и доказали что других решений не существует. В процессе суперкомпиляции произошла индукция по e.n и рекурсия рекурсия данная в исходной программе удалена.

Более адекватная кодировка. Counter { e.n = 'g'; } All { e.n = e.n; } Half { = ; 'gg' e.n = 'g' ; } Quoter { = ; 'gggg' e.n = 'g' ; } Остаточная программа подобна предыдущей, но содержит сто предложений.

Головоломка (Эйнштейн): ( идея использования Александра Корлюкова ) Имеются 5 домов раскрашенные в разные цвета, в каждом доме живёт один человек. Все они разной национальности, предпочтения к напиткам у всех разные, все они курят разные сорта сигарет и имеют слабость к совершенно разным животным. Дано: 1. Англичанин живёт в красном доме. 2. У шведа живёт собака. 3. Датчанин пьёт чай. 4. Зелёный дом – ближайший слева от белого дома. 5. Хозяин зелёного дома пьёт кофе. 6. Курящий сигареты PallMall держит птицу. 7. Жилец центрального дома пьёт молоко. 8. Хозяин жёлтого дома курит Dunhill. 9. Норвежец живёт в первом доме. 10. Поклонник Marlboro – сосед любителя кошек. 11. Любитель покататься на лошади – сосед фаната сигарет Dunhill. 12. Один из них предпочитает курить Winfield потягивая пиво. 13. Дом норвежца – соседний к синему дому. 14. Немец курит Rothmans. 15. Поклонник Marlboro соседствует с поклонником чистой водички. КТО Д Е Р Ж И Т Р Ы Б У ?

Вопрос: кто держит рыбку? Определение Z i есть переформулировка i-ого утверждения в терминах РЕФАЛа. LookForFish { (s.1 s.2 s.3 Fish s.5) e.b = s.1 ; (s.1 s.2 s.3 s.4 s.5) e.b = ; } * 1. Англичанин живёт в красном доме. Z1 { (Englishman Red s.3 s.4 s.5) e.b = (Englishman Red s.3 s.4 s.5) e.b; (e.1) e.b = (e.1) ; } * 2. У шведа живёт собака. Z2 { (Swede s.2 s.3 Dog s.5) e.b = (Swede s.2 s.3 Dog s.5) e.b; (e.1) e.b = (e.1) ; } * 3. Датчанин пьёт чай. Z3 { (Dane s.2 s.3 s.4 Tea) e.b = (Dane s.2 s.3 s.4 Tea) e.b; (e.1) e.b = (e.1) ; } …

Входная точка программы: $ENTRY Puzzle { e.buildings = >>> >; } Программа проверяет удовлетворяют ли выбранные входные данные условиям головоломки или нет. Если данные удовлетворяют условиям, То программа возвращает ответ на поставленный в головоломке вопрос, иначе программа попадает в ситуацию аварийной остановки (Отождествление невозможно).

Формулировка задачи и результат суперкомпиляции. Параметризованная входная конфигурация: Параметр s.ij соответствует одному объекту в i-ом доме, каждая пара скобок представляет дом. Остаточная программа: $ENTRY Puzzle { (Norwegian Yellow Dunhill Cat Water ) (Dane Blue Marlboro Horse Tea ) (Englishman Red PallMall Bird Milk ) (German Green Rothmans Fish Coffee) (Swede White Winfield Dog Beer ) = German ; }

Фильтрация $ENTRY Puzzle { e.buildings = >>> >; } Порядок фильтров Z i может быть изменён. Время суперкомпиляции зависит от этого порядка. Число всех возможных вариантов перебора в Головоломке равно 5 25 (примерно ). Если компьютер будет перебирать со скоростью миллиард вариантов в секунду, то ему понадобится 9 лет. Суперкомпилятор (подобно PROLOG интерпретатору) сужает входные Параметры согласно образцам, данным в фильтрах, и обнаруживает что область определения состоит из одной точки; она и является ответом на вопрос. Дополнительный эксперимент показывает, что подсказку Z 15 можно убрать из описания головоломки: ответ тот же самый (немец).

Литература [1] Turchin, V. F., The concept of a supercompiler, ACM Transactions on Programming Languages and Systems, 1986, 8: [2] Nemytykh A.P., and Turchin V.F. The Supercompiler Scp4: sources, on- line demonstration. [3] Nemytykh A.P., The Supercompiler Scp4: General Structure., LNCS vol. 2890, pp , [4] Nemytykh A.P., A Note on Elimination of Simplest Recursions. In Proc. of the ACM SIGPLAN Asia-PEPM'02, ACM Press, [5] Nemytykh A.P., Playing on REFAL. In: Proc. of the PU03, pp:29-39, Institute of Informatics Systems, Novosibirsk, Russia, [6] Lisitsa A., and Nemytykh A.P., Verification of parameterized systems using supercompilation. In Proc. of the APPSEM05, Fraunchiemsee, Germany, September 2005.