Стр. 4 - Ил.С. Свирин, П.А. Силин, В.В. Сюзев, Е.А. Зарецкая - Математическая модель взаимных блокировок. Корректное использование исключающих семафоров

выполнение (независимо от того, переходил ли субъект в состояние

ожидания или нет).

Введем понятие глобального времени системы. Глобальное время

системы нужно для установления отношения порядка между локаль-

ными временными моментами различных субъектов, которые пока ни-

как между собой не связаны. Фактически глобальное время системы

можно рассматривать как шкалу обычного физического времени (с

присоединенной к ней бесконечностью

R

∪ {∞}

), на которую ото-

бражены моменты локального времени. Соответственно, та или иная

динамика выполнения системы будет эквивалентна группе отображе-

ний из локального времени субъекта в глобальное время:

8

i

:

S

i

2

S T

i

:

{

0

, . . . , n

i

} →

R

∪ {∞}

.

Здесь под

S

понимается система субъектов, а под

T

i

— отображение

из локального времени

i

-го субъекта в глобальное время. Опишем

естественные ограничения на данную совокупность отображений.

Во-первых, никакие два различных момента локального времени

не должны соответствовать одной точке глобального времени (в рам-

ках модели считается, что события не могут происходить одновре-

менно). Из этого правила существует исключение — если

i

-й субъект

приступает к захвату

k

-го исключающего семафора и он в состоя-

нии его захватить, то

t

(

S

i

, L

k

?) =

t

(

S

i

, L

k

!)

, где

t

обозначает момент

глобального времени. Это правило связано с аксиомой модели, по-

стулирующей, что успешный захват (преодоление) средства синхро-

низации осуществляется субъектом мгновенно. Если же при попытке

захвата субъект переходит в состояние ожидания, то эти два момента

локального времени соответствуют различным моментам глобального

времени.

Во-вторых, каждое из отображений должно быть монотонным, т.е

если

τ

(

S

i

, O

1

)

< τ

(

S

i

, O

2

)

, то

t

(

S

i

, O

1

)

< t

(

S

i

, O

2

)

. Это правило отве-

чает за сохранность естественного порядка событий во времени, т.е.

если на пути выполнения одно событие предшествует другому, то и

во времени должен сохраниться тот же порядок.

Сформулируем проблему поиска потенциальных взаимных бло-

кировок в терминах локального и глобального времени. Необходимо

определить все такие совокупности последовательностей локальных

моментов времени (путей выполнения субъектов), которые допуска-

ют отображения в глобальное время (динамики выполнения системы),

отображающее часть локальных моментов времени в бесконечность,

т.е. приводящие к взаимным блокировкам.

Перейдем к определению таких путей для наиболее простого слу-

чая — систем линейных субъектов (такие субъекты будем называть

простыми), которые оперируют только с исключающими семафорами.

ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2012

115