There is one new predefined local process variable:
_prioritywhich 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 cIn 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.
/*** 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 |