/*
From ratan@facility Fri Feb 17 16:20:27 1995
Received: from sunset.cs.utah.edu by bliss.cs.utah.edu (8.6.9/utah-2.15sun-leaf)
	id JAA03737; Fri, 17 Feb 1995 09:20:26 -0700
From: ratan@facility
Received: from lal.cs.utah.edu by sunset.cs.utah.edu (8.6.9/utah-2.15sun-leaf)
	id JAA10122; Fri, 17 Feb 1995 09:20:25 -0700
Received: by lal.cs.utah.edu (8.6.9/utah-2.15sun-leaf)
	id JAA20451; Fri, 17 Feb 1995 09:20:24 -0700
Date: Fri, 17 Feb 1995 09:20:24 -0700
Message-Id: <199502171620.JAA20451@lal.cs.utah.edu>
To: ganesh@facility
Subject: locking protocol
Content-Length: 3256
Status: R
*/

/* Three processes, and one lock */

#define PID byte
/* #define NEVER */

bit mutex[3];
PID po[3];
chan request[3] = [2] of {PID};
chan q_len_ch[3] = [1] of {byte};
chan waiters[3] = [2] of {PID};
byte qlen[3];   /* How many are waiting? */
bit locked[3];

proctype acquire(PID me)
{
    PID thread;
    byte count;
    loop:
        /* Try to acquire the lock */
        atomic { mutex[me] == 0 ->
                 mutex[me] = 1
        };
        if
        :: po[me] == me -> locked[me] = 1;
                            mutex[me] = 0
        :: po[me] != me ->
                        request[po[me]]!me;
                        mutex[me] = 0;
                        /* Wait until reply comes back */
                        atomic {q_len_ch[me] ? [count] && mutex[me]==0 ->
                                po[me] = me;
                                mutex[me] = 1;
                                q_len_ch[me] ? count;
                                qlen[me] = qlen[me]+count;
                                count = 0
                        };
                        ( len(waiters[me]) == qlen[me] );
                        locked[me] = 1;
                        mutex[me]=0
        fi;
/*  */
#ifndef ONEPROC
    progress:
#endif
                        /* Acquire continued */
    release:
#ifdef ONEPROC
        if
        :: atomic {
            /* Is process0 making progress? */
            (me == 1) -> skip;
            progress: skip
        }
        :: (me != 0)
        fi;
#endif
        atomic {
            mutex[me] == 0 ->
            locked[me] = 0;
            mutex[me] = 1
        };
        if
        :: qlen[me] ->
            waiters[me] ? po[me];
            qlen[me] = qlen[me]-1;
            q_len_ch[po[me]] ! qlen[me];
            do
            :: qlen[me] -> atomic {
                waiters[me] ? thread;
                waiters[po[me]] ! thread;
                thread = 0;
                qlen[me] = qlen[me]-1
               }
            :: !qlen[me] -> break
            od
        :: !qlen[me] -> skip
        fi;
        mutex[me] = 0;
        assert (qlen[me] >= 0);
    goto loop
}


/*  */

proctype handle(int me)
{
    PID requester;

    do
    :: atomic {
            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] < 3)
        :: po[me] == me && !locked[me] ->
                    q_len_ch[requester] ! 0;
                    assert (qlen[me] == 0);
                    po[me] = requester
        fi;
        mutex[me] = 0
    od
}

/*  */
                     /* One lock at a time only */
#ifdef NEVER
never {
    do
    ::1 -> skip
    ::locked[0] && (locked[1] || locked[2]) -> goto error
    ::locked[1] && locked[2] -> goto error
    od;

    error:
    end: skip
}
#endif

init {
    byte cnt;

    atomic {
        do
        :: cnt == 3-> break
        :: cnt != 3-> run acquire(cnt);
                      run handle(cnt);
                      cnt = cnt+1
        od
    }
}