Abstract Federated learning (FL) is a machine learning setting where clients keep the training data decentralized and collaboratively train a model either under the coordination of a central server (centralized FL) or in a peer-to-peer network (decentralized FL). Correct orchestration is one of the main challenges. In this paper, we formally verify the correctness of two generic FL algorithms, a centralized and a decentralized one, using the Communicating Sequential Processes (CSP) calculus and the Process Analysis Toolkit (PAT) model checker. The CSP models consist of CSP processes corresponding to generic FL algorithm instances. PAT automatically proves the correctness of the two generic FL algorithms by proving their deadlock freedom (safety property) and successful termination (reachability and liveness property). The CSP models are constructed as a faithful representation of the real Python code and are expressed directly in CSP# language that PAT uses. Then they are automatically checked top-down by PAT. The Python code follows a restricted actor-based programming model, and the construction of CSP# code from such Python code is performed systematically. The process is described in detail, ensuring that the models correspond to the actual code. It represents a basis for developing tools for automatic translation of certain classes of Python code to CSP models, expressed in CSP#.

Session subtyping is a cornerstone of refinement of communicating processes: A process implementing a session type (i.e., a communication protocol) T can be safely used whenever a process implementing one of its supertypes T ′ is expected, in any context, without introducing deadlocks nor other communication errors. As a consequence, whenever T ≤ T ′ holds, it is safe to replace an implementation of T ′ with an implementation of the subtype T , which may allow for more optimised communication patterns. We present the first formalisation of the precise subtyping relation for asynchronous multiparty sessions. We show that our subtyping relation is sound (i.e., guarantees safe process replacement, as outlined above) and also complete : Any extension of the relation is unsound. To achieve our results, we develop a novel session decomposition technique, from full session types (including internal/external choices) into single input/output session trees (without choices). We cover multiparty sessions with asynchronous interaction, where messages are transmitted via FIFO queues (as in the TCP/IP protocol), and prove that our subtyping is both operationally and denotationally precise. Our session decomposition technique expresses the subtyping relation as a composition of refinement relations between single input/output trees and provides a simple reasoning principle for asynchronous message optimisations.

Session subtyping is a cornerstone of refinement of communicating processes: a process implementing a session type (i.e., a communication protocol) T can be safely used whenever a process implementing one of its supertypes T ′ is expected, in any context, without introducing deadlocks nor other communication errors. As a consequence, whenever T T ′ holds, it is safe to replace an implementation of T ′ with an implementation of the subtype T , which may allow for more optimised communication patterns. We present the first formalisation of the precise subtyping relation for asynchronous multiparty sessions. We show that our subtyping relation is sound (i.e., guarantees safe process replacement, as outlined above) and also complete : any extension of the relation is unsound. To achieve our results, we develop a novel session decomposition technique, from full session types (including internal/external choices) into single input/output session trees (without choices). Previous work studies precise subtyping for binary sessions (with just two participants), or multiparty sessions (with any number of participants) and synchronous interaction. Here, we cover multiparty sessions with asynchronous interaction, where messages are transmitted via FIFO queues (as in the TCP/IP protocol), and prove that our subtyping is both operationally and denotationally precise. In the asynchronous multiparty setting, finding the precise subtyping relation is a highly complex task: this is because, under some conditions, participants can permute the order of their inputs and outputs, by sending some messages earlier or receiving some later, without causing errors; the precise subtyping relation must capture all such valid permutations — and consequently, its formalisation, reasoning and proofs become challenging. Our session decomposition technique overcomes this complexity, expressing the subtyping relation as a composition of refinement relations between single input/output trees, and providing a simple reasoning principle for asynchronous message optimisations.