Теория распараллеливания и синхронизация. Демьянович Ю.К - 100 стр.

UptoLike

ВУЗ: 

СПбГУ | Санкт-Петербург

Составители: 

Рубрика: 

вообще никогда не получить этот ресурс; естественно, что в этом
случае вся задача не будет выполнена.
Пусть free — булевская переменная, прин им ающая з начение
TRUE, когда ресурс доступен, а FALSE, когда он занят. Для простоты
будем считать, что все запросы имеют различные значе ния time.
Обозначим pairs — множество пар (time, id), упорядоченное по
возрастанию параметра time; тогда глобальный инвариант метода
“кратчайшее расстояние” может быть записан в виде
INV : ([pairs — упорядоченный набор])∧
(free ⇒ (pairs == ∅));
таким образом, pairs — упорядоченный набор, и если free = TRUE,
то pairs — пустой набор.
Вначале предикат INV истинен, т.к. pairs — пустое множество,
и free = TRUE.
Поскольку запрос может быть удовлетворен, как только ресурс
станет доступным, то можно предложить такое решение задачи о
распределении ресурсов по упомянутому методу:
bool free = true; #bool free разделяемая переменная
request(time, id) : < await (free) free = false; >
release( ) : < free = true; >
Операции request/release реализуем следующим способом:
request(time, id) :
P(e);
if (!free) DELAY;
free = false;
SIGNAL;
release( );
P(e);
free = true;
SIGNAL;
В данном случае во фрагменте DELAY процесс должен
101

Страницы