Hernán Melgratti

Florian Furbach, Lucas Clorius, Roland Kuhn et al.

Swarm protocols are a recently introduced formalism for specifying, implementing, and verifying peer-to-peer systems called swarms. A swarm consists of distributed agents called machines that communicate by asynchronous event propagation. Following a local-first model, each machine can progress without requiring continuous connectivity to other machines. Existing models of swarms are not compositional, making the modular development of large and complex swarm applications as well as the reuse of code difficult. We address these issues by presenting novel theory and techniques for the compositional specification, verification, and implementation of swarms. These results enable the correct compositional reuse of pre-existing swarm protocols and machine implementations. We implement these contributions in a companion software artifact which enables the automatic integration of independently designed and verified swarm components.

Hernán Melgratti, Claudio Antares Mezzina, G. Michele Pinna

Event structures have emerged as a foundational model for concurrent computation, explaining computational processes by outlining the events and the relationships that dictate their execution. They play a pivotal role in the study of key aspects of concurrent computation models, such as causality and independence, and have found applications across a broad range of languages and models, spanning realms like persistence, probabilities, and quantum computing. Recently, event structures have been extended to address reversibility, where computational processes can undo previous computations. In this context, reversible event structures provide abstract representations of processes capable of both forward and backward steps in a computation. Since their introduction, event structures have played a crucial role in bridging operational models, traditionally exemplified by Petri nets and process calculi, with denotational ones, i.e., algebraic domains. In this context, we revisit the standard connection between Petri nets and event structures under the lenses of reversibility. Specifically, we introduce a subset of contextual Petri nets, dubbed reversible causal nets, that precisely correspond to reversible prime event structures. The distinctive feature of reversible causal nets lies in deriving causality from inhibitor arcs, departing from the conventional dependence on the overlap between the post and preset of transitions. In this way, we are able to operationally explain the full model of reversible prime event structures.

Laura Bocchi, Hernan Melgratti, Emilio Tuosto

Choreographies specify multiparty interactions via message passing. A realisation of a choreography is a composition of independent processes that behave as specified by the choreography. Existing relations of correctness/completeness between choreographies and realisations are based on models where choices are non-deterministic. Resolving non-deterministic choices into deterministic choices (e.g., conditional statements) is necessary to correctly characterise the relationship between choreographies and their implementations with concrete programming languages. We introduce a notion of realisability for choreographies - called whole-spectrum implementation - where choices are still non-deterministic in choreographies, but are deterministic in their implementations. Our notion of whole spectrum implementation rules out deterministic implementations of roles that, no matter which context they are placed in, will never follow one of the branches of a non-deterministic choice. We give a type discipline for checking whole-spectrum implementations. As a case study, we analyse the POP protocol under the lens of whole-spectrum implementation.