Skip to content

Latest commit

 

History

History
137 lines (115 loc) · 8.07 KB

index.md

File metadata and controls

137 lines (115 loc) · 8.07 KB

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.