Specifying Token Ring for Mutual Exclusion

Updated

Mutual exclusion is a common term appearing frequently in computer sciences. In essence, it’s a mechanism of concurrency control allowing exclusive access to some resource (or “critical region”). Token passing is an algorithm for distributed mutual exclusion (DME) and will be our focus in this post.

DME specifications usually make the following assumptions:

Thing we might want to guarantee for DME specifications are:

In addition, we need to analyze DME algorithms' performance metrics, which usually includes:

Let’s take a token ring as an example. In a token ring, a client holds a token and then sends it to the next one after exiting its critical section. When we make assumptions about a token ring, we

token-ring

We want to guarantee that

To analyze token performance, we use the above performance metrics (message complexity, response time, and throughput)

A naive specification for mutex in Ivy would be:

action grant(v:id)
action release(v:id)

specification {
    var lock(X:id):bool
    after init {
        lock(X) := false;
    }
    
    before grant {
        require ~lock(X);
        lock(v) := true
    }

    before release {
        require lock(v);
        lock(v) := false
    }
}

To see token ring in action, we use the demo from Ken’s presentation:

#lang ivy1.8

include network
include numbers

global {
    type host_id = {0..max}
    alias token = uint[1]
    instance net : tcp.net(token)
}

process host(self:host_id) = {
    import action grant
    export action release

    specification {
        var lock : bool

        after init {
            lock := false;
        }

        before grant {
            require forall X. ~host(X).lock;
            lock := true;
        }

        before release {
            require lock;
            lock := false;
        }
    }

    implementation {
        instance sock : net.socket

        after init {
            if self = 0 {
                pass
            }
        }

        action pass = {
            var tok : token;
            var next := 0 if self = max else self + 1;
            sock.send(host(next).sock.id, tok);
        }

        implement sock.recv(src:tcp.endpoint, val:token) {
            grant;
        }

        implement release {
            pass;
        }
    }
}

We put the above code into a file called token_ring.ivy and compile it using ivyc token_ring.ivy. Then we launch the program using ivy_launch max=2 token_ring.ivy, which opens three terminal windows.

If we type in host(1) with host.release, we see in host(2) it outputs host.grant, which seems to show that the token work properly. However, if we type host.release again in host(1), host.grant will show up again in host(2), resulting in multiple tokens getting created, which violates the requirement that there is at most one token in the ring at any given time.

If we execute ivyc target=test token_ring.ivy && ivy_launch max=2 token_ring.ivy, then we see the token ring work properly. The reason is we have specified the requirement for grant and release (require forall X. ~host(X).lock for grant and require lock for release).

grant is an action imported from the environment, thus we know when grant happens, all clients in the network do not hold a lock. On the other hand, release is an action exported from the system, which means the tester must perform grant given the host has the lock. So the tester won’t perform release multiple times like we did above because the tester can not violate the require lock requirement.