51
правка
Изменения
→Базовые определения
{{Определение
|id = system_execution
|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> \rightarrow_H - </tex> это отношение частичного строгого порядка на множестве операций (транзитивное, антирефлексивное, асимметричное)
* <tex> e \rightarrow_H f </tex> означает, что операция <tex> e </tex> '''произошла до''' операции <tex> f </tex> в исполнении <tex> H </tex>
'''Замечание''': чаще всего исполнение <tex> H </tex> понятно из контекста и опускается<br /> }} {{Определение|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>
}}
{{Определение
|id = global_time_model |definition = [[Файл: Global time modeling.png|справа|400px|thumb|Отношения между операциями <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 />'''Замечание''': глобального времени не существует из-за физических ограничений, поэтому в доказательствах такая модель не используется, но помогает при визуализации различных исполнений
}}
