Синхронизация часов: различия между версиями

Ключевой конструкцией, используемой в [ ], является граф синхронизации выполнения, определяемый путем объединения понятий локального времени и спецификации реального времени следующим образом.

Определение 1. Пусть f$ – ракурс выполнения системы, а H – спецификация реального времени для f$. Граф синхронизации, порожденный f$ и H, является ориентированным взвешенным графом Грц = (V;E;w), где V – множество событий в /}, и для каждой упорядоченной пары событий p q в /}, такой, что H(p; q) < 1, существует ориентированное ребро (p; q) 2 E.

Вес ребра (p, q) равен w(p; q) = H(p; q)-UT(p) + LT(q).

Естественное понятие расстояния от события p до события q в графе синхронизации Г, обозначаемое drip, Ф> определяется длиной кратчайшего взвешенного пути от p до q, или бесконечностью, если q недостижимо из p. Поскольку веса могут быть отрицательными, необходимо доказать, что понятие точно определено: действительно, было показано, что если Грн получен из выполнения с ракурсом f$, удовлетворяющего спецификации реального времени H, то Грн не содержит ориентированных циклов с отрицательным весом.

Теорема 1. Пусть a – выполнение с ракурсом f$. Тогда a удовлетворяет спецификации реального времени H тогда и только тогда, когда RT(p) - RT(q) < dr(p, q) + LT(p) - LT(q) для любых двух событий p и q в Грн.