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