FTSyn:
A Framework for the Synthesis of Fault-Tolerant Distributed Programs
Problem:
·
Can we write programs that write programs?
· Perhaps, a simpler problem:
Can
we write programs that take a given program p and a desired concern, and then
generate a version of p that supports the new concern in addition to its
existing behaviors?
My research work is focused on solving the above problems. Thus far, I have been involved in the development of algorithms that add fault-tolerance properties to distributed programs. Based on these synthesis algorithms, I have developed an extensible framework for the synthesis of fault-tolerant distributed programs from their fault-intolerant versions. The framework is extensible in the sense that developers of fault-tolerance can easily integrate their own heuristics and algorithms into the framework.
Q:
Hmm! Wait a minute! Do you mean you can take a C++ or Java program and generate
its fault-tolerant version?
A:
Yes, and No.
No.
Right now, by program, we mean an abstract structure (i.e., synchronization
skeleton) of a program. The abstract program is not as detailed as a C++ or Java
program. In our framework, we represent the abstract programs by Dijkstra’s
guarded commands.
Yes.
There are several approaches for taking a program written in common programming
languages and extract its abstract structure in guarded commands. Also, there
are approaches for transforming a guarded command program to a C++ or Java
program. Thus, in the future, we will integrate these transformational approaches into
our framework.
Q:
What are the real-world applications that you have synthesized so far?
A: At this time, our synthesis framework is in the early stages of its lifetime, and as a result, we have been able to synthesize programs with small state space (e.g., 1.3 million states). For example, we have synthesized an agreement program with a general process and 4 non-general processes that are subject to Byzantine and fail-stop faults simultaneously. We have also synthesized a token ring program with 5 processes that tolerates the corruption of all processes. A fault-tolerant alternating bit protocol and triple modular redundancy are among programs that we have synthesized using our framework.
As an illustration of the applicability of our approach for the synthesis of real-world applications, we have automatically synthesized the controller of an altitude switch that has already been synthesized by the SCR method.
All in all,
these examples show that our framework has the potential to handle different
types and natures of faults, and also, is able to synthesize programs that are
simultaneously subject to more than one types of faults.
Q: So, where can I find a copy of your framework?
A: Drop me a line (aebnenas at mtu dot edu) and I will send you the Java source code of FTSyn.
Q: Do you have any document regarding the design and the user interface of the framework?