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

Here 15Mar2009 to 22May2026. Now at https://www.teigfam.net/oyvind/home/technology/009-the-knock-come-deadlock-free-pattern/