Spinroot

A forum for Spin users

You are not logged in.

#1 2012-12-20 06:46:12

maxnelso
Member
Registered: 2012-12-20
Posts: 1

Deadlock in model

Hi,

I'm kind of new to Spin and I was hoping for some help on a problem I'm having. I have a pretty basic state machine with only 6 states and two threads working in these states. Threads can move from state to state by hearing messages from other threads or on its own. All in all, this seems like a perfect application for Spin.

The problem is when I run the verifier on my pml file (i.e, I do the commands "spin -a twothreads.pml", "cc pan.c", "./a.out", "spin -t twothreads.pml"), I'm getting deadlocked in my program and I'm not sure why. It prints out the final state of the program where it claims there are no more executable actions:

        queue 1 (threadBuffers[0]): [CLAUSE][CLAUSE][CLAUSE][CLAUSE][CLAUSE][CLAUSE][CLAUSE][CLAUSE]
        queue 2 (threadBuffers[1]): [CLAUSE][CLAUSE][CLAUSE][CLAUSE][CLAUSE][CLAUSE][CLAUSE][CLAUSE]
        states[0] = 0
        states[1] = 0

However in my pml file I have (inside a do loop, and i is either 0 or 1 depending on the thread):

         ::  (states[i] == 0)  -> /*read something from the buffer*/             
             threadBuffers[1-i] ? msg;                                             
             if                                                                   
                 ::(msg == CLAUSE) ->                                             
                      skip; /*do nothing*/

                  ...(other code down here)


So shouldn't it at least have the option of dequeuing one of these CLAUSE messages from the queue? I guess I must not understand completely what the verifier is doing. Here is the link to the entire pml file if that will help:

https://dl.dropbox.com/u/68065978/twothreads.pml

Sorry if the terminology I'm using isn't quite right or if I didn't make sense! Thanks for any help, I appreciate it!

-Max

Last edited by maxnelso (2012-12-20 06:47:25)

Offline

#2 2012-12-20 17:14:00

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

Re: Deadlock in model

in the deadlock state itself the two worker processes are at line 34 (internal state 4)
where they are waiting to send a new CLAUSE message:  threadBuffers[i] ! CLAUSE ;
That is the deadlock state. Neither Worker can send the message because both queues are full.
Note that at this point each Worker process has evaluated and passed the condition
(states[i] == 0) ->  and is now waiting, forever, at the next statement, which is the send operation.

Offline

Board footer

Powered by FluxBB