Promela Reference -- priority(2)

Promela

Declarator

priority


NAME
priority - setting and using process priorities

SYNTAX
active [ '[' const ']' ] proctype name ( [ decl_lst ] ) priority const { sequence }
run name ( [ arg_lst ] ) priority const
get_priority(expr) (Version 6.2)
set_priority(expr, expr) (Version 6.2)

DESCRIPTION
In versions of Spin older than 6.2 the use of process priorities was restricted to random simulations to determine the probability that specific processes are scheduled for execution.
Starting with Spin Version 6.2, process priorities have stronger semantics, used in both simulation and verification. In this mode, a process can only execute statements if it is (one of) the highest priority process(es) in the system. Priorities can be queried and manipulated with the two new function calls get_priority and set_priority.

The new behavior can be disabled with option spin -o6 ....

A process priority can be specified either with an optional parameter to a run operator, or as a suffix to an active proctype declaration. The optional priority field follows the closing brace of the parameter list in a proctype declaration.

The default execution priority for a process is 1. Higher numbers indicate higher priorities. In the original (pre Version 6.2) semantics, a priority 10 process is 10 times more likely to execute in a simulation than a priority 1 process. In the new (post Version 6.2) semantics, a priority 10 process always takes priority over a priority 1 process, unless it is blocked. Only the highest priority enabled process can execute statements.

The priority specified in an active proctype declaration affects all processes that are initiated through the active prefix, but no others. A process instantiated with a run statement is always assigned the priority that is explicitly or implicitly specified there (overriding the priority that may be specified in the proctype declaration for that process).

The predefined local process variable:

	_priority
holds the current priority of the executing process.

Two new predefined functions can be used to query and change process priorities. They are:

	get_priority(p)    which returns the priority of process p
	set_priority(p,c)  which sets priority of process p to c
The parameters p and c in these examples can be arbitrary Promela expressions.

EXAMPLES

	run name(...) priority 3
	active proctype name() priority 12 { sequence }
If both a priority clause and a provided clause are specified, the priority clause should appear first, for instance:
	active proctype name() priority 5 provided (a < b) {...}
A more complete example:
	byte cnt;
	
	active proctype medium() priority 5
	{
		set_priority(0, 8);
		printf("medium %d - pid %d pr %d pr1 %d\n",
			_priority,
			_pid,
			get_priority(_pid),
			get_priority(0));
		cnt++
	}
	
	active proctype high() priority 10
	{
		_priority = 9;
		printf("high %d\n", _priority);
		cnt++
	}
	
	active proctype low() priority 1
	{
		/*
		 * this process can only execute if/when it is the
		 * highest priority process with executable statements
		 */
	
		assert(_priority == 1 && cnt == 2);
		printf("low %d\n", _priority);
	}

NOTES
The use of priorities is not compatible with the use of rendezvous statements (synchronous channels), and for a full verification partial order reduction should be disabled.

SEE ALSO
active
proctype
provided

See also this overview


Spin Online References
Promela Manual Index
Promela Grammar
Spin HomePage
(Page updated: 4 May 2012)