Swarm(1)User CommandsSwarm(1)

NAME

SYNTAX

    swarm [-F config_file] [option]*

DESCRIPTION

    Swarm generates a script that performs many small verification jobs in parallel, in an attempt to increase the problem coverage for very large verification problems. It is meant to be used on models for which standard verification with exhaustive, bitstate, hash-compaction etc. either runs out of memory, or takes more time than is available (e.g., days or weeks). Swarm uses parallelism and search diversification to reach its objectives.

    The user can use a configuration file to define how many processing cores are available, how much memory can be used, and how much time is available, among a range of other optional parameter settings. Based on this information, swarm generates the script that runs as many independent jobs as possible in parallel, without exceeding any of the user-defined constraints.

OPTIONS

    The typical use of swarm is with the help of a configuration file in which all options are recorded, for instance as follows: 
    	$ swarm -F swarm.lib > script
	$ sh script
    A sample configuration file can be found in /lib/swarm/swarm.lib, which looks as follows. 
    	# Swarm configuration file
	#
	# there are 4 main parts to this file:
	# (1) ranges, (2) limits, (3) compilation options, and
	# (4) runtime options
	# the default settings for each are shown below
	# comments start with a # symbol, fields are separated by tabs
	
	# ranges
	w	20	32	# min and max -w parameter
	d	100	10000	# min and max search depth
	k	2	5	# min and max nr of hash functions
	
	# limits
	cpus	2		# nr available cpus
	memory	513MB	# max memory to be used; recognizes MB,GB
	time	1h		# max time to be used; h=hr, m=min, s=sec
	vector	500	# bytes per state, used for estimates
	speed	250000	# states per second processed
	file	model.pml	# file with spin model
	
	# compilation options (each line defines a search mode)
	# each option currently must include -DBITSTATE
	-DBITSTATE			# standard dfs
	-DBITSTATE -DREVERSE	# reversed process ordering
	-DBITSTATE -DT_REVERSE	# reversed transition ordering
	-DBITSTATE -DRANDOMIZE=123	# randomized transition ordering
	-DBITSTATE -DRANDOMIZE=173573	# ditto, with different seed
	
	# some other possible modes:
	# -DBITSTATE -DT_REVERSE -DREVERSE	# combination
	# -DBITSTATE -DT_REVERSE -DRANDOMIZE	# combination
	
	# runtime options (one line)
	-n
    Some (though not all) options can also be set on the command line. Options are set in the order in which they are encountered. This means that command line options can be used to override settings in a configuration file or vice versa, if both are used.

    The following command line options are recognized: 

    	-f model_name = a required argument if no config_file is used.

	-bN = the number of bytes per state(default -b500)
	-cN = the number of cpus available (default -c1)
	-mN = the amount of available physical mem, optional suffix M or G, (default -m512M)
	-sN = the number of states stored per second (default -s250000)
	-tN = the number of hours available for the runs (default -t1.0)
	-dN = the maximum search depth (default -d10000)
	-uN = the minimum search depth (default -u128)
	-v  = verbose mode (default is non-verbose)
    The shell variable CCOMMON can be used to define standard compile time parameters that should be used for all runs (the default setting is CCOMMON="-O2 -DSAFETY").
    The shell variable RCOMMON can be used to define run time parameters that are to be used for all runs (the default setting is RCOMMON="-n").

EXAMPLES

    A typical run of swarm looks as follows. 
    	$ swarm -F config_file
	swarm: 95 runs, avg time per cpu 3599.5 sec
	$ sh script
    Without a config file, with the Spin model in file model.pml, and executing on a quad-core machine with 16 GB of memory, with a time-bound of 2 hours for the verification: 
    	$ swarm -c4 -m16G -t2 -f model.pml > script
	swarm: 51 runs, avg time per cpu 7199.2 sec
	$ sh script
    When executed, the last script will create four additional shell scripts, named script0 .. script3, one for each available cpu core, and populates each script with commands. Before executing those commands, the main script calls spin to generate pan.c and related files, and compiles them for a range of different search methods. The execution of a script either stops when an error trail is found, or when the time limit is reached. By default, swarm assumes that states are analyzed at an average rate of 250,000 states per second. If this estimate is too high, the execution of the script will take proportionally more time than planned, if the estimate is too low then it will take less time. Once the rate is known (which if important can easily be determined with a small separate run in bitstate mode), it can be specified on the command line to improve accuracy. For instance, if the verification is known to execute at a rate of 100,000 states per second, the last swarm command can be made more precise, as: 
    	$ swarm -c4 -m16G -t2 -s100000 -f model.pml > script
	swarm: 48 runs, avg time per cpu 7198.5 sec

FILES

    /lib/swarm/swarm.lib # sample config file

SOURCE

BUGS

    bugs@spinroot.com

SEE ALSO

spinroot homepage last update: april 26, 2008