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