The goal of this project funded by EPSRC is to study the problem of automatically synthesizing a distributed system starting from a formal specification.
We study the complexity of and efficient procedures for automatic synthesis for various abstract models for specification and implementation. We focused on the synthesis of asynchronous automata from regular specifications (using heuristics for a famous construction by Zielonka), but we also studied the synthesis of asynchronous circuits from Signal Transition Graphs (STG) specifications.

Some current achievements are:

• a complexity study of the problem of checking the distributed implementability of a regular specification,
• an efficient polynomial-time test for the distributed implementability of an STG-specification, and
• a prototype implementation of heuristics for the synthesis of asynchronous automata that was able to automatically synthesize new solutions for classical problems.

A mutual exclusion situation appears when two or more processes are trying to access for `private' use a common resource. A distributed solution to the mutual exclusion problem should be a collection of programs, one for each process, such that their concurrent execution satisfies three properties:

• mutual exclusion (it is never the case that two processes have simultaneous access to the resource),
• absence of starvation (if a process requests access to the resource, the request is eventually granted), and
• deadlock freedom.

We can construct regular expressions to capture the desired properties. (For instance, for mutual exclusion, after one process enters the critical section, the other one cannot also enter it without the first to exit. Since we work with finite strings, we are forced to implement a weaker version of the absence of starvation property.)
The deterministic automaton accepting the desired behaviour is given below (ignore the colors for the moment). When we try to apply the synthesis approach we find a conflict between the blue and the red edges labeled by enter₁ and enter₂. The heuristics implemented in our synthesizer for asynchronous automata SynAsync, will solve the conflict by deleting one of the edges, in this case the red one (see below).

After deleting the red edge, the automaton satisfies the conditions of being transformable into an asynchronous automaton accepting the same language and this is done using a classic construction by Zielonka. The procedure is to unfold the automaton (in the same way a graph is unfolded into a tree) according to certain conditions. Since we are interested in `small' solutions, we have another heuristic that attempts to stop earlier then the normal procedure using an on-the-fly test whether we the current unfolding is isomorphic with the global transition system of an asynchronous automaton. The result produced by the heuristic is presented below.

The heuristics is successful in the sense that we obtained a solution with 20 global states as opposed to 4799 states that would have been generated by Zielonka's construction without any additions. The above automaton is isomorphic with the global transition system of an asynchronous automaton, which consists of a set of local automata communicating by rendez-vous. The final step is to produce the local components from the above global presentation. This is done by grouping the states in equivalence classes guided by the initial specified distribution of the action on the given processes. We do not depict the result of this procedure as this is not really legible. Nevertheless, we provide below its translation (derived by hand) into pseudo-code:

The synthesized mutual exclusion algorithm has two components synchronizing on two shared variables v₁ and v₂ ranging over the domains {0,1,2,3,4} and {0,1,2,3} respectively. (The labels associated with the commands suggest their type, for example r₁ means a request of the first process and x₂ means an exit from the critical section of the second process. The command corresponding to a label is executed atomically and the program pointers for the two components advance only as a result of a goto command.)

We end with a couple of remarks. We see that the algorithm is asymmetric, due to the removal of the red edge in the original specification. Also, it uses variables with larger domains than those appearing in the literature, and a human finds it difficult to understand why it is correct. Notice, however, that this is the case with most of computer generated outputs, whether they are HTML text, program code, or a computer generated proof of a formula in a logic.