Слабый конъюнктивный предикат (WCP) — различия между версиями
Yeputons (обсуждение | вклад) |
|||
| Строка 1: | Строка 1: | ||
[[Категория: Параллельное программирование]] | [[Категория: Параллельное программирование]] | ||
| − | '''Слабый конъюнктивный предикат (WCP)''' | + | '''Слабый конъюнктивный предикат (WCP)''' — [[Глобальные свойства системы|предикат]], имеющий вид конъюнкции локальных предикатов над состоянием каждого процесса. |
| + | {{Определение | ||
| + | |definition= | ||
| + | Слабый конъюктивный предикат $P$ '''истинен''', если он истенен на хотя бы одном согласованном срезе | ||
| + | }} | ||
| + | Сложные предикаты, составленные как логическая комбинация локальных предикатов, можно представить в дизъюнктивной нормальной форме и рассмотреть как дизъюнкцию слабых конъюктивных предикатов. | ||
| − | + | === Примеры === | |
| − | + | Позволяет обнаружить некоторые нежелательные предикаты. | |
| − | + | Обнаруживает ошибки, которые могли бы быть скрыты в определенном запуске из-за race conditions. | |
| − | |||
| − | |||
| − | + | Например, классическую проблема взаимного исключения: локальный предикат "процесс в критической секции". | |
| + | Если есть срез, в котором два процесса в критической секции, то всё плохо. | ||
| + | А если такого нет, то любые две критические секции упорядочены. | ||
| − | + | Ещё пример WCP предиката: “в системе нет координатора”, причем локальное условие – “я не координатор”. | |
Версия 21:22, 2 июня 2019
Слабый конъюнктивный предикат (WCP) — предикат, имеющий вид конъюнкции локальных предикатов над состоянием каждого процесса.
| Определение: |
| Слабый конъюктивный предикат $P$ истинен, если он истенен на хотя бы одном согласованном срезе |
Сложные предикаты, составленные как логическая комбинация локальных предикатов, можно представить в дизъюнктивной нормальной форме и рассмотреть как дизъюнкцию слабых конъюктивных предикатов.
Примеры
Позволяет обнаружить некоторые нежелательные предикаты. Обнаруживает ошибки, которые могли бы быть скрыты в определенном запуске из-за race conditions.
Например, классическую проблема взаимного исключения: локальный предикат "процесс в критической секции". Если есть срез, в котором два процесса в критической секции, то всё плохо. А если такого нет, то любые две критические секции упорядочены.
Ещё пример WCP предиката: “в системе нет координатора”, причем локальное условие – “я не координатор”.
