ParB

This page explains how to run the distributed model checking prototype.

Note that the implementation does not work with Windows, only Linux andMac OS are supported.

It is required to set the limits for shared memory on some systems, this can be done using sysctl. Here is a little script that sets the limits. It takes the size of shared memory as parameter (usually the size of your memory in GB). You need to run the script with root rights.

#!/bin/bash
if [ $# -gt 0 ]; then
    echo "Setting SHM sizes:"
    sysctl -w kern.sysv.shmmax=`perl -e "print 1073741824*$1"`
    sysctl -w kern.sysv.shmseg=4096
    sysctl -w kern.sysv.shmall=`perl -e "print 262144*$1"`
    echo "Here are the current values:"
    sysctl -a | grep shm
else
    echo "You need to provide the size of shared memort (in full GB)"
fi

After setting up shared memory, you can use the parB.sh script that comes with the ProB distribution (see Download).

Usage

./parB <Nr. of workers> <logfile> <file>

Example usage:

$ ./parB.sh 2 ~/parB.log scheduler.mch

The script can only be used for computation on a single physical computer. If you want to use multiple computers, the setup is a bit more complex:

On each physical computer you need to start exactly one copy of lib/hasher.
Multiple Copies of probcli configured as workers:

probcli -zmq_worker2 <MASTER_IP> <MASTER_PORT> 0

A single instance of probcli configured as the master:

probcli -zmq_master2 <MINIMAL QUEUE SIZE> <MAX NR OF STATES> <MASTER_PORT>  0 <LOGFILE> <MODEL_FILE>

As a rule of thumb use one real core for each of the processes. On hyperthreads the model checking still becomes faster, but the speedup is only 1/4 for each additional hyperthread.

If something goes wrong it may be necessary to clean up your shared memory. You can find out if there are still memory blocks occupied using ipcs. Removal can be done using:

ipcrm -M `ipcs | grep <YOUR USERNAME> | grep -o "0x[^ ]*" | sed ':a;N;$!ba;s/\n/ -M /g'`