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.
See: examplespec/TokenRingThreeBit.prot
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 that 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 5
Is the protocol stabilizing on a ring of size 3?
protocon -verify -x tmp/3bit.prot -def N 3
How about of size 4 or 6?
protocon -verify -x tmp/3bit.prot -def N 4
protocon -verify -x tmp/3bit.prot -def N 6
Probably 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 6
But 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 that 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 ]
See: examplesoln/TokenRingThreeBit.prot
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.