The Arrow Distributed Directory protocol (DH 98)

This interesting example describes a protocol used in systems that share a unique resource, like
for instance a token that gives privileges to it's owner. Working on a determined connectivity
structure, a minimum spanning tree, the nodes in the system evolve by requesting, waiting, getting
and releasing the object. The connectivity structure evolves along with the nodes in such a way that
the links give the direction to either the object or the nodes that are waiting for it. Since there can
be several nodes requesting the object in parallel a waiting queue can be established, distributed
throughout the system.

First off the nodes behavior is defined: A TerminalOwner that waits for requests for the object,
being that no request has arrived to it; an Owner that either accepts requests for the object or
releases it to the head of the waiting queue; An Idle that passes along requests for the object or
makes it's own request for it; A TerminalWaiter that either passes along requests for the object
or receives it and a Waiter that has the same choice, differing only on the necessary update of
the connectivity links.

defproc 
    TerminalOwner(find,move,obj) =
        find?(mymove,myfind).Owner(find,move,myfind,mymove,obj)
and
    Owner(find,move,link,queue,obj) = 
        select {
            find?(mymove,myfind).(Owner(find,move,myfind,queue,obj) |
                                  link!(mymove,find));
            tau.(Idle(find,move,link) | queue!(obj))
        }
and
    Idle(find,move,link) =
        select {
            find?(mymove,myfind).(Idle(find,move,myfind) |
                                  link!(mymove,find));
            tau.(TerminalWaiter(find,move) | link!(move,find))
        }
and
    TerminalWaiter(find,move) =
        select {
            find?(mymove,myfind).Waiter(find,move,myfind,mymove);
            move?(obj).TerminalOwner(find,move,obj)
        }
and
    Waiter(find,move,link,queue) =
        select {
            find?(mymove,myfind).(Waiter(find,move,myfind,queue) |
                                  link!(mymove,find));
            move?(obj).Owner(find,move,link,queue,obj)
        };

A very simple system is then defined, considering only three nodes.

defproc
    Dir =  
        new find1,move1,find2,move2,find3,move3,obj in 
            ( obj!() |
                TerminalOwner(find1,move1,obj) |
                Idle(find2,move2,find1) |
                Idle(find3,move3,find2));

We then check to see if the system has always a reduction in every possible configuration.

defprop deadlockfree = always(<>true);

check Dir |= deadlockfree;

We now intend to verify that the object will be possibly acquired, in exclusive mode, by any node.
First off we specify that an object has as behavior a possible emission on a channel after which
it becomes the empty process. We also define a node as being a single point in space that is able
to receive two names in a channel, since all nodes are able to accept requests for the object.

defprop object(s) = < s! > 0;

defprop node(f) = 1 and (fresh a. fresh b. < f?(a,b) > true);

We then state that for a node to own the object it just has to contain an occurrence of the object's
name, and to own the object exclusively the node has to own it while the rest of the system has no
occurrences of the object's name.

defprop owns(i,obj) = (node(i) and @obj);

defprop exclusive(i,obj) = (owns(i,obj) | not @obj);

Finally we specify our liveness property by stating that all nodes in the system can come to acquire
exclusive access to the object at some point in time.

defprop live = hidden obj.
    inside (object(obj) |
            forall i. ((node(i) | true) => eventually exclusive(i,obj)));

We check to see if the system satisfies this property for every possible configuration.

check Dir |= always(live);