Distributed Model Checking

Revision as of 10:35, 26 January 2018 by Philipp Koerner (talk | contribs) (fix table)

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) :


Parameter Default Description Applicable for...
port 5000 TCP ports should be used starting at... master, worker
ip localhost IP of the master component master
max_states 0 how many states should be checked at most (0 means all) master
tmpdir /tmp/ directory for temporary files master, worker
logdir ./distb-logs directory for log output (must exist) master, worker
proxynumber 0 which proxy should the component connect to (if multiple run on the same machine) worker
max_states_in_memory 1000 how many states may be kept in memory before written into a database worker