Базовые определения и формализм

Определения

Определение:

Исполнение системы [math]-[/math] это пара [math] (H, \rightarrow_H)[/math], где: [math] H - [/math] множество операций [math] e, f, g\ldots [/math] (чтение, запись ячеек памяти и т.п.), произошедших во время исполнения [math] \rightarrow_H - [/math] это отношение частичного строгого порядка на множестве операций (транзитивное, антирефлексивное, асимметричное) [math] e \rightarrow_H f [/math] означает, что операция [math] e [/math] произошла до операции [math] f [/math] в исполнении [math] H [/math] Замечание: чаще всего исполнение [math] H [/math] понятно из контекста и опускается

Определение:

Пусть [math] e, f \in H. [/math] Тогда говорят, что [math] e [/math] параллельна [math] f [/math], если [math] e \not \rightarrow f \land f \not \rightarrow e. [/math] Обозначение: [math] e || f [/math]

Определение:

Система [math]–[/math] это множество всех возможных исполнений. Говорим, что система имеет свойство [math]P[/math], если каждое исполнение системы имеет свойство [math] P [/math]

Определение:

Модель глобального времени определим так, что это модель, в которой в качестве операции используется временной интервал: [math] e = [t_{inv}(e), t_{res}(e)], [/math] причём [math] t_{inv}(e), t_{res}(e) \in \mathbb{R} [/math]. Зададим в этой модели отношение [math] \rightarrow [/math] следующим образом: [math] e \rightarrow f = t_{inv}(f) \gt t_{res}(e) [/math]. Неформально это означает, что вход в функцию, выполняющую операцию [math] f [/math], был осуществлён строго позже, чем был получен результат работы функции, выполняющей операцию [math] e [/math]. Замечание: глобального времени не существует из-за физических ограничений, поэтому в доказательствах такая модель не используется, но помогает при визуализации различных исполнений

Определение:

Исполнение системы [math] H [/math] называется последовательным, если [math] \forall e, f \in H: (e = f) \lor (e \rightarrow f) \lor (f \rightarrow e) [/math]. То есть, если все операции линейно-упорядочены отношением "произошло до".

Конфликты и гонки данных

Определение:

Две операции над одной переменной, одна из которых это запись, называются конфликтующими'. Соответственно, бывают read-write и write-write конфликты.

Определение:

Если две конфликтующие операции произошли параллельно, то такая ситуация называется гонка данных (data race) Замечание: наличие гонки данных является свойством конкретного исполнения.

Определение:

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