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

2Актуальность Верификация автоматическая проверка свойств распределенных вычислительных систем с целью повышения их надёжности: –Корректность параметризованных коммуникационных протоколов. –Программные модели распределенных вычислительных систем. –Моделирование недетерминированности выбора очередного действия эволюции вычислительной системы. Все данные задачи являются актуальными для развития технологий GRID

3 Цели исследований Разработка методов верификации и анализа программ, протоколов, распределённых вычислительных систем и цифровых устройств. –Изучение процесса верификации как параметризованного тестирования. –Разработка методов верификации основанных на автоматической специализации программных моделей вычислительных систем. –Разработка методов автоматического построения тестовых гипотез, указывающих на возможные ошибки в вычислительных системах.

4 Традиционная верификация на базе моделей Проверяемая программа Модель программы Критические свойства Спецификация Верификатор Контрпример Верно исправления моделирование формализация

5 Тестирование Проверяемая программа Критические свойства спецификация- предикат Исполнение Контрпример Верно исправления формализация Спецификация композиция конкретные данные

6 Параметризованное тестирование Проверяемая программа Критические свойства спецификация- предикат Специализация Контрпример Программа, вычисляющая константу Верно исправления формализация Спецификация композиция параметризованный контекст синтаксически очевидная

7 Традиционная верификация на базе моделей Проверяемая программа Модель программы Критические свойства Спецификация Верификатор Контрпример Верно исправления моделирование формализация

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

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

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

11 Пример дерева развёртки программы (дерева конфигураций) 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

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

13 Аппроксимация образа функции один из ключевых инструментов

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

15 Верификация программных моделей распределенных вычислительных систем - II Типы верифицированных параметризованных коммуникационных протоколов включают: –Snooping cache coherence протоколы. –Directory-based cache coherence consistency протоколы. –Java multi-threads протоколы.

16 Пример: MESI параметризованный протокол когерентности кэш-памяти (I). Здесь modified, exclusive, shared, invalid – натуральные переменные EFSM модели, представляющие абстрактные счетчики оригинальной параметризованной модели: их имена обозначают состояния кэша (cache); значения переменных – число caches находящихся в соответствующем состоянии.

17 Пример: MESI параметризованный протокол когерентности кэш-памяти (II). Параметризованная начальная конфигурация: Недопустимые состояния (нарушающие свойство корректности) задаются неравенствами:

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

19 Индуктивное автоматическое доказательство корректности MESI протокола.

20 О структуре автоматического доказательства. Граф на предыдущей странице показывает структуру индуктивного доказательства корректности MESI протокола. Этот граф построен из остаточной программы (результата суперкомпиляции) и отражает её синтаксические свойства. –Индукция по длине последовательности действий (времени) преобразующей вычислительную систему. –Автоматическое построение обобщенных гипотез индукции посредством обобщения конфигураций (состояний) протокола. –Индукционные гипотезы доказываются одновременно (параллельно).

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

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

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

24 Ошибка в спецификации Xerox PARC Dragon протокола С помощью суперкомпилятора SCP4 (специализатора программ) в одной из спецификаций этого протокола, обнаруженной в литературе, найдена ошибка и построен тест, указывающий на эту ошибку. Giorgio Delzanno. Automatic Verification of Parameterized Cache Coherence Protocols. Proc. of 13th Int. Conference on Computer Aided Verification LNCS 1855, Springer Verlag, 2000, pp: 53–68.

25 Поиск теста, указывающего на ошибку Если повезёт, то тест представлен явно в синтаксисе программы: F( описание теста ) = Ложь; ….. F( …. ) = Истина; ….. F( …. ) = Истина; В общем случае необходим анализ программы (раскрутка её снизу вверх от выходов Ложь ).

26 Публикации-I [1] Немытых А.П., Суперкомпилятор SCP4: Общая структура. Монография. Издательство УРСС, Москва, стр. [2] Лисица А.П. и Немытых А.П., Верификация как параметризованное тестирование (Эксперименты с суперкомпилятором SCP4). ЖурналПрограммирование, 1, стр.22-34, [3] Lisitsa A.P. and Nemytykh A.P., Reachability Analysis in Verification via Supercompilation. International Journal of Foundation of Computer Science (IJFCS), Vol. 19, No. 4 (August 2008), pp , [4] Lisitsa A.P., and Nemytykh A.P., A Note on Specialization of Interpreters, Lecture Notes in Computer Science, Vol. 4649, pp , The Proc. of CSR07, [5] Lisitsa A.P. and Nemytykh A.P., Extracting Bugs from the Failed Proofs in Verification via Supercompilation, In: Tests and Proofs: Papers Presented at the Second International Conference TAP 2008, Italy, / Reports of the Faculty of Informatics, Univesitat Koblenz-Landau, No 5/2008, pp: 49-65, 2008.

27 Публикации-II [6] Lisitsa A.P., and Nemytykh A.P., 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: [7] Nemytykh A.P., 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: , [8] Mechveliani S.D., 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: , [9] Mechveliani S.D., A Predicate Calculus Prover Based on Completion and Boolean Term Algebra. Технический отчёт No института RICAM Австрийской академии наук, г. Линц, Австрия, 2006.

28 Международное сотрудничество The University of Liverpool, United Kingdom. Johann Radon Institute for Computational and Applied Mathematics (RICAM), Austrian Academy of Sciences, г. Линц.

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

30 Публикации-I [1] Немытых А.П., Суперкомпилятор SCP4: Общая структура. Монография. Издательство УРСС, Москва, стр. [2] Лисица А.П. и Немытых А.П., Верификация как параметризованное тестирование (Эксперименты с суперкомпилятором SCP4). ЖурналПрограммирование, 1, стр.22-34, [3] Lisitsa A.P. and Nemytykh A.P., Reachability Analysis in Verification via Supercompilation. International Journal of Foundation of Computer Science (IJFCS), Vol. 19, No. 4 (August 2008), pp , [4] Lisitsa A.P., and Nemytykh A.P., A Note on Specialization of Interpreters, Lecture Notes in Computer Science, Vol. 4649, pp , The Proc. of CSR07, [5] Lisitsa A.P. and Nemytykh A.P., Extracting Bugs from the Failed Proofs in Verification via Supercompilation, In: Tests and Proofs: Papers Presented at the Second International Conference TAP 2008, Italy, / Reports of the Faculty of Informatics, Univesitat Koblenz-Landau, No 5/2008, pp: 49-65, 2008.

31 Публикации-II [6] Lisitsa A.P., and Nemytykh A.P., 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: [7] Nemytykh A.P., 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: , [8] Mechveliani S.D., 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: , [9] Mechveliani S.D., A Predicate Calculus Prover Based on Completion and Boolean Term Algebra. Технический отчёт No института RICAM Австрийской академии наук, г. Линц, Австрия, 2006.