Стр. 6 - Ил.С. Свирин, П.А. Силин, В.В. Сюзев - Математическая модель многопоточной программы и правила безопасного многопоточного программирования
Упрощенная HTML-версия
τ
(
S
k
,
L
i
)
J
L
τ
(
S
k
,
L
j
), если в цепочке выполнения
k
-го субъекта
j
-й
семафор захватывается до того, как
i
-й семафор отпущен после захва-
та.
Расширим введенную операцию. Будем сравнивать исключающие
семафоры, принадлежащие различным субъектам. Отметим, что
i
-й
исключающий семафор
k
-го субъекта локально меньше
j
-го семафо-
ра
m
-го субъекта, и запишем
τ
(
S
k
,
L
i
)
J
L
τ
(
S
m
,
L
j
)
, если существует
такое натуральное
n
>
1
и такие субъекты S
x
(1)
, . . . ,
S
x
(
n
−
1)
и исключа-
ющие семафоры
y
(1)
, . . . , y
(
n
−
1)
, что
τ
(
S
k
,
L
i
)
J
L
τ
(
S
k
,
L
y
(1)
)
,
τ
(
S
x
(1)
,
L
y
(1)
)
J
L
τ
(
S
x
(1)
,
L
y
(2)
)
,
. . . . . . . . . . . . . . . . . . . . .
τ
(
S
x
(
n
−
1)
,
L
y
(
n
−
1)
)
J
L
τ
(
S
x
(
n
−
1)
,
L
y
(
n
)
)
,
τ
(
S
m
,
L
y
(
n
)
)
J
L
τ
(
S
m
,
L
j
)
,
где для каждого из субъектов операция
J
L
понимается в точности так,
как была введена ранее.
Отметим, что
r
-й исключающий семафор
m
-го субъекта локаль-
но меньше
j
-й сигнальной переменной
m
-го субъекта, и запишем
τ
(
S
m
,
L
r
)
J
L
τ
(
S
m
,
A
j
(
W
j
))
, если взаимодействие с оператором ожи-
дания
j
-й сигнальной переменной происходит после захвата
r
-го ис-
ключающего семафора и до его отпускания.
Считаем, что в системе субъектов S
=
{
S
1
, . . . ,
S
n
}
i
-я сигнальная
переменная с памятью (без памяти) находится под локальным влия-
нием
j
-й переменной с памятью (без памяти), если либо существует
субъект S
k
из S, цепочка выполнения которого содержит оператор
установки
i
-й сигнальной переменной с памятью (оператор отправки
или широковещания для переменной без памяти) и оператор ожидания
j
-й переменной с памятью (без памяти), либо существует субъект S
k
из S, цепочка выполнения которого содержит оператор отправки
i
-й
сигнальной переменной с памятью (без памяти) и оператор захвата
p
-
го исключающего семафора, причем выполнены следующие условия:
τ
(
S
k
,
L
p
)
J
L
τ
(
S
m
,
L
r
)
и
τ
(
S
m
,
L
r
)
J
L
τ
(
S
m
,
A
j
(
W
j
))
.
В этом случае запишем
τ
(
S
k
,
P
i
(
E
i
,
B
i
))
H
L
τ
(
S
m
,
A
j
(
W
j
))
, где воз-
можно
m
=
k
.
Предположим, что есть система субъектов S
=
{
S
1
, . . . ,
S
n
}
, взаи-
модействующих с сигнальными переменными (с памятью и без памя-
ти)
{
1
, . . . , k
}
. Система субъектов S называется локально слабо упоря-
доченной по сигнальным переменным, если для любого подмножества
i
1
, . . . , i
j
из
{
1
, . . . , k
}
сигнальных переменных не существует такого
100
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2012
