Spinroot

A forum for Spin users

You are not logged in.

#1 General » Scope for labels again » 2011-05-12 11:45:26

jiong
Replies: 3

Hi Gerard,
Thanks for the update of Spin 6.1.0 that fixed the problem I raised last time:

inline test_inline(a)
{
  test_inline1(a);
  assert(a == 1);
  goto Return;
Return:
  a = 1;
}

inline test_inline1(a)
{
  goto Return;
Return:
  a = 2;
}

active proctype test()
{
  int a = 0;
  test_inline(a);
}

But I still got problem on the labels declared in an inline. Basically I hope to call an inline more than once in a process, like below:

inline test_inline(a)
{
  assert(a == 1);
  goto Return;
Return:
  a = 1;
}

active proctype test()
{
  int a = 0;
  test_inline(a);
  test_inline(a);
}

SPIN rejects to compile it because of duplicate Return label:
spin: test1.pml:7, Error: label Return redeclared    saw ''}' = 125'

I really hope the scoped label can be supported just like a normal variable in an inline. This makes it much simpler to extract a C function as inline. Is it possible?

#2 General » SPIN vs. Zing » 2011-03-19 09:22:37

jiong
Replies: 0

Hi,
Anyone has experiences with Zing ([url]http://research.microsoft.com/en-us/projects/zing/[/url]) and how does it compare with SPIN in terms of efficiency of state exploration and ease of C language mapping?
I took a quick look at its manual ([url]http://research.microsoft.com/en-us/projects/zing/zinglanguagespecification.pdf[/url]) and its language seems more expressive than Promela. It supports function calls and modular programming. Thanks!

Jiong

#3 Re: General » Model pan.c cannot compile with both embedded LTL and -DNP cflag » 2011-02-17 05:35:45

Great! Thanks, Gerard! I am looking forward to the new version out!

#5 Re: General » Model pan.c cannot compile with both embedded LTL and -DNP cflag » 2011-02-17 01:41:43

I am using 6.0.1 with
spin -a -q test.spn && gcc -O2 -DNP pan.c -o pan

Weird you cannot reproduce it...

#6 General » Model pan.c cannot compile with both embedded LTL and -DNP cflag » 2011-02-14 13:20:00

jiong
Replies: 6
init {
  skip;
}

ltl p1 { [](true) };
ltl p2 { [](true) };

In file included from pan.c:30:
pan.h:205: error: "NCLAIMS" undeclared here (not in a function)
make: *** [test1] Error 1

Is it a bug?

#8 Re: General » Does New Scope Rule Apply to Labels? » 2011-02-11 09:14:34

Hi Gerard, do you have plan to enable the scoped labels in the near future?

#9 Re: General » Fairness and "provided clause" » 2011-02-11 09:13:18

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

#10 Re: General » Fairness and "provided clause" » 2011-02-11 05:22:43

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

#11 Re: General » Fairness and "provided clause" » 2011-02-10 06:58:38

Yes, that is expected behavior with fair spinlock.

#12 Re: General » Fairness and "provided clause" » 2011-02-10 06:53:11

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

#13 General » Fairness and "provided clause" » 2011-02-10 05:49:00

jiong
Replies: 8

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!

#14 General » Enum Extraction of MODEX » 2011-02-06 03:12:04

jiong
Replies: 1

I found Enum is extracted as global variables by MODEX and even the values are re-assigned. This produces problem when I try to share header files between C and extracted model. This also causes functional issue when some C code relies on the exact value of the Enum.
What is the design intention to extract Enum in this way? Is it possible to extract Enum just as is?

#15 Re: General » Does New Scope Rule Apply to Labels? » 2011-02-06 02:53:51

Thanks spinroot for the reply. I hope the scoped labels can also be supported in the future as it is much easier to extract C function calls with inline expansion. To extract functions as inline is so far the only way I found feasible to support concurrent function calls. But there might be duplicate labels when there are multiple calling points for an inline function in a process, like the example below:

inline function1()
{
  // some code here
  goto Return_function1;
  // some code here
Return_function1: skip;
}

proctype test()
{
  // two calls to function1
  function1();
  function1();
}

Of course, I can work around the issue the gotos:

proctype test()
{
  int ret;
  ret = 0;
  goto function1_wrap;
L0:
  ret = 1;
  goto function1_wrap;
L1:

function1_wrap:
  function1();
  if
  ::ret == 0 -> goto L0;
  ::ret == 1 -> goto L1;
  ::else -> assert(false);
  fi;
}

But the scoped label approach is obviously more elegant. What do you think?

#16 General » Does New Scope Rule Apply to Labels? » 2011-02-05 03:46:57

jiong
Replies: 7

Hi, is the new scope rule in Spin6 supposed to work for labels too? Please take a look at the example below:

inline test_inline(a)
{
  test_inline1(a);
  assert(a == 1);
  goto Return;
Return:
  a = 1;
}

inline test_inline1(a)
{
  goto Return;
Return:
  a = 2;
}

active proctype test()
{
  int a = 0;
  test_inline(a);
}

If I understand correctly, the "goto Return" should jump to the "Return" in the same scope (inside inline function). If that is true, the assert(a==1) should fail. But in real case, it is not executed at all. The second "goto" jumps to the first "Return". Is that expected?

#17 Re: General » How to Extract Interruptible C Model » 2011-02-04 05:52:58

Hi theo.ruys, I agree with you that an additional scheduler process is needed if we use "provided clauses" here. The schedule process is just a model of interrupt controller in the system.

Of course, you might not need it as it seems both the interrupt source and handling happen locally in your model. But if there are external interrupts like interrupt from devices or interrupt from other processes, we have to model it with a global pending flag. So with global guard conditions, I do not understand why partial order reduction could be applied to "unless" but not to "provided". The semantics look very similar actually...

#18 Re: General » How to Extract Interruptible C Model » 2011-02-03 04:42:50

theo.ruys, I think you can use a global pending array, with each slot represents one user process like below:

bool pending[NUM_USER_PROCS];

proctype user(int proc_id) provided (pending[proc_id] == false)
{
  // do something
}

proctype handler(int proc_id)
{
  do
  ::pending[proc_id] -> handle it; pending[proc_id] = false;
  od
}

To model priority, you can use two pending arrays and put a "provided clause" to the low priority handler process. Does that work?

#19 Re: General » How to Extract Interruptible C Model » 2011-02-02 09:07:42

Hi spinroot, it is interesting to know "provided clause" can do the job. Thanks for the info. Just a side note that you do not need to make interrupt handling atomic here - it can interleave with other processes.
And also I found the process parameters can also be referenced in "provided clause" while the doc at "[url]http://spinroot.com/spin/Man/provided.html[/url]" says that is not allowed. It is confusing. smile

#20 Re: General » How to Extract Interruptible C Model » 2011-02-01 02:50:21

Hi theo.ruys, thanks for the reply. The solution you provided is similar to explicit POLL_INTERRUPT for each line. But special care should be taken of the labeling and "ret" tracking on statements in loops. Basically
[list=1]
[*]The first statement of each choice share the same label with loop head. [/*]
[*]For each choice without break, the "ret" of last statement should point to the loop head. [/*]
[*]For each choice with break, the "ret" of last statement should point to the following statement after loop. [/*]
[/list]
Please correct me if I am wrong.

I thought about this solution with MODEX automation and it looks like a good option! But anyway I would prefer a more intuitive solution like if SPIN itself could support interrupt modeling.

#21 General » Extract Function for Concurrent Callers with MODEX? » 2011-01-31 15:13:18

jiong
Replies: 1

MODEX has option to extract callable functions with -L -E or -L -e and Icall can be used on the caller side. But I found this extraction cannot correctly simulate the scenario of concurrent callers. For example,

void thread1_entry()
{
  A();
}

void thread2_entry()
{
  A();
}

void A();
{
  // do some complex stuff
}

The thread1_entry() and thread2_entry() run concurrently and can be extracted with -L -a directly. I can also use "%X -L A -E A" to extract function A(), but the problem is that there is only one process for A() so A() cannot be re-entered. But in real C code, A() can be re-entered and called concurrently by the two threads.

A possible way to solve this issue is to map A() as inline. But I found it is not easy to handle function parameters and return value then. Especially if A() has a deep call tree, like A() calls B(), B() calls C() etc. This will produce many inline functions and make things even worse...

Is there any better way to handle this issue? Thanks!

#22 Re: General » How to Extract Interruptible C Model » 2011-01-30 02:38:49

Yep, really ugly! smile
Or we can explicitly poll interrupt without using unless, just like the first example.
Or if SPIN could provide more primitives to support interrupt in the future, that would be even better! More specifically, we might have a primitive like "interruptible":

active proctype test()
{
  { a++; a++; a++; } interruptible { pending -> handle; };
  assert(a == 3);
}

#23 Re: General » How to Extract Interruptible C Model » 2011-01-30 01:24:26

That is because the interrupt should not impact the normal execution flow. So in the example, the value of "a" should always be 3, just like no interrupt ever occurring.

#24 Re: General » How to Extract Interruptible C Model » 2011-01-29 02:42:10

Not exactly because interrupt occurs asynchronously. Take a look at the example below:

int a = 0;
bool pending = false;

active proctype test()
{
        { a++; } unless { pending -> pending = false; };
        { a++; } unless { pending -> pending = false; };
        { a++; } unless { pending -> pending = false; };
        printf ("a = %d\n", a);
        assert (a == 3);
}

active proctype controller()
{
end:
        do
        ::pending = true;
        ::pending = pending;
        od;
}

"a" could be any value from 0 to 3 here.

#25 Re: General » How to Extract Interruptible C Model » 2011-01-28 06:34:19

Yep, which means it cannot accurately model interrupt behavior. smile

Board footer

Powered by FluxBB