эти потоки в некоторое общее состояние, характеризующееся тем, что
первый исключающий семафор из двух уже захвачен, а второй — еще
нет.
Как следует из определений, условие
τ
(
S
k
, L
i
)
J
G
τ
(
S
m
, L
j
)
вле-
чет условие
τ
(
S
k
, L
i
)
J
L
τ
(
S
m
, L
j
)
. Обратная импликация не верна,
поскольку некоторый набор локальных состояний может не реализо-
вываться одновременно глобально.
Докажем теорему о взаимных блокировках системы простых субъ-
ектов, оперирующих с исключающими семафорами.
Теорема.
В системе простых субъектов
S
=
{
S
1
, . . . , S
k
}
, опе-
рирующих с исключающими семафорами, существует динамика вы-
полнения системы, приводящая ее в ситуацию взаимной блокировки
субъектов, тогда и только тогда, если существуют такие субъек-
ты
S
i
1
и
S
i
2
и
j
-й исключающий семафор, для которых выполнено
τ
(
S
i
1
, L
j
)
J
G
τ
(
S
i
2
, L
j
). Возможно,
i
1 =
i
2
.
Доказательство.
Пусть в системе простых субъектов
S
=
{
S
1
, . . .
. . . , S
k
}
существует динамика, приводящая систему в ситуацию взаим-
ной блокировки. Это означает, что часть субъектов системы (
S
n
1
, . . .
. . . , S
np
) находится в состоянии ожидания при попытке захвата некото-
рого исключающего семафора. Обозначим множество исключающих
семафоров, на которых ожидают субъекты, через
e
1
, . . . , e
f
.
Из определения взаимной блокировки следует, что каждый из ис-
ключающих семафоров
e
1
, . . . , e
f
должен быть захвачен одним из субъ-
ектов
S
n
1
, . . . , S
np
, участвующих во взаимной блокировке.
Рассмотрим субъект, захвативший
e
1
, он принадлежит
{
S
n
1
, . . .
. . . , S
np
}
, обозначим его
S
r
1
; так как он является участником взаимной
блокировки, то он ожидает на исключающем семафоре из множества
{
e
1
, . . . , e
f
}
, обозначим его через
q
1
. Если
e
1
=
q
1
, то остановим про-
цесс поиска, в противном случае — продолжим. Рассмотрим субъект
S
r
1
2 {
S
n
1
, . . . , S
np
}
. Пусть он ожидает на исключающем семафоре
q
2
2 {
e
1
, . . . , e
f
}
. Если
q
2
=
q
1
или
q
2
=
e
1
остановим поиск, в про-
тивном случае — продолжим. Множество
{
e
1
, . . . , e
f
}
конечно и его
мощность не превосходит числа субъектов, участвующих во взаимной
блокировке, поскольку на каждом из средств синхронизации ожидает
как минимум один субъект. Следовательно, продолжая процесс поиска,
рано или поздно найдем субъект, ожидающий на исключающем сема-
форе, который уже был рассмотрен в этом поиске (т.е. уже захвачен
каким-то из ранее рассмотренных субъектов). Пусть это будет субъект
S
nu
, ожидающий на исключающем семафоре
e
w
, где
e
w
=
e
y
, который
захвачен
S
nx
. Без ограничения общности перенумеруем субъекты и
исключающие семафоры таким образом, что рассмотренная цепочка
субъектов от
S
nx
до
S
nu
получит номера по порядку от
S
n
1
до
S
nd
, а
118
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2012
1,2,3,4,5,6 8,9,10