This thesis delves into the intricate realm of concurrent and distributed systems, a vital aspect of modern technology. It focuses on message-passing concurrency, which plays a pivotal role in achieving horizontal scalability, a key requirement in today’s technological landscape. The study is primarily conducted within the Rust programming language, renowned for its emphasis on memory safety and efficiency. The motivation behind this research stems from the critical need to ensure communication safety within concurrent systems, particularly in Rust environments.
To contextualise the research, the thesis provides a historical overview of Session Types (ST) theories, tracing their evolution from Binary Session Types (BST) to the more advanced Affine Asynchronous Timed Multiparty Session Types (ATMP). A practical Travel agency scenario is used as a guiding example to demonstrate the incremental advancements in this field. The core contributions of this thesis lie in the development and implementation of the MultiCrusty framework in Rust. MultiCrusty is designed to support Affine Multiparty Session Types (AMPST) and ATMP, addressing challenges such as constructing multiparty channels through binary channels, ensuring deadlock-freedom, liveness, and enforcing affineness. One significant contribution is the introduction of MeshedChannels within MultiCrusty, a structure that encapsulates binary channels in a specific order to guarantee communication safety. This framework, MultiCrustyA, facilitates essential operations like message sending and receiving, making choices, handling recursion, and closing connections over synchronous communications.
Methodologies such as Top-Down and Bottom-Up are employed to ensure the framework’s performance superiority compared to other related tools, especially in scenarios involving a high number of participants and complex interactions. Additionally, MultiCrustyA is extended to incorporate Affine Asynchronous Timed Multiparty Session Types in a version named MultiCrustyT , further enhancing its capabilities in handling asynchronous communications and time constraints, and demonstrating minimal overhead compared to previous the implementation.