51
правка
Изменения
→Условия согласованности
{{Определение
|id = global_time_model
|definition = [[Файл: Global time modeling.png|справа|400px|thumb|Отношения между операциями <tex> e, f, g </tex> процессов <tex> P, Q, R </tex> в модели глобального времени]]
'''Модель глобального времени''' определим так, что это модель, в которой в качестве '''операции''' используется временной интервал: <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 = restriction_on_thread
|definition = [[Файл: Well formed.png|справа|400px|Пример правильного и неправильного исполнения]]'''Сужение''' исполнения <tex> (H, \rightarrow) </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> <br />}}{{Определение|id = well_formed_control_flow|definition = Исполнение называется '''правильным''' (англ. ''well-formed''), если его сужение на каждый поток <tex> P </tex> является последовательным.
}}
{{Определение
=== Условия согласованности ===
{{Определение
|id = agreement
|definition = '''Согласованность''' является аналогом ''корректности'' в многопоточном программировании. <br />
'''Базовое требование согласованности:''' корректные последовательные программы должны cчитаться согласованными при любом их исполнении в одном потоке
}}
{{Определение
|id = legacy_control_flow
|definition = Последовательное исполнение является '''допустимым''' (англ. ''legal''), если выполнены последовательные спецификации всех объектов.
}}
{{Определение
|id = legacy_control_flow
|definition = Исполнение '''последовательно согласовано''', если можно сопоставить '''эквивалентное''' ему (состоящее из тех же событий и операций) допустимое последовательное исполнение, которое сохраняет программный порядок, то есть порядок операций на каждом потоке. <br / > '''Замечание: ''' Последовательная согласованность на каждом объекте не влечёт последовательную согласованность исполнения
}}
[[Файл: Legal execution.png|400px|Допустимое и недопустимое исполнения]] [[Файл: Seq agreed.png|400px|Последовательно согласованное исполнение]] [[Файл: Contrexample seq agr on object.png|thumb|400px|справа|Пример отсутствия последовательной согласованности исполнения при последовательной согласованности на каждом объекте (<tex> s, t - </tex> две FIFO очереди)]]
{{Определение
|id = linearizabilty
|definition = Исполнение <tex> (H, \rightarrow_H) </tex> '''линеаризуемо''', если существует эквивалентное ему допустимое последовательное исполнение <tex> (L(H), \rightarrow_{L(H)}) </tex>, называемое '''линеаризацией''', и верно что <tex> \forall e, f \in H: e \rightarrow_H f \Rightarrow e \rightarrow_{L(H)} f </tex>, то есть сохраняется отношение "произошло до".
}}
[[Файл: Linearizability.png|400px|Пример линеаризуемого исполнения]]
=== Декомпозиция исполнения ===
