Dynamic Composition and Concurrency in I/O Automata: The Ioa++ Framework
摘要
This paper presents ioa++, a C++ framework that extends the formal I/O automata model to support dynamic composition and concurrency in practical distributed systems. I/O automata provide a rigorous basis for modeling reactive systems with well-defined interfaces and compositional semantics. The ioa++ framework builds on this foundation with runtime support for dynamic system reconfiguration, concurrency-aware scheduling, and non-blocking I/O via POSIX file descriptors. We demonstrate the utility of ioa++ through a layered implementation of a TCP-based leader election protocol using the asynchronous LCR algorithm. Empirical results show that ioa++ achieves near-ideal speed-up (up to \(1.95\times \) with two threads) when sufficient independent actions exist, and incurs minimal overhead (average dispatch time of 4316ns in single-threaded and 6067ns in multi-threaded settings). The framework is open-source, supports simulation and real deployments, and encourages direct reasoning from code due to its close alignment with formal models. Our work bridges the gap between theoretical models and real-world systems, offering a practical tool for building modular and concurrent distributed software.