No edit summary |
No edit summary |
||
| Line 25: | Line 25: | ||
$ ./parB.sh 2 ~/parB.log scheduler.mch | $ ./parB.sh 2 ~/parB.log scheduler.mch | ||
== Running in the Cloud/Cluster == | |||
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: | 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: | ||
| Line 35: | Line 36: | ||
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. | 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. | |||
== Cleaning up == | |||
If something goes wrong it may be necessary to clean up your shared memory. | 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 <tt>ipcs</tt>. | You can find out if there are still memory blocks occupied using <tt>ipcs</tt>. | ||
Removal can be done using: | Removal can be done using: | ||
ipcrm -M `ipcs | grep <YOUR USERNAME> | grep -o "0x[^ ]*" | sed ':a;N;$!ba;s/\n/ -M /g'` | ipcrm -M `ipcs | grep <YOUR USERNAME> | grep -o "0x[^ ]*" | sed ':a;N;$!ba;s/\n/ -M /g'` | ||
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:
probcli -zmq_worker2 <MASTER_IP> <MASTER_PORT> 0
probcli -zmq_master2 <MIN 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.
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.
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'`