ParB - Revision history

Michael Leuschel at 08:13, 29 May 2021

2021-05-29T08:13:43Z

← Older revision		Revision as of 08:13, 29 May 2021
Line 20:		Line 20:

	Usage		Usage
	./parB <Nr. of workers~~> <logfile~~> <file>		./parB <Nr. of workers> <file> [preferences to master/workers]

	Example usage:		Example usage:

Michael Leuschel: /* parB2.sh */

2020-04-23T08:37:05Z

parB2.sh

← Older revision		Revision as of 08:37, 23 April 2020
Line 127:		Line 127:

	== parB2.sh ==		== parB2.sh ==

			This file provides a few more options:

	<pre>		<pre>

Michael Leuschel: /* Files */

2020-04-23T08:35:41Z

Files

@@ Line 123: / Line 123: @@
 echo "Starting master: $dirname/$PROBCOMMAND -bf -zmq_master master $FILE $*"
 time "$dirname/$PROBCOMMAND" -bf -zmq_master master $FILE $*
 fi
 </pre>

Michael Leuschel: /* Files */

2020-04-23T08:35:07Z

Files

← Older revision		Revision as of 08:35, 23 April 2020
Line 58:		Line 58:
	= Files =		= Files =

	* [[:~~File~~:~~parB~~.~~sh]~~]		== parB.sh ==

			<pre>
			#!/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
			</pre>

Michael Leuschel at 08:33, 23 April 2020

2020-04-23T08:33:17Z

← Older revision		Revision as of 08:33, 23 April 2020
Line 55:		Line 55:
	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'`

			= Files =

			* [[:File:parB.sh]]

Jens Bendisposto: /* Running in the Cloud/Cluster */

2015-03-18T12:17:58Z

Running in the Cloud/Cluster

← Older revision		Revision as of 12:17, 18 March 2015
Line 29:		Line 29:

	* On each physical computer you need to start exactly one copy of <tt>lib/hasher</tt>.		* On each physical computer you need to start exactly one copy of <tt>lib/hasher</tt>.
			lib/hasher <MASTER_IP> <MASTER_PORT> 1
	* Multiple Copies of <tt>probcli</tt> configured as workers:		* Multiple Copies of <tt>probcli</tt> configured as workers:
	probcli -zmq_worker2 <MASTER_IP> <MASTER_PORT> 0		probcli -zmq_worker2 <MASTER_IP> <MASTER_PORT> 0
Line 40:		Line 41:
	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.		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.

	== Options ==		== Options ==

Jens Bendisposto at 12:14, 18 March 2015

2015-03-18T12:14:04Z

← Older revision		Revision as of 12:14, 18 March 2015
Line 33:		Line 33:
	* A single instance of <tt>probcli</tt> configured as the master:		* A single instance of <tt>probcli</tt> configured as the master:
	probcli -zmq_master2 <MIN QUEUE SIZE> <MAX NR OF STATES> <MASTER_PORT> 0 <LOGFILE> <MODEL_FILE>		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.		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.		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.

			== Options ==
			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)

	== Cleaning up ==		== Cleaning up ==

Jens Bendisposto at 10:31, 18 March 2015

2015-03-18T10:31:08Z

← Older revision		Revision as of 10:31, 18 March 2015
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'`

Jens Bendisposto at 10:27, 18 March 2015

2015-03-18T10:27:13Z

← Older revision		Revision as of 10:27, 18 March 2015
Line 31:		Line 31:
	probcli -zmq_worker2 <MASTER_IP> <MASTER_PORT> 0		probcli -zmq_worker2 <MASTER_IP> <MASTER_PORT> 0
	* A single instance of <tt>probcli</tt> configured as the master:		* A single instance of <tt>probcli</tt> configured as the master:
	probcli -zmq_master2 <~~MINIMAL~~ QUEUE SIZE> <MAX NR OF STATES> <MASTER_PORT> 0 <LOGFILE> <MODEL_FILE>		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.		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.

Jens Bendisposto at 10:20, 18 March 2015

2015-03-18T10:20:55Z

@@ Line 1: / Line 1: @@
-This page explains how to run the distributed model checking Prototype.
+This page explains how to run the distributed model checking prototype.
 Usage
   ./parB <Nr. of workers> <logfile> <file>
 Example usage:
   $ ./parB.sh 2 ~/parB.log scheduler.mch