Tech posts by aclassifier
Also see Designer's note page

You are at http://oyvteig.blogspot.com
Archive by month and about me: here
Last edit: 4Sept2015
Started move: September 2012
All updates at http://www.teigfam.net/oyvind/home/, but the overview is updated

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);
    }
}


4 comments:

  1. 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. 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. 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. 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

Archive and about

Popular Posts

Øyvind Teig

My photo
Trondheim, Norway

All new blogs and new home page start at
http://www.teigfam.net/oyvind/home

Overview of old blog notes here

My technology blog was at
http://oyvteig.blogspot.com

and my handicraft blog was at
http://oyvteig-2.blogspot.com

PS: just call me "Oyvind"