Базовые определения и формализм — различия между версиями

Материал из Викиконспекты
Перейти к: навигация, поиск
(Декомпозиция исполнения)
м (rollbackEdits.php mass rollback)
 
(не показано 11 промежуточных версий 3 участников)
Строка 3: Строка 3:
 
{{Определение
 
{{Определение
 
|id = system_execution
 
|id = system_execution
|definition = '''Исполнение системы''' <tex>-</tex> это пара <tex> (H, \rightarrow_H)</tex>, где:
+
|definition =  
 +
[[Файл: Happens before.png|400px|справа|thumb|Отношения между операциями <tex> e, f, g </tex> процессов <tex> P, Q, R </tex>]]
 +
'''Исполнение системы''' <tex>-</tex> это пара <tex> (H, \rightarrow_H)</tex>, где:
 
* <tex> H - </tex> множество '''операций''' <tex> e, f, g\ldots </tex> (чтение, запись ячеек памяти и т.п.), произошедших во время исполнения
 
* <tex> H - </tex> множество '''операций''' <tex> e, f, g\ldots </tex> (чтение, запись ячеек памяти и т.п.), произошедших во время исполнения
 
* <tex> \rightarrow_H - </tex> это отношение частичного строгого порядка на множестве операций (транзитивное, антирефлексивное, асимметричное)
 
* <tex> \rightarrow_H - </tex> это отношение частичного строгого порядка на множестве операций (транзитивное, антирефлексивное, асимметричное)
 
* <tex> e \rightarrow_H f </tex> означает, что операция <tex> e </tex> '''произошла до''' операции <tex> f </tex> в исполнении <tex> H </tex>
 
* <tex> e \rightarrow_H f </tex> означает, что операция <tex> e </tex> '''произошла до''' операции <tex> f </tex> в исполнении <tex> H </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_ops
 
|definition = Пусть <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>
 
 
}}
 
}}
  
Строка 21: Строка 19:
  
 
{{Определение
 
{{Определение
|id = global_time_model  
+
|id = global_time_model
|definition = '''Модель глобального времени''' определим так, что это модель, в которой в качестве '''операции''' используется временной интервал: <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 />'''Замечание''': глобального времени не существует из-за физических ограничений, поэтому в доказательствах такая модель не используется, но помогает при визуализации различных исполнений
+
|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> \rightarrow </tex> следующим образом: <tex> e \rightarrow f = t_{inv}(f) > t_{res}(e) </tex>. Неформально это означает, что вход в функцию, выполняющую операцию <tex> f </tex>, был осуществлён строго позже, чем был получен результат работы функции, выполняющей операцию <tex> e </tex>. <br />'''Замечание''': глобального времени не существует из-за физических ограничений, поэтому в доказательствах такая модель не используется, но помогает при визуализации различных исполнений
 
}}
 
}}
  
Строка 47: Строка 46:
 
{{Определение
 
{{Определение
 
|id = restriction_on_thread
 
|id = restriction_on_thread
|definition = '''Сужение''' исполнения <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>
+
|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 = well_formed_control_flow
 
|definition = Исполнение называется '''правильным''' (англ. ''well-formed''), если его сужение на каждый поток <tex> P </tex> является последовательным.
 
 
}}
 
}}
 
{{Определение
 
{{Определение
Строка 63: Строка 60:
  
 
=== Условия согласованности ===
 
=== Условия согласованности ===
 +
{{Определение
 +
|id = agreement
 +
|definition = '''Согласованность''' является аналогом ''корректности'' в многопоточном программировании. <br />
 +
'''Базовое требование согласованности:''' корректные последовательные программы должны cчитаться согласованными при любом их исполнении в одном потоке
 +
}}
 +
 
{{Определение
 
{{Определение
 
|id = legacy_control_flow
 
|id = legacy_control_flow
|definition = Последовательное исполнение является '''допустимым''' (англ. ''legal''), если выполнены последовательные спецификации всех объектов.
+
|definition =  
 +
Последовательное исполнение является '''допустимым''' (англ. ''legal''), если выполнены последовательные спецификации всех объектов.
 
}}
 
}}
 +
 
{{Определение
 
{{Определение
 
|id = legacy_control_flow
 
|id = legacy_control_flow
|definition = Исполнение последовательно согласовано, если можно сопоставить '''эквивалентное''' ему (состоящее из тех же событий и операций) допустимое последовательное исполнение, которое сохраняет программный порядок, то есть порядок операций на каждом потоке. <br / > Последовательная согласованность на каждом объекте не влечёт последовательную согласованность исполнения
+
|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
 
|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>, то есть сохраняется отношение "произошло до".
 
|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|Пример линеаризуемого исполнения]]
  
 
=== Декомпозиция исполнения ===
 
=== Декомпозиция исполнения ===
Строка 81: Строка 91:
 
|definition = Определим '''декомпозицию исполнения''' как пятёрку <tex> (H, G, \rightarrow_G, inv, res) </tex>, где
 
|definition = Определим '''декомпозицию исполнения''' как пятёрку <tex> (H, G, \rightarrow_G, inv, res) </tex>, где
 
* <tex> H -</tex> множество '''операций''' <tex> (\forall e \in H: e \subset G) </tex>
 
* <tex> H -</tex> множество '''операций''' <tex> (\forall e \in H: e \subset G) </tex>
* <tex> G -</tex> множество '''событий''' </tex>
+
* <tex> G -</tex> множество '''событий'''  
 
* <tex> \rightarrow_G - </tex> отношение строгого порядка '''произошло до''' на '''событиях''' из <tex> G </tex>
 
* <tex> \rightarrow_G - </tex> отношение строгого порядка '''произошло до''' на '''событиях''' из <tex> G </tex>
 
* <tex> inv, res: H \rightarrow G - </tex> такие функции, что
 
* <tex> inv, res: H \rightarrow G - </tex> такие функции, что
Строка 93: Строка 103:
  
 
== Свойства линеаризуемости ==
 
== Свойства линеаризуемости ==
 +
 +
{{Определение
 +
|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.''' Чтобы среди точек линеаризации был порядок, согласованный с семантикой низкоуровневых операций, достаточно чтобы операции низкого уровня были атомарны (линеаризуемы)
 +
 +
== Источники информации ==
 +
 +
* [https://en.wikipedia.org/wiki/Linearizability Linearizability]
 +
* [https://cs.brown.edu/~mph/HerlihyW90/p463-herlihy.pdf Maurice P. Herlihy and Jeannette M. Wing  {{---}} Linearizability: A Correctness Condition for Concurrent Objects]
 +
 +
[[Категория: Параллельное программирование]]

Текущая версия на 19:34, 4 сентября 2022

Определения

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

Определение:
Отношения между операциями [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, f, g [/math] процессов [math] P, Q, R [/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]
Замечание: в правильном исполнении сужение на объекты не всегда является последовательным


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

Определение:
Согласованность является аналогом корректности в многопоточном программировании.
Базовое требование согласованности: корректные последовательные программы должны cчитаться согласованными при любом их исполнении в одном потоке


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


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


Допустимое и недопустимое исполнения Последовательно согласованное исполнение
Пример отсутствия последовательной согласованности исполнения при последовательной согласованности на каждом объекте ([math] s, t - [/math] две FIFO очереди)
Определение:
Исполнение [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] верны два условия:

  1. Можно выбрать точки линеаризации [math] p: H \rightarrow G [/math]
  2. [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]:

  1. [math] e \rightarrow_H f [/math] (дано)
  2. [math] res(e) \rightarrow_G inv(f) [/math] (по определению [math] \rightarrow_H [/math])
  3. [math] p(e) \rightarrow_G res(e) [/math] (по определению декомпозиции и точек линеаризации)
  4. [math] inv(f) \rightarrow_G p(f) [/math] (по определению декомпозиции и точек линеаризации)
  5. [math] p(e) \rightarrow_G p(f) [/math] (по транзитивности)
  6. [math] p(e) \rightarrow_{L(P)} p(f) [/math] (по определению линеаризации)
  7. [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. Чтобы среди точек линеаризации был порядок, согласованный с семантикой низкоуровневых операций, достаточно чтобы операции низкого уровня были атомарны (линеаризуемы)

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