4551
правка
Ресинхронизация схемы: инкрементный подход: различия между версиями
Материал из WEGA
Ресинхронизация схемы: инкрементный подход (посмотреть исходный код)
Версия от 13:04, 11 июня 2017
, 11 июня 2017→Основные результаты
Irina (обсуждение | вклад) |
Irina (обсуждение | вклад) |
||
| Строка 75: | Строка 75: | ||
Для сокращения длительности цикла переменную r необходимо изменить, сделав ее ближе к r'. Следует отметить, что в контексте ресинхронизации важны не абсолютные значения r, но их разности. Если <math>\langle r, t \rangle \;</math> является решением задачи ресинхронизации, то <math>\langle r + c, t \rangle \;</math>, где <math>c \in \mathbb{Z} \;</math> – произвольная константа, также будет являться решением. Следовательно, r может быть сделана «ближе» к r' за счет размещения большего количества регистров между u и v, то есть либо за счет уменьшения r[u], либо за счет увеличения r[v]. Отметим, что v можно легко определить из соотношения t[v] = max(t). Независимо от того, какое значение (r[v] или r[u]) выбрано для изменения, изменение должно быть единичным, поскольку r не следует чрезмерно корректировать. Таким образом, после корректировки будут по-прежнему выполняться соотношения <math>r[v] - r[u] \le r'[v] - r'[u] \;</math> или, что эквивалентно, <math>r[v] | Для сокращения длительности цикла переменную r необходимо изменить, сделав ее ближе к r'. Следует отметить, что в контексте ресинхронизации важны не абсолютные значения r, но их разности. Если <math>\langle r, t \rangle \;</math> является решением задачи ресинхронизации, то <math>\langle r + c, t \rangle \;</math>, где <math>c \in \mathbb{Z} \;</math> – произвольная константа, также будет являться решением. Следовательно, r может быть сделана «ближе» к r' за счет размещения большего количества регистров между u и v, то есть либо за счет уменьшения r[u], либо за счет увеличения r[v]. Отметим, что v можно легко определить из соотношения t[v] = max(t). Независимо от того, какое значение (r[v] или r[u]) выбрано для изменения, изменение должно быть единичным, поскольку r не следует чрезмерно корректировать. Таким образом, после корректировки будут по-прежнему выполняться соотношения <math>r[v] - r[u] \le r'[v] - r'[u] \;</math> или, что эквивалентно, <math>r[v] - r'[v] \le r[u] - r'[u] \;</math>. Поскольку v легко определить, выберем для увеличения r[v]. Время прибытия t[v] можно незамедлительно уменьшить до d[v]. Это позволяет уточнить вторую команду: | ||
<math>\neg P3 \and P2 \and \exist v \in V: t[v] = max(t) \to r[v], t[v] :=r[v] + 1, d[v] \;</math>. | |||
Поскольку во время выполнения этой операции регистры перемещаются, предикат P2 может перестать выполняться. Однако первая команда восстановит статус кво. Эта команда увеличивает t для некоторых вершин; некоторые из них даже могут превысить значение max(t) до перемещения регистра. Аналогичное рассуждение для <math>\langle r, t \rangle \;</math> показывает, что их значения r также подвергаются увеличению. Таким образом, для реализации данного «насколько возможно быстрого» (As-Soon-As-Possible, ASAP) увеличения r необходимо сделать моментальный снимок max(t), пока предикат P2 еще актуален. Физически такой моментальный снимок записывает один такт применимой длительности <math>\phi \;</math> и может быть реализован при помощи добавления к циклу еще одной команды: | |||
Однако подобная ASAP-операция может ускорить r[u] даже в случае w[u | <math>P2 \and \phi > max(t) \to \phi := max(t) \;</math>. | ||
Однако подобная ASAP-операция может ускорить r[u] даже в случае w[u, v] - r[u] + r[v] = 0 для ребра (u, v). Это означает, что P0 может быть уже не инвариантом. Однако перемещение P0 из инварианта в цель цикла не составит проблемы, поскольку для этого в цикл можно добавить одну команду: | |||
<math>\exist (u, v) \in E: r[u] - r[v] > w[u, v] \to r[v] := r[u] - w[u, v] \;</math>. | |||
