Spinroot

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