Orientation on Odd-Sized Rings

Ring Orientation
Odd-Sized Ring Orientation
1. Problem Instance
2. Stabilizing Version
Daisy Chain Orientation

1. Ring Orientation

OrientRing. (spec, args, soln)

2. Odd-Sized Ring Orientation

OrientRingOdd. (spec, args, soln)

The examplespec/OddOrientRing.prot file specifies a bidirectional ring topology where processes wish to agree with each other on a direction around the ring. The topology is taken from the paper by Hoepman titled Uniform Deterministic Self-Stabilizing Ring-Orientation on Odd-Length Rings.

2.1. Problem Instance


// Ring orientation using the state-reading model.
// See examplesoln/OrientRingOdd.prot for the stabilizing version.

constant N := 3;

puppet variable color[Nat % N] <- Nat % 2;
puppet variable phase[Nat % N] <- Nat % 2;
direct variable way[Nat % (2*N)] <- Nat % 2;

// Eventually, all processes are pointing in the same direction.
((future & shadow) % puppet)
  (forall i <- Nat % N :
   way[2*i] == way[2*(i+1)]
  );

process P[i <- Nat % N]
{
  symmetric (hand_idx, j)  <- {# (2*i, i-1), (2*i+1, i+1) #}
  {
    write: way[hand_idx];
    read: color[j], phase[j];
  }
  write: color[i], phase[i];

  // Assume that some direction is chosen at all times.
  (assume & closed)
    (way[2*i] != way[2*i+1]);
}

Each process P[i] reads color[i-1], color[i+1], phase[i-1], and phase[i+1] and writes color[i], phase[i], way[2*i], and way[2*i+1].

Eventually we want all the way[2*i] values to equal each other and differ from the way[2*i+1] values. That is, we want each process to agree on a direction.

The color and phase variables are labeled as puppet because we allow the protocol to use them to achieve convergence.

The invariant is labeled as ((future & shadow) % puppet) since we only require closure within a new invariant I' rather than I. Also, the behavior of the protocol within the new invariant I' must be the same as the underlying (i.e., shadow) protocol within I.

2.2. Stabilizing Version


// Ring orientation protocol using the state-reading model defined in
// Title: Uniform Deterministic Self-Stabilizing Ring-Orientation on Odd-Length Rings
// Author: Jaap-Henk Hoepman
// Year: 1994

constant N := 3;

puppet variable color[Nat % N] <- Nat % 2;
puppet variable phase[Nat % N] <- Nat % 2;
direct variable way[Nat % (2*N)] <- Nat % 2;

// Eventually, all processes are pointing in the same direction.
((future & shadow) % puppet)
  (forall i <- Nat % N :
   way[2*i] == way[2*(i+1)]
  );

process P[i <- Nat % N]
{
  symmetric (hand_idx, j)  <- {# (2*i, i-1), (2*i+1, i+1) #}
  {
    write: way[hand_idx];
    read: color[j], phase[j];
  }
  write: color[i], phase[i];

  // Assume that some direction is chosen at all times.
  (assume & closed)
    (way[2*i] != way[2*i+1]);

  // Actions a,b,c,d from the paper
  puppet action:
    ( color[i-1]==color[i+1] && (color[i]==color[i-1] || phase[i]==1)
     -->
      color[i]:=1-color[i-1];
      phase[i]:=0;
    );

  // Actions e,f from the paper
  puppet action:
    (    color[i-1]==color[i] && color[i]!=color[i+1] && phase[i-1]==1 && phase[i]==0 && phase[i+1]==0
      || color[i+1]==color[i] && color[i]!=color[i-1] && phase[i+1]==1 && phase[i]==0 && phase[i-1]==0
     -->
      color[i] := 1-color[i];
      phase[i] := 1;
      way[2*i] := phase[i-1];
      way[2*i+1] := phase[i+1];
    );

  // Actions g,h,i,j from the paper
  puppet action:
    (    color[i-1]==color[i] && phase[i-1]==phase[i] && color[i]!=color[i+1]
      || color[i+1]==color[i] && phase[i+1]==phase[i] && color[i]!=color[i-1]
     -->
      phase[i] := 1-phase[i];
    );
}

3. Daisy Chain Orientation