Tuesday, July 19, 2011

Infernal dinner synchronization problem

Imagine group of hungry people with spoons sitting around pot of stew. Spoon’s handle long enough to reach the pot but it is longer than the arm and no one can feed himself. People are desperate. This is a picture described in recently found piece of lost chapter of Dante’s Inferno. In order to help them Dante suggested to feed one another.

Only one person can feed another at the same time. While feeding someone else a person cannot eat. People must not starve meaning once hungry a person will be fed. It is assumed that spoon’s handle allows to feed any other person expect for yourself.

We’ll develop algorithm to let unfortunate ones to synchronize with each other and not to starve. It may seems similar to dinning philosophers problem but the latter has a limited choice of selecting the order of taking forks and the degree of contention is low. However in infernal dinner problem choice space and degree of contention is comparable with the problem size which is the number of people (a person may choose to try to feed any other person while potentially contending with all other but the person to be fed).

Here are few important observations:

  • If everyone want to eat or to feed others at the same time they are doomed to deadlock. So at any given point in time at least one person must be willing to eat and at least one person to feed.
  • If a person fed someone next time he must eat and if a person ate next time he must feed thus they won’t get to all want to do the same situation that is a deadlock.
  • In order to prevent starvation some sort of fairness must be guaranteed. One person must not be able to get fed infinitely many times while there are other people waiting.
  • People must somehow agree in pairs (hungry one and not) to feed each other and while doing so others must not be able to pair with them.

The first two are quite straightforward. Any person will either be hungry or not and every time a person eats the state changes. At the beginning at least one person is hungry and at least one is not.

The last two are more tricky. As you remember there two types of people those that are hungry and those who do not. Let’s assume there are hungry people that line up and wait to be fed. Then people that are willing to feed come and take one by one from the head of the line hungry people and feed them. If no more hungry people left they also line up and wait for hungry people. They basically switched. This a an idea of how hungry and non-hungry people can pair to feed each other. While a pair of people is outside of the queue nobody else can interfere them.

The queue is represented through linked linked list of the following form h->n0->n1->…->nk where h is a sentinel head node. Head and tail are never equal to null as in case of empty queue they both point to sentinel node. Nodes are added to the tail and removed from the head. In order to remove node from the beginning of the queue head node must be advanced to its successor that must not be non null otherwise the queue is considered empty. Adding is trickier. It is based on the fact that once next of a node is set it is never changed. It is done in two steps. First tail’s next is set to the node to be added and up on success (at this point the node is visible to other threads) tail is advanced to newly added node. Because this process is not atomic other threads may observe the change half way through. In that case a thread may help to finish adding the node by advancing the tail and retry its own operation.

Now to the line up part. Essentially there are two cases:

  • When the queue is empty or there are already nodes of the same type
    • new node must be added to the end of the queue and waited upon until paired with someone else
  • Otherwise a node at the beginning must be removed and waiting thread notified of formed pair

Based on this rules waiting queue will either be empty or contain nodes of the same type which is equivalent to a line of either hungry or non-hungry people.

Here goes the implementation.

class SyncQueue<T>
{
    private volatile Node m_head;
    private volatile Node m_tail;

    public SyncQueue()
    {
        // Head is a sentinel node and will never be null
        m_head = new Node(default(T), false);
        m_tail = m_head;
    }

    public T Exchange(T value, bool mark, CancellationToken cancellationToken)
    {
        var node = new Node(value, mark);
        // Do until exchanged values with thread of 
        // a different type
        while (true)
        {
            cancellationToken.ThrowIfCancellationRequested();

            var head = m_head;
            var tail = m_tail;

            // If the waiting queue is empty or already contains
            // same type of items
            if (head == tail || tail.m_mark == mark)
            {
                // Attempt to add current item to the end of the 
                // waiting queue
                var nextToTail = tail.m_next;
                // To avoid costly interlocked operations check 
                // if assumtion about the tail is still correct
                if (tail != m_tail)
                    continue;
                // If next to what observed to be the tail is 
                // not null then the tail fell behind
                if (nextToTail != null)
                {
                    // Help to advance tail to the last node 
                    // and do not worry if it will fail as 
                    // someone else succeed in making tail up 
                    // to date
                    Interlocked.CompareExchange(ref m_tail, nextToTail, tail);
                    // And retry again
                    continue;
                }
                // Try to append current node to the end of the 
                // waiting queue by setting next of the tail
                // This is a linearization point of waiting case
                // (adding node to the end of the queue)
                if (Interlocked.CompareExchange(ref tail.m_next, node, null) != null) 
                    // Retry again if lost the race
                    continue;
                // Advance the tail with no check for success as 
                // in case of failure other thread is helping to
                // advance the tail
                Interlocked.CompareExchange(ref m_tail, node, tail);
                // Wait until exchange is complete
                var spin = new SpinWait();
                while (node.m_mark == mark)
                {
                    spin.SpinOnce();
                    cancellationToken.ThrowIfCancellationRequested();
                }
                // Correct value will be observed as reading mark 
                // implies load acquire semantics
                return node.m_value;
            }
            // Non empty waiting queue with items of a different 
            // type was observed thus attempt to exchange with 
            // thread waiting at the head of the queue through 
            // dequeueing
            var nextToHead = head.m_next;
            // Check if observed head is still consistent and it
            // has successor
            if (head != m_head || nextToHead == null)
                continue;
            // Observed non-empty queue can either grow which is
            // fine as we are interested here in the head node 
            // otherwise attempt below will fail and will retry 
            // again.
            // Attempt to advance head that is a sentinel node 
            // to its successor that holds sought value and is 
            // supposed to be new sentinel.
            // This is a linearization point of releasing case 
            // (removing node from the beginning of the queue)
            if (Interlocked.CompareExchange(ref m_head, nextToHead, head) != head) 
                // Retry if lost the race
                continue;
            // At this point head's successor is dequeued and no
            // longer reachable so values can be safely exchanged
            var local = nextToHead.m_value;
            nextToHead.m_value = value;
            // Switch mark to let waiting thread know that 
            // exchange is complete and making it the last store
            // with release semantics makes sure waiting thread 
            // will observe correct value
            nextToHead.m_mark = mark;

            return local;
        }
    }

    class Node
    {
        internal volatile Node m_next;
        internal volatile bool m_mark;
        internal T m_value;

        internal Node(T value, bool mark)
        {
            m_value = value;
            m_mark = mark;
        }
    }
}

class Human
{
    private volatile bool m_hungry;

    public Human(bool hungry)
    {
        m_hungry = hungry;
    }

    public void WaitAndEat(SyncQueue<Human> waitingQueue, CancellationToken cancellationToken)
    {
        var spin = new SpinWait();
        while (true)
        {
            spin.Reset();
            // The hell seems to have frozen =)
            cancellationToken.ThrowIfCancellationRequested();

            // Pair with someone either to feed hungry man 
            // or eat yourself if hungry
            var pairedWith = waitingQueue.Exchange(this, m_hungry, cancellationToken);
            if (!m_hungry)
                // Feed hungry man
                pairedWith.Feed();
            else
                // Wait to be fed
                while (m_hungry)
                {
                    spin.SpinOnce();
                    cancellationToken.ThrowIfCancellationRequested();
                }
        }
    }

    private void Feed()
    {
        // Switch to non hungry as just ate
        m_hungry = !m_hungry;
    }
}

The infernal dinner is served =)