Spinroot

A forum for Spin users

You are not logged in.

#1 2011-01-27 14:14:19

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

How to Extract Interruptible C Model

I'd like to model a bunch of interruptible C code with SPIN/MODEX.  Basically the normal execution of C code could be interrupted anytime and the control is handed over to an interrupt handler. After the handling of interrupt, the normal execution is resumed. A direct way I can think of is to modify MODEX so that on each c_code line extracted, there is an accompanying code to poll interrupt like below:

#define POLL_INTERRUPT interrupt_lock = 0; atomic { if ::interrupt_lock == 0 -> interrupt_lock = 1 }
proctype interrupt_handler()
{
Continue:
  atomic { if ::(interrupt_lock == 0 && interrupt_cnt > 0) -> interrupt_lock = 1 };
  
  // handle interrupt here...
  
  interrupt_cnt--;
  interrupt_lock = 0;
  goto Continue;
}

proctype some_extracted_func()
{
  POLL_INTERRUPT;
  // two of the extracted lines below:
  c_code { bla bla bla }; POLL_INTERRUPT;
  c_code { bla bla bla }; POLL_INTERRUPT;
}

So POLL_INTERRUPT is inserted for each extracted line. Anyone knows if there is better way to do this? Are there any theoretical or empirical studies on the model checking of C code with interruptions? Thanks.

Offline

#2 2011-01-28 03:08:21

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

Re: How to Extract Interruptible C Model

maybe you can handle this with an unless construct:
   [url]http://spinroot.com/spin/Man/unless.html[/url]
but you'd have to separate out each statement in the C code fragment
as a separate statement, so that it becomes interruptable.
that is, instead of saying:
   c_code { s1; s2; s3; };
you'd make that into:
    {
       c_code { s1; };
       c_code { s2; };
       c_code { s3; };
    } unless
    {   interrupt_pending ->
         handle_interrupt
    }
except of course that the unless is more like an exception: after
you take the unless escape you do not return to the main sequence...

the way you wrote it would avoid that, but it's kinda verbose.
modex does not do this type of instrumentation by default alas,
so you'd have to figure out some other way to achieve it...

Offline

#3 2011-01-28 03:14:49

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

Re: How to Extract Interruptible C Model

OK. So to make it more like interrupt than exception, I have to wrap each c_code with unless:
{ c_code {s1} } unless { pending -> handle };
{ c_code {s2} } unless { pending -> handle };
{ c_code {s3} } unless { pending -> handle };
Thanks for the reply!

Offline

#4 2011-01-28 03:17:45

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

Re: How to Extract Interruptible C Model

well, yes that would be one way of doing it
a bit ugly, but i guess it would do the job

Offline

#5 2011-01-28 03:34:57

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

Re: How to Extract Interruptible C Model

So do you have other recommendations to make it more elegant? Will the interrupt model be considered in SPIN's future design?

Offline

#6 2011-01-28 06:09:49

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

Re: How to Extract Interruptible C Model

no i have no better suggestions.
but i'll think about it some more

Offline

#7 2011-01-28 06:27:05

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

Re: How to Extract Interruptible C Model

Thanks spinroot! And I am afraid "{ c_code {s1} } unless { pending -> handle };" just doesn't work because c_code {s1} might be skipped...

Offline

#8 2011-01-28 06:32:21

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

Re: How to Extract Interruptible C Model

but it can only be skipped if 'pending' is true before s1 even starts....

Offline

#9 2011-01-28 06:34:19

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

Re: How to Extract Interruptible C Model

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

Offline

#10 2011-01-28 22:27:56

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

Re: How to Extract Interruptible C Model

but if the interrupt is already pending before s1 starts, then wouldn't the interrupt be handled before s1 executes?

Offline

#11 2011-01-29 02:42:10

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

Re: How to Extract Interruptible C Model

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.

Offline

#12 2011-01-29 05:10:32

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

Re: How to Extract Interruptible C Model

that's correct, and with the construct precisely as you gave it spin will be able to show that too.
just replace the assertion with any of these:
assert(a != 0)
assert(a != 1)
assert(a != 2)
assert(a != 3)
and spin can show you the counter-example that gives a sequence leading to each of these values.
so i'm still not sure why you believe this doesn't accurately capture the notion of an asynchronous interrupt?

Offline

#13 2011-01-30 01:24:26

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

Re: How to Extract Interruptible C Model

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.

Offline

#14 2011-01-30 02:34:03

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

Re: How to Extract Interruptible C Model

I understand -- then the only way to handle it would be to add the statement itself to the end of the escape clause in each case -- really ugly, but it would then look like this:
  { a++ } unless { pending -> ...handle_interrupt...; pending = false; a++ };
etc

Offline

#15 2011-01-30 02:38:49

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

Re: How to Extract Interruptible C Model

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);
}

Last edited by jiong (2011-01-30 04:01:13)

Offline

#16 2011-01-30 20:13:32

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

Re: How to Extract Interruptible C Model

good point, and worth considering

Offline

#17 2011-01-31 22:56:17

theo.ruys
Administrator
Registered: 2010-11-18
Posts: 11

Re: How to Extract Interruptible C Model

When I need to model an interrupt in Promela, I usually encode return addresses by hand.
Your example would then become something like this:

int  a = 0;
bool pending = false;

active proctype test()
{
    byte ret = 0;
    {
    skip;
l0: atomic { a++; ret=1; }
l1: atomic { a++; ret=2; }
l2: atomic { a++; ret=3; } 
    } unless { 
        pending -> pending = false; 
        if 
        :: ret==0 -> goto l0 
        :: ret==1 -> goto l1
        :: ret==2 -> goto l2
        :: else   
        fi
    }
    
    assert(a == 3);
}

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

It is a bit tedious, but not as ugly as the separate unless construct for each statement.
To minimize the extra code clutter at the end of the unless (i.e., the if-clause), you could use a CPP macro for the calculation of the return address. And even the statements of the body could probably be encoded in a CPP macro to hide the labels and the saving of the return addresses.

You could even make this work for a priority level interrupt mechanism, i.e., with a nested unless.

Last edited by theo.ruys (2011-01-31 22:57:14)

Offline

#18 2011-02-01 02:50:21

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

Re: How to Extract Interruptible C Model

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.

Offline

#19 2011-02-01 22:21:05

theo.ruys
Administrator
Registered: 2010-11-18
Posts: 11

Re: How to Extract Interruptible C Model

jiong: Yes, your POLL_INTERRUPT solution is an explicit implementation of Promela's unless statement.

And yes, if the body is more complicated (with if-clauses and/or do-loops), the instrumented body also gets more complicated. But essentially you should explicitly identify the state of each statement (using a ret-value and optionally a label) within the body and jump back to the correct statement.

I agree with you that (more) support for interrupt handling would be great.
Perhaps it would not even be that hard to implement. For example, a 'resume' (or 'return') statement could be added to Promela. This statement could then only be used within an unless-clause and would resume execution of the code at the state in the body that was interrupted.

Each time when SPIN would take an unless transition, it should save the outgoing state (i.e., the return address) within the body. As unless-clauses may be nested, the implementation in SPIN should keep a stack of "return addresses" (for each process). Although this may seem "expensive" with respect to the size of the state vector, this is not really the case. Due to the static nature of the unless-clauses the maximum depth of the return stack is known at compile-time.

Offline

#20 2011-02-02 07:49:28

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

Re: How to Extract Interruptible C Model

maybe this is also worth considering, and a lot simpler to boot:

simply define a separate asynchronous process "interrupt_handler" that responds to pending becomes true and then executes the response atomically:

active proctype handler()
{
   do
   :: atomic { pending -> ....whatever....; pending = false }
   od
}

it would work precisely as you intend -- by interleaving the execution of the main process with the interrupt -- which then is executed atomically in between the statements of the main process -- whenever it becomes executable

now the tricky thing is to force it to happen -- so that it cannot be postponed and so that the main process stops
this you can do with a 'provided clause' on the main process, like so:

active proctype user() provided (pending == false)
{
  c_code { a++; };
  c_code { a++; };
  ....etc
}

Offline

#21 2011-02-02 09:07:42

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

Re: How to Extract Interruptible C Model

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

Offline

#22 2011-02-02 12:07:43

theo.ruys
Administrator
Registered: 2010-11-18
Posts: 11

Re: How to Extract Interruptible C Model

Hi spinroot,

Your solution with the provided-clause surely works.
And for a single user process it is quite elegant.

But what if there are more user processes running?
And how to deal with a priority-based interrupt mechanism?

In a recent project, I had to model two concurrent processes that both had local interrupt mechanisms. The interrupt mechanism was also priority based: a lower interrupt could be interrupted by a higher interrupt. The only way to model it elegantly was to use a nested unless-clause and manually keeping track of the return addresses. A special construct like resume (or return) would have been very helpful.

Offline

#23 2011-02-03 04:42:50

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

Re: How to Extract Interruptible C Model

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?

Offline

#24 2011-02-03 16:47:32

theo.ruys
Administrator
Registered: 2010-11-18
Posts: 11

Re: How to Extract Interruptible C Model

jiong, I guess it might work in that way.
But it is not very elegant and straightforward, IMO.

A solution with "user processes with provided clauses" has some disadvantages:
* You need a scheduler process which sets the pending[] elements and which makes sure that the handler process with the highest priority get scheduled first. In case a lower priority interrupt process gets interrupted, the scheduler process should also make sure that this lower priority interrupt process will finish, before the user process can continue. This scheduler process might be a complex thing, and IMO, SPIN should take care of this scheduling;
* All local variables that may trigger an interrupt procedure have to be made global as the scheduler process has to see them;
* The provided clause prevents SPIN partial order reduction algorithm. This might be expensive in terms of the number of states;
* (minor) Each handler will gets its own process. This might not increase the number of states, but it will increase the size of the state vector.

A (simple?) extension to the Promela language (i.e., a resume/return statement) would make modelling interrupts so much easier...

Offline

#25 2011-02-04 05:52:58

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

Re: How to Extract Interruptible C Model

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

Offline

Board footer

Powered by FluxBB