Составители:
Часто множество ссылок процесса совпадает с объединением
множества записи и множества чтения.
По отношению к взаимному вмешательству критические пере-
менные — это переменные в утверждениях.
В простейшем случае (см. параграф 5) если множество запи-
си одного процесса не пересе кается с множеством ссылок другого
процесса и наоборот, то эти процессы не могут влиять друг на дру-
га.
Например, для программы
co x = x + 1; // y = y + 1; oc
имеем
{x == 0} x = x + 1 {x == 1}
{y == 0} y = y + 1 {y == 1}
Каждый процесс имеет один оператор присваивания и два утвер-
ждения: нужно доказать 4 теоремы взаимного невмешательства.
Каждая из них тривиально истинна, ибо процессы ссылаются на
разные переменные и подстановки в аксиоме присваивания будут
пустыми.
Непересекающиеся множества запис и и ссылок характерны
для итерационных процессов (например, для процессов, связанных
с перемножением матриц, с исследованием разных ветвей дерева, с
транзакциями в различных частях базы данных и т.д.).
§12 Ослабленные утверждения
Ослабленное утверждение допускает больше состояний програм-
мы, чем утверждение, которое могло бы быть истинным для изо-
лированного процесса.
В качестве примера рассмотрим приведенную ранее програм-
му:
{x == 0}
co{x == 0 ∨ x == 2}
< x = x + 1; >
{x == 1 ∨ x == 3}
35
Страницы
- « первая
- ‹ предыдущая
- …
- 32
- 33
- 34
- 35
- 36
- …
- следующая ›
- последняя »
