/* See the comment below on how to prevent a "priority inversion" (starving the acquire process) */

proctype handle(int me)
{   
    PID requester;

    do
    :: atomic {
            empty(q_len_ch[me]) && /*<<-- THIS PREVENTS starvation of "acquire" <<--*/
            mutex[me] == 0 && request[me]?[requester] ->
            mutex[me] = 1;
            request[me] ? requester
        };
        if
        :: po[me] != me -> request[po[me]] ! requester
        :: po[me] == me && locked[me] ->
                    waiters[me] ! requester;
                    qlen[me] = qlen[me] + 1;
                    assert (qlen[me] < NPROC)
        :: po[me] == me && !locked[me] ->
                    q_len_ch[requester] ! 0;
                    assert (qlen[me] == 0);
                    po[me] = requester
        fi;
        mutex[me] = 0
    od
}