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

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

Текущая версия на 19:08, 4 сентября 2022

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

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

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

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

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

Примеры

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

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

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