Join-calculus examples

In this post I will take you through a few examples of join-calculus.

Reader-writer lock

The reader-writer lock is a classic and important concurrency construct. It controls access to a share resource so that multiple readers can have concurrent access while the writer is given exclusive access.

public class ReaderWriterLock {

    public void GetWriter() { getWriter.Invoked(); }
    public void ReleaseWriter() { releaseWriter.Invoked(); }
    public void GetReader() { getReader.Invoked(); }
    public void ReleaseReader() { releaseReader.Invoked(); }

    private async Idle() { return idle.Invoked(); }
    private async Readers(int n) { return readers.Invoked(n); }
    private async Writer() { return writer.Invoked(); }

    #region privates
    private Join mJoin;

    private SyncMethod getWriter;
    private SyncMethod releaseWriter;
    private SyncMethod getReader;
    private SyncMethod releaseReader;

    private AsyncMethod idle;
    private AsyncMethod readers;
    private AsyncMethod writer;
    #endregion

    public ReaderWriterLock() {
        #region initialization
        mJoin = new Join();

        getWriter = mJoin.NewSyncMethod(GetWriter);
        releaseWriter = mJoin.NewSyncMethod(ReleaseWriter);
        getReader = mJoin.NewSyncMethod(GetReader);
        releaseReader = mJoin.NewSyncMethod(ReleaseReader);
        idle = mJoin.NewAsyncMethod(Idle);
        readers = mJoin.NewAsyncMethod(Readers);
        writer = mJoin.NewAsyncMethod(Writer);
        #endregion

        (getWriter & idle).Do(() => {
            Writer();
        });

        (releaseWriter & readers).Do((int n) => {
            Readers(n);
            throw new Exception("Cannot release writer lock if not taken");
        });

        (releaseReader & idle).Do(() => {
            Idle();
            throw new Exception("Cannot release reader lock if not taken");
        });

        (releaseWriter & writer).Do(() => {
            Idle();
        });

        (getReader & idle).Do(() => {
            Readers(1);
        });

        (getReader & readers).Do((int n) => {
            Readers(n + 1);
        });

        (releaseReader & readers).Do((int n) => {
            if (n == 1)
                Idle();
            else
                Readers(n - 1);
        });

        //start state
        Idle();
    }
}

This join class is best represented as a state diagram:

Let’s follow the state machine with a concrete example. We start in the Idle state, a reader requesting a lock takes us to the Readers(1) state. If the reader releases its lock we are back in the Idle state. Now a writer can get the writer lock, which takes us to the Writer state. Releasing the writer lock takes us back to our starting point. This diagram gives a very good picture of the actual state machine. The states correspond to private asynchronous methods of which only ever one can exist at a given time. The transitions are performed by the public synchronous methods.

The code has two additional chords which are not represented in the diagram:

(releaseWriter & readers).Do((int n) => {
    Readers(n);
    throw new Exception("Cannot release writer lock if not taken");
});

(releaseReader & idle).Do(() => {
    Idle();
    throw new Exception("Cannot release reader lock if not taken");
});

These will report forbidden transitions by throwing an exception. Note that both will preserve the state.

The fair reader-writer lock

It is well known that the above implementation of the reader writer lock cannot guarantee that a writer will ever get a chance to get the lock. The fix is a simple one: make sure that no reader is allowed to obtain a lock if a writer is waiting for its lock, in which case only transitions to fewer reader states are allowed. The implementation requires the creation of a few more states to encode this requirement:

The new states IdleWriter and FewerReaders mirror the previous states for the case where the writer lock has been requested with a call to GetWriter. The only possible transition from FewerReaders states is with the ReleaseReader messages. This state machine differs from the unfair reader-writer one in the behaviour of the GetWriter synchronous message which must block until the writer lock has been acquired, i.e. until the Writer state has been reached. This is represented in the diagram with the dashed arrow and the & round box. The associated chords are

    (getWriter & readers).Do((int n) => {
        FewerReaders(n);
        ZeroReader();
    });

    (zeroReader & idleWriter).Do(() => {
        Writer();
    });

were the call to ZeroReader will block until the idleWriter message has been received. The full code for the join class is:

public class FairReaderWriterLock {

    public void GetWriter() { getWriter.Invoked(); }
    public void ReleaseWriter() { releaseWriter.Invoked(); }
    public void GetReader() { getReader.Invoked(); }
    public void ReleaseReader() { releaseReader.Invoked(); }

    private async Idle() { return idle.Invoked(); }
    private async Readers(int n) { return readers.Invoked(n); }

    private async FewerReaders(int n) { return fewerReaders.Invoked(n); }
    private void ZeroReader() { zeroReader.Invoked(); }
    private async IdleWriter() { return idleWriter.Invoked(); }
    private async Writer() { return writer.Invoked(); }

    #region privates
    private Join mJoin;

    private SyncMethod getWriter;
    private SyncMethod releaseWriter;
    private SyncMethod getReader;
    private SyncMethod releaseReader;

    private AsyncMethod idle;
    private AsyncMethod readers;

    private AsyncMethod idleWriter;
    private AsyncMethod writer;
    private AsyncMethod fewerReaders;
    private SyncMethod  zeroReader;
    #endregion

    public FairReaderWriterLock() {
        #region initialization
        mJoin = new Join();

        getWriter = mJoin.NewSyncMethod(GetWriter);
        releaseWriter = mJoin.NewSyncMethod(ReleaseWriter);
        getReader = mJoin.NewSyncMethod(GetReader);
        releaseReader = mJoin.NewSyncMethod(ReleaseReader);
        idle = mJoin.NewAsyncMethod(Idle);
        readers = mJoin.NewAsyncMethod(Readers);

        fewerReaders = mJoin.NewAsyncMethod(FewerReaders);
        zeroReader = mJoin.NewSyncMethod(ZeroReader);
        idleWriter = mJoin.NewAsyncMethod(IdleWriter);
        writer = mJoin.NewAsyncMethod(Writer);
        #endregion

        (getWriter & idle).Do(() => {
            Writer();
        });

        (releaseWriter & writer).Do(() => {
            Idle();
        });

        (getReader & idle).Do(() => {
            Readers(1);
        });

        (getReader & readers).Do((int n) => {
            Readers(n + 1);
        });

        (releaseReader & readers).Do((int n) => {
            if (n == 1)
                Idle();
            else
                Readers(n - 1);
        });

        (getWriter & readers).Do((int n) => {
            FewerReaders(n);
            ZeroReader();
        });

        (zeroReader & idleWriter).Do(() => {
            Writer();
        });

        (releaseReader & fewerReaders).Do((int n) => {
            if (n == 1)
                IdleWriter();
            else
                FewerReaders(n - 1);
        });

        //initial state
        Idle();
    }
}

Discussion

It is always useful to illustrate a system with a diagram, however some features of join-calculus are difficult to represent diagrammatically. Time evolutions can be also useful to illustrate the joining of messages:

These might well be very useful but they do not give a full picture of all possible transitions. Alternatively one could have a graphical representation of all chords:

Two words of explanations, the round boxes represent chords. Incoming arrows are incoming messages, outgoing arrows are messages called in the body of the chord. Solid lines indicate synchronous messages, while dashed lines represent asynchronous messages. The arrows starting with an empty circle indicate messages originating from outside the join class.

This diagram shows the blocking nature of the GetWriter message better than the previous one. But I am not sure how clear it really is, it would probably be enough to add a few more states to make it impossible to read.

Most of the complexity of our diagrams stems from the proliferation of states. Would it be possible to reduce the number of states? Could we encode the actual state as message arguments as we are doing it for the number of readers? We could have something like State(bool,int), the bool would be true if a writer is waiting for the lock, false otherwise, and a positive integer value represent the number readers, while a value of -1 would indicate that the writer lock is taken.

The chords would take the following form

    state(false,  n >= 0)  & getReader     => state(false , n+1);
    state(writer, n > 0)   & releaseReader => state(writer, n-1);
    state(false,  n == -1) & releaseWriter => state(false, 0);
    state(false,  n >= 0)  & getWriter     => state(true, n); zeroReader;
    state(true,   n == 0)  & zeroReader    => state(false, -1);

The number of chords has been reduced from ten to five. They could well be cases where the reduction could be even more significant.

This would require the library to be extended to support the following construct:

    (getWriter & state.When( (w,n) => !w && n>=0) ).Do((w,n) => {
        State(true, n);
        ZeroReader();
    });

Which would be more efficient but less powerful that the following:

    (getWriter & state).When( (w,n) => !w && n>=0) ).Do((w,n) => {
        State(true, n);
        ZeroReader();
    });

where the predicate applies to the whole chord. In this case the predicate would have to be evaluated against all possible combinations of queued up messages. In the first case, where the predicate is attached to the method itself, the predicate acts as a simple filter on the messages, which is much easier to implement and much more efficient at run-time. This per-method option makes it however impossible to combine arguments from different messages in the predicate.