Mixed Choice in Asynchronous Multiparty Session Types

Key Points

• The central aim is to develop a framework that enables asynchronous mixed choice in multiparty session types while maintaining consistency among distributed participants.
• Developed a core construct for asynchronous mixed choice, allowing transient inconsistencies.
• Proved the correctness of the framework through a progress property and operational correspondence.
• Implemented a toolchain to specify and validate asynchronous multiparty session types.
• Reimplemented aspects of the RabbitMQ AMQP client using the toolchain and the Erlang programming language.
• The framework ensures that all participants eventually achieve a mutually consistent state despite transient inconsistencies.
• The toolchain successfully specifies and validates async MST protocols featuring mixed choice.
• Demonstrated the practicality of the framework through the reimplementation of parts of the amqp_client.