ViSiDiA is a tool for implementing, simulating, testing and visualizing distributed algorithms. It is motivated by the important theoretical results on the use of graph relabelling systems to encode distributed algorithms and to prove their corretness.

The high level encoding of distributed algorithms in form of rewriting systems allows a better description and presentation of these algorithms. The result is a formal approach to decribe and study distributed algorithms in a unified and simple way.

ViSiDiA provides a library together with an easy interface to implement distributed algorithms described by means of local computations.

This tool can be used to visualize and experiment distributed algorithms, and therefore helps in their design and their validation.

Several distributed algorithms have been already implemented and can be directly animated.

Consider an anonymous network of processors with arbitrary topology, represented as a connected, undirected graph where vertices denote processors, and edges denote direct communication links. An algorithm is encoded by means of local relabellings. Labels attached to vertices and edges are modified locally, that is on a subgraph of fixed radius k of the given graph, according to certain rules depending on the subgraph only (k-local computations). The relabelling is performed until no more transformation is possible.

The corresponding configuration is said to be in normal form. Two sequential relabelling steps are said to be independent if they are applied on disjoint subgraphs. In this case they may be applied in any order or even concurrently.

The model of distributed computation is an asynchronous distributed network of processes which communicate by exchanging messages. To overcome the problem of certain nondeterministic distributed algorithms as well as to have efficient and easy implementations, we use randomization. Each process tries at random to synchronize with one of its neighbours or with all of its neighbours depending on the model we choose, then once synchronized, local computations can be done. A synchronization between two neighbours is called a rendez-vous, and a synchronization between a vertex and all its neighbours is called a star synchronization. Procedures implementing synchronizations are provided by the primitives rendezVous, starSynchro1 and starSynchro2 (given below). These procedures allows local computations to be performed between a processorand its neighbour(s) through a transcient synchronization. The visualization of an algorithms shows all the synchronizations which can happen at the same time. Exchanged messages and the processor states are also displayed on-the-fly.

The tool provides a GUI which can be used to draw by ``drag and drop'' a graph which will model the network. The user can add, delete, or select vertices, edges or subgraphs. Visual attributes of vertices and edges such as labels, colors or shapes have default values, but they can be easily customized, for instance to assign an initial labelling to the vertices of the graph, such as a label A to a particular vertex, and N to all other vertices. Note that N is the default label of vertices.

A library of high level primitives is available to program the corresponding local computations. The following java code shows the implementation of the spanning tree.

while (run) {

   neighbour = rendezVous();

   sendTo(neighbour,myLabel);

   neighbourLabel=receiveFrom(neighbour);

   if (myLabel == 'N') && (neighbourLabel == 'A'){

        myLabel = 'A';

        edge[neighbour]=1

        }

   breakSynchro();

}

Note that one has to choose first the type of local computation by choosing one of the three primitives: rendezVous(), starSynchro1(), and starSynchro2()) which are implemented as follows:

1. rendezVous(): a function that returns the neighbour with whom the synchronization occurs.
2. starSyncho1(): returns the center of the star during a star synchronization. Only the center can update its attributes.
3. starSynchro2(): returns the center of the star during a star synchronization. The center and its neighbours can update their attributes.

After compiling the module implementing the relabelling system, the user can execute it by pressing on appropriate buttoms provided by the interface. The system automatically creates and assigns to each vertex a java thread which will run a copy (a clone) of the code implementing the relabelling system. The user can observe the messages exchanged between vertices (threads), and their states. In particular, label changes of vertices can be seen on-line. The whole algorithm is animated in such a way that the user can follow its execution. Moreover, the number of exchanged messages is computed and displayed. This can be used to perform experiments on particular distributed algorithms described within our framework.

Many examples of distributed, described by graph relabelling systems, are given in Examples. For each of these examples, we give the relabelling system and a few screenshots.

An interesting advantage of our approach is that we only need to implement local rewritings to code complicated distributed algorithms. Therefore, visualizing the execution of these algorithms consists of animating distributed local computations.