[an error occurred while processing this directive]
Bild mit Unilogo
homeicon university sucheicon search siteicon sitemap kontakticon contact impressicon legal notice
unilogo University of Stuttgart 
Institute of Formal Methods in Computer Science

Software Reliability and Security Group

[an error occurred while processing this directive] englishicon
 


 

asynchronous bees
[yet another distributed system...]

Automatic Synthesis of Distributed Systems
Members Professor Javier Esparza
PhD student Claus Schröter
PhD student Alin Stefanescu
Funding EPSRC Grant R64322/01 (running 1.10.2001-30.09.2004)
[Final EPSRC report on the project]
Research 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.
Details can be found in the Publications and Implementations sections below.
Example 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
req1 , enter1 , exit1 , req2 , enter2 , exit2
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 req1 and req2 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 enter1 and enter2. 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).

mutex initial

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.

mutex unfolded

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:

synthesized mutex algorithm

The synthesized mutual exclusion algorithm has two components synchronizing on two shared variables v1 and v2 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 r1 means a request of the first process and x2 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.

Implementations SynAsync - a synthesizer for asynchronous automata
Logic implementations complementing SynAsync
Implementation of the consistency test for STGs
Publications

To appear

Javier Esparza. A polynomial-time algorithm for checking consistency of free-choice signal transition graphs. Fundamenta Informaticae, To appear.
GZipped PostScript (150 kB)
Info
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.
GZipped PostScript (119 kB)
PDF (258 kB)
Info
Tech report version

2004

Saravanan Mahadevan. Implementation of a consistency test for free-choice signal transition graphs. Master's thesis, INFOTECH, University of Stuttgart, 2004.
PDF (482 kB)
Info
See www.fmi.uni-stuttgart.de ...
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.
GZipped PostScript (473 kB)
Info
Keijo Heljanko and Alin Stefanescu. Complexity results for checking distributed implementability. Technical Report 05/2004, Universität Stuttgart, 2004.
PDF (324 kB)
Info
Slides 

2003

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.
PDF (242 kB)
Info
Full versionSlidesImplementation
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.
GZipped PostScript (233 kB)
Info

2002

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.
GZipped PostScript (56 kB)
Info
See www.fmi.uni-stuttgart.de ...
Slides