Spinroot

A forum for Spin users

You are not logged in.

#1 2015-12-02 17:52:07

ChristianH
Member
Registered: 2015-12-02
Posts: 7

Nested Unless Statements and the -J option produce unexpected output

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

The 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?

Offline

#2 2015-12-02 21:40:32

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

Re: Nested Unless Statements and the -J option produce unexpected output

This is an interesting example. What happens is the following.
With the -J flag the inner unless guard is evaluated first, which then leads to
the execution to move to the guard statement "abortFlag == true;"
but when we execute this statement, the escape that is defined for that clause
is evaluated -- which is the guard of the outer unless statement,
which is of course also true -- and then execution moves there, leading to
the execution of the "Wrong Unless" both with and without the -J flag.
Clearly this is counter-intuitive, but given the semantics it seems hard to
avoid this.

Offline

#3 2015-12-03 08:16:22

ChristianH
Member
Registered: 2015-12-02
Posts: 7

Re: Nested Unless Statements and the -J option produce unexpected output

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

Offline

#4 2015-12-03 18:42:27

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

Re: Nested Unless Statements and the -J option produce unexpected output

I completely agree.  That initial guard statement of the inner unless is not actually executed.
It is initially selected for execution, but then spin determines that it has an active escape as well, so that
also gets overruled and the outer unless takes over.

I fully agree with your assessment though. How could one define the semantics of nested unless to prevent this?

Offline

#5 2015-12-04 10:59:30

ChristianH
Member
Registered: 2015-12-02
Posts: 7

Re: Nested Unless Statements and the -J option produce unexpected output

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.

Offline

Board footer

Powered by FluxBB