Верификация как параметризованное тестирование Алексей П. Лисица The University of Liverpool. Андрей П. Немытых Институт Программных Систем РАН. - презентация

1 Верификация как параметризованное тестирование Алексей П. Лисица The University of Liverpool. Андрей П. Немытых Институт Программных Систем РАН.

2 Тестирование Пусть дана общерекурсивная функция 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, на котором корректность нарушается.

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

4 Понятие протокола Протоколом называется любая игра. –Если при некоторых состояниях игры возможен выбор следующего хода, то игра называется недетерминированной. –Примеры: футбол, шахматы, игра на бирже. Инвариант игры, который выполняется в любой момент времени, называется свойством корректности протокола. –Примеры: Футбол – мяч не касается руки полевого игрока. Шахматы – на одной клетке поля находится не более одной фигуры. Игра на бирже – от перестановки мест слагаемых сумма не меняется.

5 Верификация параметризованных систем суперкомпилятором 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, Steve German's directory-based consistency protocol. Ряд успешных экспериментов по верификации по постусловию модельных протоколов описанных в формализме сетей Петри.

6 Параметризованные cache coherence протоколы Процессоры используют элементы быстрой памяти (кэш) для работы с копиями блоков основной (медленной) памяти. Протоколы когерентности кэш-памяти призваны гарантировать совпадение кратных копий одного и того же блока.

7 Класс параметризованных cache coherence протоколов Дано n корзин. Пусть i-ая корзина содержит x i камней. Шаг игры есть перекладывание y ik камней из i-ой корзины в k-ую корзину (для всех 0 < i,k < n+1), если y ik удовлетворяют некоторым условиям. Если в данный момент времени возможны несколько различных ходов, тогда случайным образом выбирается один из них.

8 Свойства корректности cache coherence протоколов Пусть дана начальная конфигурация такой игры, тогда свойство корректности есть свойство недостижимости конфигураций определённого вида. –Конфликтная (аварийная ситуация). Как правило, для создания ДТП достаточно двух участников уличного движения.

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

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

11 Математическая индукция и свойства обобщения конфигураций Выбор конфигураций для обобщения: –вариант упрощающего предпорядка Higman-Kruskal-а; –монотонность по функциям-конструкторам: F 1 (t 1,t 2 ) = t 1 t 2, F 2 (t 1 ) = (t 1 ), F f (t 1 ) = t 1 F 1 (t 1,t 2 ), t 2 F 1 (t 1,t 2 ), t 1 F 2 (t 1 ), t 1 F f (t 1 ) –согласованность с функциями-конструкторами: t 1 t 2 F 2 (t 1 ) F 2 (t 2 ), F f (t 1 ) F f (t 2 ) F 1 (t, t 1 ) F 1 (t, t 2 ), F 1 (t 1, t) F 1 (t 2, t) –отделение базисных случаев индукции от регулярных: () (SYMBOL), () (s.variable) Основное свойство: –Для любой бесконечной последовательности термов t 1, t 2, … существует пара t i, t k, такая что i < k и t i t k.

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

13 Языковая зависимость (протокол 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 ); … }

14 Параметры кодировки I Перестановка предложений функции выбора очередного действия. Теорема: Факт удачной верификации протокола не зависит от выбранной перестановки предложений функции выбора очередного действия. RandomAction { … rm (invalid I e.1) (modified e.2) (shared e.3) (exclusive e.4)(owned e.5) = … ; … wh2 (invalid e.1) (modified e.2) (shared e.3) (exclusive I e.4)(owned e.5) = … ; wm (invalid I e.1)(modified e.2) (shared e.3) (exclusive e.4) (owned e.5) = … ; … }

15 Параметры кодировки II Перестановка аргументов конкатенации. Экспериментальное наблюдение: Факт удачной верификации протокола не зависит от выбранной перестановки аргументов конкатенации. RandomAction { … … = (invalid e.x1) (modified ) (shared I e.x3 e.x4) (exclusive )(owned e.x2 e.x5); … }

16 Системы Диафантовых линейных равенств (неравенств) NP-полная проблема. –Язык спецификации удачно проверифицированных cache coherence протоколов. –Естественность унарного представления натуральных чисел. –Естественность ассоциативной конкатенации как языка описания таких систем. Некоторые удачные эксперименты. –Верификация протоколов. –Исчерпывающее решение задачи Миссионеры и каннибалы (А.В. Корлюков). –Верификация решения детской задачки Малые чирки.

17 Кодировка протоколов посредством Java программ Specification, Verification, and Synthesis of Concurrency Control Components by Tuba Yavuz­Kahveci and Tevfik Bultan. ( ) Airport Ground Traffic Control протокол:

18 Алгоритмы верификации программ (проверка моделей программ) Проверка моделей. –Верификация систем с конечным (но очень большим) числом состояний. –Использование полуразрешающих алгоритмов и эффективных структур данных. –Надежды использования алгоритма Маканина в задачах верификации программ преобразующих строчки символов.

19 Литература [1] Lisitsa A. P., and Nemytykh A.P., Verification of parameterized systems using supercompilation. In Proc. of the APPSEM05, Fraunchiemsee, Germany, September [2] Lisitsa A. P., and Nemytykh A.P., Towards verification via supercompilation. In Proc. of the COMPSAC2005, [3] Лисица А.П., и Немытых А.П., Верификация как параметризованное тестирование (Эксперименты с суперкомпилятором SCP4). ЖурналПрограммирование, 1, [4] Лисица А.П., и Немытых А.П., Работа над ошибками, Программные системы: теория и приложения, Физматлит, Том 1, стр , [5] Lisitsa A. P., and Nemytykh A.P., Reachability Analysis in Verification via Supercompilation, Accepted by the Workshop on Reachability Problems [6] Lisitsa A. P., and Nemytykh A.P., A Note on Specialization of Interpreters, Accepted by the conference CSR07.

20 Спасибо!