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

UptoLike

p = p + 1;
}
}
process Consumer {
int b[n];
while (c < n) {
< await (p > c); >
b[c] = buf;
c = c + 1;
}
}
Процессы Producer и Consumer получают доступ к переменной
buf по очереди, а разделяемые переменные p и c служат счетчи-
ками помещенных и извлеченных элементов (соответственно). На-
чальные значения этих переменных 0.
Приведенная выше формула PC : c <= p <= c + 1 означает, что
Producer может поместить в буфер столько же, сколько забирает
Consumer или Producer может поместить на единицу больше, чем
забирает Consumer.
Процесс находится в состоянии активного ожидания: он за-
нят проверкой условия в операторе await, что можно рассматри-
вать как повторение цикла до тех пор, пока упомянутое условие не
будет выполнено.
§9 Обзор логики программирования (ЛП)
Логика программирования является формальной логической систе-
мой, позволяющей устанавливать и обосновывать свойства про-
грамм.
В логике программированиея имеются:
символы,
формулы,
аксиомы,
правила вывода.
К символам относятся:
29