protocon

Protocol Examples

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

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.

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.
• ColorRingDizzy (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.

Maximal Matching

Matching is well-known problem from graph theory. A matching is a set of edges that 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.
• MatchRingDizzy (spec, args) - Maximal matching on an unoriented ring.
• SegmentRing info - A problem similar to matching where a ring is segmented into chains.

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.

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.

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.

<— Leader Election –> <— Reduction from 3-SAT –>

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.

This site is open source. Improve this page.