Описание корректного поведения процессов
P
j
имеет вид
ϕ
=
j
=
m
∧
j
=1
(
g
j
⊃
♦
(
¬
r
j
))
.
Общая формулировка свойства отзывчивости может быть получе-
на, исходя из следующих соображений. Переменные
r
j
и
g
j
являют-
ся соответственно входными и выходными переменными диспетчера.
Значения переменных
r
j
устанавливаются процессами
P
1
, . . . , P
A
.
Тогда свойство отзывчивости выглядит следующим образом:
ϕ
⊃
ξ.
Свойства предшествования.
Предусмотренная реакция
(
s
(
b
(
t
0
)
⊃
w
1
P
w
2
)
∧
[(
w
2
∧
N
¬
w
2
)
⊃
N
(
w
1
P
w
2
)]
.
Пример.
Распределение ресурсов. Вернемся к рассмотренному ра-
нее примеру сдиспетчером
G
, который распределяет ресурс между
процессами
P
1
, . . . , P
t
. Простейший протокол взаимодействия между
процессом
P
i
и диспетчером определяется следующими четырьмя вы-
ражениями:
(
r
i
∧ ¬
g
i
)
⊃
N
r
i
.
(1)
Это выражение говорит о том, что если
r
i
истинна, а
g
i
ложна, т.е.
запросна ресурссо стороны
P
i
имеется, но он еще не предоставлен,
то процесс
P
i
обязан настаивать на своем требовании, подтверждая
значение
r
i
в следующем такте.
(
r
i
∧
g
i
)
⊃
N
g
i
.
(2)
Это выражение означает, что если ресурс был предоставлен про-
цессу
P
i
, то диспетчер не имеет права отнять его до тех пор, пока
пользователь не присвоит
r
i
ложное значение.
(
r
i
∧
g
i
)
⊃
N
¬
r
i
.
(3)
Это утверждение означает, что если диспетчер еще не признал
отказа от ресурса пользователя
P
i
, то
P
i
не может выставлять нового
требования.
(
¬
r
i
∧ ¬
g
i
)
⊃
N
¬
g
i
.
(4)
Это утверждение означает, что если ресурс не занят процессом
P
i
и не затребован им, то ресурс не предоставляется процессу, который
его не требует. Все это и есть описание свойства предусмотренной
реакции. Выполнение перечисленных свойств вместе со следующими
дополнительными выражениями гарантирует правильное поведение
программы:
72 ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2005. № 4
