(→Files) |
|||
Line 127: | Line 127: | ||
== parB2.sh == | == parB2.sh == | ||
This file provides a few more options: | |||
<pre> | <pre> |
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:
lib/hasher <MASTER_IP> <MASTER_PORT> 1
probcli -zmq_worker2 <MASTER_IP> <MASTER_PORT> 0
probcli -zmq_master2 <MIN QUEUE SIZE> <MAX NR OF STATES> <MASTER_PORT> 0 <LOGFILE> <MODEL_FILE>
The minimal queue length is used to determine if a worker is allowed to share its queue. The experiments have shown, that a number between 10 and 100 is fine. parB will stop after (at least) the maximal number of states have been explored, a value of -1 will explore all states (beware of this, if the state space is infinite!).
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.
We plan to develop a control interface that allows configuring the logical network in a more convenient way and running the model checker from within ProB.
You can use preferences in parB.sh (and the master) :
./parB <Nr. of workers> <logfile> <file> <additional probcli options> ./probcli <additional probcli options> -zmq_master2 <MIN QUEUE SIZE> <MAX NR OF STATES> <MASTER_PORT> 0 <LOGFILE> <MODEL_FILE> <additional probcli options>
If you use -strict, parB will stop as soon as a violation is found, otherwise parB will explore the full state space (up to the maximal number of states)
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'`
#!/bin/bash PROBCOMMAND=probcli if [ $# -lt 2 ] then echo "Too few parameters ($#) for parB" echo "Usage ./parB <Nr. of workers> <file> [preferences to master/workers]" exit -1 else PARB=$0 CORES=$1 FILE=$2 shift shift echo "Running ProB in Parallel (on .prob files)" # dirname if [ -h "$PARB" ] then realname=`readlink "$PARB"` dirname=`dirname "$realname"` else dirname=`dirname "$PARB"` fi #ulimit -d unlimited echo "Directory: $dirname" # dirname if [ -h "$PARB" ] then realname=`readlink "$PARB"` dirname=`dirname "$realname"` else dirname=`dirname "$PARB"` fi #ulimit -d unlimited # setting the library path to find the zmq shared libraries system=`uname` if [ $system = "Linux" ]; then export LD_LIBRARY_PATH="$dirname/lib${LD_LIBRARY_PATH:+:${LD_LIBRARY_PATH}}" fi echo "Directory: $dirname" echo "Starting workers in parallel" echo "$dirname/$PROBCOMMAND -zmq_worker <worker-id> $*" for (( i = 0 ; i < $CORES; i++ )) do "$dirname/$PROBCOMMAND" -zmq_worker $i $* & done ##Usage: ./proxy <master IP> <port start> <own IP> <queue threshold> <logfile> [<proxynumber>] echo "Starting proxy server: $dirname/lib/proxy localhost 5000" "$dirname/lib/proxy" localhost 5000 localhost 50 loggyMcLogface-proxy & echo "Starting master: $dirname/$PROBCOMMAND -bf -zmq_master master $FILE $*" time "$dirname/$PROBCOMMAND" -bf -zmq_master master $FILE $* fi
This file provides a few more options:
#!/bin/bash PROBCOMMAND=probcli if [ $# -lt 5 ] then echo "Usage ./parB2 <Nr. of workers> <minimum que size> <max number of states> <Port (usually 5000)> <logdir> <model>" exit -1 else echo "Running ProB in Parallel (on .prob files)" # dirname if [ -h "$0" ] then realname=`readlink "$0"` dirname=`dirname "$realname"` else dirname=`dirname "$0"` fi ulimit -d unlimited echo "Directory: $dirname" mkdir -p $5 # dirname if [ -h "$0" ] then realname=`readlink "$0"` dirname=`dirname "$realname"` else dirname=`dirname "$0"` fi ulimit -d unlimited # setting the library path to find the zmq shared libraries system=`uname` if [ $system = "Linux" ]; then export LD_LIBRARY_PATH="$dirname/lib${LD_LIBRARY_PATH:+:${LD_LIBRARY_PATH}}" fi echo "Directory: $dirname" #cd $dirname #ls echo "Starting workers in parallel" for (( i = 0 ; i < $1; i++ )) do "$dirname/$PROBCOMMAND" -bf -zmq_worker $i -p logdir $5 & done echo "Starting proxy server: $dirname/lib/proxy localhost $4 localhost $2 $5/log-proxy " "$dirname/lib/proxy" localhost $4 localhost $2 $5/log-proxy & echo "Starting master: $dirname/$PROBCOMMAND -bf -zmq_master master -p queue_threshold $2 -p max_states $3 -p port $4 -p logdir $5" time "$dirname/$PROBCOMMAND" -bf -zmq_master master $6 -p queue_threshold $2 -p max_states $3 -p port $4 -p logdir $5 fi