A forum for Spin users
You are not logged in.
Pages: 1
Thanks for your quick answer.
Just out of curiosity, what is the reason for POR being incompatible with proctype priorities and also with provided clauses? It seems to me that provided clauses only contribute as additional guards to the transitions of the underlying automaton, which occurs to me as being quite similar to an if-statement with a conjunction of conditions in each option. But that's probably to simple :-).
Hello everybody,
I have a two questions regarding priorities of proctypes in Spin.
* The manpage on priorities (http://spinroot.com/spin/Man/priority.html) concludes with the remark that "for a full verification partial order reduction should be disabled". What confuses me is the "should" in the remark. My question is: are there any potential errors that I might miss in my model if I use proctype priorities in combination with POR?
* What does "full verification" mean in this context? The behavior that a low-prio proctype cannot execute a statement if a higher-prio proctype can execute some statement is absolutely intended in my model and also guaranteed by the system that shall be verified. It is clear, however, that the verification would not capture the entire statespace if the priorities weren't enforce in the verified system.
Cheers,
Christian
Hi folks,
I potentially found a bug in Spin today. Consider the following minimal example:
init{
byte childPid = run SomeProc();
assert(childPid == 1);
}
proctype SomeProc(){
skip;
}This model is syntactically correct (as confirmed by spin) and it violates none of the restrictions for the run-expression mentioned on the man pages. However, as it turns out, this model is not translated into compilable C-code by Spin leading to the following compile error:
pan.c: In function ‘addproc’:
pan.c:830:39: error: ‘II’ undeclared (first use in this function)
((P0 *)pptr(h))->childPid = addproc(II, 1, 1);
^I guess this should be fixed.
By the way, the example compiles (and verifies) correctly if we do not use run in the init expression for the variable childPid (i.e., declaring childPid first and then using the run expression as right-hand side of an assignment).
Cheers,
Christian
Hi folks,
I stumbled across some unexpected behavior when using Spin today. By accident, I defined a proctype with parameters named "start1" and "start2", which seemed to be totally OK from my perspective. The Spin syntax checker is also fine with it, however, when I tried to run the verifier on my model, I received an bunch of strange looking errors:
pan.h:416:16: error: expected identifier before numeric constant
#define start2 0 /* np_ */
^
pan.c:24:45: note: in definition of macro ‘Offsetof’
#define Offsetof(X, Y) ((ulong)(&(((X *)0)->Y)))
^
pan.h:175:41: note: in expansion of macro ‘start2’
#define Air1 (sizeof(P1) - Offsetof(P1, start2) - 1*sizeof(int))
^
pan.c:524:40: note: in expansion of macro ‘Air1’
short Air[] = { (short) Air0, (short) Air1, (short) Air2 };
^
In file included from pan.c:31:0:
pan.c: In function ‘addproc’:
pan.h:417:16: error: expected identifier before numeric constant
#define start1 1
^
pan.c:816:20: note: in expansion of macro ‘start1’
((P1 *)pptr(h))->start1 = par0;
^
pan.h:416:16: error: expected identifier before numeric constant
#define start2 0 /* np_ */
^
pan.c:817:20: note: in expansion of macro ‘start2’
((P1 *)pptr(h))->start2 = par1;
^
pan.c: In function ‘c_locals’:
pan.h:417:16: error: expected identifier before numeric constant
#define start1 1
^
pan.c:13964:52: note: in expansion of macro ‘start1’
printf(" int start1: %d\n", ((P1 *)pptr(pid))->start1);
^
pan.h:416:16: error: expected identifier before numeric constant
#define start2 0 /* np_ */
^
pan.c:13965:52: note: in expansion of macro ‘start2’
printf(" int start2: %d\n", ((P1 *)pptr(pid))->start2);You can use the following minimal example to reproduce the error:
init{
run someProc(1,2);
}
proctype someProc(int start1; int start2){
skip;
}So, what's the problem here? As it turns out, Spin generates the following Macros in pan.h:
#define start2 0 /* np_ */
#define start1 1and these Macros interfere with the variables that are generated for the parameters that I used in my model. I guess that there are more macros that your variable names might interfere with. Thus, whenever you encounter such errors, consider renaming the variables and parameters that the C preprocessor complains about when trying to expand macros. I hope this post helps some people saving some time :-).
In addition, it might be worth renaming those macros in future versions using some less common names, for example, by prefixing them with "Spin__Macro__" or something like this.
Cheers,
Christian
I fully agree that defining the semantics of a nested unless is difficult and that any choice for a semantics will probably not match the expectations of all users.
The fundamental difference between unless and an exception handler as in Java is obviously that the exception handler consumes the exception, while the unless
is based on a boolean condition that is not trivially consumed. Thus, we may "fall through" different unless statements to the most outside one that is enabled.
My expectation was that I would be able to "consume" the boolean condition that triggered the unless by making it false in the second statement of an atomic sequence
right after checking the condition. As it turns out, I should have used d_step instead of atomic for this purpose. Then, the -J option also works as intended.
Long story short, here is the corrected example code:
bit abortFlag;
bit waitFlag;
bit triggerFlag;
bit result;
init{
atomic{
run procA();
run procB();
}
(_nr_pr == 1);
assert(result == true);
}
proctype procA(){
byte x;
{
x = 4;
{ do
:: {
triggerFlag = true;
x = 6;
}
od } unless atomic {d_step{abortFlag == true; abortFlag = false;} printf("Right Unless"); result = true;}
} unless atomic {d_step{abortFlag == true; abortFlag = false;} printf("Wrong Unless"); result = false;}
}
proctype procB(){
if
:: triggerFlag == true -> abortFlag = true;
fi
}Interestingly, the code will not work as intended when omitting the curly braces around the do-loop.
When omitting the braces, the inner unless will not be considered if the last executed statement of procA is x=6
leading to an assertion error in init. Although it cannot leave the loop, spin does not consider the corresponding state
(probably the one after x=6 and before the jump to the beginning of the do-loop) as part of the block
that is defined by the do-loop and that should be used as the main sequence for the inner unless.
Thanks for your answer! Thus I have to change my model. However, I have two follow up comments / questions on this matter.
Given your explanations, I don't see the point of having the -J option at all.
The order in which unless statements are evaluated does not matter if, in any case, execution jumps to the outmost unless that is enabled.
If a nested unless is only fully executed if all outer unless statements are not enabled, then this unless statement will also be
executed while evaluating unless statements in the regular order from outside in. So, toggling the -J option has no effect on the execution.
Thus, what is the intended use for the -J option?
In addition, I conclude from your explanations that only the guard condition "abortFlag == true;" of the inner unless is executed.
But this condition is also the guard condition of an atomic sequence. I would not have expected that Spin jumps out of an
atomic sequence due to an unless guard. In my opinion, this infringes the semantics of the atomic keyword as "defining a
fragment of code that is to be executed indivisibly" given that the statements in my atomic sequence do not block.
I agree that the semantics is really counter-intuitive at this point...
Hello Spin experts,
I stumbled over some unexpected behavior with respect to the use of nested unless statements and the -J options for generating the pan. I've created the following minimal working example for illustrating my problem:
bit abortFlag;
bit waitFlag;
bit triggerFlag;
bit result;
init{
atomic{
run procA();
run procB();
}
(_nr_pr == 1);
assert(result == true);
}
proctype procA(){
byte x;
do
:: {
x = 4;
do
:: {
triggerFlag = true;
(waitFlag == true); //wait here for abort
x = 6;
}
od unless atomic {abortFlag == true; printf("Right Unless"); result = true; abortFlag = false;}
}
od unless atomic {abortFlag == true; printf("Wrong Unless"); result = false; abortFlag = false;}
}
proctype procB(){
if
:: triggerFlag == true -> abortFlag = true;
fi
}I execute the verification using iSpin that generates the following sequence of calls:
spin -a -J TestModel.pml
gcc -DMEMLIM=1024 -O2 -DXUSAFE -DSAFETY -DNOCLAIM -w -o pan pan.c
./pan -m10000 -JThe behavior that I would expect if I set the -J option is the following:
1. procB sets the abortSignal to true
2. the inner unless statement is being executed (the one with "Right Unless") and the inner loop is left
3. the outer loop is not left so we loop and reenter the inner
4. we encounter an invalid end state while waiting on (waitFlag == true)
In fact, Spin does the following, which seems strange to me:
1. procB set the abortSignal to true
2. From the counterexample, I can see that spin kind of "touches" the inner unless but immediately proceeds to the outer unless ("Wrong Unless" in the code) without executing the "Right Unless".
3. Thus, it only outputs "Wrong Unless" and leaves the outer loop.
4. That causes procA to terminate and the assertion in my init process to fail.
Is this behavior of spin intended or a bug? Or am I using the -J option in the wrong way?
Pages: 1