Изменения
больше определений
== Определения ===== Базовые определения ===
{{Определение
|id = system_execution
}}
|id = conflict
|definition = Две операции над одной переменной, одна из которых это запись, называются '''конфликтующими'''. Соответственно, бывают '''read-write''' и '''write-write''' конфликты.
}}
|id = data_race
|definition = Если две конфликтующие операции произошли параллельно, то такая ситуация называется '''гонка данных ''' (англ. ''data race)''' ) <br /> '''Замечание''': наличие гонки данных является свойством конкретного '''исполнения'''.
}}
|definition = Программа называется '''корректно синхронизированной''', если в '''любом допустимом''' исполнении нет гонок данных.
}}
=== Правильное исполнение ===
{{Определение
|id = restriction_on_thread
|definition = '''Сужение''' исполнения <tex> H </tex> на поток <tex> P - </tex> исполнение, в котором остались только операции, происходящие в потоке <tex> P </tex>. <br /> Обозначение: <tex> \left.H\right|_P </tex>. Формально <tex> \left.H\right|_P = \{e \in H|\ proc(e) = P\}</tex>
}}
{{Определение
|id = well_formed_control_flow
|definition = Исполнение называется '''правильным''' (англ. ''well-formed''), если его сужение на каждый поток <tex> P </tex> является последовательным.
}}
{{Определение
|id = program_order
|definition = Объединение всех сужений на потоки называется '''программным порядком''' (англ. ''program order'' или ''po'').
}}
{{Определение
|id = restriction_on_object
|definition = '''Сужение''' исполнения <tex> H </tex> на объект <tex> x - </tex> исполнение, в котором остались только операции, взаимодействующие с объектом <tex> x </tex>. <br /> Обозначение: <tex> \left.H\right|_x </tex>. Формально <tex> \left.H\right|_x = \{e \in H|\ obj(e) = x\}</tex> <br /> '''Замечание''': в правильном исполнении сужение на объекты не всегда является последовательным
}}
=== Условия согласованности ===
{{Определение
|id = legacy_control_flow
|definition = Последовательное исполнение является '''допустимым''' (англ. ''legal''), если выполнены последовательные спецификации всех объектов.
}}
{{Определение
|id = legacy_control_flow
|definition = Исполнение последовательно согласовано, если можно сопоставить '''эквивалентное''' ему (состоящее из тех же событий и операций) допустимое последовательное исполнение, которое сохраняет программный порядок, то есть порядок операций на каждом потоке. <br / > Последовательная согласованность на каждом объекте не влечёт последовательную согласованность исполнения
}}
{{Определение
|id = linearizabilty
|definition = Исполнение '''линеаризуемо''', если существует эквивалентное ему допустимое последовательное исполнение, которое сохраняет порядок отношения <tex> \rightarrow </tex>.
}}
== Свойства линеаризуемости ==
