A forum for Spin users
You are not logged in.
Pages: 1
Hi, when I was using "provided clause" to model interrupts, I found it is hard to make sure fairness with SPIN. Take a look at an example below:
int a = 0;
byte lock_owner;
byte lock_next;
byte pending[2];
inline spin_lock()
{
byte next_to_wait;
atomic {
if
::lock_owner == lock_next -> lock_next = (lock_next + 1) % 128;
::else ->
{
next_to_wait = lock_next;
lock_next = (lock_next + 1) % 128;
lock_owner == next_to_wait;
}
fi;
}
}
inline spin_unlock()
{
lock_owner = (lock_owner + 1) % 128;
}
proctype user(int id) provided (pending[id] == 0)
{
end:
do
::spin_lock();
pending[1-id]++;
a = id + 1;
spin_unlock();
od;
}
proctype handler(int id)
{
do
::pending[id] > 0 -> pending[id]--;
od;
}
init {
atomic {
run user(0);
run user(1);
run handler(0);
run handler(1);
}
}
ltl p1 { []<>(a == 1) && []<>(a == 2) };
So I am using fair spinlock here to make sure both user(0) and user(1) have chance to enter critical section. But because "pending[id]" condition continually changes, the LTL cannot hold even if the weak fairness is turned on. Is there any option to solve this issue with SPIN? Thanks!
Last edited by jiong (2011-02-10 06:06:27)
Offline
Thanks Gerard. Could you please show me how to express the strong fairness with the given example?
Offline
Yes, that is expected behavior with fair spinlock.
Offline
OK, I managed to enhance the code to check the starvation with the given example:
inline spin_lock()
{
byte next_to_wait;
atomic {
if
::lock_owner == lock_next -> lock_next = (lock_next + 1) % 128;
::else ->
{
in_wait[id] = true;
next_to_wait = lock_next;
lock_next = (lock_next + 1) % 128;
lock_owner == next_to_wait;
in_wait[id] = false;
}
fi;
}
}
inline spin_unlock()
{
lock_owner = (lock_owner + 1) % 128;
}
So I use in_wait array to track the waiting states and use the ltl to check starvation:
ltl p1 { [](in_wait[0] == true -> <>(in_wait[0] == false)) };
Not sure if the LTL expression is accurate but the acceptance verification seems to run forever...
Offline
yes that looks right
i'd recommend changing 128 to something much smaller -- you don't need the larger value to prove/disprove the property, but it does affect the complexity of the verification
why not pick something quite small like 4?
Offline
yep, that's faster with the default depth limit but still runs for 85s with a big depth value like 10M. I assume that is expected.
Offline
did you also try breadth-first search? of bounded context switching...
(compile pan.c with either -DBFS or with -DBCS) which both will give you shorter trails, but no necessarily a shorter runtime
you can also speed things up a bit with -DCOLLAPSE or -DHC
it's always difficult to predict runtimes or complexity -- maybe that's why it's good to have a tool that can figure it all out and discover how complex something really is :-)
Offline
Pages: 1