Изменения

'''Слабый конъюнктивный предикат (WCP)''' – — [[Глобальные свойства системы|предикат]], имеющий вид конъюнкции локальных предикатов над состоянием каждого процесса.{{Определение|definition=Слабый конъюктивный предикат $P$ '''истинен''', если он истенен на хотя бы одном согласованном срезе}}Сложные предикаты, составленные как логическая комбинация локальных предикатов, можно представить в дизъюнктивной нормальной форме и рассмотреть как дизъюнкцию слабых конъюктивных предикатов.

Его истинность будем определятьБолее того: некоторые сложные нелокальные предикаты тоже можно так записать.Например, как истинность хотя бы если есть предикат на одном согласованном срезебулевских переменных из разных процессов: $x = y$, то можно записать формулу: $(x = 0 \land y = 0) \lor (x = 1 \land y = 1)$.

'''Локальный предикатТеорема''' – : если слабый конъюктивный предикат по состоянию одного процесса. Напримерверен хоть на одном согласованном срезе, если у процесса есть состояние то в множестве согласованных срезов с верным предикатом существует наименьший элемент (переменнаят.е. который вкладывается во все остальные) x. Это следует из того, то локальным что пересечение согласованных срезов является согласованным срезом: пересечение всех срезов с верными предикатом может быть (x < 0)будет срезом и, более того, в каждом процессе граница этого среза включается хотя бы в один из исходных, следовательно, на границе в каждом процессе соответствующий локальный предикат будет верен.

Используется для нежелательных предикатов=== Примеры ===Позволяет обнаружить некоторые нежелательные предикаты.Обнаруживает ошибки, например, классическая проблема взаимного исключениякоторые могли бы быть скрыты в определенном запуске из-за race conditions.

Обнаруживает ошибкиНапример, которые могли бы быть скрыты классическую проблема взаимного исключения для двух процессов: локальный предикат "процесс в определенном запуске из-за race conditionsкритической секции".Если есть срез, в котором два процесса в критической секции, то всё плохо.А если такого нет, то любые две критические секции упорядочены.

Пример Ещё пример WCP предиката: “в системе нет координатора”, причем локальное условие – “я не координатор”.