состояния системы, при котором каждый оператор отправки, широко-
вещания и установки E
u
(
B
u
,
P
u
)
, где
u
из
{
i
1
, . . . , i
j
}
, находился бы в
отношении локальной зависимости
τ
(
S
p
,
E
u
(
B
u
))
H
L
τ
(
S
q
,
W
v
(
A
v
))
, где
v
из
{
i
1
, . . . , i
j
}
, т.е. все операторы широковещания, отправки и уста-
новки из данного множества одновременно находятся под локальным
влиянием операторов ожидания из данного множества. Кроме того,
в системе не существует сигнальных переменных, для которых при-
сутствуют только операторы ожидания, но нет операторов отправки,
широковещания или установки.
Введены все необходимые определения для формулировки основ-
ного результата математической модели взаимных блокировок, кото-
рый является логическим основанием всех правил корректного ис-
пользования средств синхронизации на основе данной модели.
Теорема
.
Пусть имеется система субъектов S
=
{
S
1
, . . . ,
S
n
}
с
точками ветвления и точками зацикливания. Проделаем для субъек-
тов данной системы линеаризацию по точкам зацикливания. Полу-
чившуюся систему обозначим S
0
. Рассмотрим все различные систе-
мы субъектов, составленные по следующему принципу
:
на
i
-м месте
в системе стоит субъект из декомпозиции S
0
i
. Предположим, что для
каждой системы S
00
из этого множества выполнены два условия
:
1)
для любого исключающего семафора
(
например,
j
-го
)
не выпол-
няются соотношения вида
τ
(
S
00
k
,
L
j
)
J
L
τ
(
S
00
m
,
L
j
));
2)
система S
00
слабо локально упорядочена относительно сигналь-
ных переменных. Тогда в основной системе S нет потенциальных си-
туаций взаимной блокировки.
Под линеаризацией понимается замена цикла точкой ветвления,
где одна ветвь содержит цикл точки ветвления, а другая не содержит
операторов взаимодействия.
Под декомпозицией субъекта с точками ветвления понимается мно-
жество его цепочек выполнения, каждая из которых рассматривается
как линейный субъект.
Перейдем к правилам корректного использования средств синхро-
низации. Правила получены теоретическим путем на основе матема-
тической модели взаимных блокировок. Фактически правила предста-
вляют собой набор относительно простых конструкций, применение
которых в процессе разработки ПО позволяет получать системы, обла-
дающие достаточными (как было показано в модели, описанной выше)
для отсутствия блокировок свойствами.
Базовые правила
, которые необходимо соблюдать независимо от
степени мастерства разработчика:
Правило 1.
Все субъекты системы должны быть однородными
с точки зрения логики использования исключающих семафоров, т.е.
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2012
101
1,2,3,4,5,6 8,9,10,11,12,13,14,15,16,...17