Spinroot

lz

Member

Registered: 2012-05-14

Posts: 9

Priority out of range ...

Consider the following extract of code :

#define PRIO_MAX  35        // or 255
proctype T(byte calcul, periode, id) {
int prio_normale;
   /**/ prio_normale = get_priority(_pid);
   // or
   /**/ prio_normale = _priority;
   set_priority(_pid, PRIO_MAX);
   skip;
   set_priority(_pid, prio_normale);
}
init { atomic { run T(25, 100, 0) priority 30;
                    run T(30, 150, 1) priority 20;
                    run T(75, 200, 2) priority 10;
                  //run idle(3);
                  }
}

Simulation is OK, but the verification (partial order reduction disabled)
generates the following message:

spin -a  Error_Prio.pml
gcc -DMEMLIM=1024 -O2 -DXUSAFE -DSAFETY -DNOCLAIM -DNOREDUCE -w -o pan pan.c
./pan -m10000  -E -n
Pid: 2076
pan:1: priority is out of range (at depth 5)
pan: wrote Error_Prio.pml.trail

Do you have a comment, thanking you.

spinroot

forum

Registered: 2010-11-18

Posts: 700

Website

Re: Priority out of range ...

It is a bug.  You can bypass it by using:
spin -o1 -a Error_Prio.pml

The bug is in the dead variable elimination code.
In the current version Spin fails to see that prio_normale is used
after the assignment (in the last statement of proctype T)
and therefore it sets the value to 0, which is outside the valid range
which then triggers the error report.
So another way to circumvent the problem is to use prio_normale
in a printf statement or in an expression after the assignment.
(It only fails to notice the read access to prior_normale if it appears
in a call to set_priority.)
This will be fixed in Spin version 6.4.4 -- the next release.
Thanks for the excellent bug report!