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

Определения

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

Определение:

Отношения между операциями [math] e, f, g [/math] процессов [math] P, Q, R [/math] Исполнение системы [math]-[/math] это пара [math] (H, \rightarrow_H)[/math], где: [math] H - [/math] множество операций [math] e, f, g\ldots [/math] (чтение, запись ячеек памяти и т.п.), произошедших во время исполнения [math] \rightarrow_H - [/math] это отношение частичного строгого порядка на множестве операций (транзитивное, антирефлексивное, асимметричное) [math] e \rightarrow_H f [/math] означает, что операция [math] e [/math] произошла до операции [math] f [/math] в исполнении [math] H [/math] Замечание: чаще всего исполнение [math] H [/math] понятно из контекста и опускается Пусть [math] e, f \in H. [/math] Тогда говорят, что [math] e [/math] параллельна [math] f [/math], если [math] e \not \rightarrow f \land f \not \rightarrow e. [/math] Обозначение: [math] e || f [/math]

Определение:

Система [math]–[/math] это множество всех возможных исполнений. Говорим, что система имеет свойство [math]P[/math], если каждое исполнение системы имеет свойство [math] P [/math]

Определение:

Модель глобального времени определим так, что это модель, в которой в качестве операции используется временной интервал: [math] e = [t_{inv}(e), t_{res}(e)], [/math] причём [math] t_{inv}(e), t_{res}(e) \in \mathbb{R} [/math]. Зададим в этой модели отношение [math] \rightarrow [/math] следующим образом: [math] e \rightarrow f = t_{inv}(f) \gt t_{res}(e) [/math]. Неформально это означает, что вход в функцию, выполняющую операцию [math] f [/math], был осуществлён строго позже, чем был получен результат работы функции, выполняющей операцию [math] e [/math]. Замечание: глобального времени не существует из-за физических ограничений, поэтому в доказательствах такая модель не используется, но помогает при визуализации различных исполнений

Определение:

Исполнение системы [math] (H, \rightarrow) [/math] называется последовательным, если [math] \forall e, f \in H: (e = f) \lor (e \rightarrow f) \lor (f \rightarrow e) [/math]. То есть, если все операции линейно-упорядочены отношением "произошло до".

Конфликты и гонки данных

Определение:

Две операции над одной переменной, одна из которых это запись, называются конфликтующими. Соответственно, бывают read-write и write-write конфликты.

Определение:

Если две конфликтующие операции произошли параллельно, то такая ситуация называется гонка данных (англ. data race) Замечание: наличие гонки данных является свойством конкретного исполнения.

Определение:

Программа называется корректно синхронизированной, если в любом допустимом исполнении нет гонок данных.

Правильное исполнение

Определение:

Сужение исполнения [math] (H, \rightarrow) [/math] на поток [math] P - [/math] исполнение, в котором остались только операции, происходящие в потоке [math] P [/math]. Обозначение: [math] \left.H\right|_P [/math]. Формально [math] \left.H\right|_P = \{e \in H|\ proc(e) = P\}[/math] Исполнение называется правильным (англ. well-formed), если его сужение на каждый поток [math] P [/math] является последовательным.

Определение:

Объединение всех сужений на потоки называется программным порядком (англ. program order или po).

Определение:

Сужение исполнения [math] (H, \rightarrow) [/math] на объект [math] x - [/math] исполнение, в котором остались только операции, взаимодействующие с объектом [math] x [/math]. Обозначение: [math] \left.H\right|_x [/math]. Формально [math] \left.H\right|_x = \{e \in H|\ obj(e) = x\}[/math] Замечание: в правильном исполнении сужение на объекты не всегда является последовательным

Условия согласованности

Определение:

Последовательное исполнение является допустимым (англ. legal), если выполнены последовательные спецификации всех объектов.

Определение:

Исполнение последовательно согласовано, если можно сопоставить эквивалентное ему (состоящее из тех же событий и операций) допустимое последовательное исполнение, которое сохраняет программный порядок, то есть порядок операций на каждом потоке. Последовательная согласованность на каждом объекте не влечёт последовательную согласованность исполнения

Определение:

Исполнение [math] (H, \rightarrow_H) [/math] линеаризуемо, если существует эквивалентное ему допустимое последовательное исполнение [math] (L(H), \rightarrow_{L(H)}) [/math], называемое линеаризацией, и верно что [math] \forall e, f \in H: e \rightarrow_H f \Rightarrow e \rightarrow_{L(H)} f [/math], то есть сохраняется отношение "произошло до".

Декомпозиция исполнения

Определение:

Определим декомпозицию исполнения как пятёрку [math] (H, G, \rightarrow_G, inv, res) [/math], где [math] H -[/math] множество операций [math] (\forall e \in H: e \subset G) [/math] [math] G -[/math] множество событий [math] \rightarrow_G - [/math] отношение строгого порядка произошло до на событиях из [math] G [/math] [math] inv, res: H \rightarrow G - [/math] такие функции, что [math] \forall e \in H: inv(e) \rightarrow_G res(e) [/math] [math] \forall e \in H, g \in e, g \neq inv(e), g \neq res(e): inv(e) \rightarrow_G g \rightarrow_G res(e) [/math]

Определение:

Определим произошло до на операциях: [math] \forall e, f \in H: e \rightarrow_H f = res(e) \rightarrow_G inv(f) [/math]

Свойства линеаризуемости

Определение:

Пусть дана декомпозиция [math] (H, G, \rightarrow_G, inv, res) [/math]. Тогда определим точки линеаризации как функцию [math] p: H \rightarrow G [/math] такую, что: [math] \forall e \in H: p \neq inv(e) \land p \neq res(e) [/math] [math] P = p(H) \subset G -[/math] множество всех точек линеаризации [math] (L(P), \rightarrow_{L(P)}) -[/math] линеаризация [math] (G, \rightarrow_G) [/math], то есть [math] \forall e, f \in H: p(e) \rightarrow_G p(f) \Rightarrow p(e) \rightarrow_{L(P)} p(f) [/math]

Утверждение (эквивалентное определение линеаризуемости):

Пусть дана декомпозиция [math] (H, G, \rightarrow_G, inv, res) [/math]. Исполнение [math] (H, \rightarrow_H) [/math] является линеаризуемым [math] (L(H), \rightarrow_{L(H)}) [/math] тогда и только тогда, когда[math]^*[/math] верны два условия: Можно выбрать точки линеаризации [math] p: H \rightarrow G [/math] [math] \forall e, f \in H: e \rightarrow_{L(H)} f \Leftrightarrow p(e) \rightarrow_{L(P)} p(f) [/math] [math]*[/math] Для существования точек линеаризации из линеаризации необходимо, чтобы бы выполнялось: [math] \forall e, f \in H: e \rightarrow_{L(H)} f \Rightarrow \exists a \in e, b \in f: a \rightarrow_G b. [/math]

[math]\triangleright[/math]

[math] \Leftarrow [/math] Пусть есть точки линеаризации [math] \forall e \in H: p(e) \in G [/math], полный порядок [math] \rightarrow_{L(P)} [/math] над ними. Требуется найти линеаризацию [math] (L(H), \rightarrow_{L(H)}) [/math]. Определим [math] L(H) [/math] как [math] H [/math], так как они по определению линеаризации должны быть эквивалентны, а [math] \rightarrow_{L(H)} [/math] определим, воспользовавшись вторым условием предпосылки. Докажем корректность такой линеаризации, то есть что [math] \forall e, f \in H: e \rightarrow_H f \Rightarrow e \rightarrow_{L(H)} [/math]: [math] e \rightarrow_H f [/math] (дано) [math] res(e) \rightarrow_G inv(f) [/math] (по определению [math] \rightarrow_H [/math]) [math] p(e) \rightarrow_G res(e) [/math] (по определению декомпозиции и точек линеаризации) [math] inv(f) \rightarrow_G p(f) [/math] (по определению декомпозиции и точек линеаризации) [math] p(e) \rightarrow_G p(f) [/math] (по транзитивности) [math] p(e) \rightarrow_{L(P)} p(f) [/math] (по определению линеаризации) [math] p(e) \rightarrow_{L(H)} p(f) [/math] (по определению [math] \rightarrow_{L(H)} [/math]) [math] \Rightarrow [/math] Добавим события [math] \forall e \in H: p(e) [/math] в [math] G [/math] такие, что [math] inv(e) \rightarrow_G p(e) \rightarrow_G res(e) [/math] и для которых выполнено требование из [math]*[/math]. Эти точки и будут точками линеаризации. Итак, построены точки линеаризации, которые, очевидно, сохраняют линеаризацию по их построению.

[math]\triangleleft[/math]

Следствие 1. Для модели глобального времени эта теорема верна в обе стороны: действительно дополнительное требование выполняется, так как каждая операция в нём является непрерывным множеством.

Следствие 2. Чтобы среди точек линеаризации был порядок, согласованный с семантикой низкоуровневых операций, достаточно чтобы операции низкого уровня были атомарны (линеаризуемы)

Источники информации

• Linearizability
• Maurice P. Herlihy and Jeannette M. Wing — Linearizability: A Correctness Condition for Concurrent Objects