Изменения

== Определения ===== Базовые определения ===

|definition = [[Файл: Happens before.png|400px|справа|thumb|Отношения между операциями <tex> e, f, g </tex> процессов <tex> P, Q, R </tex>]]'''Исполнение системы''' <tex>-</tex> это пара <tex> (H, \rightarrow_H)</tex>, где:

* <tex> e \rightarrow_H f - </tex> означает, что операция <tex> e </tex> '''произошла до''' операции <tex> f </tex> в исполнении <tex> H </tex>'''Замечание''': чаще всего исполнение <tex> H </tex> понятно из контекста и опускается<br /> Пусть <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>

|id = parallel_opssystem|definition = Пусть '''Система''' <tex> e, f \in H–</tex> это множество всех возможных исполнений. <br /tex> Тогда говорятГоворим, что '''система имеет свойство <tex> e P</tex> '''параллельна, если ''каждое'' исполнение системы имеет свойство <tex> P </tex>}} {{Определение|id = global_time_model|definition = [[Файл: Global time modeling.png‎|справа|400px|Отношения между операциями <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> \not rightarrow </tex> следующим образом: <tex> e \rightarrow f \land = t_{inv}(f \not \rightarrow ) > t_{res}(e) </tex>. Неформально это означает, что вход в функцию, выполняющую операцию <tex> f </tex>Обозначение: , был осуществлён строго позже, чем был получен результат работы функции, выполняющей операцию <tex> e || f </tex>. <br />'''Замечание''': глобального времени не существует из-за физических ограничений, поэтому в доказательствах такая модель не используется, но помогает при визуализации различных исполнений

|id = systemsequenced_control_flow|definition = Исполнение системы <tex> (H, \rightarrow) </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 = correctly_syncronized|definition = Программа называется '''корректно синхронизированной''', что если в '''любом допустимом''' исполнении нет гонок данных.}} === Правильное исполнение ==={{Определение|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 />Исполнение называется '''правильным''' (англ. ''well-formed''), если его сужение на каждый поток <tex> P </tex> является последовательным.}}{{Определение|id = program_order|definition = Объединение всех сужений на потоки называется '''программным порядком''' (англ. ''program order'' или ''po''). }}{{Определение|id = restriction_on_object|definition = '''Сужение'каждое'' исполнения <tex> (H, \rightarrow) </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 = 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|Пример линеаризуемого исполнения]] === Декомпозиция исполнения ==={{Определение|id = decomosition|definition = Определим '''декомпозицию исполнения''' как пятёрку <tex> (H, G, \rightarrow_G, inv, res) </tex>, где* <tex> H -</tex> множество '''операций''' <tex> (\forall e \in H: e \subset G) </tex>* <tex> G -</tex> множество '''событий''' * <tex> \rightarrow_G - </tex> отношение строгого порядка '''произошло до''' на '''событиях''' из <tex> G </tex>* <tex> inv, res: H \rightarrow G - </tex> такие функции, что** <tex> \forall e \in H: inv(e) \rightarrow_G res(e) </tex>** <tex> \forall e \in H, g \in e, g \neq inv(e), g \neq res(e): inv(e) \rightarrow_G g \rightarrow_G res(e) </tex>}}{{Определение|id = was_before_event|definition = Определим '''произошло до''' на '''операциях''': <tex> \forall e, f \in H: e \rightarrow_H f = res(e) \rightarrow_G inv(f) </tex>}} == Свойства линеаризуемости == {{Определение|id = linearization_points|definition = Пусть дана декомпозиция <tex> (H, G, \rightarrow_G, inv, res) </tex>. Тогда определим '''точки линеаризации''' как функцию <tex> p: H \rightarrow G </tex> такую, что:* <tex> \forall e \in H: p \neq inv(e) \land p \neq res(e) </tex> * <tex> P = p(H) \subset G -</tex> множество всех точек линеаризации* <tex> (L(P), \rightarrow_{L(P)}) -</tex> линеаризация <tex> (G, \rightarrow_G) </tex>, то есть <tex> \forall e, f \in H: p(e) \rightarrow_G p(f) \Rightarrow p(e) \rightarrow_{L(P)} p(f) </tex>}} {{Утверждение|about=эквивалентное определение линеаризуемости|statement=Пусть дана декомпозиция <tex> (H, G, \rightarrow_G, inv, res) </tex>. Исполнение <tex> (H, \rightarrow_H) </tex> является линеаризуемым <tex> (L(H), \rightarrow_{L(H)}) </tex> тогда и только тогда, когда<tex>^*</tex> верны два условия:# Можно выбрать '''точки линеаризации''' <tex> p: H \rightarrow G </tex># <tex> \forall e, f \in H: e \rightarrow_{L(H)} f \Leftrightarrow p(e) \rightarrow_{L(P)} p(f) </tex><tex>*</tex> Для существования точек линеаризации из линеаризации необходимо, чтобы бы выполнялось: <tex> \forall e, f \in H: e \rightarrow_{L(H)} f \Rightarrow \exists a \in e, b \in f: a \rightarrow_G b. </tex>|proof=<tex> \Leftarrow </tex>Пусть есть точки линеаризации <tex> \forall e \in H: p(e) \in G </tex>, полный порядок <tex> \rightarrow_{L(P)} </tex> над ними. Требуется найти линеаризацию <tex> (L(H), \rightarrow_{L(H)}) </tex>. Определим <tex> L(H) </tex> как <tex> H </tex>, так как они по определению линеаризации должны быть эквивалентны, а <tex> \rightarrow_{L(H)} </tex> определим, воспользовавшись вторым условием предпосылки. Докажем корректность такой линеаризации, то есть что <tex> \forall e, f \in H: e \rightarrow_H f \Rightarrow e \rightarrow_{L(H)} </tex>:# <tex> e \rightarrow_H f </tex> (дано)# <tex> res(e) \rightarrow_G inv(f) </tex> (по определению <tex> \rightarrow_H </tex>)# <tex> p(e) \rightarrow_G res(e) </tex> (по определению декомпозиции и точек линеаризации)# <tex> inv(f) \rightarrow_G p(f) </tex> (по определению декомпозиции и точек линеаризации)# <tex> p(e) \rightarrow_G p(f) </tex> (по транзитивности)# <tex> p(e) \rightarrow_{L(P )} p(f) </tex>(по определению линеаризации)# <tex> p(e) \rightarrow_{L(H)} p(f) </tex> (по определению <tex> \rightarrow_{L(H)} </tex>) <tex> \Rightarrow </tex>Добавим '''события''' <tex> \forall e \in H: p(e) </tex> в <tex> G </tex> такие, что <tex> inv(e) \rightarrow_G p(e) \rightarrow_G res(e) </tex> и для которых выполнено требование из <tex>*</tex>. Эти точки и будут точками линеаризации. Итак, построены точки линеаризации, которые, очевидно, сохраняют линеаризацию по их построению.