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

UptoLike

ВУЗ: 

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

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

Рубрика: 

Предикат PC в начальном состоянии является истинным, по-
скольку p и c равны 0. Процесс доказательства имеет вид:
1) int buf, p = 0, c = 0;
2) {PC : (c <= p <= c + 1) ∧ (a[0 : n − 1] == A[0 : n − 1])∧
3)
(p == c + 1) ⇒ (buf == A[p − 1])
}
4) process Producer {
5) int a[n]; # предполагается, что a[i] инициализирован
с помощью A[i]
6) {IP : PC ∧ (p <= n)}
7) while (p < n) {
8) {PC ∧ (p < n)}
9) < await (p == c); > # ожидание опустошения буфера
10) {PC ∧ (p < n) ∧ (p == c)}
11) buf = a[p];
12) {PC ∧ (p < n) ∧ (p == c) ∧ (buf == A[p])}
13) p = p + 1;
14) {IP}
15) }
16) {PC ∧ (p == n)}
17) }
18) process Consumer {
19) int b[n];
20) {IC : PC ∧ (c <= n) ∧ (b[0 : c − 1] == A[0 : c − 1])}
21) while (c < n) {
22) {IC ∧ (c < n)}
23) < await (p > c); > # ожидание заполнения буфера
24) {IC ∧ (c < n) ∧ (p > c)}
25) b[c] = buf;
26) {IC ∧ (c < n) ∧ (p > c) ∧ (b[c] == A[c])}
27) c = c + 1;
28) {IC}
40

Страницы