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

Overview

There is one new predefined local process variable:

	_priority

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

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

Limitations

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
	}