Safe Socket Lifecycles in Completion-based Asynchronous I/O Systems : A Communicating Finite-State Machine Approach to Socket Lifetime Safety

Sammanfattning

High-performance networked systems are increasingly reliant on completion-based asynchronous I/O to achieve better networking performance when handling a large number of concurrent connections. While these systems deliver performance benefits, they also introduce significant complexity in reasoning about resource life-times. Conventional testing and debugging techniques are inadequate to verify non-deterministic behavior inherent in asynchronous systems. In this thesis, we study formal modeling and verification of socket life-cycles incompletion-based asynchronous I/O systems. We present a refined Communicating Finite State Machine model that captures socket states and transitions that utilize reference counting to avoid illegal behavior occurring. Using the SPIN model checker and the Promela modeling language, we verify that the refined model preserves safety properties across all possible global configurations and compare it to a naive design as well. Our results confirm that integrating explicit life-time management into asynchronous CFSM models lead to stronger safety guarantees. We also show that deterministic control over socket state transitions can be achieved in inherently non-deterministic completion-based systems by enforcing state-dependent transition rules through a finite-state model. The findings underscore the importance of formal reasoning in the design of asynchronous I/O systems, where both performance and safety must be addressed.