Слабый конъюнктивный предикат (WCP) — различия между версиями

Материал из Викиконспекты
Перейти к: навигация, поиск
Строка 14: Строка 14:
 
Обнаруживает ошибки, которые могли бы быть скрыты в определенном запуске из-за race conditions.
 
Обнаруживает ошибки, которые могли бы быть скрыты в определенном запуске из-за race conditions.
  
Например, классическую проблема взаимного исключения: локальный предикат "процесс в критической секции".
+
Например, классическую проблема взаимного исключения для двух процессов: локальный предикат "процесс в критической секции".
 
Если есть срез, в котором два процесса в критической секции, то всё плохо.
 
Если есть срез, в котором два процесса в критической секции, то всё плохо.
 
А если такого нет, то любые две критические секции упорядочены.
 
А если такого нет, то любые две критические секции упорядочены.
  
 
Ещё пример WCP предиката: “в системе нет координатора”, причем локальное условие – “я не координатор”.
 
Ещё пример WCP предиката: “в системе нет координатора”, причем локальное условие – “я не координатор”.

Версия 22:09, 2 июня 2019

Слабый конъюнктивный предикат (WCP)предикат, имеющий вид конъюнкции локальных предикатов над состоянием каждого процесса.

Определение:
Слабый конъюктивный предикат $P$ истинен, если он истенен на хотя бы одном согласованном срезе

Сложные предикаты, составленные как логическая комбинация локальных предикатов, можно представить в дизъюнктивной нормальной форме и рассмотреть как дизъюнкцию слабых конъюктивных предикатов.

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

Примеры

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

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

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