Базовые определения и формализм — различия между версиями
(Первые определения) |
Anverk (обсуждение | вклад) (Ещё определения) |
||
| Строка 5: | Строка 5: | ||
* <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> e \rightarrow_H f </tex> означает, что операция <tex> e </tex> '''произошла до''' операции <tex> f </tex> в исполнении <tex> H </tex> |
'''Замечание''': чаще всего исполнение <tex> H </tex> понятно из контекста и опускается | '''Замечание''': чаще всего исполнение <tex> H </tex> понятно из контекста и опускается | ||
}} | }} | ||
| Строка 11: | Строка 11: | ||
{{Определение | {{Определение | ||
|id = parallel_ops | |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> | + | |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> |
| − | Обозначение: <tex> e || f </tex> | ||
}} | }} | ||
{{Определение | {{Определение | ||
|id = system | |id = system | ||
| − | |definition = '''Система''' <tex>–</tex> это множество всех возможных исполнений. Говорим, что '''система имеет свойство <tex>P</tex>''', если ''каждое'' исполнение системы имеет свойство <tex> P </tex> | + | |definition = '''Система''' <tex>–</tex> это множество всех возможных исполнений. <br />Говорим, что '''система имеет свойство <tex>P</tex>''', если ''каждое'' исполнение системы имеет свойство <tex> P </tex> |
| + | }} | ||
| + | |||
| + | {{Определение | ||
| + | |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 />'''Замечание''': глобального времени не существует из-за физических ограничений, поэтому в доказательствах такая модель не используется, но помогает при визуализации различных исполнений | ||
| + | }} | ||
| + | |||
| + | {{Определение | ||
| + | |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>. То есть, если все операции линейно-упорядочены отношением "произошло до". | ||
| + | }} | ||
| + | |||
| + | ;Конфликты и гонки данных | ||
| + | : {{Определение | ||
| + | |id = conflict | ||
| + | |definition = Две операции над одной переменной, одна из которых это запись, называются '''конфликтующими'''. Соответственно, бывают '''read-write''' и ''write-write''' конфликты. | ||
| + | }} | ||
| + | : {{Определение | ||
| + | |id = data_race | ||
| + | |definition = Если две конфликтующие операции произошли параллельно, то такая ситуация называется '''гонка данных (data race)''' <br /> '''Замечание''': наличие гонки данных является свойством конкретного '''исполнения'''. | ||
| + | }} | ||
| + | : {{Определение | ||
| + | |id = data_race | ||
| + | |definition = Программа называется '''корректно синхронизированной''', если в '''любом допустимом''' исполнении нет гонок данных. | ||
}} | }} | ||
Версия 17:19, 30 сентября 2018
Определения
| Определение: |
Исполнение системы это пара , где:
|
| Определение: |
| Пусть Тогда говорят, что параллельна , если Обозначение: |
| Определение: |
| Система это множество всех возможных исполнений. Говорим, что система имеет свойство , если каждое исполнение системы имеет свойство |
| Определение: |
| Модель глобального времени определим так, что это модель, в которой в качестве операции используется временной интервал: причём . Зададим в этой модели отношение следующим образом: . Неформально это означает, что вход в функцию, выполняющую операцию , был осуществлён строго позже, чем был получен результат работы функции, выполняющей операцию . Замечание: глобального времени не существует из-за физических ограничений, поэтому в доказательствах такая модель не используется, но помогает при визуализации различных исполнений |
| Определение: |
| Исполнение системы называется последовательным, если . То есть, если все операции линейно-упорядочены отношением "произошло до". |
- Конфликты и гонки данных
| Определение: |
| Две операции над одной переменной, одна из которых это запись, называются конфликтующими'. Соответственно, бывают read-write и write-write конфликты. |
| Определение: |
| Если две конфликтующие операции произошли параллельно, то такая ситуация называется гонка данных (data race) Замечание: наличие гонки данных является свойством конкретного исполнения. |
| Определение: |
| Программа называется корректно синхронизированной, если в любом допустимом исполнении нет гонок данных. |
