Spinroot

A forum for Spin users

You are not logged in.

#1 2012-06-07 09:01:49

qweasdzxcqwe
Member
Registered: 2012-06-07
Posts: 3

Algorithmic complexity

What complexity has an algorithm to verify the absence of deadlocks, which is used in SPIN model checker?
Case study: we need only to find deadlocks in our model and each operator in Promela language is an synchronization operator.


Example:
byte semA=1;
byte semB=1;
active proctype P()
{
    printf("MSC: Noncritical section P");
    atomic
    {
        semA>0;
        semA--
    }
    atomic
    {
        semB>0;
        semB--
    }
    printf("MSC: Critical section P");
    semB++;
    semA++;
}
active proctype Q()
{
    printf("MSC: Noncritical section Q ");
    atomic
    {
        semB>0;
        semB--
    }
    atomic
    {
        semA>0;
        semA--
    }
    printf("MSC: Critical section Q");
    semA++;
    semB++;
}

Thanks for reply smile

Offline

#2 2012-06-07 16:25:36

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

Re: Algorithmic complexity

Technically, the complexity is PSPACE
In practice though, worst case complexity is very rarely seen.

Offline

#3 2012-06-29 08:24:57

qweasdzxcqwe
Member
Registered: 2012-06-07
Posts: 3

Re: Algorithmic complexity

Thanks for your help. Could you help me with command arguments for spin. Which arguments I need to use for getting the best performance if I want only to check deadlock abscence?

Now I use such command:
spin -a -X pan_in
gcc -w -o pan {other gcc flags} pan.c
./pan -v -X -m1000000 -w19 -A -n -c1

I am not an expert in using Spin and I think that more optimal way of using command arguments exist smile

Offline

#4 2012-06-29 17:17:23

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

Re: Algorithmic complexity

it will depend on your specific model -- how many states there are,
and whether or not you have enough memory to store all states in memory.
for a large model, you would compile, for instance, with: gcc -O2 -DHC4 -o pan pan.c
if the model is still larger, you would use: gcc -O2 -DBITSTATE -o pan pan.c
and then run with something line: ./pan -w30  (or a lower or higher number depending
on how much memory your machine has)

Offline

#5 2012-06-30 18:20:22

qweasdzxcqwe
Member
Registered: 2012-06-07
Posts: 3

Re: Algorithmic complexity

Thanks for your answer.

Offline

Board footer

Powered by FluxBB