Изменения

* <tex> e \rightarrow_H f - </tex> означает, что операция <tex> e </tex> '''произошла до''' операции <tex> f </tex> в исполнении <tex> H </tex>

|definition = Пусть <tex> e, f \in H. </tex> Тогда говорят, что <tex> e </tex> '''параллельна''' <tex> f </tex>, если <tex> e \not \rightarrow f \land f \not \rightarrow e. </tex><br /> Обозначение: <tex> e || f </tex>

|definition = '''Система''' <tex>–</tex> это множество всех возможных исполнений. <br />Говорим, что '''система имеет свойство <tex>P</tex>''', если ''каждое'' исполнение системы имеет свойство <tex> P </tex>}} {{Определение|id = global_time_model |definition = '''Модель глобального времени''' определим так, что это модель, в которой в качестве '''операции''' используется временной интервал: <tex> e = [t_{inv}(e), t_{res}(e)], </tex> причём <tex> t_{inv}(e), t_{res}(e) \in \mathbb{R} </tex>. Зададим в этой модели отношение <tex> \rightarrow </tex> следующим образом: <tex> e \rightarrow f = t_{inv}(f) > t_{res}(e) </tex>. Неформально это означает, что вход в функцию, выполняющую операцию <tex> f </tex>, был осуществлён строго позже, чем был получен результат работы функции, выполняющей операцию <tex> e </tex>. <br />'''Замечание''': глобального времени не существует из-за физических ограничений, поэтому в доказательствах такая модель не используется, но помогает при визуализации различных исполнений}} {{Определение|id = sequenced_control_flow|definition = Исполнение системы <tex> H </tex> называется '''последовательным''', если <tex> \forall e, f \in H: (e = f) \lor (e \rightarrow f) \lor (f \rightarrow e) </tex>. То есть, если все операции линейно-упорядочены отношением "произошло до".}} ;Конфликты и гонки данных: {{Определение|id = conflict|definition = Две операции над одной переменной, одна из которых это запись, называются '''конфликтующими'''. Соответственно, бывают '''read-write''' и ''write-write''' конфликты.}}: {{Определение|id = data_race|definition = Если две конфликтующие операции произошли параллельно, то такая ситуация называется '''гонка данных (data race)''' <br /> '''Замечание''': наличие гонки данных является свойством конкретного '''исполнения'''. }}: {{Определение|id = data_race|definition = Программа называется '''корректно синхронизированной''', если в '''любом допустимом''' исполнении нет гонок данных.