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

    }

}

009 - The "knock-come" deadlock free pattern

Intro and disclaimer

This note is based on a published paper [1]. At the time of publication (2005) I did not think that chapter 10 would describe any more than an interesting case of software engineering. To this date it stays so. However, people have asked me about this pattern. This note therefore describes nothing new, but will add some more discussion.

Disclaimers: 1.) Should anybody claim this pattern as already used, invented or even patented, prior to 2005 - good! It is not known to me (but now I do know that I am not alone, see bullet list below). Please mail me if this is the case - so that I may be abe to honour it here - or obsolete - at least the suggested name. 2.) Even if the pattern is deadlock free, there may be errors in this note. 3.) Any usage of this pattern is out of my control and responsibility.

• In Jan.10 I discovered that the "USL Distributed Event Driven Protocol" seems to be similar. See [4].
• In Feb.10 I was made aware that the OpenComRTOS also uses a mechanism in the same street. See [5].

I have named the pattern "knock-come" for a rather obvious reason - the explicit behaviour it must display in order to function properly. The name does not fully describe the behaviour, but it should hold as a reminder.

Rationale

When two software threads or rather, processes, need to talk with each other at the same time, we would get a deadlock if they were communicating over synchronous, blocking channels. This note describes a simple software pattern that removes the possibility of deadlock. It also shows a formal model and verification of the algorithm, written in Promela and evaluated with Spin [2].

The original description, from [1] - of the "knock-come" pattern:

10. Deadlock avoidance

Where two processes spontaneously need to send data to each other, a blocking communication scheme might cause deadlock. This is a state where processes try to communicate – in a circular pattern – blocking for each other to become ready, and therefore unable to proceed. This is pathological and must not happen. All processes run at the same priority, so any priority inversion problem is ruled out in the system.

Figure at http://www.teigfam.net/oyvind/pub/ercim05_at_euromicro-2005/Figure_chapter_10.jpg from [1]. 

The pattern we chose to avoid this was to give the processes clear roles: slave and master. Master may send on the blocking channel any time (solid arrows) when it has something. Slave would never block on any spontaneous message, since the asynchronous “poll me” message (stippled arrow) lets the slave go on and not block, and then instead hang in an INPUT or ALT on the input channel. When the “OK, come on” message arrives from the master, the agreed upon protocol assures no deadly embrace.

Software architecture


Figure at http://www.teigfam.net/oyvind/pub/CPA2006/presentation/Fig1.jpg, from [3].

We see two processes, the top and bottom P_.. processes. The left dotted lines, downwards are asynchronous non-blocking send channels. One one of them is of interest now. Let's call it the knock channel (Chan_202 in the figure). It carries no data.

The other arrows are one up-going come channel (Chan_201) and the down-going channel (Chan_200). Both are synchronous non buffered and blocking send and receive. Both carry data, together with a tag that describes the contents. They are drawn like a two-way channel, but they are two one-way channels. In addition to the come message, these channels are also used to send the actual data - in both directions.

Message sequence in words

Whenever the bottom process needs to send data, it may do it any time. It is the master.

Whenever the top process, the slave, needs to send data, it may send one only query ("knock") any time. For the 1.) data up and the 2.) query - not to deadlock, the query is sent as a no data "interrupt" signal. The slave would send only once per session, so P1_Slave will always proceed (and not block) on this sending.

Whenever the bottom process decides that it has time to handle the query, it sooner or later sends the "ok, come on" up and immediately waits for the slave to respond to that message by sending the data down. Whenever the data has left slave, the sequence with the query may be repeated.

By sooner or later we mean that in the meantime the master may send any number of messages up. As we started with saying, the master may send any time.

The reason why the knock /query / interrupt channel has no data, is really that is simply that it does not need to have any data. Also, in real life, it is simple to implement an asynch channel with zero buffer.

Formal proof of deadlock freedom

The Promela model code below verifies to no "invalid end state", using spin / xspin. This means that it will not deadlock. Observe that with LEN set to zero it will deadlock. It has been modeled to resemble how the processes are coded with a standard synchronous methodology (language or library) - where only inputs may be ALT'ed over. (Note 010 above gives a very interesting deadlock free alternative.)

The code is my initial iteration on the theme:

mtype =
{
    M_KNOCK_DIRDOWN,
    M_COME_DIRUP,
    M_DATA_DIRUP,
    M_DATA_DIRDOWN
};

#define LEN 1 /* Invalid end state (ie deadlock) if this is zero */

chan Chan_knock_down = [LEN] of {mtype}; /* Chan_202 */
chan Chan_data_down  = [0]   of {mtype}; /* Chan_200 */
chan Chan_data_up    = [0]   of {mtype}; /* Chan_201 */

proctype P1_Slave (chan Chan_knock_out, Chan_data_in, Chan_data_out)
{
    bool Knock_send;
    bool Knock_sent = false; /* necessary? */

    Run:
        if
        ::  Knock_send = true;  /* non-deterministic setting to true.. */
        ::  Knock_send = false; /* ..or false */
        fi;

        if
        ::  (Knock_sent == false) && (Knock_send == true) ->

            /* Am slave, but want to get rid of my data now */
            Chan_knock_out ! M_KNOCK_DIRDOWN;
            Knock_sent = true;

        ::  else -> skip;
        fi;

        if
        ::  Chan_data_in ? M_DATA_DIRUP -> skip;

            /* Am slave, always able to receive from master */

        ::  Chan_data_in ? M_COME_DIRUP ->

            /* Got "come" from master, do it */
            Chan_data_out ! M_DATA_DIRDOWN;
            Knock_sent = false; 
        fi;
        goto Run;
};

proctype P2_Master (chan Chan_knock_in, Chan_data_in, Chan_data_out)
{
    bool Knock_received = false;
    bool Data_send;

    Run:
        if
        ::  Data_send = true;  /* non-deterministic setting to true.. */
        ::  Data_send = false; /* ..or false */
        fi;

        if
        ::  (Data_send == true) ->

            /* Is master, may always send */
            Chan_data_out ! M_DATA_DIRUP;

        ::  (Knock_received == true) ->

            /* Send "come" and get data, according to "contract" */
            Knock_received = false;
            Chan_data_out  ! M_COME_DIRUP;
            Chan_data_in   ? M_DATA_DIRDOWN;

        ::  else -> skip;
        fi;

        if
        ::  Chan_knock_in ? M_KNOCK_DIRDOWN ->
            /* Slave "knocks" */
            Knock_received = true;

        ::  timeout -> skip;
            /* global "else" to make "Chan_knock_in" input a poll */
        fi;
        goto Run;
};

init
{
    atomic
    {
        run P1_Slave  (Chan_knock_down, Chan_data_up,   Chan_data_down);
        run P2_Master (Chan_knock_down, Chan_data_down, Chan_data_up);
    }
}

Daisy-chaining this pattern

This pattern scales. You may take a slave's Chan_data_down and connect to another's Chan_data_up, and let a new master have one more Chan_knock_down from each new slave. This daisy-chains with loop-back, equal slaves, which must then share via-traffic for the others. I have proven it deadlock free with a slightly modifed Promela model.

References

[1] - From message queue to ready queue. Øyvind Teig, 2005. Subtitle: Case study of a small, dependable synchronous blocking channels API. "Ship & forget rather than send & forget". Ref chapter "10 - Deadlock avoidance". See http://www.teigfam.net/oyvind/pub/pub_details.html#Ercim05 and read at http://www.teigfam.net/oyvind/pub/ercim05_at_euromicro-2005/paper.pdf. In First ERCIM Workshop on Software-Intensive Dependable Embedded systems. Editors: Amund Skavhaug, Erwin Schoitsch. ISBN 2-912335-15-9, IEEE Computer press

[2] - Promela and Spin. See http://spinroot.com/ and http://en.wikipedia.org/wiki/Promela

[3] - No Blocking on Yesterday’s Embedded CSP Implementation. Øyvind Teig. Subtitle: The Rubber Band of Getting it Right and Simple. In Communicating Process Architectures 2006, Peter Welch, Jon Kerridge, and Fred Barnes (Eds.) IOS Press, 2006, pages 331-338, ISBN 1-58603-671-8. Read at http://www.teigfam.net/oyvind/pub/pub_details.html#NoBlocking

[4] - "USL Distributed Event Driven Protocol", described in Universal Systems Language: Lessons Learned from Apollo. Margaret H. Hamilton and William R. Hackler, Hamilton Technologies, Inc. In IEEE Computer, Dec. 2008 pp. 34-43
("USL"). Also see my 007 - Synchronous and asynchronous, where this is discussed thorouhgly.

[5] - Comment [C.4] of 007 - Synchronous and asynchronous

--