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

Материал из Викиконспекты
Перейти к: навигация, поиск
Строка 1: Строка 1:
 
[[Категория: Параллельное программирование]]
 
[[Категория: Параллельное программирование]]
'''Слабый конъюнктивный предикат (WCP)''' – предикат, удовлетворяющий двум условиям:
+
'''Слабый конъюнктивный предикат (WCP)''' – предикат, имеющий вид конъюнкции локальных предикатов над состоянием каждого процесса.
* имеет вид конъюнкции локальных предикатов над состоянием каждого процесса;
+
 
* его истинность есть истинность хотя бы на одном согласованном срезе.
+
Его истинность будем определять, как истинность хотя бы на одном согласованном срезе.
  
 
'''Локальный предикат''' – предикат по состоянию одного процесса. Например, если у процесса есть состояние (переменная) x, то локальным предикатом может быть (x < 0).
 
'''Локальный предикат''' – предикат по состоянию одного процесса. Например, если у процесса есть состояние (переменная) x, то локальным предикатом может быть (x < 0).

Версия 14:01, 15 марта 2018

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

Его истинность будем определять, как истинность хотя бы на одном согласованном срезе.

Локальный предикат – предикат по состоянию одного процесса. Например, если у процесса есть состояние (переменная) x, то локальным предикатом может быть (x < 0).

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

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

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