Стр. 1 - Ил.С. Свирин, П.А. Силин, В.В. Сюзев, Е.А. Зарецкая - Математическая модель взаимных блокировок. Корректное использование исключающих семафоров
Упрощенная HTML-версия
УДК 004.451.23
И л. С. С в и р и н, П. А. С и л и н,
В. В. С ю з е в, Е. А. З а р е ц к а я
МАТЕМАТИЧЕСКАЯ МОДЕЛЬ ВЗАИМНЫХ
БЛОКИРОВОК. КОРРЕКТНОЕ ИСПОЛЬЗОВАНИЕ
ИСКЛЮЧАЮЩИХ СЕМАФОРОВ
Одной из основных проблем разработки многопоточного программ-
ного обеспечения является взаимная блокировка потоков, кото-
рую чрезвычайно трудно выявить. Введена математическая мо-
дель взаимных блокировок.
E-mail:
Ключевые слова
:
многопоточное программное обеспечение, взаимные
блокировки, верификация.
При разработке многопоточного ПО возникает ряд проблем, одна
из них — это обеспечение доступа различных потоков к разделяемым
ресурсам, для решения которой предоставляются современные сред-
ства синхронизации, что, в свою очередь, приводит к возникновению
взаимных блокировок — ситуаций, когда потоки ожидают событие,
которое никогда не произойдет.
Известно несколько подходов к решению этой проблемы: динами-
ческий анализ [1, 2], статический анализ [3–6] и верификация моделей
по методу Model Checking [7–10].
Подход, представленный в настоящей статье, относится к верифи-
кации моделей. Применение такого подхода позволит разработчику
ПО избегать появления потенциальных ситуаций взаимной блокиров-
ки в процессе проектирования и разработки ПО.
Настоящая статья содержит описание математической модели, в
рамках которой формализованы основные понятия, необходимые для
определения взаимных блокировок в многопоточном ПО. В рамках
представленной модели доказан критерий отсутствия в ПО потенци-
альных ситуаций взаимных блокировок. Приведены основные поня-
тия, используемые в модели, введен математический аппарат, необ-
ходимый для доказательства критерия отсутствия в ПО потенциаль-
ных ситуаций взаимных блокировок (этот критерий доказан), а также
указаны направления, в которых можно расширить область действия
данного критерия.
Основые понятия модели.
Для моделирования ситуаций взаим-
ных блокировок в многопоточном ПО введены следующие понятия:
разделяемый ресурс, субъект доступа, средство синхронизации и вза-
имная блокировка.
Субъект доступа
моделируется на основе системы переходов, ко-
торая описывает возможные пути выполнения субъекта с точки зре-
112
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2012
