Составители:
b[c] = buf;
c = c + 1;
}
}
Условие синхронизации процессов имеет вид
PC : c <= p <= c + 1;
это означает, что Producer делает число “поставок” столько или на
единицу больше числа “потреблений”.
Замечание. Здесь представлен лишь фрагмент программы;
можно считать, что процессы Producer и Consumer выполняются
каждый на своем вычислительном модуле параллельной ВС.
Процессы Producer и Consumer по-очереди получают доступ к
переменной buf. Сначала Producer помещает первый элемент мас-
сива a в переменную buf, затем Cinsumer извлекает его, а Producer
помещает в buf следующий элемент массива и т.д.
В переменных p и c ведется подсчет числа помещенных и из-
влеченных эл ем ентов соответственно.
Для синхронизации доступа к переменной buf используются
операторы await. Когда выполняется условие p == c буфер пуст
(последний помещенный в него элемент извлечен). Когда выполня-
ется условие p > c, буфер заполнен.
Предположим, что сначала элементы массива a[j] содержат
значения A[j] (здесь A[j] — целые числа). Наша цель — доказать,
что при условии завершения программы значения элементов масси-
ва b[n] будут совпадать с A[n], т.е. со значениями элементов массива
a[n].
Введем глобальный инвариант
PC : (c <= p <= c + 1) ∧ (a[0 : n − 1] = A[0 : n − 1])
∧
(p == c + 1) ⇒ (buf == A[p − 1])
.
Поскольку процессы чередуют доступ к buf, то в любой момент
значение p равно c или больше c на 1. Массив a[n] не изменяется,
и поэтому значением a[i] всегда является A[i]; наконец, если p на
единицу больше, чем c, то буфер содержит A[p − 1].
39
Страницы
- « первая
- ‹ предыдущая
- …
- 36
- 37
- 38
- 39
- 40
- …
- следующая ›
- последняя »
