Введение к работе
Актуальность темы
С массовым переходом на персональные компьютеры, поддерживающие мпогоноточные вычисления, возросла важность корректного написания многонитсвых программ. Написать и протестировать мпогоноточные программы значительно сложнее в силу плохой предсказуемости порядка выполнения и синхронизации потоков. При параллельном программировании актуальными становятся проблемы тупиков и состояний гонки. Состояния гонки (race condition) - это ситуации конкурентного доступа, возникающие, когда несколько потоков одновременно обращаются к одному и тому же ресурсу, причем порядок обращений точно не определен. TaKfix ситуаций нужно избегать, поскольку они могут стать причиной ошибок, которые трудно обнаружить и исправить. Существующие методики поиска состояний гонки обычно разделяют на статический, динамический анализ, проверку на основе моделей и доказательства корректности программ.
Формальное доказательство корректности программы является очень трудоемкой процедурой. Его сложность возрастает в случае параллельных) программирования, и оно практически не применяется при промышленной разработке программного обеспечения.
В основе статического и динамического подходов лежит одна общая идея -выявление и контроль за ключевыми моментами, такими, как захват или освобождение блокировок. Но методы детектирования состояний гонки — разные. Статический анализ — это анализ кода без исполнения программы. В случае параллельных приложений статический анализ крайне сложен, и часто невозможно предсказать поведение программы, так как неизвестен допустимый набор входных значений для различных функций и способ их вызова. Эти значения можно прогнозировать на основе остального кода, но крайне ограниченно, так как возникает огромное пространство возможных состояний, и объем проверяемой информации (вариантов) увеличивается до недопустимых значений. Также средства статического анализа часто дают большое количество ложных сообщений о потенциальных ошибках и требуют немалых усилий для их минимизации. При динамическом анализе ведется поиск ошибок по результатам конкретного запуска приложения. В этом случае симптомы наличия состояний гонки могут проявиться только тогда, когда два потока получают доступ к некорректно защищенной области памяти почти в одно и тоже время, то есть программа может корректно работать в течение долгих месяцев пока не проявится состояние гонки. Это обстоятельство объясняет тот факт, что если речь заходит о проверке программы на многопроцессорной машине, то положительные отчеты динамических анализаторов воспринимаются с большим скепсисом.
Проверка па основе моделей представляет собой метод верификации правильности работы конечного автомата, в котором применяется параллельная обработка. Этот метод позволяет формально обосновать отсутствие дефектов в тестируемой части кода на основе заданных разработчиком правил преобразования данных. Проверка на основе моделей относительно эффективна лишь на небольших блоках программ. В большинстве случаев невероятно сложно автоматически вывести модель из программного кода, а создание моделей вручную является ничуть не более простой операцией.
Открытой проблемой является построение метода, которой позволит обнаружить все состояния гонок, приводящих к некорректной работе программы (дальше - неразрешенное состояние гонки), без ложных срабатываний. Наибольший интерес представляет автоматизированный анализ неблокирующихся реализаций различных алгоритмов, приобретающих все большую популярность. Такие реализации могут быть более безопасными и эффективными при большом количестве конкурирующих потоков исполнения, чем их классические аналоги, использующие синхронизационные примитивы.
В работе предложен метод, позволяющий обнаружить неразрешенные состояния гонки и конкретные ситуации их возникновения в многопоточных алгоритмах, удовлетворяющих ряду ограничений. Метод не претендует на анализ произвольного алгоритма любой сложности - указанные неблокирующиеся реализации алгоритмов содержат относительно небольшое число строк кода, используемых ячеек памяти и ветвлений.
Цель работы, задачи исследования
Цель диссертационной работы — математическое моделирование многопоточных алгоритмов путем анализа инструкций потоков, некоторые из которых используют разделяемую память, с целью обнаружения состояний конкурентного доступа к памяти, приводящих к некорректной работе алгоритмов.
Задачи исследования:
Моделирование многопоточных алгоритмов, работающих на разделяемой памяти.
Разработка критериев наличия состояний конкурентного доступа к памяти, приводящих к некорректной работе алгоритма.
Разработка методики автоматизированного тестирования, определяющей наличие состояний конкурентного доступа к памяти, приводящих к некорректной работе многопоточной программы.
Оценка сложности методики автоматизированного тестирования в различных случаях.
Научная новизна
Научная новизна работы заключается в предложенной методике формализации и моделирования процесса исполнения многопоточных
алгоритмов. Разработанная методика автоматизированного тестирования для определенных условий может существенно уменьшить сложность анализа многопоточных алгоритмов.
Практическая ценность
Результаты исследования могут быть использованы па практике для определения наличия состояний гонки, и применимы, в том числе, к анализу пеблокирующихся реализаций различных алгоритмов.
Положения, выносимые на защиту:
-
Математическая модель процесса исполнения мпогопоточных алгоритмов путем анализа инструкций потоков на платформах архитектуры х8б.
-
Критерии наличия состояний конкурентного доступа к памяти, приводящих к некорректной работе многопоточных алгоритмов, и методика автоматизированной проверки данных критериев в мпогопоточных алгоритмах, удовлетворяющих ряду условий и оценки сложности данной методики.
-
Анализ задач параллельного программирования па основе предложенной методики автоматизированного тестирования.
Публикации и апробация результатов
По теме диссертации опубликовано 14 работ, в том числе две [1,4] - в изданиях, рекомендованных ВАК РФ. В работах с соавторами соискателем лично выполнено следующее: построение математической модели исполнения многопоточных алгоритмов, разработка метода нахождения состояний гопки в потоках, работающих на разделяемой памяти, анализ задач параллельного программирования с помощью данного метода.
Результаты диссертационного исследования докладывались, обсуждались и получили одобрение специалистов на научных семинарах и конференциях:
XXXV международная молодежная научная конференция «Гагаринские чтения», Москва, 2009 г.,
I международная научно-техническая конференция "Компьютерные науки и технологии", Белгород, 2009 г.,
Международная научно-техническая конференция "Многопроцессорные вычислительные и управляющие системы 2009", Дивноморское, 2009 г.,
XI, XIII Всероссийские научно-практические конференции «Научное творчество молодежи», Кемерово, 2007,2009 гг.,
XLVII, XLVIII научные конференции МФТИ, - Москва: МФТИ, 2004-2005 гг.,
Научные семинары кафедры информатики МФТИ, 2007-2009 гг.
Структура и объем работы
