Use Potential Functions to explore Algorithms Worst-Case

Foreword

A simulator is useful to study the time complexity of algorithms. For example, one can experimentally check whether existing theoretical bounds are correct or tight. Simulations are also useful to get insights when no bound is known. In this context, we are therefore interested in finding the worst-cases (in steps).

We propose here to demonstrate how to use sasa to that end, focusing on one of the two sources of non-determinism in self-stabilizing algorithms: the scheduling of process activations, a.k.a., daemon1

For a given topology and an initial configuration, the stabilization time in steps of an algorithm depends on the choices made by the daemon. Finding a worst-case stabilization time requires to explore all the illegitimate configurations of the transition system, that can be huge. We propose here how to use sasa to explore efficiently and/or partially this state space.

Let’s download an example available in the git repository (if you haven’t already done this clone in other vtt posts) and go to the coloring directory.

[ -d "sasa" ] || git clone https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa.git
cd sasa/test/coloring

In average, for the test/coloring/ algorithm on a 5x5 grid using the default (distributed) daemon, a silent configuration is reached in a little bit more than 3 steps.

make grid5.dot # generate a 5x5 grid
make grid5.cmxs # compile what's needed
n=100 # let's run 100 simulations on this topology
count=`for ((a=1; a <= $n ; a++)) do sasa grid5.dot; done | grep silent | cut -d ' ' -f8 | paste -sd+ | bc`
average=`echo "$count / $n" | bc -l ` # and compute the resulting average step number
    printf  "In average, the distributed daemon needs %.2f steps (%d/%d)\n" $average $count $n

1

  In average, the distributed daemon needs 3,25 steps (325/100)

For most algorithms, the central daemon requires more steps:

count=`for ((a=1; a <= $n ; a++)) do sasa -cd grid5.dot; done | grep silent | cut -d ' ' -f8 | paste -sd+ | bc`
average=`echo "$count / $n" | bc -l `
    printf  "In average, the distributed daemon needs %.2f steps (%d/%d)\n" $average $count $n

1

  In average, the distributed daemon needs 9,28 steps (928/100)

But following the ideas presented in this article we can do better (or worst, depending on the point of view) by defining a potential function.

Define a potential function

A potential function associate to any configuration a number that measures its distance to the set of legitimate configurations. Such functions are useful to prove that an Algorithm converges: one just need to show that each step lead to a configuration that is strictly smaller.

In sasa, potential functions can be used used to guide daemons to search for worst case scenarios using a greedy approach: always chose the action that maximize the potential.

In order to define such a potential function, one has to respect the following API: Link to the Potential Functions API

For the coloring algorithm, using the number of color clashes is a good and simple way to define the potential (it is not always that easy):

let clash_number pidl get =
  let clash = ref 0 in
  let color pid = fst (get pid) in
  List.iter (fun pid ->
      List.iter (fun (n,_) -> if state n = color pid then incr clash) (snd (get pid)))
    pidl;
  float_of_int !clash

let potential = Some clash_number

Then one can launch a sasa simulation that takes advantage of this potential function:

 sasa grid5.dot --greedy-central-daemon # or sasa grid5.dot -gcd

 # Automatically generated by /home/jahier/.opam/4.14.0/bin/sasa version "v4.12.0" ("03b830c")
# on crevetete the 24/5/2023 at 14:58:52
#sasa grid5.dot --greedy-central-daemon

#seed 406940804
#inputs
#outputs "p0_c":int "p1_c":int "p2_c":int "p3_c":int "p4_c":int "p5_c":int "p6_c":int "p7_c":int "p8_c":int "p9_c":int "p10_c":int "p11_c":int "p12_c":int "p13_c":int "p14_c":int "p15_c":int "p16_c":int "p17_c":int "p18_c":int "p19_c":int "p20_c":int "p21_c":int "p22_c":int "p23_c":int "p24_c":int "Enab_p0_conflict":bool "Enab_p1_conflict":bool "Enab_p2_conflict":bool "Enab_p3_conflict":bool "Enab_p4_conflict":bool "Enab_p5_conflict":bool "Enab_p6_conflict":bool "Enab_p7_conflict":bool "Enab_p8_conflict":bool "Enab_p9_conflict":bool "Enab_p10_conflict":bool "Enab_p11_conflict":bool "Enab_p12_conflict":bool "Enab_p13_conflict":bool "Enab_p14_conflict":bool "Enab_p15_conflict":bool "Enab_p16_conflict":bool "Enab_p17_conflict":bool "Enab_p18_conflict":bool "Enab_p19_conflict":bool "Enab_p20_conflict":bool "Enab_p21_conflict":bool "Enab_p22_conflict":bool "Enab_p23_conflict":bool "Enab_p24_conflict":bool "p0_conflict":bool "p1_conflict":bool "p2_conflict":bool "p3_conflict":bool "p4_conflict":bool "p5_conflict":bool "p6_conflict":bool "p7_conflict":bool "p8_conflict":bool "p9_conflict":bool "p10_conflict":bool "p11_conflict":bool "p12_conflict":bool "p13_conflict":bool "p14_conflict":bool "p15_conflict":bool "p16_conflict":bool "p17_conflict":bool "p18_conflict":bool "p19_conflict":bool "p20_conflict":bool "p21_conflict":bool "p22_conflict":bool "p23_conflict":bool "p24_conflict":bool "legitimate":bool potential:real round:bool round_nb:int


#step 0
#outs 1 2 0 2 0 0 2 2 2 1 0 0 3 1 1 1 0 3 1 0 0 1 1 2 1 f t f t f t t t t t t t t t t f t t t f f t t f f f f f f f t f f f f f f f f f f f f f f f f f f f f 24. f 0

#step 1
#outs 1 2 0 2 0 3 2 2 2 1 0 0 3 1 1 1 0 3 1 0 0 1 1 2 1 f t f t f f t t t t t t t t t f t t t f f t t f f f f f f f f f f f t f f f f f f f f f f f f f f f f 22. f 1

#step 2
#outs 1 2 0 2 0 3 2 2 2 3 0 0 3 1 1 1 0 3 1 0 0 1 1 2 1 f t f t f f t t t f t t t t t f t t t f f t t f f f f f t f f f f f f f f f f f f f f f f f f f f f f 20. f 1

#step 3
#outs 1 2 0 1 0 3 2 2 2 3 0 0 3 1 1 1 0 3 1 0 0 1 1 2 1 f t f f f f t t t f t t t t t f t t t f f t t f f f f f f f f f f t f f f f f f f f f f f f f f f f f 18. f 1

#step 4
#outs 1 2 0 1 0 3 2 2 0 3 0 0 3 1 1 1 0 3 1 0 0 1 1 2 1 f t f f f f t t f f t t t t t f t t t f f t t f f f t f f f f f f f f f f f f f f f f f f f f f f f f 16. f 1

#step 5
#outs 1 3 0 1 0 3 2 2 0 3 0 0 3 1 1 1 0 3 1 0 0 1 1 2 1 f f f f f f t t f f t t t t t f t t t f f t t f f f f f f f f t f f f f f f f f f f f f f f f f f f f 14. f 1

#step 6
#outs 1 3 0 1 0 3 1 2 0 3 0 0 3 1 1 1 0 3 1 0 0 1 1 2 1 f f f f f f f f f f t t t t t f t t t f f t t f f f f f f f f f f f f f f t f f f f f f f f f f f f f 12. f 1

#step 7
#outs 1 3 0 1 0 3 1 2 0 3 0 0 4 1 1 1 0 3 1 0 0 1 1 2 1 f f f f f f f f f f t t f t t f t f t f f t t f f f f f f f f f f f f f f f f t f f f f f f f f f f f 10. f 1

#step 8
#outs 1 3 0 1 0 3 1 2 0 3 0 0 4 1 2 1 0 3 1 0 0 1 1 2 1 f f f f f f f f f f t t f t f f t f t f f t t f f f f f f f f f f f f t f f f f f f f f f f f f f f f 8. f 1

#step 9
#outs 1 3 0 1 0 3 1 2 0 3 2 0 4 1 2 1 0 3 1 0 0 1 1 2 1 f f f f f f f f f f f t f t f f t f t f f t t f f f f f f f f f f f f f f f t f f f f f f f f f f f f 6. f 1

#step 10
#outs 1 3 0 1 0 3 1 2 0 3 2 0 4 3 2 1 0 3 1 0 0 1 1 2 1 f f f f f f f f f f f t f f f f t f f f f t t f f f f f f f f f f f f f f f f f f t f f f f f f f f f 4. f 1

#step 11
#outs 1 3 0 1 0 3 1 2 0 3 2 0 4 3 2 1 2 3 1 0 0 1 1 2 1 f f f f f f f f f f f f f f f f f f f f f t t f f f f f f f f f f f f f f f f f f f f f f f t f f f f 2. f 1

#step 12
#outs 1 3 0 1 0 3 1 2 0 3 2 0 4 3 2 1 2 3 1 0 0 3 1 2 1 f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f f t 0. t 1

This algo is silent after 12 moves, 12 steps, 1 round.

Note that you may obtain a different number of steps, as such greedy daemon remains non-deterministic, since when several actions can lead to the same (highest) value of the potential, one is chosen at random.

For this particular algorithm, using a non-central daemon would not be a good idea, because:

  1. non-central greedy daemons are much more costly: 2^n-1 possibilities (where n is the number of enabled processes) should be considered instead of n for central daemons
  2. the coloring algorithm does not converge under distributed algorithm
 sasa grid5.dot --greedy-daemon # or sasa grid5.dot -gd

nb: you might need to be patient if a lot of clashes exist in the initial configuration.

nb 2: sometimes its converges!

# Automatically generated by /home/jahier/.opam/4.14.0/bin/sasa version "v4.12.0" ("03b830c")
# on crevetete the 24/5/2023 at 15:16:13
#sasa grid5.dot --greedy-daemon

#seed 625362118
#inputs
#outputs "p0_c":int "p1_c":int "p2_c":int "p3_c":int "p4_c":int "p5_c":int "p6_c":int "p7_c":int "p8_c":int "p9_c":int "p10_c":int "p11_c":int "p12_c":int "p13_c":int "p14_c":int "p15_c":int "p16_c":int "p17_c":int "p18_c":int "p19_c":int "p20_c":int "p21_c":int "p22_c":int "p23_c":int "p24_c":int "Enab_p0_conflict":bool "Enab_p1_conflict":bool "Enab_p2_conflict":bool "Enab_p3_conflict":bool "Enab_p4_conflict":bool "Enab_p5_conflict":bool "Enab_p6_conflict":bool "Enab_p7_conflict":bool "Enab_p8_conflict":bool "Enab_p9_conflict":bool "Enab_p10_conflict":bool "Enab_p11_conflict":bool "Enab_p12_conflict":bool "Enab_p13_conflict":bool "Enab_p14_conflict":bool "Enab_p15_conflict":bool "Enab_p16_conflict":bool "Enab_p17_conflict":bool "Enab_p18_conflict":bool "Enab_p19_conflict":bool "Enab_p20_conflict":bool "Enab_p21_conflict":bool "Enab_p22_conflict":bool "Enab_p23_conflict":bool "Enab_p24_conflict":bool "p0_conflict":bool "p1_conflict":bool "p2_conflict":bool "p3_conflict":bool "p4_conflict":bool "p5_conflict":bool "p6_conflict":bool "p7_conflict":bool "p8_conflict":bool "p9_conflict":bool "p10_conflict":bool "p11_conflict":bool "p12_conflict":bool "p13_conflict":bool "p14_conflict":bool "p15_conflict":bool "p16_conflict":bool "p17_conflict":bool "p18_conflict":bool "p19_conflict":bool "p20_conflict":bool "p21_conflict":bool "p22_conflict":bool "p23_conflict":bool "p24_conflict":bool "legitimate":bool potential:real round:bool round_nb:int


#step 0
#outs 0 1 0 1 0 0 3 0 3 1 2 0 0 3 0 0 2 2 2 1 0 0 1 2 1 t f t f f t f t t f f t t t f t t t t t t t f t t f f f f f f f f f f f f f f f f f f f f f f f t t f 22. f 0

#step 1
#outs 0 1 0 1 0 0 3 0 3 1 2 0 0 3 0 0 2 2 2 1 0 0 1 0 0 t f t f f t f t t f f t t t f t t t t f t t f t t f f f f f f f f f f f f f f f f f f f f f f f t f f 20. f 1

#step 2
#outs 0 1 0 1 0 0 3 0 3 1 2 0 0 3 0 0 2 2 2 1 0 0 1 3 0 t f t f f t f t t f f t t t f t t t t f t t f f f f f f f f f f f f f f f f f f f f f t f f f f f f f 18. f 1

#step 3
#outs 0 1 0 1 0 0 3 0 3 1 2 0 0 3 0 0 2 2 0 1 0 0 1 3 0 t f t f f t f t t f f t t t f t t t f f t t f f f f f f f f f f f f f f f f f f f f f f f f t f f f f 16. f 1

#step 4
#outs 0 1 0 1 0 0 3 0 3 1 2 0 0 3 0 0 2 2 0 1 0 3 1 3 0 t f t f f t f t t f f t t t f t t t f f t f f f f f f f f f f f f f f f f f f f t f f f f t f f f f f 14. f 1

#step 5
#outs 0 1 0 1 0 0 3 0 3 1 2 0 0 3 0 1 2 2 0 1 1 3 1 3 0 t f t f f t f t t f f t t t f t t t f f t f f f f f f f f f f f f f f f f f f f t f f f f t f f f f f 14. f 1

#step 6
#outs 0 1 0 1 0 0 3 0 3 1 2 0 0 3 0 0 2 2 0 1 0 3 1 3 0 t f t f f t f t t f f t t t f t t t f f t f f f f f f f f f f f f f f f f f f f t f f f f t f f f f f 14. f 1
...

nb: as you may notice, with the 625362118 seed, we reach at step 6 the same configuration as at step 4! This actually a proof of non-convergence.

Concluding remark

The coloring algorithm is a good example for illustrating potential functions because it is very simple. On the other hand, it is a rather poor example in the sense that it does not do better than a random central daemon to find worst-cases (cf this article for more details).

The sasa git repo contains several examples of potential functions, e.g.,

  1. The other source of non-determinism is when choosing an initial configuration, but it is the subject of another tutorial: find-worst-case-configuration [return]