Слабый конъюнктивный предикат (WCP) — различия между версиями
Yeputons (обсуждение | вклад) |
м (rollbackEdits.php mass rollback) |
||
| (не показано 5 промежуточных версий 4 участников) | |||
| Строка 3: | Строка 3: | ||
{{Определение | {{Определение | ||
|definition= | |definition= | ||
| − | Слабый | + | Слабый конъюнктивный предикат $P$ '''истинен''', если он истинен на хотя бы одном согласованном срезе |
}} | }} | ||
Сложные предикаты, составленные как логическая комбинация локальных предикатов, можно представить в дизъюнктивной нормальной форме и рассмотреть как дизъюнкцию слабых конъюктивных предикатов. | Сложные предикаты, составленные как логическая комбинация локальных предикатов, можно представить в дизъюнктивной нормальной форме и рассмотреть как дизъюнкцию слабых конъюктивных предикатов. | ||
| Строка 9: | Строка 9: | ||
Более того: некоторые сложные нелокальные предикаты тоже можно так записать. | Более того: некоторые сложные нелокальные предикаты тоже можно так записать. | ||
Например, если есть предикат на булевских переменных из разных процессов: $x = y$, то можно записать формулу: $(x = 0 \land y = 0) \lor (x = 1 \land y = 1)$. | Например, если есть предикат на булевских переменных из разных процессов: $x = y$, то можно записать формулу: $(x = 0 \land y = 0) \lor (x = 1 \land y = 1)$. | ||
| + | |||
| + | '''Теорема''': если слабый конъюктивный предикат верен хоть на одном согласованном срезе, то в множестве согласованных срезов с верным предикатом существует наименьший элемент (т.е. который вкладывается во все остальные). Это следует из того, что пересечение согласованных срезов является согласованным срезом: пересечение всех срезов с верными предикатом будет срезом и, более того, в каждом процессе граница этого среза включается хотя бы в один из исходных, следовательно, на границе в каждом процессе соответствующий локальный предикат будет верен. | ||
=== Примеры === | === Примеры === | ||
Текущая версия на 19:08, 4 сентября 2022
Слабый конъюнктивный предикат (WCP) — предикат, имеющий вид конъюнкции локальных предикатов над состоянием каждого процесса.
| Определение: |
| Слабый конъюнктивный предикат $P$ истинен, если он истинен на хотя бы одном согласованном срезе |
Сложные предикаты, составленные как логическая комбинация локальных предикатов, можно представить в дизъюнктивной нормальной форме и рассмотреть как дизъюнкцию слабых конъюктивных предикатов.
Более того: некоторые сложные нелокальные предикаты тоже можно так записать. Например, если есть предикат на булевских переменных из разных процессов: $x = y$, то можно записать формулу: $(x = 0 \land y = 0) \lor (x = 1 \land y = 1)$.
Теорема: если слабый конъюктивный предикат верен хоть на одном согласованном срезе, то в множестве согласованных срезов с верным предикатом существует наименьший элемент (т.е. который вкладывается во все остальные). Это следует из того, что пересечение согласованных срезов является согласованным срезом: пересечение всех срезов с верными предикатом будет срезом и, более того, в каждом процессе граница этого среза включается хотя бы в один из исходных, следовательно, на границе в каждом процессе соответствующий локальный предикат будет верен.
Примеры
Позволяет обнаружить некоторые нежелательные предикаты. Обнаруживает ошибки, которые могли бы быть скрыты в определенном запуске из-за race conditions.
Например, классическую проблема взаимного исключения для двух процессов: локальный предикат "процесс в критической секции". Если есть срез, в котором два процесса в критической секции, то всё плохо. А если такого нет, то любые две критические секции упорядочены.
Ещё пример WCP предиката: “в системе нет координатора”, причем локальное условие – “я не координатор”.
