51
правка
Изменения
→Свойства линеаризуемости
== Свойства линеаризуемости ==
{{Определение
|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>. Эти точки и будут точками линеаризации. Итак, построены точки линеаризации, которые, очевидно, сохраняют линеаризацию по их построению.
}}
'''Следствие 1.''' Для модели глобального времени эта теорема верна в обе стороны: действительно дополнительное требование выполняется, так как каждая операция в нём является непрерывным множеством.
'''Следствие 2.''' Чтобы среди точек линеаризации был порядок, согласованный с семантикой низкоуровневых операций, достаточно чтобы операции низкого уровня были атомарны (линеаризуемы)
