Spinroot

A forum for Spin users

You are not logged in.

#1 2011-11-13 04:55:32

awesan
Member
Registered: 2011-04-30
Posts: 45

strong vs weak fairness in SPIN

Q1.
In the SPIN book page-182 line-13 reads "Not surprisingly, therefore SPIN only includes support for weak fairness, and not for strong fairness". I hope this statement does not hold good any more and the current version of the SPIN does support strong fairness, right? If the option "-f" to pan is passed, model is verified for weak-fairness and if it is not passed, then the model is verified for strong-fairness, I suppose.

Q2.
***************************
byte x = 2;

active proctype A()
{   
    do
    ::    x = 3 - x; 
        progress: skip;
    od
}

active proctype B()

    do
    ::    x = 3 - x;
        //progress: skip;
    od
}
***************************
In the above model, I am observing the following results for strong fairness and weak fairness for different permutations of enabling the progress label.

(1) no progress label          : strong fairness : failure
(2) no progress label          : weak fairness   : failure
(3) progress label in only A : strong fairness : failure
(4) progress label in only A : weak fairness   : success
(5) progress label in both    : strong fairness : success
(6) progress label in both    : weak fairness   : success

I understand the result for (1), (2), (5) and (6). I do not understand why (4) is "success", when (3) is "failure". For the case (4), I added proctype (C) with the same body and without the progress label defined and SPIN reports still success. Could you please explain?

Offline

#2 2011-11-13 05:27:41

awesan
Member
Registered: 2011-04-30
Posts: 45

Re: strong vs weak fairness in SPIN

I found the definitions for Absolute Fairness, Strong Fairness and Weak Fairness from the following URL interesting : http://www.ccs.neu.edu/home/wahl/Publications/fairness.pdf
I guess SPIN supports "Strong Fairness" (-l option and not -f option for pan) and "Weak fairness" (-l and -f options for pan). Is that right? Or the definitions above are different from SPIN's definition of fairness? Thanks in advance.

Offline

#3 2011-11-13 07:43:33

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

Re: strong vs weak fairness in SPIN

re strong and weak fairness
Spin only has builtin support for weak fairness, as defined in the book.
You can define any other type of fairness through the use of LTL, or with the help of never-claims though.
So Spin itself can support strong fairness as well, but you then have to define it yourself -- it is not predefined.
Without -f, no fairness is assumed. With -f only weak fairness is assumed.
Note that the option -l is for non-progress cycle detection -- it is not related to any form of fairness.

Offline

#4 2011-11-14 00:37:33

awesan
Member
Registered: 2011-04-30
Posts: 45

Re: strong vs weak fairness in SPIN

My assumption - not selecting "weak" is "strong" - is pretty bad. Thanks for the explanation. Your prompt response keeps me getting farther in understanding model checking. Thanks very much again.

Last edited by awesan (2011-11-15 02:23:46)

Offline

#5 2011-11-17 07:53:58

awesan
Member
Registered: 2011-04-30
Posts: 45

Re: strong vs weak fairness in SPIN

Hi there,
Thanks again for all the help so far. I have a question about verification for strong fairness in the following model :
**************************
inline acq_sem(sem)
{
    atomic {
        sem > 0 ->
            sem--;
    }
}

inline rel_sem(sem)
{
    sem++;
}

#define MAX_SEM_VAL 2
int sem = MAX_SEM_VAL;

active proctype P()
{
end:
    do
    ::
         skip; // in order to specify label l0 inside the loop
l0:
        acq_sem(sem);
l1:
        rel_sem(sem);
l2:
        skip;
    od;
}

active [2] proctype Q()
{
end:
    do
    ::    acq_sem(sem);
        rel_sem(sem);
    od;
}
ltl p1 { [] (sem >=0 && sem <= MAX_SEM_VAL) }

ltl p2 { [] (P@l1 -> <> P@l2) }

ltl p2a { [] (P@l0 -> <> P@l2) }

ltl p2b { ([] <> P@l0) -> ([] <> P@l2) }

ltl p2c { (<> P@l0) -> (<> P@l2) }

**************************
I see that "p2a" fails when it is verified for acceptance cycles with weak-fairness constraint enforced whereas "p2" passes. This is due to the fact that P@l0 does not remain continuously executable(enabled) whereas P@l1 remains continuously executable thus satisfying the weak fairness constraint. So far, so good. Now, I want to express strong fairness constraint through LTL and my attempt is "p2b". P@l0 would be enabled infinitely often but not continuously enabled and hence I expect P to acquire semaphore eventually. However, acceptance cycle verification fails. I tried "p2c" though it does not look quite correct to me, but it also fails on verification for acceptance cycles. Can strong fairness for this example ("If P tries to acquire semaphore infinitely often and the other processes do release semaphore such that P@l0 becomes "enabled" infinitely often, it will eventually acquire the semaphore") be specified using LTL? Or, do I need to write a "never" claim for this? Thanks in advance.

Offline

#6 2011-11-17 18:45:18

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

Re: strong vs weak fairness in SPIN

A good question, and this can be tricky to do.
With a never claim it is not too difficult. I think this one does the trick.
It reveals no counter-examples with ./pan -a and captures the property.
I'd have to think much harder about expressing this in LTL though....


never {    /* P infinitely often at l0, but never at l2 */
S0:
    do
    :: P@l0 && !(P@l2) -> break        /* P reaches l0 */
    :: !(P@l0) && !(P@l2)
    od;
accept:    !(P@l2);                /* pass accept */
S1:    do
    :: !(P@l0) && !(P@l2) -> goto S0    /* P leaves l0 */
    :: !(P@l2)
    od
}

Offline

#7 2011-11-18 03:09:13

awesan
Member
Registered: 2011-04-30
Posts: 45

Re: strong vs weak fairness in SPIN

Thanks very much Dr.Holzmann for the quick response and the solution. I did verify that your claim verified without errors. I replaced "l2" with "l1" in the never claim and it also verified without errors and since "rel_sem" does not block, I thought that would be a good and sufficient test. I have a few questions:

Q-1.
I tried to come up with a few never claims myself and I either got verification errors or no verification errors. But, when there was no verification error, I was not convinced that I wrote the never claim correctly (It was not resembling what you have provided). In the process, for one or two claims, I was certain I got it wrong (since the number of states reported during verification was spectacularly low (like 1 or 2) ). However, when the verification states and transitions seemed to be above 20 and 70 respectively, I could not tell for sure whether I got the claim correctly or not. Mostly, I could reason LTL formulae and simple never claims with confidence that I have got the claim right (and I should fix the model, if errors are reported). However, if the claim itself is  tricky (like this one) and there is no verification error, I am just not sure whether I am verifying what I intending to verify. If you don't mind, could you please explain briefly how you came up with this claim? Especially, I did not understand how and why you got the "accept" label in the middle. When labels l0 and l2 (or l0 and l1 in the never claim written with replacing l2 by l1) point to different states, is the check for "P@l2" not redundant in the condition "P@l0 && !(P@l2)"?

Q-2.
I get the following warning:
*******************************************************************************************
warning: for p.o. reduction to be valid the never claim must be stutter-invariant
(never claims generated from LTL formulae are stutter-invariant)
*******************************************************************************************
Do I need to make sure that the never claim is "stutter-invariant", if I write a never claim and not use LTL as in this case? Is there a way to do it?

Q-3.
My google-search did not find one. Is there a never claim to LTL converter? (I see we can do the other way around obviously). Or, is it not theoretically possible (forgive my ignorance)?

Q-4.
iSpin threw the following error when I tried to click on "claim_never_0" to view the state diagram. However, I could create the .dot file and .ps file from command line and use a ps file viewer. So, not a big deal. However, if you want to fix it, here is the bug report.
*******************************************************************************************
unexpected "," outside function argument list
in expression "50 * 1, height="
unexpected "," outside function argument list
in expression "50 * 1, height="
    (parsing expression "50 * 1, height=")
    invoked from within
"expr 50 * $mf"
    (procedure "find_field" line 10)
    invoked from within
"find_field "width="  $line"
    (procedure "display_graph" line 129)
    invoked from within
"display_graph claim_never_0"
    (command bound to event)
*******************************************************************************************
Thanks again for your time and help.

Last edited by awesan (2011-11-18 05:13:15)

Offline

#8 2011-11-18 05:55:57

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

Re: strong vs weak fairness in SPIN

Q1: I placed the accept label outside the loop on S1, to make sure that we don't accept on the wrong condition. Note that we want to check for "P infinitely often at l0, but never at l2 "  and if the accept is on S1 then we don't capture the fact that P has to move through l0 repeatedly.
Q2: that's the standard warning that Spin generates. i'm fairly certain that this property is stutter invariant, but if you're not sure, simply turn off partial order reduction and repeat the verification (use -DNOREDUCE in the compilation of pan.c)
Q3: you can express more properties in never claims than in LTL, so there cannot be such a converter (LTL defines only a sub-set of the omega-regular properties)
Q4: i'll check it out -- thanks for the bug report!

Offline

Board footer

Powered by FluxBB