Distributed Model Checking - Revision history

Philipp Koerner: add new preference

2018-01-26T13:19:46Z

add new preference

← Older revision		Revision as of 13:19, 26 January 2018
Line 46:		Line 46:

	<nowiki>/path/to/prob/probcli -zmq_worker <unique identifier> &</nowiki>		<nowiki>/path/to/prob/probcli -zmq_worker <unique identifier> &</nowiki>

			== Additional Preferences ==

	You can fine-tune the following parameters by adding -p NAME VALUE to the corresponding call (e.g., ./probcli -zmq_worker worker1 -p port 5010 -p max_states_in_memory 100) :		You can fine-tune the following parameters by adding -p NAME VALUE to the corresponding call (e.g., ./probcli -zmq_worker worker1 -p port 5010 -p max_states_in_memory 100) :
Line 66:		Line 68:
	\|-		\|-
	\| max_states_in_memory \|\| 1000 \|\| how many states may be kept in memory before written into a database \|\| worker		\| max_states_in_memory \|\| 1000 \|\| how many states may be kept in memory before written into a database \|\| worker
			\|-
			\| hash_cycle \|\| 25 \|\| minimum amount of milliseconds that has to pass between hash code updates from the master \|\| master
	\|}		\|}

Philipp Koerner: fix table

2018-01-26T10:35:39Z

fix table

← Older revision		Revision as of 10:35, 26 January 2018
Line 61:		Line 61:
	\| tmpdir \|\| /tmp/ \|\| directory for temporary files \|\| master, worker		\| tmpdir \|\| /tmp/ \|\| directory for temporary files \|\| master, worker
	\|-		\|-
	logdir \|\| ./distb-logs \|\| directory for log output (must exist) \|\| master, worker		\| logdir \|\| ./distb-logs \|\| directory for log output (must exist) \|\| master, worker
	\|-		\|-
	proxynumber \|\| 0 \|\| which proxy should the component connect to (if multiple run on the same machine) \|\| worker		\| proxynumber \|\| 0 \|\| which proxy should the component connect to (if multiple run on the same machine) \|\| worker
	\|-		\|-
	max_states_in_memory \|\| 1000 \|\| how many states may be kept in memory before written into a database \|\| worker		\| max_states_in_memory \|\| 1000 \|\| how many states may be kept in memory before written into a database \|\| worker
	\|}		\|}

Philipp Koerner: startup

2018-01-26T10:35:14Z

startup

← Older revision		Revision as of 10:35, 26 January 2018
Line 27:		Line 27:
	sudo sysctl -w kern.sysv.shmseg=4096		sudo sysctl -w kern.sysv.shmseg=4096
	sudo sysctl -w kern.sysv.shmall=18446744073692774399</nowiki>		sudo sysctl -w kern.sysv.shmall=18446744073692774399</nowiki>


			== Running ''distb'' ==

			Run once per machine:

			<nowiki>/path/to/prob/lib/proxy $MASTER_IP 5000 $IP 30 $LOGFILE_PROXY $PROXY_NUMBER</nowiki>

			Note that on Linux systems you might need to set the LD_LIBRARY_PATH variable to find the ZeroMQ libraries beforehand (for all components):

			<nowiki>export LD_LIBRARY_PATH=/path/to/prob/lib</nowiki>

			Run once per model checking:

			<nowiki>/path/to/prob/probcli -bf -zmq_master <unique identifier> $MODEL</nowiki>

			Run as many workers as you want:

			<nowiki>/path/to/prob/probcli -zmq_worker <unique identifier> &</nowiki>

			You can fine-tune the following parameters by adding -p NAME VALUE to the corresponding call (e.g., ./probcli -zmq_worker worker1 -p port 5010 -p max_states_in_memory 100) :


			{\| class="wikitable"
			! Parameter !! Default !! Description !! Applicable for...
			\|-
			\|port \|\| 5000 \|\| TCP ports should be used starting at... \|\| master, worker
			\|-
			\| ip \|\| localhost \|\| IP of the master component \|\| master
			\|-
			\| max_states \|\| 0 \|\| how many states should be checked at most (0 means all) \|\| master
			\|-
			\| tmpdir \|\| /tmp/ \|\| directory for temporary files \|\| master, worker
			\|-
			logdir \|\| ./distb-logs \|\| directory for log output (must exist) \|\| master, worker
			\|-
			proxynumber \|\| 0 \|\| which proxy should the component connect to (if multiple run on the same machine) \|\| worker
			\|-
			max_states_in_memory \|\| 1000 \|\| how many states may be kept in memory before written into a database \|\| worker
			\|}

Philipp Koerner: add distributed model checking page

2018-01-26T10:23:20Z

add distributed model checking page

New page

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:

<nowiki>sysctl -a | grep shm</nowiki>

Per default, recent versions of Ubuntu set the following values:

<nowiki>kernel.shmall = 18446744073692774399
kernel.shmmax = 18446744073692774399
kernel.shmmni = 4096</nowiki>

On Mac OS X, the keys might be different and you can set them by executing:

<nowiki>sudo sysctl -w kern.sysv.shmmax=18446744073692774399
sudo sysctl -w kern.sysv.shmseg=4096
sudo sysctl -w kern.sysv.shmall=18446744073692774399</nowiki>