Algorithmic complexity

qweasdzxcqwe · 2012-06-07 09:01:49

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

spinroot · 2012-06-07 16:25:36

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

qweasdzxcqwe · 2012-06-29 08:24:57

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

spinroot · 2012-06-29 17:17:23

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)

qweasdzxcqwe · 2012-06-30 18:20:22

Thanks for your answer.

Spinroot

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

Algorithmic complexity

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

Re: Algorithmic complexity

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

Re: Algorithmic complexity

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

Re: Algorithmic complexity

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

Re: Algorithmic complexity

Board footer