Ресинхронизация схемы: инкрементный подход: различия между версиями

Для завершения разработки алгоритма осталось реализовать проверку <math>\neg P3</math>. Из предыдущего обсуждения мы уже знаем, что из <math>\neg P3</math> следует, что существует такая вершина u, что <math>r[u] - r'[u] \ge r[v] - r'[v] \;</math> после каждого увеличения r[v]. Это означает, что <math>max_{v \in V} \; r[v] - r'[v]</math> не будет увеличиваться. Иначе говоря, существует по меньшей мере одна вершина v, у которой r[v] не будет меняться. До увеличения r[v] имеет место соотношение wu^v — r[u] + r[v] < 0, где wu^v > 0 – исходное количество регистров на одной пути из u в v, в результате чего неравенство r[v] — r[u] < 1 остается верным даже после увеличения r[v]. Из этого следует, что будет по меньшей мере i + 1 вершин, у которых r не превышает i для 0 < i < jVj. Иными словами, алгоритм может по-прежнему увеличивать r, и когда какое-либо значение r достигнет j Vj, это показывает, что условие P3 удовлетворяется. Таким образом, полный алгоритм имеет следующую форму: r, t,<j) := 0,d,oo; dofP1g

9(u; v) 2 E: r[u] — r[v] = w[u; v]

A t[v] - t[u] < d[v] ! t[v] := t[u] + d[v] (8v2 V: r[v] < jVj)

A 9v 2 V: t[v] >ф^ r[v]; t[v] := r[v] + 1;d[v] (9v2 V:r[v] > jVj)

A 9v 2 V: t[v] > ф ! r[v]; t[v] := r[v] + 1;d[v] P0 A P2 А ф > max(t) ! ф := max(t) 9(u; v) 2 E: r[u] — r[v] > w[u; v]

-> r[v] := r[u] -w[u,v] odfP0 Л P1 Л P2 Л P3g :