A forum for Spin users
You are not logged in.
Thanks spinroot! And I am afraid "{ c_code {s1} } unless { pending -> handle };" just doesn't work because c_code {s1} might be skipped...
So do you have other recommendations to make it more elegant? Will the interrupt model be considered in SPIN's future design?
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!
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.