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

Материал из Викиконспекты
Перейти к: навигация, поиск
(Условия согласованности)
(Определения)
Строка 27: Строка 27:
 
{{Определение
 
{{Определение
 
|id = sequenced_control_flow
 
|id = sequenced_control_flow
|definition = Исполнение системы <tex> H </tex> называется '''последовательным''', если <tex> \forall e, f \in H: (e = f) \lor (e \rightarrow f) \lor (f \rightarrow e) </tex>. То есть, если все операции линейно-упорядочены отношением "произошло до".
+
|definition = Исполнение системы <tex> (H, \rightarrow) </tex> называется '''последовательным''', если <tex> \forall e, f \in H: (e = f) \lor (e \rightarrow f) \lor (f \rightarrow e) </tex>. То есть, если все операции линейно-упорядочены отношением "произошло до".
 
}}
 
}}
  
Строка 47: Строка 47:
 
{{Определение
 
{{Определение
 
|id = restriction_on_thread
 
|id = restriction_on_thread
|definition = '''Сужение''' исполнения <tex> H </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 = '''Сужение''' исполнения <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>
 
}}
 
}}
 
{{Определение
 
{{Определение
Строка 59: Строка 59:
 
{{Определение
 
{{Определение
 
|id = restriction_on_object
 
|id = restriction_on_object
|definition = '''Сужение''' исполнения <tex> H </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 /> '''Замечание''': в правильном исполнении сужение на объекты не всегда является последовательным
+
|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 /> '''Замечание''': в правильном исполнении сужение на объекты не всегда является последовательным
 
}}
 
}}
  

Версия 22:03, 30 сентября 2018

Определения

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

Определение:
Исполнение системы [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], то есть сохраняется отношение "произошло до".


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