t
(
S
nd
, L
ed
!)
6
t
6
t
(
S
nd
, L
ed
+1
?)
,
t
(
S
i
2
, L
ed
+1
!)
6
t
6
t
(
S
i
2
, L
j
?)
.
Второе условие означает, что каждый из субъектов подсистемы
{
S
i
1
, S
n
1
, . . . , S
nd
, S
i
2
}
не может захватить исключающий семафор, на-
ходящийся в правой части неравенств для этого субъекта. Докажем это
утверждение на примере субъекта
S
i
1
. Итак,
S
i
1
не может захватить
исключающий семафор
e
1
, поскольку тот уже захвачен субъектом
S
n
1
.
Для того чтобы субъект
S
n
1
освободил исключающий семафор
e
1
, ему
по первому условию необходимо захватить исключающий семафор
e
2
,
который удерживается субъектом
S
n
2
. Переходя по цепочке, получаем,
что субъекту
S
i
2
, чтобы освободить исключающий семафор
e
d
+1
, не-
обходимо первоначально захватить по первому условию
j
-й семафор,
который он захватить не может (с этого начинался проход по цепочке).
Получается, что ни один из субъектов не может захватить исключа-
ющий семафор из правой части второй группы неравенств (второе
условие). Это свойство не зависит от действий остальных субъектов.
Случай
i
1 =
i
2
доказывается аналогично. Теорема доказана и в
обратную сторону.
I
Выводы.
Рассмотрена математическая модель взаимных блоки-
ровок, сочетающая в себе формализм и наглядность, необходимые
для построения на ее основе системы формальных правил коррект-
ного использования средств синхронизации, понятной конечному раз-
работчику ПО. В рамках модели доказан критерий наличия ситуаций
взаимной блокировки в системе линейных субъектов, оперирующих с
исключающими семафорами. Поскольку из глобального меньше сле-
дует локальное меньше, то из критерия может быть получено важное
следствие, существенно упрощающее механизм доказательства отсут-
ствия в модели ПО потенциальных ситуаций взаимной блокировки.
Следствие.
Если в системе субъектов
S
нет таких субъектов
S
i
1
и
S
i
2
и
j
-го исключающего семафора, для которых выполнено
τ
(
S
i
1
, L
j
)
J
L
τ
(
S
i
2
, L
j
)
, то в системе нет потенциальных ситуаций
взаимной блокировки. Как и ранее, возможно,
i
1 =
i
2
.
Дальнейшая работа будет заключаться в расширении модели для
случая сигнальных переменных и субъектов произвольной структу-
ры с последующим получением из данной модели системы правил
корректного использования средств синхронизации.
СПИСОК ЛИТЕРАТУРЫ
1. S a v a g e S., B u r r o w s M., N e l s o n G., S o b a l v a r r o P. and
A n d e r s o n T. Eraser: A dynamic data race detector for multi-threaded programs
// Proceedings of the 16th ACM Symposium on Operating Systems Principles. –
1997. – P. 27–37.
120
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2012
1,2,3,4,5,6,7,8 10