Distributed Model Checking

Distributed Model Checking allows to check invariants and deadlock-freedom (and assertions) with additional computational power. The distributed version of ProB is named distb. In the following, we will document how to run it.

Overview

distb consists of three components.

• A master which coordinates the model checking process. Per distributed model checking, it must run exactly once.
• A proxy which coordinates workers on its machine. It should run (at least, but usually) once per participating machine.
• A worker which does the actual work. A good number of workers usually is close to the amount of available (physical) CPU cores of a participating machine.

Setting up shared memory

It might be necessary to increase the limits of how much shared memory may be allocated, both per segment and overall. This is, to our knowledge, required for Mac OS X and older versions of Ubuntu. You can view the limits by running:

sysctl -a | grep shm

Per default, recent versions of Ubuntu set the following values:

kernel.shmall = 18446744073692774399
kernel.shmmax = 18446744073692774399
kernel.shmmni = 4096

On Mac OS X, the keys might be different and you can set them by executing:

sudo sysctl -w kern.sysv.shmmax=18446744073692774399
sudo sysctl -w kern.sysv.shmseg=4096
sudo sysctl -w kern.sysv.shmall=18446744073692774399

Running distb

Run once per machine:

/path/to/prob/lib/proxy $MASTER_IP 5000 $IP 30 $LOGFILE_PROXY $PROXY_NUMBER

Note that on Linux systems you might need to set the LD_LIBRARY_PATH variable to find the ZeroMQ libraries beforehand (for all components):

export LD_LIBRARY_PATH=/path/to/prob/lib

Run once per model checking:

/path/to/prob/probcli -bf -zmq_master <unique identifier> $MODEL

Run as many workers as you want:

/path/to/prob/probcli -zmq_worker <unique identifier> &

You can fine-tune the following parameters by adding -p NAME VALUE to the corresponding call (e.g., ./probcli -zmq_worker worker1 -p port 5010 -p max_states_in_memory 100) :