Wednesday, March 18, 2009

010 - A running Promela model

Why does this code run and don't deadlock?

mtype = {M_UP, M_DW};

#define LEN 0

chan Chan_data_down = [LEN] of {mtype};
chan Chan_data_up   = [LEN] of {mtype};

proctype P1 (chan Chan_data_in, Chan_data_out)
{
    do
    ::  Chan_data_in  ? M_UP -> skip;
    ::  Chan_data_out ! M_DW -> skip;
    od;
};
proctype P2 (chan Chan_data_in, Chan_data_out)
{
    do
    ::  Chan_data_in  ? M_DW -> skip;
    ::  Chan_data_out ! M_UP -> skip;
    od;
};

init
{
    atomic
    {
        run P1 (Chan_data_down, Chan_data_up);
        run P2 (Chan_data_up,   Chan_data_down);
    }
}


at

4 comments:

  1. Anonymous19 March, 2009 11:09

    All statements in an if or do have the same priority here (because there isn't an unless clause). Each transition is checked for "executability". Rendezvous communication statements (synchronous send and receives) set a local variable (rv) that represent the channel and that it is synchronous.

    A wish for a send sets a "handshake" representing the wish and the channel. If a receive statement wish to receive on a channel on which a handshake is active then, provided the pattern-match fits, it will become executable (rv matches the handshake). In your example all receive-statements matches the sends, and then a non-deterministic choice is made between them. As at least one transition is possible there is no deadlock.

    Remember that the semantics are defined on the global/complete state-machine, and all statements are checked for executability before one is chosen. Hope this helps.

    ReplyDelete
  2. Natalie19 March, 2009 16:05

    Can you say why you originally thought that it should deadlock? is it because of the skip statements (which are redundant of course) ?

    ReplyDelete
  3. aclassifier19 March, 2009 20:54

    By reading it, and mentally thinking about the two equal parts, with respect to input and output. The two parties wanting and providing the services of and to each other - symmetrically - would naturally ring a deadlock bell in my head! At the moment, being new to Promela, I in a way disagree with the non-deadlocking semantics. I haven't yet learned that behaviour! Is there too much "Promela semantics" below this code, causing it not to deadlock?

    ReplyDelete
  4. aclassifier06 August, 2009 19:57

    I have tried to make a summary of this at the Wikipedia Promela article (after some private communications as well). See http://en.wikipedia.org/wiki/Promela. Try Executability.

    ReplyDelete