Compiling IOA without global synchronization

This work presents a strategy for compiling distributed systems specified in IOA, a formal language for describing such systems as I/O automata, into Java programs running on a group of networked workstations. The translation works node-by-node, translating IOA programs into Java classes that communicate using the message passing interface. 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 is part of the IOA toolkit which supports algorithm design, development, testing, and formal verification using automated tools.