Token passing systems are used for distributed mutual exclusion, where exactly one process has a token at any given time, and the token must be passed in order for other processes to have this privilege. In the context of self-stabilization, the system may be in a state with multiple tokens, and it therefore must converge to having a single token.
TokenRingDijkstra. (spec, args, soln)
TokenRing. (spec, args, synt, soln )
This is a unidirectional token ring that has 5 states per process. Without using randomization, no smaller token ring exists. Interestingly, we can still pass a token with every action in the invariant.
TokenRingSixState. (spec, args, synt, soln)
TokenRingThreeBit. (spec, args, synt, soln)
This section shows how to synthesize a self-stabilizing token ring using the same topology given by Gouda and Haddix in The Stabilizing Token Ring in Three Bits. It uses 8 states per process. Not every action in the invariant passes a token, which causes a noticeable lag for larger rings.
constant N := 3;
direct variable t[Nat % N] <- Nat % 2;
puppet variable e[Nat % N] <- Nat % 2;
puppet variable ready[Nat % N] <- Nat % 2;
// Converge to a state where one process has the token and execute the
// shadow protocol defined by the 'shadow action:' statements below.
(future & shadow)
(unique i <- Nat % N :
i == 0 && t[i-1] == t[i] // Bot has the token
||
i != 0 && t[i-1] != t[i] // P[i] has the token
);
process Bot[i <- Nat % 1]
{
// i==0
read: e[i-1], t[i-1];
write: e[i], t[i], ready[i];
// Enforce this behavior within the invariant:
shadow action: ( t[i-1] == t[i] --> t[i] := 1 - t[i-1]; );
}
process P[j <- Nat % (N-1)]
{
let i := j+1; // We really want P[1],...,P[N-1] rather than P[0],...,P[N-2].
read: e[i-1], t[i-1];
write: e[i], t[i], ready[i];
// Enforce this behavior within the invariant:
shadow action: ( t[i-1] != t[i] --> t[i] := t[i-1]; );
}
Each process can read e[i-1] and t[i-1] and can write e[i], t[i], and ready[i]. There is a distinguished process Bot which can act differently than the others.
The invariant is specified as all states where exactly one process has a token. Bot is defined to have a token when t[0] == t[N-1] and each other P process has a token when t[i] != t[i-1].
With the shadow actions, we enforce that processes act like Dijkstra's token ring on one bit (the t variables).
Let's try to find a stabilizing token ring using three bits on a ring of size 5.
protocon -x examplespec/TokenRingThreeBit.prot -o tmp/3bit.prot -def N 5Is the protocol stabilizing on a ring of size 3?
protocon -verify -x tmp/3bit.prot -def N 3How about of size 4 or 6?
protocon -verify -x tmp/3bit.prot -def N 4
protocon -verify -x tmp/3bit.prot -def N 6Probably not. Let's try again, taking those sizes into account!
protocon -x examplespec/TokenRingThreeBit.prot -o tmp/3bit.prot -def N 5 -param N 3 -param N 4 -param N 6But what if we want to search up to size 7, but it takes too long check a system of that size at each decision level? Use the -no-partial flag to just verify the protocol on that system after finding a protocol which is self-stabilizing for all smaller sizes.
protocon -x examplespec/TokenRingThreeBit.prot -o tmp/3bit.prot -def N 5 -param N 3 -param N 4 -param N 6 -param [ -def N 7 -no-partial ]
// Three bit token ring defined in
// Title: The Stabilizing Token Ring in Three Bits
// Author: Mohamed G. Gouda and F. Furman Haddix
// Year: 1996
constant N := 3;
direct variable t[Int % N] <- Int % 2;
puppet variable e[Int % N] <- Int % 2;
puppet variable ready[Int % N] <- Int % 2;
// Make the invariant exactly this, no smoothing over puppet variables is allowed.
(future & shadow)
(
// One process has the token.
(unique i <- Int % N :
i == 0 && t[i-1] == t[i]
|| i != 0 && t[i-1] != t[i]
)
//&&
//// Some process is enabled.
//// This and the actual token-passing behavior are
//// already enforced by the shadow protocol.
//// already enforced by the shadow protocol.
//(exists i <- Int % N :
// i == 0 && e[i-1] == e[i]
// || i != 0 && e[i-1] != e[i]
//)
);
process Bot[i <- Int % 1]
{
read: e[i-1], t[i-1];
write: e[i], t[i], ready[i];
// Enforce this behavior within the invariant:
shadow action:( t[i-1] == t[i] --> t[i] := 1 - t[i-1]; );
// Use these actions:
puppet action:
( e[i-1] == e[i] && t[i-1] != t[i]
--> e[i] := 1-e[i-1]; ready[i] := 0;
);
puppet action:
( e[i-1] == e[i] && t[i-1] == t[i] && !(t[i] == 1 || ready[i] == 1)
--> e[i] := 1-e[i-1]; ready[i] := 1;
);
puppet action:
( e[i-1] == e[i] && t[i-1] == t[i] && (t[i] == 1 || ready[i] == 1)
--> e[i] := 1-e[i-1]; t[i] := 1-t[i-1]; ready[i] := 0;
);
}
process P[j <- Int % (N-1)]
{
let i := j+1;
read: e[i-1], t[i-1];
write: e[i], t[i], ready[i];
// Enforce this behavior within the invariant:
shadow action:( t[i-1] != t[i] --> t[i] := t[i-1]; );
// Use these actions:
puppet action:
( e[i-1] != e[i] && t[i-1] == t[i]
--> e[i] := e[i-1]; ready[i] := 0;
);
puppet action:
( e[i-1] != e[i] && t[i-1] != t[i] && !(t[i] == 1 || ready[i] == 1)
--> e[i] := e[i-1]; ready[i] := 1;
);
puppet action:
( e[i-1] != e[i] && t[i-1] != t[i] && (t[i] == 1 || ready[i] == 1)
--> e[i] := e[i-1]; t[i] := t[i-1]; ready[i] := 0;
);
}
TokenRingThreeState. (spec, args, synt, soln)
This ring is bidirectional, and passes the token back-and-forth. Every action in the invariant passes a token.
TokenChainThreeState. (spec, args, synt, soln)
This is a bidirectional chain that passes the token back-and-forth. It uses 3 states per process. Not every action in the invariant passes a token, but the actions that do not pass the token can be run in parallel with the token-passing ones, so the performance hit is small.
TokenChainDijkstra. (spec, synt, soln)
This is a bidirectional chain that passes the token back-and-forth. It uses 4 states per process. It converges quickly and every action in the invariant passes the token.