The mutual exclusion problem was formally defined by Edsger Dijkstra in 1965.
Since then many solutions were published, one of them is a simple solution by Gary Peterson in 1981.
Information on the problem, known solutions, and related problems can be found in many books and web sites about distributed algorithms or operating systems.
In 1999, while studying a course in distributed computing given by Gadi Taubenfeld, I wondered if there is a solution that is shorter than Peterson's solution.
Since it is hard to find a solution, and even harder to prove that no simpler solution exists, I tried to use the help of my computer.
I wanted to write a program that scans all possible algorithms and checks each one if it a good solution for the mutual exclusion problem.
This led to the development of the algorithm discovery program, and to the solutions it has found.
In 2003, a paper describing the technique and algorithms found by the system
Gadi Taubenfeld and myself
was accepted to the
17th International Symposium on Distributed Computing (DISC 2003)
We present a methodology for automatic discovery of synchronization algorithms. We built a tool and used it to automatically discover hundreds of new algorithms for the well-known problem of mutual exclusion. The methodology is rather simple and the fact that it is computationally feasible is surprising. Our brute force approach may require (even for very short algorithms) the mechanical verification of hundreds of millions of incorrect algorithms before a correct algorithm is found. Although many new interesting algorithms have been found, we think the main contribution of this work is in demonstrating that the approach suggested for automatic discovery of (correct) synchronization algorithms is feasible.
1 a[me] = 1
2 b[me] = me
3 a = 0
4 a[me] = a
5 while b[next] != a
7 critical section
8 b[me] = next
Frequently asked questions
What language is the software written in?
The software has 2 main components:
The core and the user-interface.
The core is the main component, which does the algorithm generation and verification.
The core is written in C++. The user-interface is written in Java.
Can this run on Windows? Unix? Mac?
The software was developed and run on Windows.
It was written so that it should be able to compile and run on any platform,
but this has never been actually tested before, mainly due to the lack of other platforms.
Can I get the program and run it myself?
Yes, in the download page.
Can I get the source code?
Yes, in the download page.
Please send me a note if you use this program, of if
you have any questions agout it.
Can this technique solve other problems?
In theory, this technique can be applied to any problem.
In practice, the main question is how much time will it take to perform the same technique on another problem.
Problems that best fit this technique are problems that have short solutions (few lines of code, few variables), and that can be verified mechanically.
Can this technique solve single-process problems
Yes. Applying the technique to single process algorithms would allow longer algorithms (more lines of code, more variables)
to be tested in reasonable time.
What is the difference between algorithm discovery and genetic algorithm generation
Algorithms can be generated using genetic algorithms techniques. Genetic algorithms do not test all options, so they can not
be used to "prove" that no solution exists under some limitations.
Genetic algorithms work well when there is measurable gradual improvement in the result. or in other words when there is a way
to tell out of 2 algorithms that are not solutions, which is better.
This may be true for some problems, while for some other problems it is hard to find a measure of how far an algorithm is from becoming a solution.
What is the difference between algorithm discovery and algorithm synthesis
Synthesis deals with building a solution from requirements. The generated solution may not be optimized (there may be oother solutions that
are shorter, require less memory, or run faster).
When synthesis can not find a solution, it does not necessarily mean that no such solution exists.
Why use 2 different languages for generation and verification
The verification language is low level, and it's main emphasis is to clearly define states and transitions.
The generation language is designed to be readable by humans, to make the produced algorithm easy to understand.
In a sense, the distinction is the same as between a high-level programming language used by humans, and the assembly language
used by the hardware.