In this project, we have developed a strategy for compiling distributed systems specified in IOA into Java programs running on a group of networked workstations. IOA is a formal language for describing distributed systems as I/O automata. The translation works node-by-node, translating IOA programs into Java classes that communicate using the Message Passing Interface (MPI). The resulting system runs without any global synchronization. We prove that, subject to certain restrictions on the program to be compiled, assumptions on the correctness of hand-coded datatype implementations, and basic assumptions about the behavior of the network, the compilation method preserves safety properties of the IOA program in the generated Java code. We model the generated Java code itself as a threaded, low-level I/O automaton and use a refinement mapping to show that the external behavior of the system is preserved by the translation. The IOA compiler has been implemented at MIT as part of the IOA toolkit. The toolkit supports algorithm design, development, testing, and formal verification using automated tools.

The IOA language provides notations for defining both primitive and composite I/O automata. We also describe, both formally and with examples, the constraints on these definitions, the composability requirements for the components of a composite automaton, and the transformation a definition of a composite automaton into a definition of an equivalent primitive automaton.

Research Support

This project is supported by DARPA Air Force contract number FA9550-04-C-0084, DARPA Award number F33615-01-C-1896, NSF Award numbers CCR-0326277 and CCR-0121277, NSF-Texas Engineering Experiment Station grant 64961-CS, DARPA/AFOSR MURI Award F49620-02-1-0325 and MURI AFOSR Award Number SA2796PO 1-0000243658.

References

[1] Joshua A. Tauber. Verifiable Compilation of I/O Automata without Global Synchronization. PhD Thesis, Department of Electrical Engineering and Computer Science, Massachusetts Institute of Technology, Cambridge, MA 02139, February, 2005.

[2] Joshua A. Tauber and Nancy A. Lynch and Michael J. Tsai. Compiling IOA without Global Synchronization. Proceedings of the 3rd IEEE International Symposium on Network Computing and Applications (IEEE NCA04), Cambridge, MA, August 2004.

[3] Joshua A. Tauber, Dilsun K. Kaynar, Nancy A. Lynch. Correctness of a Compiler for Distributed Algorithms. Submitted for publication, 2005.