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