The design of correct distributed systems is a difficult and error-prone task.
This is due to the multitude of possible interactions between the concurrent
components of the system. The synthesis approach aims at directly
constructing a correct implementation from a given specification,
if possible.

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.

We show by means of an example an application of the synthesis of
asynchronous automata to the automatic construction of a correct implementation
for a classic distributed problem, namely mutual exclusion.
More details can be found the Concur'03 paper in the
Publications section below.

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.

Let us consider the problem for two processes. We choose the actions to be

with the intended meanings: request access to, enter and exit the critical
section giving access to the resource.
The indices 1 and 2 specify the process that executes the action.
We also give a distribution of the actions over a set of processors
modeling the natural requirement that the two request actions
req_{1} and
req_{2} are `independent'
(i.e., they can be executed in parallel in the distributed implementation).

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_{1}
and enter_{2}.
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_{1} and
v_{2} 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_{1}
means a request of the first process and
x_{2}
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.

Keijo Heljanko and Alin Stefanescu. Complexity results for checking distributed implementability. In Proceedings of the 5th International Conference on Application of Concurrency to System Design (ACSD 2005), To appear.

Saravanan Mahadevan. Implementation of a consistency test for free-choice signal transition graphs. Master's thesis, INFOTECH, University of Stuttgart, 2004.

Claus Schröter and Victor Khomenko. Parallel LTL-X model checking of high-level Petri nets based on unfoldings. In Proceedings of the 16th International Conference on Computer Aided Verification (CAV'04), volume 3114 of Lecture Notes in Computer Science, pages 109–121. Springer, 2004.

Alin Stefanescu, Javier Esparza, and Anca Muscholl. Synthesis of distributed algorithms using asynchronous automata. In R. Amadio and D. Lugiez, editors, Proceedings of the 14th International Conference on Concurrency Theory (CONCUR'03), volume 2761, pages 27–41. Springer, September 2003.

Javier Esparza. A polynomial-time algorithm for checking consistency of free-choice signal transition graphs. In Proc. of the 3rd Int. Conf. on Application of Concurrency to System Design (ACSD 2003), pages 61–70. IEEE Computer Society, 2003.

Alin Stefanescu. Automatic synthesis of distributed systems. In Proceedings of 17th IEEE International Conference on Automated Software Engineering, page 315. IEEE Computer Society, 2002. Position paper.