Стр. 5 - Ил.С. Свирин, П.А. Силин, В.В. Сюзев - Математическая модель многопоточной программы и правила безопасного многопоточного программирования

• оператором отправки (сигнала) для сигнальной переменной без
памяти. Его обозначают окружностью, внутри которой изображен сим-
вол E и номер сигнальной переменной без памяти;
• оператором широковещания для сигнальной переменной без па-
мяти. Его обозначают окружностью, внутри которой изображен сим-
вол B и номер сигнальной переменной без памяти.
Сигнальная переменная с памятью — это средство синхронизации,
имеющее целый неотрицательный счетчик. Взаимодействие потока с
сигнальной переменной с памятью приводит к уменьшению счетчи-
ка, если счетчик в момент взаимодействия уже равен нулю, то поток
переходит в состояние ожидание до тех пор, пока счетчик не будет
увеличен другим потоком.
Сигнальная переменная с памятью описывается двумя оператора-
ми взаимодействия:
• оператором ожидания на сигнальной переменной с памятью. Он
обозначается окружностью, внутри которой изображен символ A и
номер сигнальной переменной с памятью;
• оператором установки значения для сигнальной переменной с
памятью. Он обозначается окружностью, внутри которой изображен
символ P и номер сигнальной переменной без памяти.
Время выполнения субъектом оператора взаимодействия полагает-
ся равным нулю, поскольку не является существенным параметром с
точки зрения модели.
Взаимные блокировки бывают двух типов:
• полные — когда во взаимную блокировку вовлечены все субъекты
данной системы;
• частичные — когда во взаимную блокировку вовлечена только
часть субъектов системы.
Тем не менее частичные блокировки являются не менее опасными
по сравнению с полными, поскольку, как отмечалось ранее, субъекты,
попавшие в ситуацию взаимной блокировки, не могут быть выведены
из нее независимо от действий других субъектов системы. В дальней-
шем будем использовать обобщенное понятие взаимной блокировки,
включающее в себя ситуации полной и частичной блокировок.
Разделяемые ресурсы присутствуют в данной модели неявно. Они
определяются совокупностью средств синхронизации, обеспечиваю-
щих синхронный доступ субъектов к разделяемым ресурсам.
Теперь перейдем непосредственно к модели. Формализуем есте-
ственное отношение порядка (“до”–“после”), возникающее между дву-
мя операторами вдоль одной цепочки выполнения субъекта. Отметим,
что i-й и j -й исключающие семафоры сравнимы по k -му субъекту,
причем i-й исключающий семафор локально меньше j-го, и запишем
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2012 99