Spinroot

A forum for Spin users

You are not logged in.

#1 2011-02-10 05:49:00

jiong
Member
From: China
Registered: 2011-01-27
Posts: 30

Fairness and "provided clause"

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

#2 2011-02-10 06:51:02

spinroot
forum
Registered: 2010-11-18
Posts: 691
Website

Re: Fairness and "provided clause"

yes, you can express strong fairness (instead of the default weak fairness) in LTL, or in never claims....

Offline

#3 2011-02-10 06:53:11

jiong
Member
From: China
Registered: 2011-01-27
Posts: 30

Re: Fairness and "provided clause"

Thanks Gerard. Could you please show me how to express the strong fairness with the given example?

Offline

#4 2011-02-10 06:56:04

spinroot
forum
Registered: 2010-11-18
Posts: 691
Website

Re: Fairness and "provided clause"

so you want to show that when both users want to enter the cs, then user(0) cannot access its critical section twice in a row without user(1) getting in as well?

Offline

#5 2011-02-10 06:58:38

jiong
Member
From: China
Registered: 2011-01-27
Posts: 30

Re: Fairness and "provided clause"

Yes, that is expected behavior with fair spinlock.

Offline

#6 2011-02-11 05:22:43

jiong
Member
From: China
Registered: 2011-01-27
Posts: 30

Re: Fairness and "provided clause"

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

#7 2011-02-11 06:14:31

spinroot
forum
Registered: 2010-11-18
Posts: 691
Website

Re: Fairness and "provided clause"

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

#8 2011-02-11 09:13:18

jiong
Member
From: China
Registered: 2011-01-27
Posts: 30

Re: Fairness and "provided clause"

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. smile

Offline

#9 2011-02-11 17:34:40

spinroot
forum
Registered: 2010-11-18
Posts: 691
Website

Re: Fairness and "provided clause"

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

Board footer

Powered by FluxBB