одновременно достигли состояний
b
l
(
t
)
,
b
k
(
t
)
, требующих одного и
того же ресурса на период обработки состояний соответственно в
диапазонах
D
l
= (
b
l
(
t
)
, . . . , b
l
(
t
+
r
))
и
D
k
= (
b
k
(
t
)
, . . . , b
k
(
t
+
s
))
,
то только один процесс из указанных двух может получить доступ
к ресурсу для обработки своего диапазона состояний. Эти диапазо-
ны называются критическими секциями
.
Только один из процессов
может обрабатывать свою критическую секцию. Это и называется
взаимным исключением критических секций. Взаимное исключение
критических секций, таким образом, необходимо, когда двум или бо-
лее процессам необходим доступ к распределяемым переменным или
ресурсам, таким, например, как диски, и нам необходимо защититься
от взаимовлияния этих процессов или от попыток других процессов
получить доступ к тому ресурсу, с которым данный процесс уже име-
ет дело. Обозначим
π
(
D
j
)
условие, которое истинно, если процесс
P
j
находится в одном из состояний критической секции
D
j
. Тогда свой-
ство взаимного исключения критических секций
D
l
и
D
k
может быть
представлено следующим образом:
φ
(
x
(
t
0
))
⊃ ¬
(
π
(
D
l
)
∧
π
(
D
k
))
∧
t t
0
.
Это свойство означает, что всегда, когда процесс
P
l
обрабатывает
состояния автомата
A
l
из секции
D
l
, то процесс
P
k
не может обраба-
тывать состояния автомата
A
k
из секции
D
k
. Если ввести предикат:
s
(
b
(
t
))
— истинный, когда автомат находится в состоянии
b
(
t
)
, то с вой-
ство сигнального взаимного исключения можно выразить иначе:
φ
(
x
(
t
0
))
⊃ ¬
[(
s
(
b
l
(
t
))
∨
. . .
∨
s
(
b
l
(
t
+
r
)))
∧
(
s
(
b
k
(
t
))
∨
. . .
. . .
∨
s
(
b
k
(
t
+
r
)))]
∧
t t
0
.
Свойства осуществимости.
Абсолютная корректность.
Это свойство похоже на свойство кор-
ректного завершения и имеет смысл только для терминальных авто-
матов. Абсолютная корректность выражается следующим образом:
φ
(
x
(
t
0
))
⊃
♦
ϕ
(
b
(
t
e
)
, c
(
t
e
))
.
Гарантированное осуществление
[
s
(
b
(
t
))
∧
φ
(
x
(
t
))]
⊃
♦
[
s
(
b
(
t
))
∧
ϕ
(
c
(
t
))
∧
φ
(
x
(
t
))]
∧
t > t.
Доступность.
Рассмотрим снова процесс
P
j
, который имеет кри-
тическую секцию
D
j
. При изучении свойства взаимного исключения
было показано, как установить защиту для такой секции от вмешатель-
ства со стороны других процессов. Продолжающим и дополняющим
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2005. № 4 69
