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