ТЕСТИРОВАНИЕ, ВЕРИФИКАЦИЯ И ВАЛИДАЦИЯ ПРОГРАММ
УДК 004.92+004.94
МНОГОПОТОЧНОЕ ТЕСТИРОВАНИЕ ПРОГРАММНЫХ ИНТЕРФЕЙСОВ
© 2009 г. В. С. Мутилин
Институт системного программирования РАН 109004 Москва, ул. Солженицына, 25 E-mail: mutilin@ispras.ru Поступила в редакцию 10.11.2008 г.
В статье описывается новый метод Sapsan. Он предназначен для функционального тестирования параллельных программ, предоставляющих программный интерфейс, методы (процедуры) которого можно вызывать из нескольких потоков одновременно. Метод Sapsan позволяет проверять одно из распространенных требований к таким программам - требование сериализуемости интерфейса, заключающееся в том, что результат параллельного выполнения методов интерфейса в нескольких потоках эквивалентен некоторому последовательному выполнению этих же методов в том же состоянии. Это требование, по сути, - формализация широко используемого термина thread-safety.
1. ВВЕДЕНИЕ
В последнее время многопоточное программирование получило широкое распространение. Разрабатываемые программы с целью ускорения работы все чаще состоят из нескольких потоков, которые выполняют работу параллельно. Но разработка многопоточных программ намного сложнее последовательных. Это связано с тем, что порядок, в котором будут выполнены инструкции разных потоков, заранее непредсказуем, и разработчик должен предусмотреть корректную работу программы при всех возможных чередованиях инструкций.
В данной работе мы рассматриваем программы, предоставляющие программный интерфейс, через который с ними взаимодействуют другие программы. Интерфейс состоит из методов (процедур), описанных на языке программирования, которые можно вызывать с различными значениями параметров. Кроме того, методы интерфейса могут быть вызваны из различных потоков одновременно.
Мы решаем задачу функционального тестирования, в которой проверяем, удовлетворяет ли программа функциональным требованиям к ней. Одно из распространенных требований - это
требование сериализуемости. Это требование, по сути, является формализацией широко используемого термина thread-safety.
Пусть в некотором состоянии программы мы выполняем несколько потоков, вызывающих по одному интерфейсному методу. Мы будем называть выполнение потоков сериализуемым, если результат выполнения эквивалентен некоторому последовательному выполнению этих же потоков в том же состоянии.
На практике требования сериализуемости широко распространены. Отметим два распространенных класса таких систем: интерфейсы промежуточного уровня клиент-серверных приложений и библиотеки, предназначенные для многопоточного использования. Клиент-серверные приложения по своему назначению предоставляют клиентам сервисы. Клиенты могут использовать сервисы одновременно, при этом клиент не должен замечать присутствия других клиентов. Если два клиента совершают какие-то операции, то результат должен быть такой же, как если бы клиентов обслуживали последовательно. Данный класс систем чрезвычайно широк, так как практически все современные системы, предоставляющие сервисы, могут обслуживать нескольких клиентов одновременно.
19
2*
В библиотеках, предназначенных для многопоточного использования, такое требование выдвигается по умолчанию. Функциональные требования описываются для каждого метода в отдельности, и требуется, чтобы библиотечные методы было безопасно вызывать из нескольких потоков (thread-safe). В наших терминах это и есть требование сериализуемости.
Одними из наиболее распространенных способов проверки свойств параллельных программ являются методы проверки моделей (model checking), осуществляющие поиск чередований инструкций в параллельных потоках. В последнее время инструменты, реализующие эти методы, сделали существенный шаг вперед. Стало возможным проверять свойства для программ, написанных на широко распространенных языках программирования, а не на простых модельных языках. Так, инструмент Java PathFinder [1] способен проверять свойства программ на языке программирования Java, а инструмент VeriSoft [2] предназначен для проверки программ на языке C. Однако попытки применения этих инструментов для решения задачи проверки сериализу-емости программы сталкиваются с рядом сложностей. Во-первых, чтобы запустить эти инструменты, требуется подготовить окружение, т.е. задать набор потоков, вызывающих методы интерфейса с некоторыми значениями параметров, и начальное состояние. Но так как требование сериализуемости формулируется для неограниченного числа потоков, то, проверив сериализу-емость на конечных наборах, мы не можем быть уверены, что свойство сериализуемости выполнено для программы в целом. Во-вторых, поиск занимает сравнительно большое время. В зависимости от количества потоков требуется от нескольких минут до нескольких часов. Поэтому, даже если мы ограничимся конечными наборами потоков и будем для них многократно применять поиск, это займет начительное время.
Метод Sapsan, описанный в данной статье, в принципе может быть применен для широкого класса программ на разных языках программирования. Однако в данной работе детали метода рассматриваются только для программ, написанных на языке программирования Java.
2. ФОРМАЛЬНАЯ ПОСТАНОВКА ЗАДАЧИ
Выполнение программы - это последовательность пар (Ьг1 Ъ),..., (ип ,Ъ]П), где Ьгк - выполняемый поток, Ъ^к - инструкция потока. Будем называть ек — (Ьгк,Ъ^к) единицей выполнения.
Единица выполнения переводит систему из од-
(им)
ного состояния в другое, обозначаем в -►
(им)
-► в. Выполнение е\,...,еп переводит систему из состояния в в состояние в', обозначаем в -► в'.
Если в программе возможна последовательность инструкций, представленная в выполнении, то такое выполнение называем достижимым в этой программе. Иначе такое выполнение будем называть недостижимым в программе.
Путь в потоке - это последовательность инструкций Ъ\,...,Ъп. Из любого выполнения е1,...,еп можно выделить путь для потока Ь', выбрав
из единиц выполнения ек — (Ьк, Ък), в которых Ьк — Ь', инструкции Ък в том же порядке. И обратно, если у нас есть пути р1,...,рк в потоках Ь1,...,Ьк, то мы можем составить выполнение, выбрав некоторую последовательность единиц выполнения ег — (Ьг, Ъг), где Ъг € рг так, что инструкции для каждого потока Ьг расположены в том же порядке, что и для пути рг. Отметим, что выполнение, составленное из путей в потоках, может быть недостижимым в программе.
Несколько последовательных инструкций в пути потока может принадлежать взаимоисключающему интервалу (например, блоки синхронизации и синхронизированные методы, реализованные как вход и выход из монитора). К интервалу приписан объект, по которому происходит взаимоисключение. Инструкции, принадлежащие двум взаимоисключающим интервалам с одинаковыми приписанными объектами, в любом достижимом выполнении не пересекаются, т.е. либо сначала выполняются все инструкции первого интервала, а потом второго, либо наоборот.
2.1. Сериализуемость выполнения
Определение 1. Пусть в -► в' и выполнение е1,... ,еп содержит потоки Ь1,...,Ьт и пути Ъ1,...,ЪГ в каждом потоке ¿¿. Выполнение е1,...,еп сериализуемо, если существует выполнение / = (¿¿!,Ъ\1 ),...,(и1 ),...,(ит,Ъ\т),...,
Рис. 1. Пример потоков, для которых выполнены условия сериализуемости.
гт, Ьт) такое, что ит составляют все
(I
множество потоков и выполнение f переводит
/
систему в то же состояние в , т.е. в —
Задача. Для заданной программы установить, сериализуемы ли все достижимые выполнения этой программы.
3. ДОСТАТОЧНЫЕ УСЛОВИЯ СЕРИАЛИЗУЕМОСТИ ВЫПОЛНЕНИЙ
Понятие независимости широко используется в методах верификации программ. Одно из наиболее распространенных применений - сокращение пространства поиска [3-5].
Интуитивно, две инструкции, выполняющиеся в разных потоках, независимы в некотором состоянии, если любое их выполнение в этом состоянии приводит к одному и тому же результату.
Определение 2. Единицы выполнения ег, е] независимы в состоянии программы в, если:
1. в состоянии в выполнения ei, е] и е], ег достижимы или недостижимы одновременно;
2. если в
в1 и в
в2, то в1 = в2.
Иначе единицы выполнения называют зависимыми.
Если единицы выполнения зависимы (независимы), то говорят, что зависимы (независимы) инструкции в этих выполнениях.
Рассмотрим следующее условие.
Условие 1. Пусть а1,...,ап и Ь1,...,Ьт -пути в двух потоках. Условие выполнено, если существует единственная пара (аг0 ,Ьг0) зависимых инструкций. Все остальные пары (аг,Ь]),
(г,]) = (¿0, ]о), либо независимы во всех состояниях, либо они зависимы и выполнено:
1. аг0, аг - принадлежат одному взаимоисключающему интервалу с оЬ]1;
2. Ь]0, Ь] - принадлежат одному взаимоисключающему интервалу с оЬ]2;
3. оЬ]1 = оЬ]2.
Утверждение 1. Пусть р1,р2,---,рк - пути в потоках. Если для любой из пар путей (рг,р]) выполнено условие 1, то любое достижимое выполнение, составленное из путей р1,р2,---,рк, сериализуемо.
Для доказательства данного утверждения достаточно заметить, что в достижимом выполнении независимые инструкции можно переставлять местами, при этом результирующее состояние остается неизменным. Дополнительно заметим, что, кроме одной пары, все остальные зависимые инструкции принадлежат взаимоисключающим интервалам с одинаковыми объектами и, следовательно, в любом достижимом выполнении появляются либо сначала зависимые инструкции одного потока, затем второго, либо наоборот. Поэтому перестановкой остальных независимых инструкций получим выполнение, в котором потоки выполняются последовательно. □
Рассмотрим пример, представленный на рис. 1. Инструкции Потока 1 и Потока 2 попарно независимы, кроме пары (а2, Ь3), т.е. (аг, Ь]) - независимы ] = 1,..., 4, (г, ]) = (2, 3). Для этих потоков выполнены достаточные условия, поэтому по утверждению 1 результат любого достижимого выполнения, составленного из этих потоков, сериализуем. Проиллюстрируем доказательство
е^.е
утверждения на этом примере. Пусть, например, достижимо Выполнение 1 (рис. 1). Так как в Выполнении 1 инструкции первого потока аз, а4 можно переставлять местами с инструкциями b1,b2,b3,b4 второго потока, не меняя р
Для дальнейшего прочтения статьи необходимо приобрести полный текст. Статьи высылаются в формате PDF на указанную при оплате почту. Время доставки составляет менее 10 минут. Стоимость одной статьи — 150 рублей.