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

Математическая модель взаимных блокировок. Модель вза-
имных блокировок в многопоточном ПО опирается на четыре класса
объектов предметной области:
• разделяемый ресурс — информационный или функциональный
объект, к которому возможен доступ из разных потоков;
• субъект доступа — поток, выполняющий доступ к разделяемому
ресурсу;
• средство синхронизации — средство, ограничивающее доступ
субъектов к разделяемым ресурсам посредством перевода субъекта в
состояние ожидания доступности разделяемого ресурса;
• взаимная блокировка — ситуация, характеризующаяся тем, что
группа субъектов находится в состоянии ожидания и не может быть
выведена из него, независимо от действий других субъектов системы.
Субъект доступа моделируется на основе системы переходов, т.е.
субъект отождествляется с совокупностью своих цепочек выполне-
ния. Данная совокупность описывает всевозможные пути выполнения
субъекта с точки зрения взаимодействия со средствами синхронизации
от состояния покоя до завершающего состояния, отождествляемого с
состоянием покоя.
Отождествление состояния покоя и завершающего состояния ха-
рактеризует одно из фундаментальных свойств модели. В ней субъек-
ты доступа зациклены, т.е., если субъект завершил свое выполнение
по некоторому пути выполнения, он не обязательно будет ожидать за-
вершения выполнения остальных субъектов доступа, а может снова
начать выполнение по одному из путей.
Все цепочки выполнения субъекта линейны. Однако для отобра-
жения всевозможных цепочек выполнения, субъект может включать в
себя точки ветвления и точки зацикливания (согласно структурной те-
ореме Э. Дейкстры [11]). Отметим следующие особенности структур
ветвления и циклических структур:
• условие, по которому в точке ветвления осуществляется выбор
той или иной ветви выполнения, опускается в данной модели, посколь-
ку является несущественным с точки зрения взаимодействия субъекта
со средствами синхронизации. Предполагается, что при выполнении
субъекта может быть выбрана произвольная из ветвей;
• число итераций цикла, соответствующего точке зацикливания, не
специфицируется, т.е. считается, что субъект может выполнить произ-
вольное конечное число итераций цикла (в том числе нулевое). Данное
условие объясняется тем, что число итераций цикла может варьиро-
ваться при разных выполнениях субъекта (например, число итераций
цикла соответствует числу необработанных на данный момент запро-
сов). Данное же условие позволяет учитывать эту особенность, что
дает модели необходимую общность.
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2012 97