Составители:
29) }
30) {IC ∧ (c == n)}
31) }
В этом листинге перед каждым оператором и после него име-
ются предикаты, и каждая такая тройка {P} S {Q} истинна. Тройки
в каждом процессе образуются неп осре дствен но вокруг оператора
присваивания в каждом процессе.
Каждый процесс завершается после n итераций. Когда про-
грамма завершается, постусловия обоих процес сов истинны, так
что заключительное состояние программы удовлетворяет предика-
ту
PC ∧ (p == n) ∧ IC ∧ (c == n),
откуда следует, что массив b содержит копию массива a.
Предикаты указанных процессов не оказывают взаимного вли-
яния, ибо являются комбинациями PC и локальных предикатов, со-
ответствующих требованиям взаимного невмешательства; исклю-
чениями являются предикаты, опре дел яющие отношения между p
и c, но они не подвержены влиянию благодаря операторам await.
§15 Стратегии планирования
При наличии нескольких пр оцес сов существует несколько возмож-
ных неделимых действий. Стратегия планирования определяет,
какое из них будет выполнено следующим.
Рассмотрим программу
bool continue = true;
co while (continue);
// continue = false;
oc
Допустим, что стратегия план ировани я назначает процессор
для очередного процесса до тех пор, пока он не завершится, и лишь
затем назначается процессор для следующего процесса.
Если в данной программе назначение процессора произойдет
для первого процесса, то выполнение программы никогда не завер-
шится; а если для второго процесса, то программа завершится.
41
Страницы
- « первая
- ‹ предыдущая
- …
- 38
- 39
- 40
- 41
- 42
- …
- следующая ›
- последняя »
