Стр. 6 - Ил.С. Свирин, П.А. Силин, В.В. Сюзев, Е.А. Зарецкая - Математическая модель взаимных блокировок. Корректное использование исключающих семафоров
Упрощенная HTML-версия
Рис. 2. Пример системы субъектов
щего семафора
m
-го субъекта, и запишем
τ
(
S
k
, L
i
)
J
G
τ
(
S
m
, L
j
)
, если,
во-первых,
τ
(
S
k
, L
i
)
J
L
τ
(
S
m
, L
j
)
, т.е. существует такое натуральное
n
>
1
и такие субъекты
S
x
(1)
, . . . , S
x
(
n
−
1)
и исключающие семафоры
y
(1)
, . . . , y
(
n
−
1)
, что
τ
(
S
k
, L
i
)
J
L
τ
(
S
k
, L
y
(1)
)
,
τ
(
S
x
(1)
, L
y
(1)
)
J
L
τ
(
S
x
(1)
, L
y
(2)
)
,
. . . . . . . . . . . . . . . . . . . . . . . . . .
τ
(
S
x
(
n
−
1)
, L
y
(
n
−
1)
)
J
L
τ
(
S
x
(
n
−
1)
, L
y
(
n
)
)
,
τ
(
S
m
, L
y
(
n
)
)
J
L
τ
(
S
m
, L
j
);
во-вторых, существует набор операторов
T
для этих субъектов и мо-
мент глобального времени
t
такие, что выполняются следующие усло-
вия:
t
(
S
k
, L
i
!)
6
t
6
t
(
S
k
, L
y
(1)
?)
,
t
(
S
x
(1)
, L
y
(1)
!)
6
t
6
t
(
S
x
(1)
, L
y
(2)
?)
,
. . . . . . . . . . . . . . . . . . . . . . . . . .
t
(
S
x
(
n
−
1)
, L
y
(
n
−
1)
!)
6
t
6
t
(
S
x
(
n
−
1)
, L
y
(
n
)
?)
,
t
(
S
m
, L
y
(
n
)
!)
6
t
6
t
(
S
m
, L
j
?)
.
Второе условие завершает определение. Назовем исключающие
семафоры, между которыми устанавливается операция глобального
меньше, глобально сравнимыми.
Рассмотрим подробнее второе условие. Фактически оно означа-
ет, что существует динамика выполнения системы, которая приводит
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2012
117
