Spinroot
A forum for Spin users
You are not logged in.
- Topics: Active | Unanswered
#1 2011-11-06 18:12:28
- awesan
- Member
- Registered: 2011-04-30
- Posts: 45
Q's/errors on goto labels, progress labels and end states and iSpin
Here is the portion of a simplified model to illustrate a few questions. This models acquire_semaphore and release_semaphore functions.
********************************************
inline acq_sem1(sem)
{
L0:
atomic {
if
:: sem == 0 -> goto L0
:: else -> sem--
fi
}
}
inline acq_sem(sem) // Using do to fix the errors with above inline function
{
atomic {
do
:: sem == 0;
:: else ->
//progress: // warning, progress label inside atomic is invisible
sem--; break;
od;
}
}
inline rel_sem(sem)
{
sem++;
}
#define MAX_SEM_VAL 2
int sem = MAX_SEM_VAL;
active [3] proctype P()
{
end:
do
:: acq_sem1(sem);
progress:
rel_sem(sem);
od;
}
active proctype Check()
{
end:
do
:: skip;// This is needed to use the progress label
progress:
assert(sem >=0 && sem <= MAX_SEM_VAL);
od
}
********************************************
Q-1:
In acq_sem1, no matter where I place the label L0, I always get the error "label L0 placed incorrectly. Instead of ....., always use ....". My understanding is that I need "atomic", otherwise my assertion would fail, even if I get this to compile. It looks like SPIN has stringent restrictions on using labels and expansion of inline function inside proctype P ends up violating all limitations on where I can place the label, am I right? Or, is there a way to fix the placing of labels to get this to work?
Q-2:
So, I came up with acq_sem() function where I replaced "if" with "do...od" inside "atomic" and that seems to work. Is that the only work-around/solution for problem explained in Q-1?
Q-3:
When I verify this mode for "safety", I get the error "unreached in proctype" for both processes "P" and "Check" and this seems to be a bug, since I do have the "end" labels in both processes "P" and "Check". I got the same error when I did not have the "end" label and that was ok.
Q-4:
As you see in "acq_sem" function, I get a warning for using "progress" label inside "atomic". I am curious whether it is a deficiency that can be fixed or it is a hard-to-solve/unsolvable problem in verification when "atomic" has "progress" label. I moved the "progress" label to process "P" after calling "acq_sem". Hope that is the right way to fix it.
Q-5:
Can I use ltl formulae instead of "proctype Check" to achieve the same? I see that ltl formulae can be used inline. But, I do not find documentation "how" or examples. I have the "SPIN Model Checker" book. But, I think this is a new feature. Could you please point me to some documentation and examples of using inline ltl in SPIN models? Are there any limitations doing that as opposed to using never claims separately? Also, some documentation and examples on how to use "claim name" and "use claim" in iSpin. I have used sometime back using xSpin but iSpin seems to be different and cannot find how to use this feature correctly.
Q-6:
Is there a way to attach model files (.pml) to forum post? That would help simplify explanation and I can use line-numbers,etc to refer to in the post.
Thanks a lot in advance for any help.
Offline
#2 2011-11-06 18:36:29
Re: Q's/errors on goto labels, progress labels and end states and iSpin
re Q1, Q2 and Q4: the correct way to model the counting semaphore in Promela is (and not needing labels):
atomic { sem > 0 -> sem-- }
and to release it:
sem++
Note that Promela has blocking semantics on expressions that evaluate to false, so you don't need (and dont' want) the busy wait cycles.
Note also that inlines are simply expanded inline at the place of the call -- so whatever restrictions there are on label placement, they hold for the inlined text. (i.e., it can depend on where precisely the call is placed)
re Q3: Spin simply reports that the final state is unreached -- it doesn't say that this is an error.
If it would have considered it an error, it would have said so and produced a counter-example trail.
re Q5: yes you can use an LTL formula to check an invariant like this:
ltl p { [] (sem >=0 && sem <= MAX_SEM_VAL) }
(make sure you place this in the specification after the point where both sem and MAX_SEM_VAL have been declared/defined)
re Q6: we're having a lot of trouble with spammers on the forum (we delete some 10 to 20 spammers a day), so it probably not a good idea to allow file attachments...
Offline
#3 2011-11-06 20:33:59
- awesan
- Member
- Registered: 2011-04-30
- Posts: 45
Re: Q's/errors on goto labels, progress labels and end states and iSpin
> re Q1, Q2 and Q4: the correct way to model the counting semaphore in Promela is (and not needing labels): atomic { sem > 0 -> sem-- }
I did this correctly when I tried mutex: atomic { lock == 0 -> lock = 1}. Apparently, did not follow the idiomatic way (using blocking expression) when I wrote counting semaphore. Thanks for catching this.
Output of verification for safety with your suggestion:
depth reached 6
7 states, stored
12 states, matched
Output of verification for safety with my original implementation ("acq_sem") with the busy wait in "do...od"
depth reached 9999
7 states, stored
15 states, matched
29988 atomic steps
Also, when I kept increasing the depth limit to 100000, I still kept getting the error from pan ("error: max search depth too small"). However, I did not get any error "'Search not completed' or 'Search Truncated'. I hope the pan error about "search depth too small" can be ignored. I understand this is inefficient and I should not be writing models with the busy-wait cycles like this but I wanted to make sure this is not an incorrect model with respect to verification results.
Offline
#4 2011-11-06 20:41:50
- awesan
- Member
- Registered: 2011-04-30
- Posts: 45
Re: Q's/errors on goto labels, progress labels and end states and iSpin
Question below the model excerpt:
**********************************
inline acq_sem(sem)
{
atomic {
sem > 0 ->
progress:
sem--;
}
}
inline rel_sem(sem)
{
sem++;
}
#define MAX_SEM_VAL 2
int sem = MAX_SEM_VAL;
active [3] proctype P()
{
end:
do
:: acq_sem(sem);
//progress:
rel_sem(sem);
od;
}
***************************
Using the progress label inside atomic in acq_sem function did not throw any warnings as it used to in my original post with busy wait cycles. However, non-progress cycle verification (with weakness enabled or disabled) throws "non-progress cycle errors. However, deleting the "progress" label inside atomic and adding it in proctype P (as shown in the commented line above) verifies without errors. I guess both should succeed. If the first one fails, then "syntax check" should probably error out. Am I missing something?
Offline
#6 2011-11-06 22:54:04
- awesan
- Member
- Registered: 2011-04-30
- Posts: 45
Re: Q's/errors on goto labels, progress labels and end states and iSpin
> progress labels inside atomics are invisible -- hence you get non-progress cycle errors: the verifier does not see the label
I understand. It would be nice, if "syntax check" throws a warning or error. It did not in this case and that is confusing.
Offline