Составители:
Действительно, 1) предикат I инвариантен относительно любого
присваивания, 2) ни одно действие присваивания в другом процессе
не может повлиять на предикат L
j
, ибо левые части отличаются от
переменных в предикате L
j
.
§14 Задача копирования массива
Эта задача нам уже встречалась. Приведем одно из ее программных
решений.
int buf, p = 0, c = 0;
# особенность: буфер может хранить лишь один элемент массива
# p — число “поставок”
# c — число “потребителей”
# n — размер массива
process Producer {
int a[n];
while (p < n) {
< await (p == c); >
# дальнейшее выполнение процесса Producer откладывается
до момента, когда выполнится условие p == c
[процесс зациклен в операторе await]
buf = a[p];
p = p + 1;
}
}
process Consumer {
int b[n];
while (c < n) {
< await (p > c); >
# выполнение процесса откладывается до момента,
когда станет p > c
[процесс зациклен в операторе await]
38
Страницы
- « первая
- ‹ предыдущая
- …
- 35
- 36
- 37
- 38
- 39
- …
- следующая ›
- последняя »
