Стр. 8 - Ил.С. Свирин, П.А. Силин, В.В. Сюзев, Е.А. Зарецкая - Математическая модель взаимных блокировок. Корректное использование исключающих семафоров
Упрощенная HTML-версия
захваченные ими исключающие семафоры — от
e
1
до
e
d
. Напомним,
что в этом случае
S
nd
ожидает на
e
1
. Рассмотрим два случая:
S
n
1
=
S
nd
и
S
n
1
6
=
S
nd
.
Пусть
S
n
1
6
=
S
nd
. Для этих субъектов выполнены условия
τ
(
S
n
1
, L
e
1
!)
< τ
(
S
n
1
, L
e
2
?)
< τ
(
S
n
1
, U
e
1
)
,
. . . . . . . . . . . . . . . . . . . . . . . . . .
τ
(
S
nd
, L
ed
!)
< τ
(
S
nd
, L
e
1
?)
< τ
(
S
nd
, U
ed
)
,
поскольку каждый из субъектов захватил первое средство синхрони-
зации и, не освободив его, приступил к захвату следующего. Эти не-
равенства являются строгой записью вышеописанного поиска. Иными
словами, выполнено
τ
(
S
n
1
, L
e
1
)
J
L
τ
(
S
nd
, L
e
1
)
.
Кроме того, существует динамика, приводящая систему в состоя-
ние, в котором указанные субъекты
S
n
1
, . . . , S
nd
являются частью вза-
имной блокировки. Рассмотрим произвольный момент времени, в ко-
торый все эти субъекты находятся в состоянии ожидания. Обозначим
его
t
. Получим
t
(
S
n
1
, L
e
1
!)
6
t
6
t
(
S
n
1
, L
e
2
?)
,
. . . . . . . . . . . . . . . . . . . . . . . . . .
t
(
S
nd
, L
ed
!)
6
t
6
t
(
S
nd
, L
e
1
?)
.
Следовательно, выполнено условие
τ
(
S
i
1
, L
j
)
J
G
τ
(
S
i
2
, L
j
)
теоре-
мы, где
i
1 =
n
1
,
i
2 =
nd
,
j
=
e
1
.
Случай
S
n
1
=
S
nd
доказывается аналогично, что завершает доказа-
тельство теоремы в одну сторону (тогда).
Докажем теорему в обратную сторону (только тогда). Итак, суще-
ствуют такие субъекты
S
i
1
и
S
i
2
и
j
-й исключающий семафор, для
которых выполнено
τ
(
S
i
1
, L
j
)
J
G
τ
(
S
i
2
, L
j
)
.
Предположим, что
i
1
6
=
i
2
. Тогда имеем
τ
(
S
i
1
, L
j
!)
< τ
(
S
i
1
, L
e
1
?)
< τ
(
S
i
1
, U
j
)
,
τ
(
S
n
1
, L
e
1
!)
< τ
(
S
n
1
, L
e
2
?)
< τ
(
S
n
1
, U
e
1
)
,
. . . . . . . . . . . . . . . . . . . . . . . . . .
τ
(
S
nd
, L
ed
!)
< τ
(
S
nd
, L
ed
+1
?)
< τ
(
S
nd
, U
ed
)
,
τ
(
S
i
2
, L
ed
+1
!)
< τ
(
S
i
2
, L
j
?)
< τ
(
S
i
2
, U
ed
+1
)
и
t
(
S
i
1
, L
j
!)
6
t
6
t
(
S
i
1
, L
e
1
?)
,
t
(
S
n
1
, L
e
1
!)
6
t
6
t
(
S
n
1
, L
e
2
?)
,
. . . . . . . . . . . . . . . . . . . . . . . . . .
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2012
119
