Example List

Example files are given in three directories: (1) examplespec contains problem specifications, (2) examplesoln contains solutions, and (3) examplesynt contains solutions which retain artifacts from the specification. For each file in examplesynt, there is usually a corresponding file in examplesoln which is more presentable and simpler to verify.

Contents

1. Sum-Not-2
2. Coloring
3. Maximal Matching
4. Sorting on Chains and Rings
5. Orientation
6. Token Passing
7. Other

1. Sum-Not-2

Aly Farahat's dissertation includes a simple yet nontrivial unidirectional ring protocol. It has been extremely helpful for reasoning about the nature of livelocks in unidirectional rings and has a simple enough transition system to actually show in a presentation.

• SumNotTwo (spec)
• SumNotTarget (spec, soln) - The general case sum-not-(l-1) protocol given by Farahat.

2. Coloring

Graph coloring is a well-known problem with many applications. Each node in the graph is assigned a color. For this assignment to be called a coloring, each node must have a different color than the nodes adjacent to it. In a computer network, a coloring applies to processes that communicate directly with each other rather than nodes connected by edges.

• ColorRing [info] - 3-coloring on a ring.
• ColorRingSymm (spec, soln) - Unoriented ring.
• ColorUniRing (spec, soln) - Randomized 3-coloring on a unidirectional ring.
• ColorRingLocal [info] - Randomized distance-2 coloring on a unidirectional ring using 5 colors. Neither a process or its neighbors can have the same color as another neighbor.
• ColorRingDistrib [info] - Randomized 3-coloring on a ring where processes have communication delay.
• ColorChain (spec) - 2-coloring on a chain.
• ColorTree (spec, soln) - Tree.
• ColorTorus (spec) - Torus.
• ColorMobius (spec) - Mobius ladder.
• ColorKautz (spec) - 4-coloring on generalized Kautz graph of degree 2. We can find a protocol that stabilizes for up to 13 processes, but not 14. Tweaking the topology by reversing edges or removing orientation (even with bidirectional edges) gives definite impossibility results at around 8 processes.

3. Maximal Matching

Matching is well-known problem from graph theory. A matching is a set of edges which do not share any common vertices. For a matching to be maximal, it must be impossible to add another edge to the set without breaking the matching property.

• MatchRing [info] - Natural specification for matching using the edges in the ring. This gives the 1-bit solution.
• MatchRingThreeState [info] - Maximal matching on a ring where processes point in certain directions.
• MatchRingOneBit [info] - Using the 3-state specification, find a matching using 1 bit per process.
• SegmentRing [info] - A problem similar to matching where a ring is segmented into chains.

4. Sorting on Chains and Rings

• SortChain (spec, soln) - Sorting a chain of values. Easy to synthesize, but solution is manually simplified.
• SortRing (spec, soln) - Sorting a ring of values using a unique zero value to mark the beginning of the sequence. Easy to synthesize, but solution is manually simplified.

5. Orientation

• OrientDaisy [info] - Silent orientation for daisy chains (either ring and chain), verified for 2 to 15 processes. The version in examplesoln behaves similarly, is simpler, but is slightly less optimal.
• OrientRing [info] - Manually designed silent ring orientation, verified for 2 to 26 processes. Also works under synchronous scheduler.
• OrientRingOdd [info] - From Hoepman.
• OrientRingViaToken (spec, soln) - From Israeli and Jalfon.

6. Token Passing

• TokenRingFiveState [info] - 5-state token ring whose behavior is specified with shadow variables.
• TokenRingSixState [info] - 6-state token ring specified with variable superposition.
• TokenRingThreeBit [info] - 3-bit token ring from Gouda and Haddix.
• TokenRingFourState (synt) - 4-state token ring specified with variable superposition. This version is only stabilizing for 2 to 7 processes. It operates much like the 3-bit token ring.
• TokenRingDijkstra [info] - Dijkstra's stabilizing token ring.
• TokenChainThreeState [info] - 3-state token passing on a chain topology.
• TokenChainDijkstra [info] - Dijkstra's 4-state token passing on a chain topology.
• TokenRingThreeState [info] - 3-state token passing on a bidirectional ring. One solution is from Dijkstra, the other is from Chernoy, Shalom, and Zaks.
• TokenRingOdd (spec, soln) - Randomized token passing protocol on odd-sized rings.

7. Other

• ByzantineGenerals (spec, soln) - The Byzantine generals problem formulated as an instance of self-stabilization.
• DiningCrypto (spec, soln) - The dining cryptographers problem as an instance of self-stabilization, where the initial state is assumed to randomize the coins. We can't model anonymity, only determination of whether a cryptographer or the NSA pays for dinner.
• DiningPhilo (spec, soln) - The dining philosophers problem. This version assumes a coloring in order to break symmetry.
• DiningPhiloRand (spec, soln) - The dining philosophers problem. This version uses randomization to break symmetry.
• LeaderRingHuang (spec, soln) - Leader election protocol on prime-sized rings from Huang.
• Sat (spec) - Example reduction from 3-SAT to adding stabilization from our paper showing NP-completeness of adding convergence.
• StopAndWait (spec, soln) - The Stop-and-Wait protocol, otherwise known as the Alternating Bit protocol when the sequence number is binary.