Specification and Analysis of a Reliable Broadcasting Protocol in Maude - Dynamic Network Topology

RBP performs reliable broadcasting of information in networks with dynamic topology. Reliable broadcasting is not trivial when the topology of the network can change due to failure and mobility. The aim is to ensure that all nodes that satisfy certain connectedness criteria receive the information within finite time, and that the source is notified about it. The protocol should furthermore incur as low latency and as few messages as possible.

Similar to the static case, the network is modeled as an undirected connected graph, where each node knows its neighbors but does not know anything more about the topology. The dynamic case requires the handling of connecting and disconnecting network sections. If a new link (i,b) is established and nodes i and b reside in different, unconnected parts of the network, then messages that have been sent to i must be forwarded to b and vice a versa. For example, if i has heard the latest message from source j, and b has not yet heard it because it had no physical path to j, then i forwards this message. If i is still active for the original diffusion computation started at j, then the upcoming link only introduces a new neighbor to which i sends the latest message and waits for an acknowledgment before i acknowledges to its parent (the parent is the node which forwarded the source message to i). If i has already finished its computation for the original diffusion computation, i.e., it reported back to its parent the receipt of acks from all its direct neighbors, then i has to start a new local diffusion computation with itself as the source node. This results in all nodes in b's connected component receivin the latest message from j.

There can be more than one message in a network. For example, different partitions of the network can have different messages which are in transit, and those messages might be forwarded to another partition when a new link comes up. Thus, each node has to store the latest number of a message with respect to a specific source node. Similarly, all other information is parametric in the source node. We summarize the necessary data structure in the following:

1. Each node has a set of direct neighbors, stored in the attribute N^i.
2. A node is either ``active'' or ``passive'' wrt to sending a message of a specific source node. After node i sends out the latest message for source node j it becomes active wrt to j and stays active until it receives acknowledgments about the receipt of the message from all its direct neighbors. The state of a node is stored in the flag ST^i_j.
3. A node stores the ``parent'' for a given source node, i.e., the node from which it heard first the latest message of that source node. The parent is referred to as s^i_j. s^i_j becomes the successor node in the path back towards the source node. If i itself is the source (either of a original diffusing computation or of a local diffusion computation due to upcoming links between partitions of the network) then i=s^i_j.
4. Each neighbor is either ``active'' or ``passive'' wrt to an ongoing broadcast for a source node message. ST^i_{jk} is a flag which is set to active if node i has forwarded a message from source j to node k and has not yet received an acknowledgement for the message.
5. The sequence number of the latest message from source j seen at node i is stored in SQ^i_j. It is initially set to zero and can only be a positive number.

The following summarizes the latest version of the pseudocode for RBP in the case of dynamic networks. It underwent several revisions due to errors found by formalizing the original pseudocode with Maude and analysing it with different analysis such as default test executions and exhaustive search.

Pseudocode of RBP for Dynamic Topologies

Pseudocode and Maude specification are in tight connection. In order to read the (commented) Maude specification, one should take the following mapping table into account:

Pseudocode	Maude specification
N^i	nbs: OidSet
ST^i_j	states: IdStatusPFun
s^i_j	parents: IdIdPFun
SQ^i_j	seqNos: IdIntPFun
ST^i_{jk}	nbsStates: IdIdStatusPFun
m	M
i	A
p,q	B
j	C
msg_m for source j from p	msg M to A from B Src C
ack_m for source j from q	ack M to A from B Src C

The Maude specification for dynamic network topologies

We have defined three test configurations, namely, test1, test2, and test3. The test configuration can be described in the following way:

1. test1 describes a network with three nodes a, b, c. The nodes are all connected with each other.
2. In test2 a network with two nodes b, c is defined which are not connected. A message to establish a link between b and c is present.
3. test3 tests a failure of a link. In the network consisting of the three nodes a, b, c, node a is only connected to node b, whereas node b has also a link to c. The link between a and b eventually fails.

  eq test1 = < a : Node | nbs : nbs(b,c),  
			  states : states(state(a,passive), 
					  state(b,passive), 
					  state(c,passive)),
			  parents : mtparents,
			  seqNos : seqNos(seqNo(a,0),
					  seqNo(b,0),
					  seqNo(c,0)),
			  nbsStates : nbsStates(nbState(a,b,passive),
						nbState(a,c,passive),
						nbState(b,b,passive),
						nbState(b,c,passive),
						nbState(c,b,passive),
						nbState(c,c,passive)) >
	     < b : Node | nbs : nbs(a,c),
			  states : states(state(a,passive), 
					  state(b,passive), 
					  state(c,passive)),
			  parents : mtparents,
			  seqNos : seqNos(seqNo(a,0),
					  seqNo(b,0),
					  seqNo(c,0)),
			  nbsStates : nbsStates(nbState(a,a,passive),
						nbState(a,c,passive),
						nbState(b,a,passive),
						nbState(b,c,passive),
						nbState(c,a,passive),
						nbState(c,c,passive)) >
	     < c : Node | nbs : nbs(b,a), 
			  states : states(state(a,passive), 
					  state(b,passive), 
					  state(c,passive)),
			  parents : mtparents,
			  seqNos : seqNos(seqNo(a,0),
					  seqNo(b,0),
					  seqNo(c,0)),
			  nbsStates : nbsStates(nbState(a,a,passive),
						nbState(a,b,passive),
						nbState(b,a,passive),
						nbState(b,b,passive),
						nbState(c,a,passive),
						nbState(c,a,passive)) > .

If we execute the default interpreter of Maude on the configuration test1, we get as a result configuration a network, in which node a has send message 1 to both its neighbors b and c. Source node a is also parent of message 1 in nodes b,c. This represents a situation in which the fastest transmission paths are the ones from the source directly to its neighbors. In a real application this might not always be true, due to performance of links. It is possible that there are other paths to send a message from source a to the other nodes of the network. For instance, the message is forwarded via neighbor b to node c. These alternative executions show up in an exhaustive search as presented further down.

More test runs are given in the following file:
Test runs using Maude's default interpreter

Sample execution:
1. Store Maude specification as "rbpDynamic.maude"
2. Start full-maude
3. "Maude> in rbpDynamic.maude"
4. Execute sample runs, e.g., "Maude> (rew test1 .)"

Maude's default interpreter only executes one of the many possible rewrite paths starting with a given initial term. For a deeper analysis, we provide a strategy which returns all nonrewritable states reachable from the initial state. This strategy is parametric in the underlying protocol, and thus, reusable for both, the static and the dynamic case.

The specification of the strategy

Test runs of this exhaustive search strategy for the dynamic case

Sample execution:
1. Store Maude specification for strategy as "strat.maude"
2. Start full-maude
3. "Maude> in rbpDynamic.maude"
4. "Maude> in strat.maude"
5. Execute sample runs, e.g., "Maude> (red irreducibleforms(RBP, {'test1}'Configuration, allstaticrules) .)"

If we execute the search strategy on the initial configuration test1, we get three different final states:

1. The first term corresponds to the default execution of test1.
2. The second term represents the situation in which b forwarded message 1 from source a to node c, before the message which has been send directly by a arrived. Thus, node c has b as the parent for source a stored ('parents`:_['parent[{'a}'Oid,{'b}'Oid]]).
3. The third result term represents the situation in which node c forwarded the message from the source node a to node b.

If we execute the search strategy on the initial configuration test3, we get four different final states:

1. The first final configuration corresponds a network with nodes a,b,c, where only link between b and c exists. The link between a and b failed before node a could send a message.
2. The second configuration represents the state in which a could send its message to b and b received this message before the link between a and b failed. Node b also forwarded the message to c.
3. In the third final configuration node a could send out the message, but the link between a and b broke down before b received that message. Consequently, neither b nor c received a's message.
4. The fourth result term is similar to the second one. The only difference is that the parent in node a has been deleted.

[Maude Home Page]