Стр. 5 - Ил.С. Свирин, П.А. Силин, В.В. Сюзев, Е.А. Зарецкая - Математическая модель взаимных блокировок. Корректное использование исключающих семафоров
Упрощенная HTML-версия
Введем следующие определения.
Однородным субъектом будем называть такой субъект, в котором
логика использования исключающих семафоров соответствует сле-
дующему правилу: если
τ
(
S
k
, L
i
!)
< τ
(
S
k
, L
j
?)
< τ
(
S
k
, U
i
)
, тогда
τ
(
S
k
, U
j
)
< τ
(
S
k
, U
i
)
, причем под операторами освобождения
U
i
и
U
j
понимаются первые встретившиеся после операторов захвата
L
i
?
и
L
j
?
операторы. Перефразировать это определение можно следую-
щим образом, если после захвата
i
-го исключающего семафора до его
освобождения можно захватить
j
-й исключающий семафор, то снача-
ла должен быть освобожден
j
-й семафор и только затем
i
-й, иными
словами, “первый захвачен — последний освобожден”.
В дальнейшем будем рассматривать только однородные субъекты.
Условие
τ
(
S
k
, L
i
!)
< τ
(
S
k
, L
j
?)
< τ
(
S
k
, U
i
)
— чрезвычайно важное
для спецификации ситуаций взаимной блокировки, поэтому введем
специальное обозначение:
τ
(
S
k
, L
i
)
J
L
τ
(
S
k
, L
j
)
и будем говорить,
что
i
-й и
j
-й исключающие семафоры сравнимы по
k
-му субъекту,
причем
i
-й исключающий семафор локально меньше
j
-го. Символ
L
указывает на локальную природу данного сравнения.
Расширим введенную операцию. Сравним исключающие семафо-
ры. Отметим, что
i
-й исключающий семафор
k
-го субъекта локально
меньше
j
-го семафора
m
-го субъекта и
τ
(
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
)
.
Поясним определение примером на рис. 2. Для этой системы субъ-
ектов выполнено соотношение
τ
(
S
1
, L
1
)
J
L
τ
(
S
4
, L
5
)
, поскольку су-
ществуют субъекты
S
2
и
S
3
и исключающие семафоры 2, 3, 4 такие,
что выполнены следующие соотношения:
τ
(
S
1
, L
1
)
J
L
τ
(
S
1
, L
2
)
,
τ
(
S
2
, L
2
)
J
L
τ
(
S
2
, L
3
)
,
τ
(
S
3
, L
3
)
J
L
τ
(
S
3
, L
4
)
,
τ
(
S
4
, L
4
)
J
L
τ
(
S
4
, L
5
)
.
Введем понятие “глобального меньше”. Будем говорить, что
i
-й ис-
ключающий семафор
k
-го субъекта глобально меньше
j
-го исключаю-
116
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2012
