An Invalid (Deadlocked) Model of Resource Sharing Problem

promela_sharing.pml

/*
 * Resource Sharing Problem (Example for Deadlock)
 */

mtype = { LOCK, UNLOCK };

proctype Client(chan to_res1, to_res2) {
    if
    ::  to_res1 ! LOCK(_pid);
        to_res2 ! LOCK(_pid);
    ::  to_res2 ! LOCK(_pid);
        to_res1 ! LOCK(_pid);
    fi;
    if
    ::  to_res1 ! UNLOCK(_pid);
        to_res2 ! UNLOCK(_pid);
    ::  to_res2 ! UNLOCK(_pid);
        to_res1 ! UNLOCK(_pid);
    fi
}

proctype Resource(chan to_res) {
    pid locker;
    pid unlocker;
    end:
    do
    ::  to_res ? LOCK(locker);
        to_res ? UNLOCK(unlocker);
        assert(locker == unlocker);
    od
}

init {
    chan to_scanner = [0] of { mtype, pid };
    chan to_printer = [0] of { mtype, pid };
    atomic {
        run Client(to_scanner, to_printer);
        run Client(to_scanner, to_printer);
        run Resource(to_scanner);
        run Resource(to_printer);
    }
}