Spin Priority-Based Search
Supported in Spin Version 6.2 and later

Overview


Spin version 6.2 introduces some new features that simplifies the modeling and verification of priority based scheduling rules, as are common in real-time embedded software (e.g. VxWorks).

There is one new predefined local process variable:

	_priority
which holds the current priority of the executing process. The default priority is 1.

There are two new predefined functions:

	get_priority(p)    which returns the priority of process p
	set_priority(p,c)  which sets priority of process p to c
In the above function calls, the parameters p and c can be any valid Promela expression.

When process priorities are used then only the highest priority enabled process can run. Process priorities must be in the range 1..255.


New Spin Option

Spin option -o6 will cause spin to revert to the old (pre 6.2.0) rules for interpreting priority annotations. That is, with option -o6 priorities are ignored during verifications and applied only to set the probability of execution during simulations. (Note that this is a very different semantics.)

Limitations

The use of the new priority features cannot be combined with the use of rendezvous statements in the same model (i.e., zero-capacity channels). For completeness, verification also requires compilation with -DNOREDUCE, although the verifier will not warn if -DNOREDUCE is omitted.

Four Examples

	/*** Example 1 ***/
	
	/* the use of 'priority' tags enforces
	   priority based scheduling
	   it can also be combined with provided clauses
	   to finetune the scheduling choices
	 */

	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);
	}

	/*** Example 2 - semaphore routines with priority inversion ***/
	
	bool sem_busy;
	byte sem_owner; /* pid of semaphore owner */
	byte sem_prior;	/* original priority of owner */
	
	inline sem_take() {
		atomic {
			do
			:: !sem_busy ->
				sem_busy = true;
				sem_owner = _pid;
				sem_prior = _priority;
				break
			:: else ->
				if
				:: get_priority(sem_owner) < _priority ->
					set_priority(sem_owner, _priority);
					(!sem_busy)
				:: else
				fi
			od
		}
	}
	
	inline sem_give() {
	
		atomic {
			sem_busy = false;
			sem_owner = 0;
			_priority = sem_prior /* we could get blocked after this */
		}
	}

	/*** Example 3 ***/
	
	chan q = [1] of { bool };
	bool ok = false;
	
	active proctype high () priority 10
	{	bool x;
	
		q?x;	/* highest priotity, but blocked */
		ok = true
	}
	
	
	active proctype low () priority 5
	{
		atomic {
			q!true;     /* executes first  */
			assert (ok) /* assertion fails */
		}
	}

	/*** Example 4 ***/
	
	/*
	 * a high priority process consumes data
	 * produced by a low priority process.
	 * data consumption and production happen under
	 * the protection of a mutex lock
	 * the mutex lock conflicts with the scheduling priorities
	 * which can prevent the high priority process from running
	 * if a medium priority process is also present
	 */
	
	mtype = { free, busy, idle, waiting, running };
	
	show mtype h_state = idle;
	show mtype m_state = idle;
	show mtype l_state = idle;
	show mtype mutex = free;
	
	proctype high()
	{
	end:	do
		:: h_state = waiting;
			atomic { mutex == free -> mutex = busy };
			h_state = running;
	
			/* critical section - consume data */
	
			atomic { h_state = idle; mutex = free }
		od
	}
	
	proctype medium() 
	{
	end:	do
		:: m_state = waiting; m_state = running; m_state = idle
		od
	}
	
	active proctype low() /* default low priority 1 */
	{
	end:	do
		:: l_state = waiting;
			atomic { mutex == free -> mutex = busy};
			l_state = running;
	
			run high() priority 10;   /* starved by medium() */
			run medium() priority 5;  /* prevents low() from releasing lock */
	
			/* critical section - produce data */
			atomic { l_state = idle; mutex = free };
			assert(false)  /* not reachable, because proctype medium runs */
		od
	}

Return to Spin homepage Page last updated May 4, 2012