Изменения

Перейти к: навигация, поиск

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

710 байт добавлено, 01:00, 6 октября 2018
Условия согласованности
{{Определение
|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|Пример линеаризуемого исполнения]]
=== Декомпозиция исполнения ===
51
правка

Навигация