SSA-Tool: Working with Self-Stabilizing Algorithms

This is a set of tools for the representation, creation, and evaluation of self-stabilizing algorithms.

Introduction

A self-stabilizing network is seen as a graph of state machines. Each privilege is realized as a transition from the current state to another state. The state of the graph is passed as input to this state machine. When the input graph matches some predicate, this privilege is set – there is some transition out of this state. This is why the choice of predicate to act upon is arbitrary: you can only move to one other state!

When every node of the graph is in an accepting state with no set predicates, then the graph has stabilized.

Privilege

• We consider graphs of finite state machines.
• Privileges are boolean functions of the FSM’s state and the states of its neighbors.
• When these functions are true, the privilege is ‘present’.

System State

• Each legitimate state must have at least one privilege present, even if the action is ‘do nothing’
• In each legitimate state, every possible action will maintain legitimacy.
• Each privilege must be present in at least one legitimate state.
• For any given pair of legitimate states, there exists a transformation between them.

Self-Stabilization

Regardless of the initial state and regardless of the privilege selected each time for the next move, at least one privilege will always be present and the system is guaranteed to find itself in a legitimate state after a finite number of moves.

References

• Edsger W. Dijkstra. 1974. Self-stabilizing systems in spite of distributed control. Commun. ACM 17, 11 (November 1974), 643-644. DOI=http://dx.doi.org/10.1145/361179.361202

Examples

# define your predicates/moves
# predicates have access to node (v) and neighborhood (N) attributes
cat <<DONE > unmarked-and-neighbors-unmarked.py
marked = v['marked']
neighbor_marked = any(map(lambda n: n['marked'], N))
RESULT = not (marked or neighbor_marked)
DONE

cat <<DONE > marked-and-neighbor-marked.py
marked = v['marked']
neighbor_marked = any(map(lambda n: n['marked'], N))
RESULT = marked and neighbor_marked
DONE

# moves can set node state
cat <<DONE > mark.py
v['marked'] = True
DONE

cat <<DONE > unmark.py
v['marked'] = False
DONE


# move predefined code to the bundle
python3 ssa.py indset.ssax new predicate can-mark -p marked bool < unmarked-and-neighbors-unmarked.py
python3 ssa.py indset.ssax new move      mark     -p marked bool < mark.py

python3 ssa.py indset.ssax new predicate must-unmark -p marked bool < marked-and-neighbor-marked.py
python3 ssa.py indset.ssax new move      unmark      -p marked bool < unmark.py

# create a new algorithm
python3 ssa.py indset.ssax new algorithm 'Independent Set'

# define rules for that algorithm
python3 ssa.py indset.ssax add-rule-to 'Independent Set' can-mark mark
python3 ssa.py indset.ssax add-rule-to 'Independent Set' must-unmark unmark

# run the algorithm
python3 ssa.py indset.ssax run 'Independent Set' gn,5 1000 100

The above run command generates 1000 graphs and iterates the algorithm 100 times on each. The properties of nodes in the graph are determined by the predicates and moves composing the rules in the algorithm. For example:

-p age range,1,120...

In this example, range is called the generator descriptor and 1,120 are its arguments. This particular specification will ensure each node has an age attribute with a value between 1 and 120. The actual graph itself is determined by the gn,5 string you see in the run command. The descriptor here (gn) determines what mathematical properties the generated graph will have (tree/path/cycle/grid/…). Note some graph-generators can provide properties of their own.

Property generators defined on predicates/moves can be overridden at run-time with the --property-override option to run.

The definitive list of graph- and property-generators (and their arguments) are available in ssa.trial.

Installing

This package can be installed locally using pip install .. Be sure to install the requirements with pip install -r requirements.txt.

Alternatively, use the targets from the Makefile: make dependencies install.