arXiv CSopen access

Compositional Design, Implementation, and Verification of Swarms (Technical Report)

Unknown · 2026 · arxiv_cs

arXiv CS · Papers · License: Open Access · 2026

cloud distributedcomputing parallelcomputing

distributed computing, parallel computing, cloud

Compositional Design, Implementation, and Verification of Swarms (Technical Report) Florian Furbach # University of Surrey, UK and Technical University of Denmark, Denmark

Lucas Clorius # Technical University of Denmark, Denmark Roland Kuhn # Ñ Actyx AG, Germany

Hernán Melgratti # Ñ

arXiv:2604.16097v1 [cs.DC] 17 Apr 2026

University of Buenos Aires & Conicet, Argentina

Alceste Scalas # Ñ Technical University of Denmark, Denmark

Emilio Tuosto # Ñ Gran Sasso Science Institute, Italy

Abstract 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. 2012 ACM Subject Classification Theory of computation → Distributed computing models; Software and its engineering → Distributed programming languages; Software and its engineering → Formal software verification Keywords and phrases Swarms, Swarm Protocols, Concurrency, Distributed Coordination, Local-first Software, Behavioural Types, Publish-Subscribe, Asynchronous Communication Related Version ECOOP’26 paper: https://doi.org/10.4230/LIPIcs.ECOOP.2026.21 Funding Research partially supported by the Horizon Europe grant 101093006 (TaRDIS) and by the Italian Ministero dell’Università e della Ricerca “Dipartimenti di eccellenza” initiative. Acknowledgements This work was inspired by the discussions at the Dagstuhl Seminar 24051 “Next Generation Protocols for Heterogeneous Systems” [9]. We thank the organisers of the meeting and Schloss Dagstuhl – Leibniz Center for Informatics for making this work possible.

Introduction

Modern distributed systems face significant challenges in ensuring reliability, availability, and scalability. Recent work on swarm protocols [41, 40] addresses these challenges by formally specifying the behavior of interacting agents capable of independent yet coordinated progress. In this approach, a swarm is modelled as an ensemble of distributed interacting agents, called machines. Each machine can coordinate with others by emitting events (i.e., messages)

Compositional Design, Implementation, and Verification of Swarms (Technical Report) q⟩

rtRe

T⟨pa

FL⟨p os⟩

1 T⟨partOK⟩

2 D⟨clo singT ime⟩

Figure 1 The swarm protocol Warehouse, involving the roles T (transport), FL (forklift), and D (door). closingTime! partReq?

closingTime? 3

1 partOK?

Figure 2 Machine M D obtained by projecting the swarm protocol Warehouse (Fig. 1) onto role D (door).

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17

// Machine implementation using the Actyx toolkit const door = Warehouse.makeMachine('D') // States const s0 = door.designEmpty('s0') .command('close', [closingTime], () => { ... return [closingTime.make({ time: new Date() })] }) .finish() const s1 = door.designEmpty('s1').finish() const s3 = door.designEmpty('s3').finish() // Accept events and change states s0.react([partReq], s1, () => { ...; return s1.make() }) s0.react([closingTime], s3, () => { ...; return s3.make() }) s1.react([partOK], s0, () => { ...; return s0.make() })

Figure 3 Implementation of a Door Machine in Actyx.

that propagate asynchronously through the swarm, and by subscribing to (some of) the events emitted by other machines. Essentially, swarms are type-based publish/subscribe systems with distributed asynchronous delivery [25]. Unlike most publish/subscribe systems that aim for causal-consistent delivery (i.e., machines share a consistent view of the global system state), swarms are designed to operate over inconsistent views, often corresponding to inconsistent cuts of the global state [7]. This design choice prioritises availability over consistency [29], following a local-first paradigm [39, 38]: each machine can make progress independently, without requiring up-to-date global information or a continuously available network connection. Such an approach enables decentralized decision-making, reducing reliance on central coordination and improving robustness. However, it also introduces potential inconsistencies: machines may take decisions based on stale or divergent state, which may later require reconciliation [44]. The approach in [41, 40] advocates the usage of behavioral types [35, 27, 6] to ensure that a swarm correctly reconciles inconsistencies. Roughly, the intended global behaviour of the swarm (i.e., the expected interactions among machines) is formalised as a swarm protocol: a specification that provides a bird’s-eye view of how machines playing different roles should interact at runtime, without causing irreconcilable inconsistencies in the overall state of the swarm. A swarm protocol G can then be projected onto the different roles to obtain the corresponding machine specifications. When an ensemble of machines, each running according to a projection of G, is deployed to form a swarm S, then (under well-formedness conditions discussed later) the swarm S is guaranteed to execute in accordance with G. A Use Case of Swarm Protocols and Swarms. To illustrate the theory and practice of swarm protocols, we present a simplified use case in factory automation (“Industry 4.0”).1 The intended global behaviour of the swarm is specified by the Warehouse protocol illustrated in Fig. 1. A machine playing the role of a transport vehicle T requests a part by emitting an event of type partReq. A machine playing the forklift role FL responds by delivering the requested part to the specified pick-up position pos. A machine playing role T then picks up the part and emits an event of type partOK. Between consecutive requests, the door D may close, emitting an event of type closingTime.

We borrow the use case of an automatic warehouse operated by a swarm which has been implemented in the open source Actyx toolkit [4].

F. Furbach, L. Clorius, R. Kuhn, H. Melgratti, A. Scalas, and E. Tuosto

T⟨partReq⟩ 0

T⟨partOK⟩ 1

A⟨car⟩ 2

Figure 4 A Factory protocol that can interface with the Warehouse (Fig. 1) using the role T.

The swarm protocol Warehouse is then projected onto its roles T, FL, and D, yielding a machine specification for each role. For example, the projection of Warehouse onto the role D (door) results in the state machine shown in Fig. 2. For each event type, say closingTime, a transition labelled closingTime! indicates that the machine emits an event of type closingTime, while a transition labelled closingTime? indicates that the machine accepts an event of that type. During the execution of a swarm, when a machine emits an event, the event is appended to the emitting machine’s local event log; then, the event asynchronously propagates to the logs of other machines. A machine changes its state only when it inspects its log and accepts an event from it; an event emission does not directly cause a state change – rather, after an event is emitted, its acceptance triggers a state transition. For example, in Fig. 2, state 0 of machine M D has a self-loop emitting an event of type closingTime, as well as a transition that accepts the same event type. The non-atomic nature of event emission (_!) and acceptance (_?) implies that events from different machines may interleave: i.e., after a machine emits an event, and before that event is accepted, other events from other machines may be emitted, propagated, and accepted. In practice, machines can be implemented using the open source Actyx toolkit [4], which provides a TypeScript API for defining swarm protocols, implementing machines, and deploying swarms. Fig. 3 shows the TypeScript implementation of the state machine M D in Fig. 2: the machine is called door and plays the role 'D' (line 2). Lines 5–12 define the states s0, s1, s3 that map to states 0, 1, and 3 in M D , respectively, as follows. Line 5 introduces the state named s0 while lines 6–9 define the transition that emits an event of type closingTime, which is declared using the command method. The elided code on line 7 implements the business logic associated with the event emission, while line 8 specifies the information attached to the emitted event (in this case, a timestamp). Lines 11 and 12 introduce the states s1 and s3. Finally, lines 15–17 define the accepting transitions. In particular, line 16 specifies that when the machine is in state s0 and receives an event of type closingTime, it accepts the event and transitions to state s3. The omitted code implements the corresponding application-specific business logic. Once the code is written, the Actyx toolkit enables static verification to check that a machine’s implementation adheres to an intended behaviour. Specifically, it provides APIs for defining swarm protocols, tools for projecting protocols onto roles, a type extraction tool that reconstructs machines from TypeScript code, and a type-checking tool to check whether the projected and extracted machines are consistent [4]. For instance, the Actyx toolkit can verify that the code in Fig. 3 conforms to the machine in Fig. 2, that is projected from Fig. 1. Going back to the theory, the use of swarm protocols ensures a key correctness property: if a swarm S consists of machines projected onto the roles of the same swarm protocol G (such as Warehouse in Fig. 1), then the swarm S enjoys eventual fidelity to G [41]. Intuitively, this means that, once every event propagates to every machine in the swarm S, all machines will reach a consensus on which events reflect a transition specified in G, and how they conform to an execution of G. This property also holds if, to increase reliability, the swarm includes multiple replicas of machines projected from the same role (e.g., in the example above, multiple machines may play the forklift role FL). The formulation and proof of eventual fidelity are quite challenging, as they must take into account the shape of G, the swarm event propagation mechanics, and the subscriptions of each machine (i.e., which events it sees).

Compositional Design, Implementation, and Verification of Swarms (Technical Report)

Our Objective: Compositional Design and Verification of Swarm Protocols. The previously-published theory [41] and implementation [4, 40] of swarm protocols only support monolithic swarm design and implementation: i.e., they do not support developing a large and complex swarm by combining modular, reusable swarm protocols and swarms that are designed, implemented, and verified independently. Consider the (simplified) protocol Factory shown in Fig. 4 where a transport (T) requests and picks a part, which is then utilised by an assembly robot (A) to build a car (emitting an event of type car). Notably, the Factory swarm protocol only specifies T’s events partReq and partOK, and does not specify how the part is obtained (i.e., what happens “in between” T’s events); such a detail could be part of another swarm protocol — such as Warehouse (Fig. 1), where T gets the part from a forklift FL. Intuitively, the Factory protocol is a high-level view of a production process, whereas the composition of Factory and Warehouse describes the complete process where both protocols run concurrently with the transport role acting as an interface between them. Now, suppose that the Factory protocol changes into an updated swarm protocol Factory′ (where, e.g., the assembly robot A coordinates with other factory devices): it would be desirable to compose Factory′ and Warehouse (unchanged), obtaining a complete, updated production process protocol. Correspondingly, the machines projected from the Warehouse swarm protocol should be reusable: for example, it should be possible to deploy the implementation of the door role D from Warehouse (shown in Fig. 3) into any swarm that is “compatible” with Warehouse, without requiring manual changes depending on whether other machines implement the protocol Factory or Factory′ . Unfortunately, this scenario cannot be addressed with swarm protocol results in literature. There is no method to design Factory and Warehouse as separate protocols and compose them at a later stage: a whole FactoryWithWarehouse swarm protocol must be designed at once, and then used to project swarm machines. Moreover, if a detail of the “factory” part of the FactoryWithWarehouse swarm protocol changes and leads to an updated protocol FactoryWithWarehouse′ , the change may also impact the machines of the “warehouse” part — e.g., the machine obtained by projecting FactoryWithWarehouse′ onto role D may differ from the projection of FactoryWithWarehouse onto D in non-trivial ways, meaning that the implementation of the Door machine in Fig. 3 may not be reusable and must be manually revised. As a consequence, developing new swarms, or adapting existing swarms to new requirements, is a challenging and time-consuming endeavour. It would be highly desirable to have methods and tools to assemble libraries of swarm protocols and corresponding ready-to-use swarm machines that can be safely and easily composed, reused, and deployed to tackle new scenarios. In this work, we introduce such methods and tools. Contributions and Outline of the Paper. We present a novel theory and implementation of compositional swarm design, development, and verification. Our approach is based on interfacing roles: given n swarm protocols G1 , . . . , Gn with suitable roles acting as interfaces, we define the composition G1 || . . . || Gn . Also, given n swarms S 1 , . . . , S n whose machines are projected from G1 , . . . , Gn , we introduce a method to compose S 1 , . . . , S n . This allows for creating large and complex swarms by reusing and composing machines that were previously projected from the individual simpler swarm protocols G1 , . . . , Gn . The details behind this broad intuition are quite subtle, due to the highly dynamic nature of swarm protocols, swarms, and their properties – and to achieve these results, we develop novel swarm-specific notions of well-formedness and compositionality. In § 2 we provide an overview of our approach. § 3 presents our new swarm protocol

F. Furbach, L. Clorius, R. Kuhn, H. Melgratti, A. Scalas, and E. Tuosto

composition and well-formedness, with a method for computing well-formed subscriptions. § 4 defines a projection of swarm protocols onto machines, a branch-tracking semantics for such machines, and proves their eventual fidelity to well-formed swarm protocols. § 5 presents our results on correctly composing swarms which realise different swarm protocols. In § 6 we discuss the companion software artifact of this paper [26]: an extension of the open source Actyx toolkit that implements the theory of §§ 3–5 to allow the practical compositional development of swarms; we compare experimental results on different strategies for computing the subscriptions of composed swarms. We discuss related work in § 7 and conclude in § 8.

Overview and Main Results

Before presenting our development, in § 2.1 we give an intuitive account of the swarm framework in [41]. Then, in § 2.2 we outline our approach and summarise our main results.

2.1

Swarms and Swarm Protocols

As mentioned in § 1, a swarm is an ensemble of machines that can make progress independently without requiring up-to-date global information or an always-active network connection. Each machine M maintains a local log l M of events received from the surrounding swarm. These events are unique and have a globally agreed-upon total order [15] (usually defined in a coordination-free manner using timestamps, which we leave implicit) and are used by M to update its state when newly arriving events alter l M . A swarm protocol G provides a global view of the intended interactions that should take place during the swarm execution. To ensure correct interaction at run-time, each swarm machine should play a specific role R in G. To this end, a machine can be obtained by projecting G onto R; the projection operation is based on the subscription of role R, i.e., which event types a machine playing role R observes while running. E.g., the machine in Fig. 2 is obtained by projecting the Warehouse protocol in Fig. 1 onto role D using a subscription that associates D with all the event types of the protocol except pos (emitted by FL). The event emission closingTime! in state 0 adds an event of type closingTime to the machine’s local log and leaves the machine in state 0, whereas accepting an event of type closingTime from the log, denoted as closingTime?, transitions the machine to state 3. For an intuitive presentation of the execution of a swarm realising the Warehouse protocol, let us consider a possible run of a swarm of three machines —M T , M FL , and M D — respectively implementing roles T, FL, and D: 1. Machine M T performs a request and emits the event partReq1 (of type partReq), which it adds to its local log l T . 2. This event is asynchronously propagated to the local log l FL = partReq1 of M FL , thus making M FL reach state 1 from where it delivers the part and emits posX (of type pos). 3. The event posX reaches M T , which picks up the part and emits the event partOK1 (of type partOK). 4. These events propagate to machine M D , who adds them to its local log l D = partReq1 · posX · partOK1 . It then closes the door emitting the event 8PM (of type closingTime). Remarkably, when deploying a swarm, multiple machines may assume the same role in G, in a way that generalises replicated state machines [47]. In our Warehouse protocol for instance, other machines may play role FL in addition to M FL . Such a machine may concurrently deliver another part by emitting an event, say posY ; eventually, all events propagate to all machines, and all machines reach the same log. For instance, the log

Compositional Design, Implementation, and Verification of Swarms (Technical Report)

Warehouse Interfacing roles Def. 1

Def. 2

Factory 7 6

Algorithm 1 Thm. 16 & § 6

Composition Defs. 34 & 36 8 Warehouse || Factory Th m . 3 8

S′

Well-formedness Branch-tracking subscri ption § 4.3 Def. 12 3 Eventual fidelity 5 Def. 31 Thm. 32

Figure 5 A synoptic view of our approach to swarm composition, with the main constructions and their dependencies.

T⟨partReq⟩ 0 || 0

FL⟨pos⟩ 1 || 1

D⟨c

2 || 1

0 || 3

osin gTim e⟩

3 || 2

e⟩

D⟨cl

osin

gTim

e⟩

0 || 2

3 || 3 D⟨cl

los

ing Tim

⟩

r A⟨ca

T⟨partOK⟩

A⟨ca

r⟩

3 || 0

Figure 6 The composition Warehouse || Factory of Warehouse and Factory.

partReq1 · posX · posY · partOK1 · 8PM · represents a case where event posY is emitted after event posX ; therefore posY will be ignored by all machines. Following [41], the key correctness property of a swarm S with respect to a protocol G is eventual fidelity. Intuitively, eventual fidelity means that once the events emitted by the machines in S propagate to the whole swarm, all machines in S reach a consensus corresponding to a valid execution of G. Notably, [41] proves that eventual fidelity is guaranteed by construction whenever G is well-formed and the machines in S are correct projections of the roles in G; in other words, the swarm S does not need any runtime orchestration to be eventually faithful to G.

2.2

Achieving Compositional Swarms

Unfortunately, as discussed in § 1, the theory and results in [41] do not feature any form of compositionality and do not support modular swarm development. In this work, our key contribution is a new approach enabling the compositional design, implementation and verification of swarms. This is a challenging endeavour that we tackle by introducing a brand new notion of well-formedness that (i) ensures eventual fidelity of a swarm to a protocol, and (ii) is preserved by composition (unlike the well-formedness in [41]). In Fig. 5 we provide an overview of our approach showing how its main constructions are related and how they interact; the overview leverages the Warehouse and Factory composition use cases in § 1. The pivotal notion upon which we develop our theory is interfacing roles, i.e., roles shared by protocols which “agree” on common event types. For instance, the transport role T is an interface between the Warehouse and Factory. Our composition operator _ || _ ( 1 in Fig. 5) essentially acts as a synchronised product of the behaviour of the protocols involved in the composition. For instance, consider the composition Warehouse || Factory of Warehouse and Factory shown in Fig. 6. All actions performed by the interfacing role T (i.e., T⟨partReq⟩ and T⟨partOK⟩) are synchronised between Warehouse and Factory while actions of non-interfacing roles (i.e., A⟨car⟩ and D⟨closingTime⟩) are interleaved. Note that (i) the interleaving of A⟨car⟩ and D⟨closingTime⟩ shows that they are concurrent and (ii) the loop in Warehouse disappears from the composed protocol since Factory requires the delivery of just one part.

F. Furbach, L. Clorius, R. Kuhn, H. Melgratti, A. Scalas, and E. Tuosto

We develop a novel compositional notion of well-formedness for swarm protocols ( 2 ). This notion provides a sufficient condition for statically verifying that a swarm is eventually faithful to a protocol ( 3 ). As part of this development, we refine the semantics of machines w.r.t. [41] by introducing a new branch-tracking mechanism. Specifically, in our new machine semantics, each emitted event contains a pointer to the most recent branching, joining, or looping event (Def. 6) that precedes it. This pointer establishes an event causality chain and allows machines to ignore events which are invalid because they are not caused by the expected branching/joining/looping event (this is illustrated in Example 29). Such a causality chain was not present nor needed in [41] – but it is necessary for swarms to work correctly with our compositional well-formedness, which removes restrictions that were assumed in [41]. Therefore, the new branch-tracking semantics allows us generalise the correctness results in [41]; moreover, it allows us to reduce the size of subscriptions needed to correctly track protocol choices ( 4 ), thus increasing the efficiency of the swarm. Crucially, well-formedness and branch tracking ensure that a swarm of machines projected from a protocol G is eventually faithful to G ( 5 ). Another contribution of this paper is the definition and implementation of Algorithm 1 ( 6 ) to compute well-formed subscriptions for the composition of a set of input swarm protocols; crucially, Algorithm 1 computes the subscriptions based on the individual structures of the input protocols (e.g., Warehouse and Factory) without computing their composition (e.g., Warehouse || Factory) as it can be exponentially larger than the input protocols ( 7 ). Finally, we develop a composition and adaptation of machines in a swarm, in such a way that the composed swarm ( 8 ) is eventually faithful to the corresponding composition of swarm protocols.

Composing Swarm Protocols

In this section we introduce the composition operation on swarm protocols (§ 3.1) and our new notion of well-formedness (§ 3.2). We then provide an effective method for computing subscriptions that guarantee the well-formedness of a protocol with respect to those subscriptions (§ 3.3 and Theorem 16). First, as in [41], we formalise a swarm protocol (or simply protocol) G as a regular term from the following coinductive grammar:2 P co G ::= where R1 , R2 , etc. range over roles i∈I Ri ⟨ti ⟩ · Gi The protocol G above specifies that (any machine implementing) role Ri is expected to emit an event of type ti (for some i ∈ I) and let the protocol continue as Gi . The summation P operator represents a nondeterministic choice, so the order of summands is immaterial. We write G = 0 if I is empty. For readability we use the infix notation for summations; for instance, for the protocol Warehouse in Fig. 1 we write: Warehouse = T⟨partReq⟩ · FL⟨pos⟩ · T⟨partOK⟩ · Warehouse + D⟨closingTime⟩ · 0

3.1

Protocol Interface and Composition

P We introduce some convenient notation: given a protocol G = i∈I Ri ⟨ti ⟩ · Gi , we write R⟨t⟩ ∈ G if R⟨t⟩ occurs anywhere in G (and likewise for t ∈ G, and R ∈ G).

A term is regular if it consists of finitely many distinct subterms. This condition ensures that the language generated by the co-inductive grammar is finitely representable either using the so-called “µ notation” [46] or as solutions of finite sets of equations [19]. Also, there is a correspondence between these structures and finite-state automata; the interested reader is referred to [19].

Compositional Design, Implementation, and Verification of Swarms (Technical Report)

In Def. 1 below we formalise when two protocols interface; intuitively, this happens when event types common to the protocols are emitted by common roles only. ▶ Definition 1 (Protocol interface). Two protocols G and G′ are interfacing iff for any R⟨t⟩ ∈ G and R′ ⟨t⟩ ∈ G′ , it holds that R = R′ . The set of interfacing roles is {R | R ∈ G ∧ R ∈ G′ }. When R⟨t⟩ ∈ G and R is an interfacing role, we say t is an interfacing event type. Def. 2 below formalises a protocol composition operator _ || _ that allows two protocols to run independently (items 1 and 2) – except for the synchronisations imposed by the events from their interfacing roles, if any (item 3). P ′ ▶ Definition 2 (Protocol composition). Given protocols G = i∈I Ri ⟨ti ⟩ · Gi and G = P ′ ′ ′ j∈J Rj ⟨tj ⟩ · Gj as well as a set of roles R, we coinductively define: G || R G′

P co := {R ⟨t ⟩ · (Gi || R G′ ) i ∈ I, Ri ∈ / R} P ′i i′ + {Rj ⟨tj ⟩ · (G || R G′j ) j ∈ J, R′j ∈ / R} P + {Ri ⟨ti ⟩ · (Gi || R G′j ) i ∈ I, j ∈ J, Ri ⟨ti ⟩ = R′j ⟨t′j ⟩}

(1) (2) (3)

We let _ || _ be left-associative and simply write G || G′ instead of G || R G′ when R is the set of roles that G and G′ interface on. By construction, _ || _ is an idempotent and commutative internal operation on protocols. Note that we do not introduce new protocol-level syntax for composed protocols: more precisely, the result of G || G′ is a protocol obtained by interleaving event types that G and G′ do not share while synchronising shared event types.3 ▶ Example 3. The swarm protocol composition Warehouse || Factory informally depicted in Fig. 6 is obtained by expanding Warehouse || {T} Factory: Warehouse || Factory = T⟨partReq⟩ · FL⟨pos⟩ · T⟨partOK⟩ · A⟨car⟩ · D⟨closingTime⟩ · 0 + D⟨closingTime⟩ · A⟨car⟩ · 0 + D⟨closingTime⟩ · 0

⋄

In general, when two swarm protocols are composed, only those interfacing event types emitted in both protocols in the same order are included in the composition; if interfacing event types are missing in a component protocol or emitted in different orders, then the composition excludes behaviour present in the component protocols, as shown in Example 4.4 ▶ Example 4 (Protocol composition and behaviour restrictions). Consider the swarm protocol Warehouse in Fig. 1, and Factory′ = T⟨partOK⟩ · T⟨partReq⟩ · A⟨car⟩ · 0. By Def. 2, the composition Warehouse || Factory′ yields D⟨closingTime⟩ · 0 because the interfacing role T in Factory′ emits an event of type partOK before those of type partReq – whereas Warehouse follows the opposite order. As another example, letting R = {T}, we have Warehouse || R 0 = D⟨closingTime⟩ · 0 – because, by Def. 2, R “blocks” the actions of role T in Warehouse as it cannot synchronise with 0. ⋄

3 4

This design decision allows us us to maintain backward compatibility with existing tools (see § 6). Such behaviour restrictions are not consequential for our theoretical development. If undesired, they can be identified by checking whether the relevant transitions of G and G′ remain present in G || G′ .

F. Furbach, L. Clorius, R. Kuhn, H. Melgratti, A. Scalas, and E. Tuosto

3.2

Well-Formedness of Swarm Protocols and Subscriptions

We now introduce our new notion of well-formedness (Def. 12), which builds upon the following three properties: confusion-freeness (Def. 5), causal consistency (Def. 8), and determinacy (Def. 10). Although these three properties have the same name as those in [41], their definitions deviate significantly to accommodate compositionality. Crucially, our wellformedness is more general than that of [41] (except in some minor corner cases discussed later in Footnote 10), hence we do not lose expressiveness. P Before proceeding, we introduce some additional notation. Given G = i∈I Ri ⟨ti ⟩ · Gi , Ri ⟨ti ⟩

the predicate G −−−→ Gi holds for all i ∈ I and indicates that some role Ri can emit an t event of type ti causing the swarm protocol G to continue as Gi . We write G − → G instead of R⟨t⟩

R⟨t⟩

G −−→ G when the role R is immaterial. We sometimes write G −−→ when there is G′ such R⟨t⟩ t that G −−→ G′ , and similarly for G − →. We write G ⊑ G′ if G is a subterm of G′ . We shorten t1 tn t1 ...tn G −→ · · · −→ G′ to G −− −−→ G′ ; therefore, given a sequence of event types l = t1 . . . tn , we t1 ...tn l ′ write G − → G if G −−−−→ G′ . By Def. 5 a protocol is confusion-free if: (1) every event type is emitted by only one role; (2) event types are deterministic, i.e., an event emision leads to only one possible continuation; and (3) the same event type can be emitted by different subterms only due to concurrency, i.e., any subterm accounts for a different interleaving of independent event types.5 ▶ Definition 5 (Confusion-Freeness). A protocol G is confusion-free if: 1. For every t ∈ G, if R⟨t⟩, R′ ⟨t⟩ ∈ G, then R = R′ . t t 2. For every G1 , G2 , G3 ⊑ G and t ∈ G, if G1 − → G2 and G1 − → G3 then G2 = G3 . 3. There are G1 , . . . , Gn for n ≥ 1 such that G = G1 || . . . || Gn and for every t ∈ G and t i ∈ {1, . . . , n}, there is at most one subterm G′ ⊑ Gi such that G′ − →. In Def. 6 below we characterise four categories of event types in a confusion-free protocol: (1) concurrent event types (i.e., those that are causally independent, see Fig. 7); (2) branching event types (i.e., those that introduce decision points, see Fig. 8); (3) joining event types (i.e., those that synchronize multiple concurrent branches, see Fig. 7); (4) looping event types (i.e., those that are repeated due to loops, see Fig. 9). Notice that these categories are not mutually exclusive: for instance, an event type can be both joining and branching, or neither. ▶ Definition 6 (Concurrent, Branching, Joining, and Looping Event Types). Let G be a confusion-free protocol. An event type t is: t t′

t′ t

1. Concurrent with a t′ ̸= t if there exist G1 , G2 ⊑ G such that G1 − →−→ G2 and G1 −→− → G2 .6 t′

2. Branching with a t′ ̸= t at G1 ⊑ G if there are G2 , G3 ⊑ G with G1 − → G2 , G1 −→ G3 such that G2 ̸= G3 and t, t′ are not concurrent. t′

t′′

3. Joining for t′ and t′′ at G3 if there are G1 , G2 , ⊑ G such that G1 −→ G3 , G2 −→ G3 , and t G3 − → where t′ and t′′ are concurrent, but neither of them is concurrent with t. l t 4. Looping if there are G′ ⊑ G and l such that G′ − →− → G′ . A subscriptions σ (Def. 7 below) specifies which roles observe which event types; Def. 8 then defines when a swarm protocol G is causally consistent w.r.t. a subscription σ.

Item 3 of Def. 5 can be expensive to check on an arbitrary G, but is immediate when the appropriate G1 , . . . , Gn are given upfront (which is the common case when composing protocols). 6 Note that our definition of “concurrent events” together with confusion-freeness (Def. 5) ensure that for ta tb tb ta all Ga , Gb ⊑ G and ta , tb ∈ G where ta , tb are concurrent and Ga −→−→ Gb , we also have Ga −→−→ Gb .

Compositional Design, Implementation, and Verification of Swarms (Technical Report)

R ′′⟨ ′′ t ⟩

′⟩

R ⟨t ′

R ′′⟨ ′′ t ⟩

R⟨t

R⟨t⟩

R ′⟨t ′ ⟩

′⟩

R ⟨t ′

⟩

Figure 7 t and t are concurFigure 8 t is branching rent; t is joining for t′ and t′′ . with t′ . ′

′′

R′ ⟨t′ ⟩ ′

Figure 9 t and t are looping.

Intuitively, causal consistency enforces two key requirements. First, each role must subscribe to the event types it emits: this will be necessary later, when we define how to project machines from G based on σ.7 Second, to follow the causal dependencies specified in the protocol, roles must subscribe to the event types directly preceding the events they emit. ▶ Definition 7 (Subscription). A subscription σ is a mapping from roles to sets of event types; i.e., σ(R) is the set of event types that role R subscribes to. ▶ Definition 8 (Causal-consistent swarm protocol). A protocol G is causal-consistent for a subscription σ if, for all t′ , R⟨t⟩ ∈ G: 1. t ∈ σ(R) and t′ R⟨t⟩

2. t′ ∈ σ(R) if t′ and t are not concurrent and there is G1 ⊑ G such that G1 −→−−→. ▶ Example 9 (Causal consistency). Consider the Factory protocol in Fig. 4. By causal consistency, the subscription σ(A) of the Assembly robot must include event types car and partOK – respectively by the first and second condition of Def. 8. ⋄ Def. 10 below characterises subscriptions of determinate protocols, namely those where each role R subscribes to the events that are crucial for tracking causality in a swarm protocol G. Intuitively, depending on the category of an event type t in G (branching, joining, or looping), Def. 10 require that (i) role R must subscribe to any event types that are branching with t (clause Branching), (ii) R must subscribe to any concurrent event types that immediatly precede t (clause Joining), and (iii) each role R must observe each loop iteration, hence there must be at least one event type in each loop that all roles subscribe to (clause Looping). Def. 10 relies on the set roles(t, G, σ), which is the set of roles that subscribe to event types in G that causally depend on t according to σ. Formally, roles(t, G, σ) = {R there are n ≥ 0, t0 , . . . , tn , l1 , . . . , ln such that: t

0 1 1 n n t0 = t, G −→ −→ −→ · · · −→ −→ and

tn ∈ σ(R), and ti , ti+1 not concurrent for all 0 ≤ i < n}. ▶ Definition 10 (Determinate protocol subscriptions). A protocol G is determinate for subscription σ if, for all G′ ⊑ G and t, R ∈ G Branching: If t is branching with t′ at G′ and R ∈ roles(t, G′ , σ), then t, t′ ∈ σ(R). Joining: If t is joining for t′ and t′′ at G′ and R ∈ roles(t, G′ , σ), then t, t′ , t′′ ∈ σ(R). l

Looping: If G′ − → G′ for some non-empty l then there are t′ ∈ l and G′′ ⊑ G′ such that ′

G′′ −→ and t′ ∈ σ(R) for all R ∈ roles(t′ , G′′ , σ). We call t′ looping in σ.

As mentioned in § 2.1, and later formalised in Def. 25, if a machine playing role R emits an event of type t, that machine will not change state unless it has an accepting transition for t. Subscribing R to t ensures that the projection of a swarm protocol onto its roles (using Def. 21) will produce machines that can change state by accepting every event type they emit.

F. Furbach, L. Clorius, R. Kuhn, H. Melgratti, A. Scalas, and E. Tuosto partReq pos partOK

▶ Example 11 (Branching vs. looping events). In Fig. 1, the loop Warehouse −−−−−→−−→−−−−→ Warehouse can be exited by event type closingTime, which branches with partReq. Consequently, subscribing to partReq and closingTime is required by clause branching of Def. 10 – and the subscription to partReq also satisfies the clause looping. In general, if a protocol contains a loop with a branching that exits the loop, then each branching event type that continues the loop is also a looping event type in the subscription (by Def. 6) and subscribing to it satisfies clause looping of Def. 10. ⋄ We now have all the ingredients to formalise when a swarm protocol is well-formed. ▶ Definition 12 (Well-formed swarm protocols). A protocol G is σ-well-formed if it is confusionfree, causal-consistent in σ, and determinate for σ (Definitions 5, 8, and 10). ▶ Example 13 (Well-formed protocol and subscription). The protocol Warehouse || Factory in Example 3 and Fig. 6 is confusion-free (by Def. 5). Now, take the assembly robot A and a subscription σ such that Warehouse || Factory is σ-well-formed (by Def. 12): rule (1) of causal consistency (Def. 8) requires car ∈ σ(A), implying A ∈ roles(partReq, Warehouse || Factory, σ); therefore, from the branching rule of determinacy (Def. 10), we have partReq, closingTime ∈ σ(A). The joining and looping rules of Def. 10 hold vacuously, as there are no joining event types or loops in Warehouse || Factory. ⋄

3.3

On Computing Subscriptions

This section introduces Algorithm 1 for computing subscriptions that guarantee wellformedness (by Def. 12) for a composition G1 || . . . || Gn of given swarm protocols G1 . . . Gn . In general, for any confusion-free swarm protocol G there is at least one subscription σ such that G is σ-well-formed: it is the “total” subscription where each role in G subscribes to all event types in G. However, if such a “total” subscription is used to project machines from G (using Def. 21 later on), then the resulting swarm would consist of complex machines that await the emission of all events emitted by all other machines, leading to inefficient executions. It is hence worthwhile to compute smaller subscriptions that preserve well-formedness. Importantly, for a composition G1 || . . . || Gn of n composable protocols (by Def. 14 below), our Algorithm 1 operates on the individual input protocols without expanding their composition (Def. 2), because the size of the expanded protocol may grow exponentially with n (as shown later in § 6.2). ▶ Definition 14 (Composable swarm protocols). A protocol is sequential if it does not contain concurrent events. A set of protocols is composable if they are pairwise interfacing and each protocol is sequential and confusion-free. Algorithm 1 takes a set {Gi }i∈I of composable protocols together with a set {σ i }i∈I of subscriptions, and generates a subscription σ such that G = G1 || . . . || Gn is σ-well-formed and σ i ⊆ σ holds for all i ∈ I. The algorithm initialises three sets: σ, initially approximating the result as the union of the given σ i . Each σ i can be understood as the specification of the event types that each role in Gi is interested in. ifr containing all interfacing roles. conc containing all potentially concurrent event types, i.e., the pairs of event types belonging to different components that are emited by non-interfacing roles. The algorithm iteratively enlarges σ by applying monotone operations corresponding to the definitions of causal-consistency (Def. 8) and branching and joining of determinacy (Def. 10), together with the new operator interfacing, which is crucial for ensuring the correct

Compositional Design, Implementation, and Verification of Swarms (Technical Report)

Algorithm 1 Computing a subscription for a composition of protocols. Input: A set {G1 , . . . , Gn } of composable protocols and a set of subscriptions {σ 1 , . . . , σ n } Output: A subscription σ ⊇ σ 1 , . . . , σ n such that G1 || . . . || Gn is σ-well-formed. Let subscribers(G, σ) denote the roles that subscribe to some event type of G in σ. S σ := i≤n σ i ifr := {R | ∃i, j ≤ n : i ̸= j ∧ R ∈ Gi ∧ R ∈ Gj } conc := {{ti , tj } | i, j ≤ n, Ri ⟨ti ⟩ ∈ Gi , Rj ⟨tj ⟩ ∈ Gj , Ri ∈ / Gj , Rj ∈ / Gi } repeat for all i ≤ n, G′i , G′′i ⊑ Gi , and R, R′ , t, t′ ∈ Gi do R⟨t⟩

t′

R⟨t⟩

Causal Consistency: If G′i −−→, then add t to σ(R); If G′i − →−−→, then add t′ to σ(R). ′ ′ Branching: If t is branching with t at Gi and R ∈ subscribers(G′i , σ), then add t, t′ to σ(R). t′ t t′′ t Joining: For all j ≤ n, G′j ⊑ Gj , and t′′ ∈ Gj such that G′i − →− →, G′j −→− →, {t′ , t′′ } ∈ conc, ′ ′′ ′ ′ ′′ {t , t} ̸∈ conc, {t , t} ̸∈ conc, and R ∈ subscribers(Gi , σ): Add t , t , t to σ(R). R⟨t⟩

Interfacing: If G′i −−→ G′′i with R ∈ ifr and R′ ∈ subscribers(G′′i , σ), then add t to σ(R′ ). end for until σ no longer changes t·l for all i ≤ n, G′i ⊑ Gi , such that G′i −−→ G′i for some t and l, and R ∈ subscribers(G′i , σ) do ′ Looping: If Gi has no looping event type in σ, then add t to σ(R). end for

synchronisation of the protocols (as will be discussed below). The iteration terminates when a fixed point is reached. The final phase ensures that every role that is involved in a term that contains a loop l is subscribed to (at least) one looping event of l. On the need of the interfacing step in Algorithm 1. One of the requirements of wellformedness (Def. 12) is determinacy (Def. 10). Checking the determinacy of a composed swarm protocol for a subscription requires the set roles(t, G′ , σ) for subterms G′ = G′1 || . . . || G′n – and computing that set would require the explicit computation of the expanded protocol G′ (using Def. 2); however, the size of the expanded G′ can be exponential in n. To avoid this exponential blow-up, Algorithm 1 uses the set subscribers(G′i , σ) (where G′i is a subterm of one of the input protocols Gi ) and its interfacing step to over-approximate the set roles(t, G, σ) without explicitly expanding G = G1 || . . . || Gn . To see why this approach yields the desired over-approximation, recall that R ∈ roles(t, G′ , σ) holds if there exists a t0 l1 t1 ln tn path G′ −→ −→−→ · · · −→ −→ such that t0 = t, tn ∈ σ(R), and every pair ti , ti+1 is not concurrent for 0 ≤ i < n. Since ti and ti+1 are not concurrent, they must either belong to the same concurrency-free input swarm protocol or they are separated by interfacing event t′

l′

t′

l′ ′

t′ ′

0 1 1 n n types that enforce their ordering. Consequently, there exists a path G′ −→ −→ −→ · · · −− →−− → ′ ′ ′ ′ satisfying the conditions above, where t1 , . . . , tn′ −1 are interfacing event types and ti , ti+1 occur within the same input protocol for 0 ≤ i < n′ . The interfacing step propagates subscriptions along this path, that is, if t′i+1 ∈ σ(R), then also t′i ∈ σ(R). Starting from t′n′ ∈ σ(R), repeated application of the interfacing step backwards along the path ensures that t′1 ∈ σ(R). Since t′1 is in the same input protocol G′i as t, we obtain R ∈ subscribers(G′i , σ). (This argument is formally stated in Lemma 39 in § A).

▶ Example 15 (Application of Algorithm 1 to Warehouse and Factory). We illustrate the application of Algorithm 1 to the protocols Warehouse and Factory (depicted in Figures 1 and 4, respectively) and two empty subscriptions σ 1 = σ 2 = ∅. It is straightforward to check that these two protocols are composable, since they are sequential, confusion-free and they interface on T. Then, the algorithm initialises σ = σ 1 ∪ σ 2 = ∅, ifr = {T}, and

F. Furbach, L. Clorius, R. Kuhn, H. Melgratti, A. Scalas, and E. Tuosto

conc = {{closingTime, car}, {pos, car}}. Note that conc over-approximates the actual pairs of concurrent event types. Indeed, only closingTime and car are concurrent in the composition Warehouse || Factory (see Fig. 6). Now the algorithm starts the iteration with the step causal consistency. Starting with role T and protocol Factory, we first add the event types partReq and partOK to σ(T) because Factory has transitions where T emits such event types. In Warehouse, the same role T emits partOK after FL emits pos; consequently pos is added to σ(T). Subscriptions for the remaining roles, shown below, are obtained analogously. T 7→ {partReq, partOK, pos}, FL 7→ {partReq, pos}, σ = D 7→ {partOK, closingTime}, A 7→ {partOK, car} Then, the branching step is executed. Note that partReq and closingTime are branching in Warehouse. Therefore, (i) partReq is added to the subscriptions of the roles already subscribed to event types of Warehouse, i.e., to D and A; (ii) analogously, closingTime is added to T, FL, and A. Step joining is not actually applied in this example because its conditions are not satisfied. Next, the interfacing step adds partOK to all roles that have subscribed to some event that follows partOK in some of the protocols; hence, partOK is added to FL because it already subscribed to partReq. The fixed point of the iteration is: T, FL 7→ {partReq, partOK, closingTime, pos} σ= D 7→ {partReq, partOK, closingTime}, A 7→ {partReq, partOK, closingTime, car} In Warehouse, the event type partReq is looping in σ. However, it was already added to the relevant roles due to the branching rule. Thus, the looping phase is not applied. ⋄ Theorem 16 below states that Algorithm 1 computes a subscription σ ensuring wellformedness of the composed protocol. (Proof in § A.) ▶ Theorem 16 (Correctness of Algorithm 1). If σ is the subscription computed from the composable protocols G1 , . . . , Gn and subscriptions σ 1 , . . . , σ n using Algorithm 1, then G1 || . . . || Gn is σ-well-formed.

Realising Swarm Protocols as Swarms of Machines

We now address the problem of correctly realising a swarm protocol G (Def. 28), i.e., constructing a swarm of machines that interact as specified by G. We begin by fixing the language for writing machines (§ 4.1). Following the standard top-down approach for behavioral types, we rely on a projection operation (§ 4.2) to derive correct machines for the different roles of a protocol. Then, we refine the swarm model introduced in [41] by adding a branch-tracking mechanism to the semantics of machines (§ 4.3) in a swarm (§ 4.4). This revised semantics is essential for (1) ensuring that the machines projected from a swarm protocol G are eventually faithful to G (§ 4.5), and (2) enabling the composition of swarms (discussed in § 5).

4.1

Machines

A machine models a swarm agent that processes a local log of events to make decisions on the emission of new events. We define a machine as a grammar term (Def. 17) with a corresponding finite-state automaton (Def. 18). ▶ Definition 17 (Machine). A machine is a regular term from the coinductive grammar:

Compositional Design, Implementation, and Verification of Swarms (Technical Report) co

M ::= κ · &i∈I ti ? Mi

where κ is a finite set of event types dubbed the emitter set

such that ti ̸= tj for all i ̸= j ∈ I. We write 0 when κ = I = ∅. ▶ Definition 18 (Machine states and transitions). A machine M from Def. 17 can be described as the deterministic finite-state automaton where: Each distinct subterm of M (finitely many since M is regular) corresponds to a state. The initial state is M itself. t?

There is an event acceptance transition M1 −−→ M2 whenever machine M1 has a branch t? leading to M2 t!

and an event emission transition M ′ −→ M ′ for any t in the emitter set of M ′ . ▶ Remark 19. The grammar-based presentation of machines (Def. 17) and the automaton presentation (Def. 18) are equivalent: each distinct subterm corresponds to a state, branches correspond to acceptance transitions, and emitter sets yield emission self-loops. ▶ Example 20. By Def. 18, the automaton depicted in Fig. 2 corresponds to the machine:8 M D = {closingTime} · (partReq? partOK? M) & (closingTime? 0) Note that a closing-time event can be emitted only from M D (the initial state in the automaton of Fig. 2) since closingTime belongs only to the emitter set of M D . Also note that in Fig. 2, emitted events appear as self-loops: this is because (by Def. 18 above) a machine remains in its current state while emitting an event; a state transition may occur only when a machine accepts an event from its log. ⋄

4.2

Projecting a Swarm Protocol onto its Roles

By Def. 21 below, the projection of a swarm protocol G onto a role R yields a machine that captures the behaviour of R in G. Specifically, the projected machine retains the event types that are either emitted or subscribed to by R – and it disregards all other event types. ▶ Definition 21 (Projection). We coinductively define the projection of a σ-well-formed swarm protocol G onto a role R as: n o co l t G ↓σR := κ · & t?(G′ ↓σR ) ∃l : G − →− → G′ and l ∩ σ(R) = ∅ and t ∈ σ(R) where

R⟨t⟩

κ = t ∃l : G − →−−→ and l ∩ σ(R) = ∅ .

Observe that, by Def. 21, the initial state of the projected machine G ↓σR has: A branch t? for every event type t that R subscribes to (by σ) and can be reached from G after a (possibly empty) sequence of events of type l not subscribed to by R. An emitter set κ consisting of all the event types that R can emit in G after a (possibly empty) sequence of events of type l not subscribed to by R. Hence, the projection G ↓σR may start by either emitting an event of a type in κ or proceed to G′ ↓σR upon accepting an event of type t. Note that an event type t that is not subscribed to by R does not appear in G ↓σR , i.e., the projected machine ignores all events of such a type t. ▶ Example 22 (Projection). Consider the swarm protocol G = Warehouse || Factory shown in Fig. 6 and the following subscription (where E stands for the set of all event types in G): σ = {T 7→ E \ {car}, D 7→ E \ {pos, car}, FL 7→ E \ {partOK, car}, A 7→ E \ {pos}} The projections of G are shown in Fig. 10.

⋄

F. Furbach, L. Clorius, R. Kuhn, H. Melgratti, A. Scalas, and E. Tuosto partReq!

partOK!

G ↓σT

closingTime?

partReq?

pos?

G ↓σD

closingTime?

partReq?

partOK?

closingTime?

partReq?

pos?

closingTime?

closingTime!

G ↓σFL

partOK?

closingTime?

G ↓σD

closingTime?

closingTime! partReq? partOK? pos!

closingTime?

partReq?

partOK?

im ngT

si clo

G ↓σFL

car

clo

me?

gTi

sin

q? tRe par

clo

sin

pos?

gTi

me?

closingTime?

car! car

partOK!

pos

partOK?

partReq?

car!

closingTime!

pos!

G ↓σA

partReq! q? tRe par

G ↓σT

Figure 10 Projection of G = Warehouse || Factory (from Fig. 6) on roles T, D, FL, and A, using the subscription σ defined in Example 22.

Figure 11 Projection of G = Warehouse (from Fig. 1) on roles T, D, and FL, using the subscription σ defined in Example 29.

Notice that in Def. 21, when constructing the projection G ↓σR there might be multiple l l ti and Gi such that G − →−→ Gi , meaning the projected machine can accept or emit ti and then reach one of potentially many different options for Gi ↓σR . Still, Lemma 23 ensures that if G is well-formed, then G ↓σR relates G to only one unique machine. ▶ Lemma 23. If G is a σ-well-formed protocol, then G ↓σR is uniquely defined for all R. Proof. (Outline; full proof in § B) The σ-well-formedness property ensures that the projection satisfies G′ ↓σR = G′′ ↓σR for all sub-terms G′ and G′′ reachable from G by event types not in σ(R)– so it does not matter which one is chosen in the construction of G ↓σR . This is because the subscription σ includes all event types that can influence the future behaviour of the projection – so in Def. 21, the event types selected in l (which are not in σ) do not influence the shape of Gi ↓σR . ◀

4.3

Branch-Tracking Machine Semantics

In this section we define how machines emit events and process their local log of events. We fix a set of events, ranged over by e; each event has a unique event type t. An event log l is a sequence e 1 · e 2 · . . . of pairwise distinct events. As anticipated in § 2.2, we incorporate a new branch-tracking mechanism to the machine semantics originally proposed in [41] to establish an explicit causal link between events. Such a link was not present nor needed in [41] – but it is necessary for swarms to work correctly with our compositional well-formedness (Def. 12), which removes restrictions assumed by the machine semantics in [41]. The behaviour of a machine M is determined by a log-processing function δ̂ (formalised in Def. 24 below). Let T be the set of all event types. In defining δ̂, we assume that machines are equipped with an additional element, which does not appear in [41]: A set of updating event types M.UP ⊆ T .9 If an event e has a type t ∈ M.UP, we call e an updating event. We also add to each event e a field e.lastup , which intuitively refers to the last updating event that caused e. A machine M processes its log starting from the oldest event. When processing an event e of type t, M performs a transition if: t?

1. There is an acceptance transition M −−→ M ′ ; i.e., M accepts events of type t; and

8 9

For readability, in our examples we often use brackets and infix notation for the branching operator &. We will see in Def. 28 that this set is populated with branching, joining, and looping event types from a swarm protocol.

Compositional Design, Implementation, and Verification of Swarms (Technical Report)

2. e.lastup coincides with the last updating event observed by M; i.e., e.lastup is the last updating event that causally preceded e. If the two conditions above hold, then M accepts e and moves to the next state M ′ , i.e., the continuation of the event acceptance transition, from which the remaning events in the log are processed. Otherwise, M skips e and processes the next event in the log. More precisely, in order to remember previously-seen updating events and check the pointer e.lastup , each machine keeps a partial mapping lastup : T ⇀ E that associates each event type t with the last updating event for the type t. The mapping lastup is built by the machine while processing a log: initially, lastup is empty (i.e., ∅) and it is updated every time a machine processes an updating event. The updating of lastup is performed as follows. Let branch(M, t) be a partial mapping that, for each machine M and event type t, gives the set event types that continue along the same branch as t until the next updating event; tn ? t ? t1 ? specifically, if M −→−− → . . . −− → with t1 , . . . , tn−1 ∈ / M.UP and t1 , . . . , tn not concurrent with t, then t1 , . . . , tn ∈ branch(M, t). The processing of an event e of type t by a machine t?

M that has an event acceptance transition M −−→ M ′ is described by the following relation: e

(M, lastup ) − → e (M, lastup ) − →

(M ′ , lastup ) (M ′ , lastup [branch(M, t) 7→ e])

if e.lastup = lastup (t) and t ∈ / M.UP if e.lastup = lastup (t) and t ∈ M.UP.

where lastup [T 7→ e] denotes the update of lastup , namely the mapping that maps each event type in the set T to event e, and behaves as lastup for other event types. The mechanism through which a machine M processes a complete event log l , or equivalently determines its current state based on l , is specified by Def. 24 below. ▶ Definition 24 (Log-processing function). The log-processing function δ̂ is defined as δ̂(M, l ) = δBT (M, l , ∅) where: δBT (M, ϵ, lastup ) = ( (M, lastup ) δBT (M ′ , l , lastup ′ ) δBT (M, e · l , lastup ) = δBT (M, l , lastup )

if (M, lastup ) − → (M ′ , lastup ′ ) otherwise.

Note that in Def. 24, δ̂ is defined in terms of the auxiliary function δBT , which is in charge of constructing lastup while traversing the log. Observe that δBT , and consequently δ̂, returns a pair (M ′ , lastup ) where M ′ is the reached machine and lastup is the mapping built after processing the log. Based on the current state computed by the log-processing function δ̂, machines generate new events according to Def. 25 below. ▶ Definition 25 (Operational semantics of machines). A machine M with a local log l emits events according to the following rule: δ̂(M, l ) = (κ · &i∈I ti ? Mi , lastup )

t∈κ t!

e has type t

(M, l ) =⇒ (M, l · e) t!

e.lastup = lastup (t) [emit]

The transition (M, l ) =⇒ (M, l · e) in Def. 25 reads as: “a machine M with a log l emits an event e of type t.” Observe that the new event e is added to the end of the local log, and the transition is possible only if, after processing l , the machine reaches a state κ · &i∈I ti ? Mi where the emission of events of type t is enabled (i.e., t ∈ κ). Moreover, e must be of type t and must reference the last updating event for t.

4.4

Swarms

A swarm (of size n) is a pair (S, l ) where:

F. Furbach, L. Clorius, R. Kuhn, H. Melgratti, A. Scalas, and E. Tuosto

S maps indices i ∈ {1, . . . , n} to machines and their local log, i.e. S(i) = (Mi , l i ); l is a global log, i.e., a sequence consisting of all events generated by the machines in S that preserves their order of generation. More formally: Every log (global or local) l ′ = e 1 · · · e n totally orders its events using a relation <l ′ defined as e i <l ′ e j iff i < j; The global log l contains all and only the events of the local logs l i (for all i ∈ {1, . . . , n}) S and preserves their respective ordering: i∈{1,...,n} l i = l and <l i ⊆<l . For brevity, we may write S instead of (S, l ) (and call S a swarm) if the global log l is empty. ▶ Remark 26. The global log l of a swarm (S, l ) does not exist in actual swarm implementations: it is a formalisation device which models the global ordering and non-deterministic propagation of events, as defined by swarm semantics formalised in Def. 27 below. ▶ Definition 27 (Swarm semantics). The behaviour of a swarm is defined by the smallest relation closed under the following rules: S(i) = (Mi , l i )

(Mi , l i ) =⇒ (Mi , l i · e)

(S, l · l ′ ) −→ (S[i 7→ (Mi , l i · e)], l · e · l ′ )

S(i) = (Mi , l i ) [Local]

<l i ⊂<l ′ ⊆<l

(S, l ) −→ (S[i 7→ (Mi , l ′ )], l )

[Prop]

In Def. 27, rule Local formalises the emission of an event enabled at the machine at S(i) of the swarm (S, l ). The emitted event e is appended to the local log of S(i) and nondeterministically merged in the global log respecting the order of events previously generated by S(i). Rule Prop models the asynchronous event log propagation among machines: for some machine Mi with a local log l i (that is strictly included in the global log l ), the rule non-deterministically selects a log l ′ ⊆ l that contains l i and transfers the events in l ′ to l i while preserving their order. Note that during an execution, machines can emit events independently, and their local log may only partially reflect the “global state” in the global log (due to the non-deterministic and asynchronous propagation of events). Def. 28 below formalises the realisation of a swarm protocol G, i.e., a swarm whose machines interact according to the roles G. ▶ Definition 28 (Realisation of a swarm protocol). A swarm (S, ϵ) of size n realises a protocol G with respect to a subscription σ iff for all i ∈ {1, . . . , n}, (i) S(i) = (Mi , ϵ), and (ii) Mi = G ↓σR for some R ∈ G; and (iii) Mi .UP is equal to the event types of G that are branching, joining, or looping in σ. We also say that Mi realises R. ▶ Example 29 (Swarm protocol realisation and execution). Let E denote the set of all event types in the Warehouseprotocol (Fig. 1) and σ = {T 7→ E, FL 7→ E \{partOK}, D 7→ E \{pos}}. By Def. 12, Warehouse is σ-well-formed. By Def. 28, the swarm S W below realises Warehouse w.r.t. σ: S W = {iT1 7→ (MT , ϵ),

iT2 7→ (MT , ϵ),

iFL 7→ (MFL , ϵ),

iD 7→ (MD , ϵ)}

where MT = Warehouse ↓σT , MFL = Warehouse ↓σFL , and MD = Warehouse ↓σD (shown in Fig. 11). Notice that the machine in S W (iT1 ) and S W (iT2 ) play the same role T. By Def. 27, a possible execution of the swarm S W is:

Compositional Design, Implementation, and Verification of Swarms (Technical Report) partReq!

(S W , ϵ) =====⇒ (S 1 , partReq 1 ) τ

= ⇒ (S 2 , partReq 1 ) pos!

===⇒ (S 3 , partReq 1 · pos 2 )

S 1 = S W [iT1 7→ (MT , partReq 1 )] S 2 = S 1 [iFL1 7→ (MFL , partReq 1 )] S 3 = S 2 [iFL 7→ (MFL , partReq 1 · pos 2 )]

= ⇒ (S 4 , partReq 1 · pos 2 )

S 4 = S 3 [iT1 7→ (MT , partReq 1 · pos 2 )]

S 5 = S 4 [iT2 7→ (MT , partReq 1 · pos 2 )]

= ⇒ (S 5 , partReq 1 · pos 2 ) partOK!

=====⇒ (S 6 , partReq 1 · pos 2 · partOK 3 ) partReq!

=====⇒ (S 7 , partReq 1 · pos 2 · partOK 3 · partReq 4 ) partOK!

=====⇒ (S 8 , l ) τ ∗

= ⇒ (S 9 , l )

S 6 = S 5 [iT1 7→ (MT , partReq 1 · pos 2 · partOK 3 )] S 7 = S 6 [iT1 7→ (MT , partReq 1 · pos 2 · partOK 3 · partReq 4 )] S 8 = S 7 [iT2 7→ (MT , partReq 1 · pos 2 · partOK 5 )] S 9 = S 8 [iT1 7→ (MT , l ), iT2 7→ (MT , l ), iFL 7→ (MFL , l ), iD 7→ (MD , l )]

where, in states S 8 and S 9 , the global log is l = partReq 1 · pos 2 · partOK 3 · partReq 4 · partOK 5 and its events carry the following pointers: partReq 1 .lastup = ⊥ (undefined) pos 2 .lastup = partOK 3 .lastup = partReq 4 .lastup = partOK 5 .lastup = partReq 1 In each state of the swarm, we compute the state of a machine for its local log using δ̂ (Def. 24), which in turn uses the branching, joining, and looping events in l to update the mapping lastup and only considers events carrying correct pointers. For this example, when the machines process the event partReq 4 , they will update their mapping lastup to obtain: lastup [partReq, pos, partOk, closingTime 7→ partReq 4 ] In this updated mapping, all event types of Warehouse point to partReq 4 , which means that the machines will only accept new events e such that e.lastup = partReq 4 . Observe that, in the execution above, the event partOK 5 was emitted by the machine with ID iT2 in response to the event partReq 1 . Hence, partOK 5 .lastup = partReq 1 = ̸ partReq 4 ; i.e., the event partOK 5 is causally linked to partReq 1 through branch tracking. Since the machines expect events, whose lastup fields refer to partReq 4 , the event partOK 5 is ignored by all machines after the logs propagate. Once this happens in state S 9 , the machines reach the states: δ̂(MT , l ) = (FL⟨pos⟩.T⟨partOK⟩.Warehouse) ↓σT δ̂(MD , l ) = (T⟨partOK⟩.Warehouse) ↓σD δ̂(MFL , l ) = (FL⟨pos⟩.T⟨partOK⟩.Warehouse) ↓σFL Here, the machines MT and MFL expect the forklift to emit an event of type pos, while MD (which does not subscribe to pos in σ) is waiting for an event of type partOK that has the correct pointer and thus follows pos in the swarm protocol Warehouse. These states are consistent with each other: (T⟨partOK⟩.Warehouse) ↓σD = ((FL⟨pos⟩.T⟨partOK⟩.Warehouse) ↓σD .Thus they correspond to a valid run of the Warehouse swarm protocol. ⋄ ▶ Remark 30. Running the swarm of Example 29 with the semantics of [41] can lead to a state where the machines irremediably diverge due to the absence of branch tracking and the resulting lack of event causality tracking. We illustrate this situation in § H.

4.5

Eventual Fidelity of Swarm Protocol Realisations

In this section, we address the problem of ensuring that a swarm behaves correctly with respect to a swarm protocol G. As our correctness criterion, we adopt the notion of eventual fidelity (Def. 31 below). Intuitively, a swarm is eventually faithful to a protocol G if, in every execution, once all machines have received all messages, they agree on the same consistent view of the execution path of G. By consistent view, we mean that machines are able to determine which events belong to the effective execution path through G and disregard all other events that may have been emitted inconsistently. We call such a view the effective log (see § C for formal definitions). When considering a global log l generated by a swarm, the

F. Furbach, L. Clorius, R. Kuhn, H. Melgratti, A. Scalas, and E. Tuosto

effective log w.r.t. G, written eff(l, G), is the sublog of l that consists solely of those events of l that follow a valid path through G. We also define the effective log with respect to a specific machine M, written eff(l, M), as the sublog of l containing only the events that M accepts (i.e., all the events not ignored by the log-processing function δ̂). To formalise the eventual fidelity of a swarm to a protocol G, we assign to every machine in the swarm some role of G: we denote this by a mapping r from machines to the roles they play. Eventual fidelity requires that if a machine M that plays role r(M) is provided with a global log l produced by the swarm, then M accepts only those events which are in the global effective log and to which r(M) subscribes. We denote such events by eff(l, G) ↓σ(r(M)) , which is the projection of eff(l, G) onto the event types that role r(M) subscribes to in σ. ▶ Definition 31 (Eventual fidelity). A swarm (S, ϵ) of size n is eventually faithful to a protocol G with respect to a subscription σ if for all l such that (S, ϵ) →∗ (S ′ , l), for all R ∈ G, and for all i ∈ {1...n}, we have eff(l, G) ↓σ(r(S(i))) = eff(l, S(i)). Theorem 32 below ensures that a realisation of a swarm protocol G (i.e., a swarm consisting of machines projected from G, by Def. 28) is eventually faithful to G. The proof is in § D. ▶ Theorem 32 (Eventual fidelity of swarm protocol realisations). If a swarm S realises a σ-well-formed protocol G, then S is eventually faithful to G with respect to σ. ▶ Example 33 (Effective logs and eventual fidelity). Consider the swarm protocol Warehouse (Fig. 1), its projected machine MD = Warehouse ↓σD , (Fig. 11), and the log l from Example 29. By Definitions 41 and 42, the effective logs for Warehouse and M D filtered from l are: eff(l , Warehouse) = partReq 1 · pos 2 · partOK 3 · partReq 4 eff(l , M D ) = partReq 1 · partOK 3 · partReq 4 Therefore, we have eff(l , Warehouse) ↓σ(D) = eff(l , M D ): hence, the effective logs for the machine and the swarm protocol align, as required by eventual fidelity (Def. 31). ⋄

Composing Machines and Swarms

In this section, we present an approach for realising a composition of swarm protocols G1 || . . . || Gn by composing swarms of pre-existing machines which realise the individual protocols Gi (for i ∈ {1, . . . , n}). This is crucial for enabling the reuse of pre-existing machines and their deployment in new, larger swarms (that we implement in § 6). We first formalise the composition of machines (§ 5.1); then, we introduce an automatic adaptation mechanism (§ 5.2) for such pre-existing machines, enabling us to compose entire swarms (Algorithm 2) while guaranteeing eventual fidelity to the composed swarm protocol (Theorem 38).

5.1

Machine Composition

Similar to swarm protocol composition (Def. 2), in Def. 34 below we define the composition of two machines M and M ′ as a synchronised product. Intuitively, if a transition is common to M and M ′ , the machines synchronise and the continuation of M || M ′ is given by the composition of both corresponding continuations of M and M ′ (clause Common Events); otherwise, the continuation of M || M ′ is the composition of the continuation of either M or M ′ with the other machine unchanged (clauses Events Unique). ▶ Definition 34 (Machine composition). Let M := κ · &i∈I ti ?M i and M ′ := κ′ · &j∈J t′j ?M ′j be machines. Let T be the set of event types that occur in both M and M ′ . The composition of M and M ′ , written M || M ′ , is defined as M || T M ′ , which in turn is coinductively defined:

Compositional Design, Implementation, and Verification of Swarms (Technical Report) co

M || T M ′ := κ′′ · &k∈K tk ?M k where K is the smallest set such that for all i ∈ I, j ∈ J: Common Events (ti ∈ T , ti = t′j ): There is a k ∈ K with tk = ti and M k = M i || T M ′j . Events Unique to M (ti ∈ / T ): There is a k ∈ K with tk = ti and M k = M i || T M ′ . ′ ′ Events Unique to M (tj ∈ / T ): There is a k ∈ K such that tk = t′j and M k = M || T M ′j . Then, the emitter set κ′′ is κ′′ = (κ ∪ κ′ ) ∩ {tk | k ∈ K}. Note that by Def. 34, the acceptance transitions of M || M ′ consist of the acceptance transitions of both M and M ′ ; common transitions are synchronised via the set T , hence they are only enabled in a state if both M and M ′ can take them. Further, an event type t belongs to the emitter set of M || M ′ if and only if (i) t belongs to the emitter set of either M or M ′ , and (ii) either t ∈ T and both machines accept t, or t ̸∈ T and one of the machines accepts t. This means a machine either implements an interfacing role and thus only emits events in T or it is non-interfacing and thus only emits events not in T . Also note that, as with swarm protocol composition (Def. 2), we do not introduce new syntax for composed machines: composed machines are treated as ordinary machines, to maintain backward compatibility with existing tooling (that we extend in § 6). ▶ Example 35 (Relating swarm protocol composition, projection, and machine composition). Consider the swarm protocols Warehouse and Factory in Figures 1 and 4, and the subscription σ from Example 22. Also consider the projected machines Warehouse ↓σD in Fig. 11, and Factory ↓σD = partReq? · partOK? · 0. If we compose these two machines (using Def. 34), then we derive the machine denoted as G ↓σD in Fig. 10, and therefore we have: Factory ↓σD || Warehouse ↓σD

= (Factory || Warehouse) ↓σD

Note that this holds because, in σ, the roles of both projected machines subscribe to the interfacing event types that synchronise the composed swarm protocols (by Def. 2). ⋄

5.2

Machine Adaptation

In Def. 36 we introduce a function A that adapts a single machine M, projected from a swarm protocol Gk , so that it behaves correctly when used in a swarm with other adapted machines that were projected from swarm protocols G1 , . . . , Gn . Intuitively, the adaptation function A restructures the transition graph of M in two steps (described in more detail below): (1) it adds automatically generated acceptance transitions to wait for extra synchronisation event types required by a composed subscription σ, and (2) it disables transitions whose continuations are incompatible with the other projections. Notably, A does not rewrite the logic of M: the adapted machine looks different from M (see Example 37 below) but is still just the original automaton with a thin structural wrapper that delays progress until required synchronisation events are emitted by other machines, or disables incompatible paths. ▶ Definition 36 (Machine adaptation for swarm composition). Let G1 , . . . , Gn be swarm protocols with subscriptions σ 1 , . . . , σ n . Let M be a machine that, for some k ∈ {1, . . . , n}, realises role R in the swarm protocol Gk for subscription σ k . Let σ be a well-formed subscription for G1 || . . . || Gn (obtained via Algorithm 1). Then, we define the machine adaptation A as: A M, (Gi )i∈{1,...,n} , R, k, σ = (G1 ↓σR || . . . || (M || Gk ↓σR ) || . . . || Gn ↓σR ) . We also set A M, (Gi )i∈{1,...,n} , R, k, σ .UP as the set of branching, joining, or looping event types selected by Algorithm 1: this overapproximates the set of branching/joining/looping event types of G1 || . . . || Gn .

F. Furbach, L. Clorius, R. Kuhn, H. Melgratti, A. Scalas, and E. Tuosto

Algorithm 2 Swarm composition (shortened version of Algorithm 3 in § E).

Input:

G1 , . . . , Gn composable protocols, which are respectively realised by swarms S 1 , . . . , S n for the subscriptions σ 1 , . . . , σ n . Mappings r1 , . . . , rn that respectively map machines to the role they implement, i.e., rk (S k (i)) is the role realised by the machine at S k (i). Output: A swarm S that realises G1 || . . . || Gn . 1: Apply Algorithm 1 to obtain a well-formed subscription σ for G1 || . . . || Gn . 2: For each swarm S k , for each machine S k (i): adapt S k (i)

into

M′

A M, (Gi )i∈{1,...,n} , rk (S k (i)) , k, σ according to Def. 36. 3: Return a swarm built up from the machines adapted in the previous step.

To better see the effect of the adaptation A in Def. 36, observe that by Algorithm 1 we have σ k ⊆ σ, hence the subscriptions σ and σ k may differ; consequently, Gk ↓σR k and Gk ↓σR may not coincide. Additionally, R might be an interfacing role; therefore, it might appear in other protocols besides Gk . Hence, the input machine M must be adapted to play role R while conforming to all protocols where R appears. Consequently, the adaption of M involves the following two steps (that were outlined above): 1. M is composed with Gk ↓σR to adapt it to the behaviour expected by the subscription σ (which may be larger than σk ). This adaptation may force M to await and accept additional events types, i.e., those in σ(R) that are not in σ k (R). 2. M is also composed with the projections obtained from the remaining protocols of the composition. This step may prune some transitions of M that are absent in the other protocols and add necessary transitions from the other protocols to ensure correct synchronisation in the composed swarm. We extend the adaptation mechanism in Def. 36 to whole swarms: Algorithm 2 takes a set of swarms that respectively realise protocols G1 , . . . , Gn , and automatically generates a swarm that realises G1 || . . . || Gn . Specifically, Algorithm 2 uses Algorithm 1 to find a suitable subscription for the composition, and then it applies the adaptation function in Def. 36. (For a more detailed version of Algorithm 2, see Algorithm 3 in § E.) ▶ Example 37 (Composing swarms by adapting their machines). Recall the swarm S W whose machines are projected from the swarm protocol Warehouse and subscription σ in Example 29. In order to compose S W with another swarm S F projected from Factory using Algorithm 2, we apply the adaptation in Def. 36 to all machines in both S W and S F , and we obtain a swarm S W || F that realises the composed protocol Warehouse || Factory. We illustrate this on the forklift machine MFL = Warehouse ↓σFL . We first apply Algorithm 1 (as in Example 15) to obtain a subscription σ ′ such that Warehouse || Factory is σ ′ -well-formed, and which contains the initial σ and the interfacing event types needed for synchronising the machines that implement Warehouse and Factory. By Def. 36, the machine adaptation of MFL is: ′ ′ A(MFL , (Warehouse, Factory) , FL, 1, σ ′ ) = MFL || Warehouse ↓σFL || Factory ↓σFL where “1” is the index of Warehouse in the tuple (Warehouse, Factory). The stages of the adaptation are depicted in Fig. 12, where the state numbers show the relationship between the original machine and its adaptations. The original MFL is adapted with the projection of its original swarm protocol (Warehouse) using σ ′ (computed with Algorithm 1) to obtain the ′ machine MFL || Warehouse ↓σFL : observe that this adapted machine has an additional state 3 which forces the machine to wait for an event of type partOK after pos, between the original ′ ′ states 2 and 4. When MFL || Warehouse ↓σFL is further composed with Factory ↓σFL , the adapted

Compositional Design, Implementation, and Verification of Swarms (Technical Report)

pos!

pos! ? Req

t par

2 pos? closingTime?

MFL

clo

sin

gTi m

tRe

par

pos!

partReq?

partReq? pos?

partOK?

closingTime?

′ MFL || Warehouse ↓σFL

clo

sin

tRe par

gTi

me?

pos?

partOK?

c 4 losin

closingTime?

gTi

me?

′ ′ (MFL || Warehouse ↓σFL ) || Factory ↓σFL

Figure 12 How Def. 36 adapts the machine MFL = Warehouse ↓σFL to Warehouse || Factory.

machine loses the possibility in state 4 of awaiting another event of type partReq and looping to state 2: hence, in state 4, the adapted machine can only await and process an event of type closingTime. Using Algorithm 2, this final machine is added to the adapted swarm S W || F . Then, Algorithm 2 repeats this adaptation for every machine in S W and S F . ⋄ We can now state the correctness of our swarm composition procedure. (Proof in § F.) ▶ Theorem 38 (Correctness of swarm adaptation and composition). Let S be a swarm obtained by applying Algorithm 2 to swarms S 1 , . . . , S n , protocols G1 , . . . , Gn and subscriptions σ 1 , . . . , σ n . Then, S is eventually faithful to G1 || . . . || Gn . The key insight in the proof of Theorem 38 is that the subscription σ computed by Algorithm 1 includes all the events needed for the synchronization of the composed swarm. This ensures that each adapted machine is a correct projection of the composed swarm protocol. Therefore, a machine adapted from the input swarm S i will execute without desynchronising and diverging from other machines adapted from another input swarm S j (for i, j ∈ {1 . . . n} such that i ̸= j).

Implementation and Experiments

We now present our implementation of the theory in §§ 3–5. In § 6.1 we discuss how we extend the open source Actyx toolkit [4] to support branch-tracking machine semantics and machine adaptation (which are key elements of our compositional approach), and to statically verify our new, compositional well-formedness of swarm protocols. Then, in § 6.2 we benchmark different strategies for computing the subscriptions of composed swarms. Our implementation is availble in the companion artifact of this paper [26].

6.1

Branch Tracking, Adaptations, and New Verification Facilities

Branch Tracking and Adaptation. The machine-runner library [3] of the Actyx toolkit features a TypeScript API to program machine implementations. For instance, Fig. 3 yields the machine implementation of a machine M (defined according to Def. 17) for the role D of our Warehouse use case. The machine-runner library also helps instantiating and running machine implementations in a swarm using the Actyx middleware [1] which implements the log propagation mechanisms described in § 4.4. Let us discuss our extension of machine-runner. In order to support our new branch-tracking semantics (Def. 24), (1) we added a pointer e.lastup (“previous updating event”) to each event e, and (2) modified machine-runner to produce and access e.lastup . We also added new methods that automatically adapt machine implementations according to Def. 36. This allows developers to re-use and deploy existing machine implementations in composed swarms. For instance, to adapt the machine implementation door of role D in Fig. 3 to the composed swarm Warehouse || Factory, a programmer can simply invoke:

F. Furbach, L. Clorius, R. Kuhn, H. Melgratti, A. Scalas, and E. Tuosto

adaptedDoor = adaptMachine('D', listOfProtocols, 0, subscriptions, [door, s0])

The parameters to adaptMachine are the machine role D, a list of the swarm protocols in the composition, the index of Warehouse in that list, a well-formed (and automatically generated) subscription for the composition, and the original door machine with its initial state. New Static Verification Facilities. The Actyx toolkit can statically verify several properties through the machine-check [2] library. More precisely, machine-check can verify (i) the well-formedness (as defined in [41]) of a protocol G under a given subscription σ and (ii) whether the machine implementation of a role R of G emits and accepts events as specified by the projection of G ↓σR . We extended machine-check to verify our new well-formedness of protocol compositions (Definitions 2 and 12), and generate subscriptions for which a composition is well-formed (Algorithm 1). We also modified the machine-check projection code (which was based on [41]) to conform to our notion of projections in Def. 21. This enables (1) the static verification of machine implementations in composed swarm protocols, and (2) the automatic adaptation of previously-implemented machines to work correctly in a composed swarm.

6.2

Experiments on Compositional Subscription Computation

A key element for the correct composition of protocols and swarms is the availability of a subscription σ suitable for composition (required by Def. 31 and Theorem 32). We analyse the performance and trade-offs of Algorithm 1, which is instrumental for computing subscriptions suitable for swarm composition (cf. § 5). Algorithm 1 may compute a subscription larger than necessary, which may lead to nonoptimal performance in the deployed swarm. Therefore, we compare Algorithm 1 with a naive algorithm (available in § G) that computes the “exact” subscription by directly applying Def. 12. More precisely, this algorithm accepts a set {G1 , . . . , Gn } of composable protocols and a set of subscriptions {σ 1 , . . . , σ n }, expands the composed protocol according to Def. 2 and applies Def. 12 to produce the smallest σ ⊇ σ 1 , . . . , σ n for which G = G1 || . . . || Gn is σ-well-formed. As mentioned in § 3.3, the expansion of the composed protocol makes the time complexity of this algorithm exponential in the number of input protocols. Benchmark Selection and Experimental Setup. We created a benchmark consisting of 454 sets of randomly-generated swarm protocols. Each set consists of n swarm protocols G1 , . . . , Gn (with n ∈ {1, . . . , 10}) with up to 9 roles each; each role emits up to 9 event types. In order to cover a broad range of possible practical cases, the random generation produces variety of branching and looping patterns. Moreover, protocols Gi and Gi+1 share an interfacing role, for all i ∈ {1, . . . , n − 1}. All randomly-generated protocols follow a pattern: two interfacing event types t1 and t2 may be separated by a random number of choices with non-interfacing event types, but t1 and t2 are always enabled in the same order in all protocols they occur in. The experiments were conducted by invoking both Algorithm 1 and our naive “exact” algorithm on empty input subscriptions: this is to compute the smallest possible output subscription for each protocol composition G1 || . . . || Gn . The execution times were measured using Criterion [24]; for each randomly-generated set of swarm protocols, Criterion invoked Algorithm 1 and the “exact” algorithm at least 50 times after 3 seconds of warm-up, reporting averages, medians, and standard deviations (including outliers).

Compositional Design, Implementation, and Verification of Swarms (Technical Report)

0.8

0.6

Efrac

107

Efrac

Time (µs, logarithmic scale)

0.4

101

102

103

104

105

Number of transitions in the composition (logarithmic scale) Exact

0.4

0.2

Exact

Alg. 1

Exact Alg. 1 [41]

Alg. 1

Figure 14 Boxplot showing the Figure 13 Execution times for generating wellaverage fraction of formed subscriptions, as a function of the number of events in the comtransitions in the composition. (AlmaLinux 9.5 on Intel puted subscriptions. Xeon Gold 6226R, 32GB of RAM; averages produced using Cri(Lower is better.) terion 0.7.0 [24] with sample size 50.)

Figure 15 Comparison of subscription sizes obtained using our definition of well-formedness and that of [41].

Results. Fig. 13 plots the execution time measured in our experiments against the number of transitions in the composition G1 || . . . || Gn ; note that the number of transitions grows exponentially in n. As expected, Algorithm 1 is faster and more scalable than the “exact” algorithm, which suffers from the exponential blow-up of the composition. For comparison, the generation of a subscription for a composition of protocols with ∼105 transitions takes ∼0.01 seconds using Algorithm 1 and ∼10 seconds using the “exact” algorithm. Notably, the trend shown in Fig. 13 persists even if we discount the time needed to expand the composition of the input protocols before invoking the “exact” algorithm: this is because the “exact” algorithm spends more time applying Def. 12 to generate a well-formed subscription for the expanded composition. Fig. 14 compares the accuracy of the two algorithms, measured as the fraction of event types involved in the generated subscription σ. Specifically, Efrac is the fraction of all event types subscribed to by a role in σ on average across all roles. For instance, Efrac = 0.2 means that, on average, a role subscribes to one out of five event types, while Efrac = 1.0 means that all roles subscribe to every event type. In general, a lower Efrac means less subscriptions and a higher degree of concurrency, leading to a swarm with smaller and more efficient machines. The plot shows that the “exact” algorithm requires roles to subscribe to ∼22.4% of all event types in the input protocols. Algorithm 1 requires subscribing to ∼29.9% of the event types, which is quite close to the “exact” algorithm. The difference occurs because Algorithm 1 may not see that parts of the input protocols become unreachable in the composition, and thus, may produce redundant subscriptions to some updating event types; also, Algorithm 1 adds interfacing event types to subscriptions (even when not required by well-formedness). This is necessary to ensure correct machine adaptation without expanding the composed protocol.

Comparing Subscription Sizes with Those of [41]. In § 2.2 we mentioned that the wellformedness definition of [41] may lead to larger subscriptions than necessary, especially compared to our Def. 12 and Algorithm 1. We now quantify this claim experimentally. Fig. 15 compares the sizes of minimal well-formed subscriptions obtained using our definition of well-formedness (Def. 12) and that of [41] for 2093 randomly generated swarm protocols. Since [41] does not support concurrent events, these 2093 protocols contain no compositions and no concurrency. As a consequence, the minimal subscriptions that ensure well-formedness (for both [41] and our Def. 12) are expected to be larger than those in Fig. 14. The plot in Fig. 15 shows that our Def. 12 and Algorithm 1 require roles to subscribe to ∼47.6% of all

F. Furbach, L. Clorius, R. Kuhn, H. Melgratti, A. Scalas, and E. Tuosto

event types in the input protocols on average, whereas [41] requires ∼70.8%.10 Fig. 15 also shows that, for non-concurrent protocols, Algorithm 1 yields the same output subscriptions as the “exact” algorithm: this is because the protocols contain no interfacing event types, nor do they exhibit behaviour restrictions like those in Example 4.

Related Work

This work embraces the research path taken in [41], advocating local-first cooperation [39, 38] in the design, analysis, and development of distributed applications modelled as swarms of machines, using swarm protocols as a specification language. We tackle the problem of compositional design and verification of swarms – which was left open in [41] and, to the best of our knowledge, is not addressed elsewhere. The importance of modularisation for managing software complexity has been well established since early work [45]: separate parts of a system should be composed via well-defined interfaces that hide implementation details between components. We accomplish this using interfacing roles (Def. 1) whose emitted events act as the glue that binds different swarm protocols and swarms into larger ones. Technical Differences w.r.t. [41]. Besides introducing our new compositionality results, in this work we simplify the theory of [41] aligning it to the common usages of the open source Actyx toolkit [4], without reducing the expressiveness of the model: The grammar in Def. 17 is as in [41], except that we do not explicitly model the “commands” a machine performs when emitting events: we assume a 1:1 correspondence between events and commands, leaving the latter implicit. Moreover, our transitions range over single event types instead of finite non-empty sequences of event types. In Def. 27, our rule Local simplifies the corresponding rule in [41]: since we have a 1:1 correspondence between events and commands, the shuffling operator of [41] is unnecessary. Also, our rule Global simplifies the corresponding rule in [41].11 A key challenge of our compositional approach, compared to the “monolithic” approach of [41], is that in the monolithic setting, the eventual fidelity of a machine M is only ensured if M knows and accepts the guard event for every command that precedes M’s event emissions – and this, in our one-event-per-command setting, would mean that M must know and accept all events that precede M’s emissions. However, in our composed swarms, a machine M projected from one swarm protocol may encounter events produced by other machines and protocols that M did not originally anticipate. To address this, our revised machine semantics (§ 4.3) tracks event causality more precisely, requiring a machine M that plays role R to accept only those events that can affect R’s behaviour. This is achieved via updating event types and our improved swarm semantics (Def. 27): each event carries minimal causal information,

In Fig. 15, the “exact” and Alg. 1 boxplot both contain two outliers with Efrac = 1, greater than all values in the boxplot for [41]. These are two very small protocols with a choice where a role R only appears in one of the branches. In this case, our Def. 12 requires R to subscribe to event types in all branches of the choice, whereas [41] only requires R to subscribe to the branch where R participates. As a result, our Def. 12 requires additional subscriptions for such cases – but it also provides a stronger guarantee w.r.t. [41]: a machine playing role R can determine if the swarm is following a branch of the swarm protocol where R is not involved. 11 More specifically, the closure property imposed on the sub-log l ′ in [41] is not necessary in this work. This is because we do not need to ensure that for each event e in the global log l emitted by a machine of a swarm S, say S(j), l includes each event e ′ that precedes e in the local log of S(j).

Compositional Design, Implementation, and Verification of Swarms (Technical Report)

i.e., a pointer to the last relevant updating event observed by the emitting machine. This allows a machine to decide whether to accept or ignore an event. The main result of [41] is that any swarm S that realises a well-formed G is eventually faithful to G; we generalise this result to composed swarms and protocols in §§ 4.5 and 5.2.

Global Types and Behavioural Types. Swarm protocols are inspired by global types, a.k.a. choreographies [33, 34]; they describe multiparty interaction pattern from a global point of view, and they can be projected onto roles to obtain local specifications, against which one can check the correctness of implementations. The literature on global types includes compositional approaches: e.g., partial choreographies that can be composed while preserving deadlock-freedom [43], and choreography refinement to replace part of a choreography with a more complex one [21]. However, the highly dynamic and non-deterministic semantics of swarms is significantly different from the semantics in global types literature. When compared to the literature on behavioural types [27, 35, 6], our approach and [41] depart from the usual assumptions in several key ways. Standard behavioural typing approaches ensure all interacting components are aware of the current state of the distributed computation. In contrast, we allow inconsistencies between machines to emerge, as long as consistency is eventually achieved [15]: e.g., machines can make transient discordant choices that are reconciled as the logs propagate in the swarm. This is akin to data replication methods, where there is a trade-off between availability, consistency, and partition tolerance [29]. Several approaches have emerged to balance this trade-off, including conflict-free replicated data types [48], cloud types [16], consistency contracts [50], invariants [31, 37, 8], linearizability [52], and operational models for applications such as GSP [17, 30]; a key difference in our approach lies in how we achieve eventual consistency, and how we introduce compositional mechanisms. Moreover, in standard behavioural type sytems, the variability in the number of participants has been addressed via parametricity, e.g. in multiparty session types [53, 22, 23, 18, 36]: this requires explicit handling of the parameters of the protocol. Instead, swarm protocols do not restrict the number of instances playing a given role. In behavioural types literature, most compositional approaches require component protocols to be aware that they are part of a composition: e.g. hybrid types [28] distinguish inter-component interactions from intra-component interactions; other approaches allow composition via open endpoints [43, 51]. An approach closer to ours is Participants-as-Interfaces (PaI) [10, 12, 13, 11, 14], where interfaces are defined by roles that perform complementary behaviours. Like us, PaI allows viewing a closed system as an open one – but PaI uses complementary roles as forwarders to connect protocols, whereas our interfacing roles simply play their roles and do not act as forwarders.

Choreographic Programming Languages [42] differ from swarm protocols in both goals and approach. Choreographic programs provide a global implementation of communicating roles via point-to-point messages, with notions of compositionality inspired by programming languages theory (e.g., higher-order choreographic programs [49, 20]). Swarm protocols and projected machines, by contrast, serve as specifications only: machines are implemented and checked separately, e.g., using the Actyx toolkit. Moreover, machines operate under asynchronous, subscription-based event propagation, with possible event reordering and machine replication. These goals and semantics are significantly different from choreographic programming languages, and thus, they lead to a different notion of composition.

F. Furbach, L. Clorius, R. Kuhn, H. Melgratti, A. Scalas, and E. Tuosto

Conclusion and Future Work

We have presented novel results on the compositional verification and implementation of swarms and swarm protocols. Our results enable the compositional verification of swarm systems, as well as the reuse of the implementations of swarm machines in larger composed systems. This enables a compositional swarm design process, as well as the seamless extension of existing swarm systems with new functionality. We believe our novel compositionality results can be applied to other local-first distributed systems. We have implemented our results in a custom version of the open source Actyx toolkit for swarm application development [4], thus enabling the compositional design and implementation of swarms in practice. We have also streamlined the swarm protocol theory presented in [41], while aligning it with the observed use of Actyx tools in the real world. Future Work. Swarms and machines have some similarity with actor systems [32, 5] (asynchronous communication, replication) but differ significantly in their semantics (out-oforder event propagation). We are not aware of specific work on the composition of actor systems – although the communicating finite-state machines used in [12, 13, 14] have analogies with actors (message buffers can be seen as a form of mailbox), hence their approach to compositionality may be applicable to actors. This is a valuable area of study, and we will investigate whether our compositionality results can be applied to actor systems. Currently, our method of composing protocols and swarms (Algorithms 1 and 2) and our correctness result (Theorem 38) are limited to compositions of sequential protocols without internal concurrency: i.e., we support compositions of the form G1 || . . . || Gn where each Gi is a sequential protocol (by Def. 14) – and this allows us to reuse and compose all swarm protocols that are well-formed according to [41], and all machines projected from such protocols. However, we do not currently support arbitrary compositions of concurrent protocols, like e.g. (G1 || G2 ) || (G3 || G4 ). To address this limitation, we plan to build upon our results and generalise them to design a full-fledged module system for swarm development. We will also study better compositional methods for the computation of subscriptions and the minimisation of swarm machines, in order to improve the precision of our Algorithm 1 (measured in § 6.2) without losing scalability for larger swarms. References 1 2 3 4 5 6

Actyx AG. Actyx decentralized event database, streaming and processing engine, 2024. URL: https://github.com/Actyx/Actyx. Actyx AG. @actyx/machine-check library, 2024. accessed 13-12-2024. URL: https://www. npmjs.com/package/@actyx/machine-check. Actyx AG. @actyx/machine-runner library, 2024. accessed 13-12-2024. URL: https://www. npmjs.com/package/@actyx/machine-runner. Actyx AG. Actyx developer website. https://developer.actyx.com, 2024. [Online; accessed on 29 October 2024]. Gul Agha. Actors: A Model of Concurrent Computation in Distributed Systems. The MIT Press, 12 1986. doi:10.7551/mitpress/1086.001.0001. Davide Ancona, Viviana Bono, Mario Bravetti, Joana Campos, Giuseppe Castagna, PierreMalo Deniélou, Simon J Gay, Nils Gesbert, Elena Giachino, Raymond Hu, et al. Behavioral types in programming languages. Foundations and Trends in Programming Languages, 3(23):95–230, 2016. Ozalp Babaoglu and Keith Marzullo. Consistent global states of distributed systems: Fundamental concepts and mechanisms. Distributed Systems, 53, 1993.

Compositional Design, Implementation, and Verification of Swarms (Technical Report)

Valter Balegas, Sérgio Duarte, Carla Ferreira, Rodrigo Rodrigues, and Nuno M. Preguiça. IPA: invariant-preserving applications for weakly consistent replicated databases. Proc. VLDB Endow., 12(4):404–418, 2018. URL: http://www.vldb.org/pvldb/vol12/p404-balegas.pdf, doi:10.14778/3297753.3297760.

Stephanie Balzer, Marco Carbone, Roland Kuhn, and Peter Thiemann. Next generation protocols for heterogeneous systems (dagstuhl seminar 24051). Dagstuhl Reports, 14(1):108– 129, 2024. doi:10.4230/DAGREP.14.1.108.

Franco Barbanera, Ugo de’Liguoro, and Rolf Hennicker. Connecting open systems of communicating finite state machines. J. Log. Algebraic Methods Program., 109, 2019. URL: https://doi.org/10.1016/j.jlamp.2019.07.004, doi:10.1016/J.JLAMP.2019.07.004.

Franco Barbanera, Mariangiola Dezani-Ciancaglini, Lorenzo Gheri, and Nobuko Yoshida. Multicompatibility for multiparty-session composition. In Proceedings of the 25th International Symposium on Principles and Practice of Declarative Programming, pages 1–15, 2023.

Franco Barbanera, Mariangiola Dezani-Ciancaglini, Ivan Lanese, and Emilio Tuosto. Composition and decomposition of multiparty sessions. J. Log. Algebraic Methods Program., 119:100620, 2021. URL: https://doi.org/10.1016/j.jlamp.2020.100620, doi:10.1016/J.JLAMP.2020. 100620.

Franco Barbanera, Ivan Lanese, and Emilio Tuosto. On composing communicating systems. In Clément Aubert, Cinzia Di Giusto, Larisa Safina, and Alceste Scalas, editors, Proceedings 15th Interaction and Concurrency Experience, ICE 2022, Lucca, Italy, 17th June 2022, volume 365 of EPTCS, pages 53–68, 2022. doi:10.4204/EPTCS.365.4.

Franco Barbanera, Ivan Lanese, and Emilio Tuosto. Composition of synchronous communicating systems. J. Log. Algebraic Methods Program., 135:100890, 2023. URL: https: //doi.org/10.1016/j.jlamp.2023.100890, doi:10.1016/J.JLAMP.2023.100890.

Sebastian Burckhardt. Principles of eventual consistency. Found. Trends Program. Lang., 1(1–2):1–150, oct 2014. doi:10.1561/2500000011.

Sebastian Burckhardt, Manuel Fähndrich, Daan Leijen, and Benjamin P. Wood. Cloud types for eventual consistency. In James Noble, editor, ECOOP 2012 – Object-Oriented Programming, pages 283–307, Berlin, Heidelberg, 2012. Springer.

Sebastian Burckhardt, Daan Leijen, Jonathan Protzenko, and Manuel Fähndrich. Global Sequence Protocol: A Robust Abstraction for Replicated Shared State. In John Tang Boyland, editor, 29th European Conference on Object-Oriented Programming (ECOOP 2015), volume 37 of Leibniz International Proceedings in Informatics (LIPIcs), pages 568–590, Dagstuhl, Germany, 2015. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik. URL: http: //drops.dagstuhl.de/opus/volltexte/2015/5238, doi:10.4230/LIPIcs.ECOOP.2015.568.

David Castro-Perez, Raymond Hu, Sung-Shik Jongmans, Nicholas Ng, and Nobuko Yoshida. Distributed programming using role-parametric session types in go: statically-typed endpoint apis for dynamically-instantiated communication structures. Proc. ACM Program. Lang., 3(POPL):29:1–29:30, 2019. doi:10.1145/3290342.

Bruno Courcelle. Fundamental properties of infinite trees. Theor. Comput. Sci., 25:95–169, 1983. doi:10.1016/0304-3975(83)90059-2.

Luís Cruz-Filipe, Eva Graversen, Lovro Lugović, Fabrizio Montesi, and Marco Peressotti. Modular Compilation for Higher-Order Functional Choreographies. In 37th European Conference on Object-Oriented Programming (ECOOP 2023), volume 263 of Leibniz International Proceedings in Informatics (LIPIcs), pages 7:1–7:37, 2023. doi:10.4230/LIPIcs.ECOOP.2023.7.

Ugo de’Liguoro, Hernán Melgratti, and Emilio Tuosto. Towards refinable choreographies. Journal of Logical and Algebraic Methods in Programming, 127:100776, 2022. doi:10.1016/j. jlamp.2022.100776.

Pierre-Malo Deniélou and Nobuko Yoshida. Dynamic multirole session types. In Thomas Ball and Mooly Sagiv, editors, POPL, pages 435–446. ACM, 2011. doi:10.1145/1926385.1926435.

F. Furbach, L. Clorius, R. Kuhn, H. Melgratti, A. Scalas, and E. Tuosto

24 25

27 28

34 35

Pierre-Malo Deniélou, Nobuko Yoshida, Andi Bejleri, and Raymond Hu. Parameterised multiparty session types. Log. Methods Comput. Sci., 8(4), 2012. doi:10.2168/LMCS-8(4: 6)2012. Criterion Developers. Criterion documentation, 2025. Accessed 18-02-2026. URL: https: //docs.rs/criterion/0.7.0/criterion. Patrick Th. Eugster, Pascal A. Felber, Rachid Guerraoui, and Anne-Marie Kermarrec. The many faces of publish/subscribe. ACM Comput. Surv., 35(2):114–131, June 2003. doi: 10.1145/857076.857078. Florian Furbach, Lucas Clorius, Roland Kuhn, Hernán Melgratti, Alceste Scalas, and Emilio Tuosto. Compositional design, implementation, and verification of swarms: Artifact, 2026. doi:10.5281/zenodo.18459720. Simon Gay and Antonio Ravara, editors. Behavioural Types: from Theory to Tools. Automation, Control and Robotics. River, 2009. Lorenzo Gheri and Nobuko Yoshida. Hybrid multiparty session types: Compositionality for protocol specification through endpoint projection. Proc. ACM Program. Lang., 7(OOPSLA), April 2023. doi:10.1145/3586031. Seth Gilbert and Nancy Lynch. Brewer’s conjecture and the feasibility of consistent, available, partition-tolerant web services. SIGACT News, 33(2):51–59, June 2002. URL: http://doi. acm.org/10.1145/564585.564601, doi:10.1145/564585.564601. Alexey Gotsman and Sebastian Burckhardt. Consistency Models with Global Operation Sequencing and their Composition. In Andréa W. Richa, editor, 31st International Symposium on Distributed Computing (DISC 2017), volume 91 of Leibniz International Proceedings in Informatics (LIPIcs), pages 23:1–23:16, Dagstuhl, Germany, 2017. Schloss Dagstuhl–LeibnizZentrum fuer Informatik. URL: http://drops.dagstuhl.de/opus/volltexte/2017/7974, doi:10.4230/LIPIcs.DISC.2017.23. Alexey Gotsman, Hongseok Yang, Carla Ferreira, Mahsa Najafzadeh, and Marc Shapiro. ’Cause i’m strong enough: reasoning about consistency choices in distributed systems. In POPL 2016, pages 371–384, 2016. Carl Hewitt, Peter Bishop, and Richard Steiger. A universal modular actor formalism for artificial intelligence. In Proceedings of the 3rd International Joint Conference on Artificial Intelligence, IJCAI’73, page 235–245, San Francisco, CA, USA, 1973. Morgan Kaufmann Publishers Inc. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. In Proceedings of the 35th annual ACM SIGPLAN-SIGACT Symposium on principles of programming languages, pages 273–284, 2008. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. Journal of the ACM (JACM), 63(1):1–67, 2016. Hans Hüttel, Ivan Lanese, Vasco T. Vasconcelos, Luís Caires, Marco Carbone, Pierre-Malo Deniélou, Dimitris Mostrous, Luca Padovani, António Ravara, Emilio Tuosto, Hugo Torres Vieira, and Gianluigi Zavattaro. Foundations of session types and behavioural contracts. ACM Comput. Surv., 49(1):3:1–3:36, 2016. Sung-Shik Jongmans and Nobuko Yoshida. Exploring type-level bisimilarity towards more expressive multiparty session types. In Peter Müller, editor, Programming Languages and Systems, pages 251–279, Cham, 2020. Springer International Publishing. Gowtham Kaki, Kapil Earanky, KC Sivaramakrishnan, and Suresh Jagannathan. Safe replication through bounded concurrency verification. Proceedings of the ACM on Programming Languages, 2(OOPSLA):1–27, 2018. Martin Kleppmann, Adam Wiggins, Peter van Hardenberg, and Mark McGranaghan. Local-first software: You own your data, in spite of the cloud. In Proceedings of the 2019 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software, Onward! 2019, page 154–178, New York, NY, USA, 2019. Association for Computing Machinery. doi:10.1145/3359591.3359737.

Compositional Design, Implementation, and Verification of Swarms (Technical Report)

42 43

45 46 47 48

50 51 52

Roland Kuhn. Local-first cooperation: Autonomy at the edge, secured by crypto, 100% available. https://www.infoq.com/articles/local-first-cooperation/, 2021. [Online; accessed on 29 October 2024]. Roland Kuhn and Alan Darmasaputra. Behaviorally typed state machines in typescript for heterogeneous swarms. In Proceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2023, page 1475–1478, New York, NY, USA, 2023. Association for Computing Machinery. doi:10.1145/3597926.3604917. Roland Kuhn, Hernán C. Melgratti, and Emilio Tuosto. Behavioural types for local-first software. In Karim Ali and Guido Salvaneschi, editors, 37th European Conference on ObjectOriented Programming, ECOOP 2023, July 17-21, 2023, Seattle, Washington, United States, volume 263 of LIPIcs, pages 15:1–15:28. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. doi:10.4230/LIPICS.ECOOP.2023.15. Fabrizio Montesi. Introduction to Choreographies. Cambridge University Press, 2023. doi: 10.1017/9781108981491. Fabrizio Montesi and Nobuko Yoshida. Compositional choreographies. In Pedro R. D’Argenio and Hernán C. Melgratti, editors, CONCUR 2013 - Concurrency Theory 24th International Conference, CONCUR 2013, Buenos Aires, Argentina, August 27-30, 2013. Proceedings, Lecture Notes in Computer Science, pages 425–439. Springer, 2013. doi:10.1007/978-3-642-40184-8\_30. D Stott Parker, Gerald J Popek, Gerard Rudisin, Allen Stoughton, Bruce J Walker, Evelyn Walton, Johanna M Chow, David Edwards, Stephen Kiser, and Charles Kline. Detection of mutual inconsistency in distributed systems. IEEE transactions on Software Engineering, (3):240–247, 1983. David Lorge Parnas. On the criteria to be used in decomposing systems into modules. Communications of the ACM, 15(12):1053–1058, 1972. Benjamin C. Pierce. Types and programming languages. MIT Press, 2002. Fred B. Schneider. Implementing fault-tolerant services using the state machine approach: A tutorial. ACM Comput. Surv., 22(4):299–319, 1990. doi:10.1145/98163.98167. Marc Shapiro, Nuno M. Preguiça, Carlos Baquero, and Marek Zawirski. Conflict-free replicated data types. In SSS 2011, pages 386–400, 2011. URL: http://dx.doi.org/10.1007/ 978-3-642-24550-3_29, doi:10.1007/978-3-642-24550-3_29. Gan Shen, Shun Kashiwa, and Lindsey Kuper. HasChor: Functional Choreographic Programming for All. Proceedings of the ACM on Programming Languages, 7(ICFP):541–565, 2023. doi:10.1145/3607849. KC Sivaramakrishnan, Gowtham Kaki, and Suresh Jagannathan. Declarative programming over eventually consistent data stores. In PLDI 2015, pages 413–424. ACM, 2015. Claude Stolze, Marino Miculan, and Pietro Di Gianantonio. Composable partial multiparty session types for open systems. Software and Systems Modeling, 22(2):473–494, 2023. Chao Wang, Constantin Enea, Suha Orhun Mutluergil, and Gustavo Petri. Replicationaware linearizability. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 980–993, 2019. Nobuko Yoshida, Pierre-Malo Deniélou, Andi Bejleri, and Raymond Hu. Parameterised multiparty session types. In C.-H. Luke Ong, editor, Foundations of Software Science and Computational Structures, 13th International Conference, FOSSACS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings, volume 6014 of Lecture Notes in Computer Science, pages 128–145. Springer, 2010. doi:10.1007/978-3-642-12032-9\_10.

F. Furbach, L. Clorius, R. Kuhn, H. Melgratti, A. Scalas, and E. Tuosto

Appendices A

Proof of Theorem 16

Algorithm 1 makes use of a key insight: the function subscribers overapproximates roles. We now outline the reasoning behind this insight and formalise it below in Lemma 39. t0 l1 ·t1 ln ·tn Suppose R ∈ roles(t, G, σ). By Def. 10 there is a path G −→ −−−→ . . . −− −→ such that t = t0 , tn ∈ σ(R), and ti , ti+1 are not concurrent for all i < n. Whenever two consecutive (and thus non-concurrent) event types ti and ti+1 along the path above belong to different input swarm protocols, the corresponding path segment li+1 must include a sequence of interfacing event types t′1 , . . . , t′m that enforce their order: i.e., li+1 = l′1 · t′1 · . . . l′n′ · t′n′ · l′n′ +1 . We take the sequence t1 . . . tn−1 and, for each such case, replace ti · ti+1 with the sequence ti · t′1 . . . t′n′ . This yields a new sequence t′′1 . . . t′′n′′ where adjacent events from different protocols are guaranteed to be interfacing. If we now discard any non-interfacing event ′′′ type from t′′1 . . . t′′n′′ , we obtain a sequence t′′′ 1 . . . tn′′′ consisting solely of interfacing event types. Since tn ∈ σ(R), by iteratively applying the Interfacing rule we get t′′′ n′′′ ∈ σ(R), ′′′ ′′′ t′′′ ∈ σ(R), . . ., t ∈ σ(R). Since the first event t and t belong to the same protocol, ′′′ 1 1 n −1 t

say Gi , we have R ∈ subscribers(G′i , σ) for some G′i ⊑ Gi with G′i − →. Therefore we conclude t that whenever R ∈ roles(t, G, σ), then R ∈ subscribers(G′i , σ) (for some G′i ⊑ Gi with G′i − →). We express this as a technical lemma: ▶ Lemma 39. We apply Algorithm 1. Assume R ∈ roles(t, G′ , σ) for some G′ ⊑ G = G1 || . . . || Gn and G′ = G′1 || . . . || G′n where G′i ⊑ Gi for i ≤ n. It holds R ∈ subscribers(t, G′i ) t for any i ≤ n with G′i − →. t

0 1 1 n n Proof of Lemma 39. Since R ∈ roles(t, G′ , σ), there is a path G′ −→ −→ −→ . . . −→ −→ in the composition G such that t = t0 , tn ∈ σ(R), and ti , ti+1 are not concurrent for i < n. We now show that we can assume WLOG that t1 . . . tn−1 are interfacing event types such that ti , ti+1 occur in the same swarm protocol for i < n. Assume, towards contradiction, that this is not the case. This means that there are ti , ti+1 that do not occur in the same swarm protocols and they are not both interfacing. Further, there are no event types in li+1 that can be added to the sequence t1 . . . tn−1 . After-all, if there were some we could add, then we could keep adding those event types to the sequence until all pairs from different protocols are interfacing. Since there are no elements in li+1 that can be added, this means there is no chain of pairwise non-concurrent event types in li+1 that starts with ti and ends in ti+1 . Thus, we can rearrange the path (by moving event types from li+1 directly before ti or directly after ti+1 ) such that ti and ti+1 are next to each other. According to the definition of swarm protocol composition, these two non-interfacing event types from different protocols are concurrent. This is a contradiction. This means whenever ti , ti+1 are from different protocols, then they are interfacing. If ti is non-interfacing, this means ti−1 and ti+1 occur in the same swarm protocol as ti and thus they are non-concurrent with each other. This means we can safely remove ti from the sequence t1 . . . tn−1 . We can safely remove all non-interfacing event types and then our WLOG assumption holds.

tn−1 ln−1 t

n Since tn−1 , tn occur in the same swarm protocol, say Gj , and G has a path −−−→−−−→−→

′ tn−1

that means there are G′ , G′′ ⊑ Gj such that G −−−→ G′′ , tn ∈ G′′ , and tn ∈ σ(R). It follows R ∈ subscribers(G′′ , σ). Recall, that t1 . . . tn−1 are interfacing. The Interfacing rule ensures tn−1 ∈ σ(R). We iterate this application of the Interfacing rule to get t1 ∈ σ(R).

Compositional Design, Implementation, and Verification of Swarms (Technical Report)

Assume t is not interfacing. This means it occurs only in one swarm protocol Gi . Then t1 ∈ σ(R) together with t1 occurs in G′i , ensures that R ∈ subscribers(G′i , σ). If t is interfacing, then t and t1 occur together in some swarm protocol. In this case, the Interfacing rule ensures t ∈ σ(R) and thus R ∈ subscribers(G′i , σ) for any i ≤ n with t G′i − →. ◀ Recall that we call those looping event type that satisfies the looping condition in Determinacy and are thus chosen as updating event types looping in σ. Proof of Theorem 16. To prove that G = G1 || . . . || Gn is σ-well-formed, we verify the following conditions: (1) confusion-freeness, (2) causal consistency, and (3) determinacy. It is easy to see that confusion-freeness (Def. 5) holds: Property (1) holds since G1 || . . . || Gn are confusion-free and interfacing. Properties (2) and (3) hold since the swarm protocol composition preserves these properties. Causal consistency is enforced by the Causal Consistency rule. We now verify that determinacy (Def. 10) holds by examining each condition that determinacy requires. Branching. Assume t is branching with t′ at G′ ⊑ G. It holds G′ = G′1 || . . . || G′n where G′i ⊑ Gi for i ≤ n and there is an i ≤ n where t branches with t′ at G′i . Thus they are not in conc. Since t and t′ are not concurrent, but both are outgoing transitions of G′ , Def. 2 (Swarm Protocol Composition) ensures there is some Gi with i ≤ n that they both occur in. For any R ∈ roles(t, G′ , σ), Lemma 39 ensures R ∈ subscribers(G′i , σ) and thus the Branching rule sets t, t′ ∈ σ(R). Joining. Assume towards contradiction that the Joining condition is not satisfied. Then tb ta t there are Ga , Gb , Gc , Gd ⊑ G with Ga −→ Gb − → Gc , Gd −→ Gb , ta and tb are concurrent but not concurrent with t and R ∈ roles(t, Gb , σ) and {ta , tb , t} ̸⊆ σ(R). It holds that since t ta ta and t are not concurrent, then it is not the case that: Ga − →−→ Gc . According to the composition of swarm protocols, this means that there is a Gi such that ta , t ∈ Gi and thus ta t {ta , t} ̸∈ conc. Further, there is a G′i ⊑ Gi such that G′i −→ − →. Analogue, we argue there is a t t b ′ ′ Gj ⊑ Gj such that Gj −→− → and thus {tb , t} ̸∈ conc. Since conc is an overapproximation of concurrent event types, it holds {ta , tb } ∈ conc. This means there is a role R ∈ roles(t, Gb , σ) t but there is no corresponding G′j ⊑ Gj with j ≤ n, G′j − →, and R ∈ subscribers(G′j , σ). This is a contradiction to Lemma 39. Looping. Assume towards contradiction that the Looping condition is not satisfied. Then l there is a G′ ⊑ G with G′ − → G′ wit l being non-empty and G′ has no looping update. Let G′ = (G′1 || . . . || G′n ). According to the composition of swarm protocols, this means that there l′

is an i ≤ n such that G′i −→ G′i and ϵ ⊂ l′ ⊆ l. If l contains an interface event type, then the interfacing rule ensures that this is a looping update. If l contains no interface event type, then neither does l′ . If G′i contains branching event types, then at least one of those event types remains in l′ , even if it may be no longer branching. We argued in paragraph Branching that the remaining one is in the necessary subscriptions to be a looping update. This is a contradiction. If G′i contains no branching event types, then Step 3 picks an event type t ∈ l′ and ensures t ∈ σ(R) for all R ∈ subscribers(G, σ). Since the looping condition is not satisfied by t, that means R ∈ roles(t, G′ , σ) but not R ∈ subscribers(G′i , σ). This is a contradiction, the argument is analogue to branching. ◀

F. Furbach, L. Clorius, R. Kuhn, H. Melgratti, A. Scalas, and E. Tuosto

Proof of Lemma 23

We introduce the concept of causal dependency between event types which is implicitly used by the function roles(t, G, σ). ▶ Definition 40 (Definition: causal dependency). An event type t′ is causally dependent on t in G if there exists a sequence of transitions t

l ·t

0 1 1 n n G −→ −− −→ . . . −− −→

where t0 = t, tn = t′ , and ti , ti+1 are not concurrent for all i < n. A role R is in the set roles(t, G, σ) if and only if there exists an event t′ in G that is causally dependent on t and that R subscribes to.

Proof of Lemma 23 by Contradiction Given a swarm protocol G, a subscription σ such that G is well-formed w.r.t. σ and a role R, we will prove that all projections of G onto R for σ behave identically. Assume, for contradiction, that there exist two distinct correct projections M 1 and M 2 such that: A: M 1 and M 2 receive different log types, or B: They emit different event types after receiving the same log type. We analyze these two cases separately.

Case A: Different Log Types. There is a shortest sequence of event types t1 , . . . , tn , t such that: t ?

t ?

1 n M 1 = G ↓σR −− → G1 ↓σR . . . −− → Gn ↓σR 1 n M 2 = G ↓σR −− → G′1 ↓σR . . . −− → G′n ↓σR

−→

Gn+1 ↓σR

̸→ −

We show that this is not the case.

Induction Hypothesis: It holds that for any pairs of sequences t ?

t ?

1 n G ↓σR −− → G1 ↓σR . . . −− → Gn ↓σR

−→ Gn+1 ↓σR

(1)

t1 ? tn ? G ↓σR −− → G′1 ↓σR . . . −− → G′n ↓σR

(2) t?

there is a G′n+1 such that we can append a transition G′n ↓σR −→ G′n+1 ↓σR to Sequence (2). We apply an induction over the length of the sequences n:

Induction Basis n = 0: Consider: G ↓σR

−→ G2 ↓σR

G ↓σR t?

It follows immediately that we can append a transition G ↓σR −→ G2 ↓σR , since it is the same projection.

Compositional Design, Implementation, and Verification of Swarms (Technical Report)

Induction Step (n − 1) → n: It follows from the definition of projections and from the Sequences 1 and 2, that t1 , . . . , tn , t is the shortest series of event types such that: ta,1

ta,k

tb,1

tb,m

1 n G −−→ Ga,1 . . . −−→ Ga,k −→ G1 . . . −→ Gn

tc,1 ...tc,l

−−−−−−→ Gc,l − → Gn+1

G −−→ Gb,1 . . . −−−→ Gb,m −→ G′1 . . . −→ G′n

(3) (4)

and the only event types in Sequence 3 and 4 that occur in σ(R) are t1 , . . . , tn , t. We assume WLOG that Sequence 3 is minimal, meaning the maximal subsequence of Sequence 3 that can be removed while still maintaining a valid path in the swarm protocol with t1 and t was removed. For readability, we write Sequence 3 as: ta,k t

ta,1

tc,l t

tc,1

1 n G −−→ . . . −−→−→ . . . −→ −−→ . . . −−→− →

We will now show that we can apply a series of changes to Sequence 3 that ensure that it has a prefix that is identical to Sequence 4. Let x be the smallest index such that ta,x ̸= tb,x (assuming it exists). Case A1. There is a ti,j in Sequence 3 such that it is the first occurence of event type tb,x after ta,x : ta,1

ta,x

ti,j

G −−→ . . . −−→ . . . −−→ . . . − → Since x is the smallest index where the sequences diverge, it holds Ga,(x−1) = Gb,(x−1) . Argument for Concurrency. Since both transitions ta,x and tb,x are outgoing from Ga,(x−1) = Gb,(x−1) and R does not subscribe to at least one of the event types, it follows that either the event types ta,x and tb,x are concurrent with each other or they are branching. If they are branching, then determinacy requires that they do not satisfy condition R ∈ roles(ta,x , Ga,(x−1) , σ) of Definition 10.Thus, t is not causally dependent on ta,x : There is no subsequence of Sequence 3 starting at ta,x and ending at t where each event type is non-concurrent with its successor (see definition of roles(t, G, σ) in Def. 10). This means we can move ta,x and all events that are causally dependent on it after t. This means ta,x can be removed. This is a contradiction to the sequence being minimal. Thus, the event types are concurrent. Since tb,x is concurrent with ta,x and they are both outgoing from Ga,(x−1) = Gb,(x−1) , ta,x

tb,x

this means Ga,(x−1) −−→ Ga,(x) −−→. Thus, tb,x and ta,x+1 are both outgoing from Ga,(x) . We can apply the Argument for Concurrency, which means they are concurrent. We iteratively apply this argument to show that tb,x is concurrent with every event type between ta,x and ti,j in Sequence 3. It follows that we can move ti,j directly before ta,x and still get a valid interleaving: ta,1 ti,j ta,x t G −−→ . . . −−→−−→ . . . − → Case A2. tb,x does not occur in Sequence 3 after ta,x : Here, we can apply the Argument for Concurrency from Case A1 and show that tb,x is concurrent with every event type after ta,x in Sequence 3. This means we can append tb,x at the end of the sequence: ta,1

ta,x

t tb,x

G −−→ . . . −−→ . . . − →−−→ . Since it is concurrent with ta,x and every event type afterwards in Sequence 3, we can move the appended tb,x directly before ta,x .

F. Furbach, L. Clorius, R. Kuhn, H. Melgratti, A. Scalas, and E. Tuosto

Conclusion. Each time we apply this change, the prefix of Sequence 3 that is equal to Sequence 4 gets one transition longer. We keep applying these changes until Ga,m = Gb,m . If no such diverging index existed, then this holds initially and no application were necessary. ta,m+1 ta,m+1 If the next transition is Ga,m −−−−→, then we move t1 directly before −−−−→ in Sequence 3, using the same concurrency argument as above. We have now adapted Sequence 3 such that it starts with the prefix tb,1

tb,m

1 G −−→ Gb,1 . . . −−−→ Gb,m −→ G′1

followed by a sequence

2 n G′1 . . . −→ G′′2 . . . −→ G′′n − → G′′n+1 .

Thus, we have constructed a sequence with a prefix that is equal to Sequence 4 until G′1 . We remove the prefix and get the following sequences for the series t2 . . . tn of length (n − 1): t ?

t ?

2 n G′1 ↓σR −− → . . . −− → G′′n ↓σR

−→ G′′n+1 ↓σR

(5)

2 n G′1 ↓σR −− → . . . −− → G′n ↓σR

(6) t?

We now apply the induction hypothesis to conclude that there is a G′n+1 with G′n ↓σR −→ t?

G′n+1 ↓σR . Since Sequence 8 also ends in G′n , we can append G′n ↓σR −→ G′n+1 ↓σR to it: t ?

t ?

1 n G ↓σR −− → G1 ↓σR . . . −− → Gn ↓σR

−→ Gn+1 ↓σR

(7)

t1 ? tn ? → G′1 ↓σR . . . −− → G′n ↓σR . G ↓σR −−

(8)

Case B: Emitting Different Event Types. We have shown that projections of the same swarm protocol receive the same log types. It remains to show that they can always emit the same set of event types after receiving the same log type. This is easy to see since the event types a projection can emit are determined by the events from its own role R that it can receive: Examine Gn ↓σR from Case A. It holds that Gn ↓σR emits event type t iff there is an R⟨t⟩ and some sequence ta,1 ta,m t Gn −−→ . . . −−−→ G′′ − → Gn+1 where R does not subscribe to any ta,1 . . . ta,m . This is the case iff there is an R⟨t⟩ and t?

Gn ↓σR −→. Since G′n ↓σR can receive the same event types, it follows G′n ↓σR −→ and thus G′n ↓σR can emit t.

Formal Definitions of Effective logs

To formally define eventual fidelity, we introduce the concept of effective global logs (Def. 41), obtained by filtering out all events e that have the wrong type according to G, or have the wrong pointer e.lastup ; to this end, Def. 41 defines a transition system of a swarm protocol with branch tracking, analogue to the transition systems of machines in Def. 24. t

▶ Definition 41 (Global effective log). Let e be of type t, e.lastup = lastup (t), and G − → G′ . e We extend the partial function − → to swarm protocols as follows: (1) if t is not updating then e e (G, lastup ) − → (G′ , lastup ); and (2) if t is updating, then (G, lastup ) − → (G′ , lastup [branch(t) 7→ e]).

Compositional Design, Implementation, and Verification of Swarms (Technical Report)

We define the global effective log filtering function eff(l, G, lastup ) as: eff(ϵ, G, lastup )

eff(e · l, G, lastup )

ϵ( e · eff(l, G′ , lastup ′ ) eff(l, G, lastup )

if (G, lastup ) − → (G′ , lastup ′ ) otherwise

Given a log l, we define the global effective log for G as eff(l, G) := eff(l, G, ∅). Similarly to Def. 41, the effective log of a machine M (Def. 42) only includes the events in a log that M actually accepts. e

▶ Definition 42 (Effective Log of a Machine). Using − → from Def. 24, we define the effective log filtering function eff(l, M, lastup ) for a machine M: eff(ϵ, M, lastup ) eff(e · l, M, lastup )

= =

ϵ(

e · eff(l, M ′ , lastup ′ )

if (M, lastup ) − → (M ′ , lastup ′ )

eff(l, M, lastup )

otherwise

Given a log l, we define the effective log for M as eff(l, M) := eff(l, M, ∅).

Proof of Eventual Fidelity

In order to prove eventual fidelity, we require some technical results: If an event e has type t, we say that R subscribes to e if t ∈ σ(R). e We define ((G, lastup ), ϵ) := (G, lastup ). If (G, lastup ) − → (G′ , lastup ′ ), then ((G, lastup ), e.l) := ((G′ , lastup ′ ), l), otherwise ((G, lastup ), e.l) := ((G, lastup ), l). We set (G, l) := ((G, ∅), l). We define the projection of a parameterized swarm protocol (G, lastup ) as the projection of the non-parameterized version of the swarm protocol G with the same parameter: (G, lastup ) ↓σR := (G ↓σR , lastup ). We write (G ↓σR , lastup ) ∼R (G′ ↓σR , lastup ′ ) if G ↓σR = G′ ↓σR and for any t ∈ σ(R) holds lastup (t) = lastup ′ (t). We call event types that are not updating simple event types. These are the event types that don’t update the branch tracking function lastup . ▶ Lemma 43. Let G be σ-well-formed and eff(l, G ↓σR ) = eff(l, G) ↓σ(R) . It follows (G ↓σR , l) ∼ (G, l) ↓σR . Proof. Let (G′ ↓σR , lastup ′ ) := (G ↓σR , l) and G′′ ↓σR [lastup ′′ ] := (G, l) ↓σR . Lemma 23 ensures G ↓σR = G′ ↓σR . Assume towards contradiction that there is an event type t ∈ σ(R) with lastup ′ (t) ̸= lastup ′′ (t). Note that the update function for the parameter of a swarm protocol is the same as the update function for the parameter of a projection. According to eff(l, G ↓σR ) = eff(l, G) ↓σ(R) , any update of the parameter that is performed by the projection is also performed by the swarm protocol. This means there was an update of the swarm protocol parameter caused by some event eb of type tb with t ∈ branch(tb ), which was not performed by the projection. Thus, eb is a branching or joining event that R does not subscribe to. This means the condition R ∈ roles(tb , Gc , σ) of Def. 10 is not satisfied. Accordingly, it holds that t, which is in branch(tb ), is not subscribed to by R, since that would ensure R ∈ roles(tb , Gc , σ). ◀ ▶ Theorem (Eventual Fidelity - Theorem 32). Every realization of a σ-well-formed swarm protocol G is eventually faithful to G and σ. Proof. Assume towards contradiction that it does not hold and there is a (S, ϵ) →∗ (S, l) and a longest prefix l ′ with l = l ′ .e.l ′′ and l ′ satisfies eventual fidelity with logs. This means there is a role R such that eff(l ′ , G ↓σR ) = eff(l ′ , G) ↓σ(R) but eff(l ′ .e, G ↓σR ) ̸= eff(l ′ .e, G) ↓σ(R) . Assume e has type t. There are two possibilities:

F. Furbach, L. Clorius, R. Kuhn, H. Melgratti, A. Scalas, and E. Tuosto

Case 1: e ∈ / eff(l ′ .e, G ↓σR ), e ∈ eff(l ′ .e, G) ↓σ(R) . e

This means there is a transition (G, l ′ ) → (G, l ′ .e) and t ∈ σ(R). It follows that there is a t transition (G, l ′ ) ↓σR → (G, l ′ .e) ↓σR . According to Lemma 43, it holds (G, l ′ ) ↓σR ∼R (G ↓σR , l ′ ). Since t ∈ σ(R), this means that the function lastup of (G, l ′ ) ↓σR assigns the same value to t t as the corresponding function of (G ↓σR , l ′ ). From this and (G, l ′ ) ↓σR → (G, l ′ .e) ↓σR follows t (G ↓σR , l ′ ) → (G ↓σR , l ′ .e). This means e ∈ eff(l ′ .e, G ↓σR ) which contradicts the assumption of Case 1.

Case 2: e ∈ eff(l ′ .e, G ↓σR ), e ∈ / eff(l ′ .e, G) ↓σ(R) , t is not joining and e.lastup ̸= NULL. Here, e is not an interface event that joins multiple concurrent branches together. Let e.lastup = e ′ and l ′ = l ′′ .e′ .l ′′′ . Since e ∈ eff(l ′ .e, G ↓σR ), we know that when e was received by R, it had the correct pointer value e′ in lastup . This value could only have been added to the function when receiving e′ . This means e′ ∈ eff(l ′ .e, G ↓σR ). From eff(l ′ , G ↓σR ) = eff(l ′ , G) ↓σ(R) follows e′ ∈ eff(l ′ , G) as well. Let R′ be the role that emitted e. This role subscribes to any event type that directly precedes t non-concurrently according to Def. 8. This means when it emitted e, it had received an event e1 that directly preceded e. That event was either branching or joining (which means it has to be e′ according to branch tracking) or it was some simple event. Assume it was a simple event. According to branch tracking semantics, this ensures e1 .lastup = e′ and thus e1 occurs in l ′ after e′ . We apply this argument iteratively until we have reached e′ . This gives us a sequence simple = en . . . e1 of simple events. If e1 was not simple, and thus it was e′ , then simple is the empty sequence. It holds simple is a subsequence of l ′′′ . According en ...e1 to the construction of simple, it holds (G, l ′′ .e′ ) −− −−→ (G, l ′′ .e′ .en . . . e1 ). Note that en is a simple event that directly succeeds e′ . If en ∈ / eff(l ′ .e, G), then this ′ means there was an earlier event en in simple that is a direct successor of e′ and that e′n also pointed to e′ . Since en is simple, it holds that e′n has the same type as en . We set en := e′n . We repeat this step until en ∈ eff(l ′ .e, G). We apply this method in sequence to en−1 . . . e1 as well. Afterwards, simple := en . . . e1 is a subsequence of eff(l ′ , G) that occurs after e′ . Let eff(l ′ , G) = l ef f 1 .e1 .l ef f 2 . According to the construction of e1 , e is a direct successor of e1 . Since e ∈ / eff(l ′ .e, G), it follows that there was another direct successor e′′ of e1 in l ef f 2 that is not concurrent with e. Case 2A: t is simple: Note that e′′ has the same type t as e (and thus R subscribes to it) and the same pointer. This means e′′ ∈ eff(l ′ , G ↓σR ) and e ∈ eff(l ′ , G ↓σR ). Since they have the same pointer, that means between receiving e′′ and e, R only received events that were either simple or concurrent with e. This means there is path ts1 . . . tsn of simple events types in the swarm protocol such that ts1 , tsn = t and n > 1. This is a contradiction to the looping condition of Determinacy. Case 2B: t is branching and not joining: This means that e′′ can also be another branching option to t and thus can be another type then e. Note that e′′ has the same pointer as e (and thus R subscribes to it). This means e′′ ∈ eff(l ′ , G ↓σR ) and e′′ is not concurrent with e. This means e′ is not the last branching event that precedes e and thus e pointer to e′ is not correct. It follows e ∈ / eff(l ′ .e, G ↓σR ) which is a contradiction to the assumption of Case 2. Case 2C: t is looping in σ and not joining and not branching: Note that e′′ has the same (updating) type as e and the same pointer as e (and thus R subscribes to it). This means e′′ ∈ eff(l ′ , G ↓σR ) and e′′ is not concurrent with e. This means e′ is not the last updating

Compositional Design, Implementation, and Verification of Swarms (Technical Report)

Algorithm 3 Swarm Composition.

Input: Confusion-free, pairwise-interfacing swarm protocols G1 . . . Gn without concurrent event types; Subscriptions σ 1 . . . σ n ; Swarms S 1 . . . S n and mappings r1 . . . rn such that, for i ∈ {1, . . . , n}: S i has empty logs and realises Gi for subscriptions σ i ; ri (j) is the role in Gi that is realised by the machine S i (j). Output: A subscription σ ⊇ σ i (for i ∈ {1, . . . , n}) such that G1 || . . . || Gn is σ-wellformed; A swarm S that realises G1 || . . . || Gn and is constructed by adapting S 1 . . . S n . 1: Construct σ using Algorithm 1 (by Theorem 16). 2: Let S = (∅, ϵ).

(Output swarm with no machines and empty global log)

3: for all k ∈ {1, . . . , n} do

for all j ∈ dom (S k ) do M := S k (j) (Select the j th machine M from swarm S k ) 6: R := rk (j) (Role of machine M in swarm protocol Gk ) 7: M ′ := A M, (Gi )i∈{1,...,n} , R, k, σ (Adapt M using Def. 36) (Add adapted machine M ′ with empty log to output swarm) 8: S ← M ′ :: S 9: end for 10: end for 4:

event that precedes e and thus e pointer to e′ is not correct. It follows e ∈ / eff(l ′ .e, G ↓σR ) which is a contradiction to the assumption of Case 2.

Case 3: e ∈ eff(l ′ .e, G ↓σR ), e ∈ / eff(l ′ .e, G) ↓σ(R) and t is joining and e.lastup ̸= NULL. e

It holds (G ↓σR , l ′ ) − →. According to the → and (G ↓σR , l ′ ) ∼R (G, l ′ ) ↓σR and thus (G, l ′ ) ↓σR − l.e

definition of projections, there is a log l that R does not subscribe to, such that (G, l ′ ) −→. We assume WLOG that l does not contain event types concurrent with t. Here, R subscribes to all event types that directly precede t according to Def. 10 (Joining). This means l e is empty and thus (G, l ′ ) ↓σR − →. It follows e ∈ eff(l ′ .e, G) which is a contradiction to e∈ / eff(l ′ .e, G) ↓σ(R) .

Case 4: e.lastup = NULL. This case is analogue to e.lastup = e′ since the cases only argue about the part of the log that follows e′ . The only difference is that l ′′ is empty and e′ is replaced by a dummy event NULL that everyone received initially. ◀

Swarm Composition Algorithm

We now use Def. 36 to introduce Algorithm 3, which constructs a composed swarm from a set of input swarms S 1 , . . . S n (all having empty logs) by adapting each input swarm machine M for the composed swarm protocol G1 || . . . || Gn . First, we obtain the well-formed subscription σ for the overall composed swarm protocol (line 1); Then, traversing the input swarms, we select each machine M and its role R (lines 5 and 6); finally, we adapt M into M ′ (line 7) and we add M ′ to the output swarm S (line 8, where the operator _ :: _ adds M ′ to the swarm S with a suitable unique index and an empty local log).

F. Furbach, L. Clorius, R. Kuhn, H. Melgratti, A. Scalas, and E. Tuosto

Proof of Theorem 38

We show that the constructed swarm is a realization of the composed swarm protocol. The algorithm adapts each input machine M = Gk ↓σR k (which is a projection of of some Gk onto a role R) using Def. 36. We will show that each adaptation is a projection of the swarm protocol composition: A M, (Gi )i∈{1,...,n} , R, k, σ = (G1 || . . . || Gn ) ↓σR .

F.1

Technical Requirement

We begin by showing that M || Gk ↓σR = Gk ↓σR holds: Since σ k ⊆ σ, any event type of Gk ↓σR k also occurs in Gk ↓σR . Thus any transition in the composition is either only a transition in Gk ↓σR or in M as well. Since Gk ↓σR k only differs from Gk ↓σR by skipping some transitions, it does not restrict the behavior of Gk ↓σR in the composition. This means that Gk ↓σR = Gk ↓σR k || Gk ↓σR holds. The condition follows.

F.2

Correct Realisation

The algorithm adapts each each input machine M = Gk ↓σR k using Def. 36. We will show that each adaptation is a projection of the swarm protocol composition: A M, (Gi )i∈{1,...,n} , R, k, σ = (G1 || . . . || Gn ) ↓σR . Recall A M, (Gi )i∈{1,...,n} , R, k, σ

= (G1 ↓σR || . . . || (M || Gk ↓σR ) || . . . || Gn ↓σR ) .

We set M k := (M || Gk ↓σR ) and M j := Gj ↓σR for j ̸= k. It remains to show that M 1 || . . . M n = (G1 || . . . || Gi ) ↓σR holds, since the condition A M, (Gi )i∈{1,...,n} , R, k, σ = (G1 || . . . || Gn ) ↓σR follows immediately. We use an induction over i ≤ n: Let M Ri := M 1 || . . . || M i for i ≤ n.

Induction Basis i = 1: It holds M R1 = M 1 = G1 ↓σR . This holds either by definition or due to Gi ↓σR = G1 ↓σR 1 || G1 ↓σR for k=1, as shown above.

Induction Hypothesis: It holds M Ri = (G1 || . . . || Gi ) ↓σR .

Induction Step i → i + 1: First, we show that for any transition t?

(G1 || . . . || Gi+1 ) ↓σR −→ (G′1 || . . . || G′i+1 ) ↓σR , t?

there is a corresponding transition M Ri+1 −→ (G′1 ↓σR || . . . || G′i+1 ↓σR ). According to the t?

composition of swarm protocols, the transition (G1 || . . . || Gi+1 ) ↓σR −→ (G′1 || . . . || G′i+1 ) ↓σR satisfies one of these cases: t? Case 1 (t ̸∈ Gi+1 ): It holds (G1 || . . . || Gi ) ↓σR −→ (G′1 || . . . || G′i ) ↓σR and thus (G′1 || . . . || G′i+1 ) ↓σR = (G′1 || . . . || G′i || Gi+1 ) ↓σR .

Compositional Design, Implementation, and Verification of Swarms (Technical Report) t?

According to the Induction Hypothesis, it holds M Ri −→ (G′1 || . . . || G′i ) ↓σR . We apply t?

the machine composition and we derive M Ri || (Gi+1 ↓σR ) −→ (G′1 || . . . || G′i ) ↓σR || Gi+1 ↓σR since t does not occur in Gi+1 ↓σR . It holds M Ri+1 = M Ri || (Gi+1 ↓σR ) and thus there is a corresponding transition from M Ri+1 . Case 2 (t ∈ Gi+1 and t ̸∈ (G1 || . . . || Gi )): It holds (G′1 || . . . || G′i+1 ) ↓σR = (G1 || . . . || Gi || G′i+1 ) ↓σR .

According to the Induction Hypothesis, it holds t ̸∈ M Ri . We apply the machine composition (M Ri+1 = M Ri || (Gi+1 ↓σR )) and we derive t?

M Ri || (Gi+1 ↓σR ) −→ (G1 || . . . || Gi ) ↓σR || G′i+1 ↓σR . Case 3 (t ∈ Gi+1 and t ∈ (G1 || . . . || Gi )): The event type is interfacing. According to t?

the definition of swarm protocol composition, it holds Gi+1 ↓σR −→ G′i+1 ↓σR as well as t?

(G1 || . . . || Gi ) ↓σR −→ (G′1 || . . . || G′i ) ↓σR . t?

We apply the machine composition and we derive M Ri || (Gi+1 ↓σR ) −→ (G′1 || . . . || G′i ) ↓σR || G′i+1 ↓σR . Having shown that for any transition of (G1 || . . . || Gi+1 ) ↓σR , there is a corresponding t? transition in M Ri+1 , we will now show that, for any transition M Ri+1 −→ (G′1 ↓σR || . . . || G′i+1 ↓σR ) t?

, there is a corresponding transition (G1 || . . . || Gi+1 ) ↓σR −→ (G′1 || . . . || G′i+1 ) ↓σR . We examine t?

the different cases for M Ri+1 −→ (G′1 ↓σR || . . . || G′i+1 ↓σR ): t?

R Case A (Gi+1 ↓σ → G′i+1 ↓σ R − R and t ̸∈ M i ): It holds t?

(G1 || . . . || Gi ) ↓σR || Gi+1 ↓σR −→ (G1 || . . . || Gi ) ↓σR || G′i+1 ↓σR . l? t?

There is a logtype l of minimal length such that l ∩ σ(R) = ∅ and Gi+1 −→−→ G′i+1 . Note that l does not contain any interfacing event types since l ∩ σ(R) = ∅ and we constructed σ in such a way that all interfacing event types are subscribed to if other subscribed event types are causally dependent on them. Since l is minimal, it only contains event types that t is causally dependent on. Since l does contains no interfacing event types, t? it holds (G1 || . . . || Gi+1 ) ↓σR −→ (G1 || . . . || Gi || G′i+1 ) ↓σR . t?

Case B (M Ri − → and t ̸∈ Gi+1 ↓σ R ): This case is analogue to the previous one. t?

R Case C (Gi+1 ↓σ → G′i+1 ↓σ → (G′1 || . . . || G′i ) ↓σ R − R and M i − R ): Note that t is an interfal

1 cing event type. There are l1 , l2 such that (l1 ∪ l2 ) ∩ σ = ∅, l1 ∩ l2 = ∅, Gi+1 −→ − → G′i+1 , and l2 t (G1 || . . . || Gi ) −→ − → (G′1 || . . . || G′i ).

Note that l1 and l2 are not subscribed to and we can assume they are minimal. Thus they do not contain any interfacing event types. This means it holds l .l

1 2 (G1 || . . . || Gi+1 ) −− −→− → (G′1 || . . . || G′i+1 )

and thus (G1 || . . . || Gi+1 ) ↓σR −→ (G′1 || . . . || G′i+1 ) ↓σR .

F. Furbach, L. Clorius, R. Kuhn, H. Melgratti, A. Scalas, and E. Tuosto

Since the projections have the same transitions and the emitter set is determined by the transitions, the projections emit the same event types. Thus they are equal: M 1 || . . . || M n = (G1 || . . . || Gn ) ↓σR . The constructed swarm is almost a realisation of the σ-well-formed composed protocol G1 || . . . || Gn . The only realisation requirement not met concerns the set of updating events: for each machine M, M. UP is an over-approximation (rather than the exact set). However, this over-approximation is sound for our purposes: for any t in that t over-approximation, if G′ − → and R ∈ roles(t, G, σ), then t ∈ σ(R). Moreover, all machines share the same set M. UP. Therefore, the proof of eventual fidelity in § D still applies under this over-approximation. Thus, Theorem 32 can still be applied for the over-approximated set of updating event types and the constructed swarm is eventually faithful to the σ-well formed composed protocol G = G1 || . . . || Gn . Thus, Theorem 38 is proven.

Inference Rules for Verifying Well-Formedness

We define rules that allow us to check the σ-well-formedness of a swarm protocol compositions. To decide whether G1 || · · · || Gn is σ-well-formed we rely on a derivation environment consisting of the sets C, S, and V , where: C is a set of unordered pairs of event types containing an overapproximation of the concurrent event types of G1 || · · · || Gn . S is the set of subterms of G1 || · · · || Gn . V is a set of subterms of G1 || · · · || Gn . When we build a derivation bottom-up, we collect in this set the subterms that we have “visisted” and recursively propagate this set between conclusions and premises of the rules. Furthermore, the inference rules make use of the auxiliary definitions in Def. 44 below. ▶ Definition 44 (Auxiliary definitions for inference rules.). A. The predicate composable({G1 , . . . , Gn }) is true iff {G1 , . . . , Gn } is composable according to Def. 14. B. For a set of swarm protocols SP = {G1 , . . . , Gn }, we denote by conc(SP ) an overapproximation of the set of concurrent event types in G1 || · · · || Gn given by: conc(SP ) = {{t′ , t′′ } | ∃Gi , Gj ∈ SP. t′ ∈ Gi ∧ t′ ∈ / Gj ∧ t′′ ∈ Gj ∧ t′′ ∈ / Gi } C. The set of subterms of a swarm protocol G = subterms(

i∈I R i ⟨ti ⟩.Gi ) = {

i∈I R i ⟨ti ⟩.Gi , is given by:

i∈I R i ⟨ti ⟩.Gi } ∪

i∈I subterms(Gi )

D. The set of event types branching with t at G according to a set of concurrent event types C is given by: t

t′

bw(t, G, C) = {t′ |G − → G′ ∧ G −→ G′′ ∧ t ̸= t′ ∧ G′ ̸= G′′ ∧ {t, t′ } ∈ / C} E. The set of event types for which t is joining at G according to a set of concurrent event types C and a set of subterms S is given by: t′

t′′

jf(t, G, C, S) = {t′ | ∃G1 , G2 ∈ S. ∃t′′ ∈ G2 . t′ ̸= t′′ ∧ G1 −→ G ∧ G2 −→ G ∧ {{t, t′ }, {t, t′′ }} ̸⊆ C ∧ {t′ , t′′ } ∈ C}

Compositional Design, Implementation, and Verification of Swarms (Technical Report)

F. The set of roles that subscribe to event types in G that causally depend on t according to the σ and the set of concurrent event types C is given by: roles(t, G, σ, C) = {R | there are n ≥ 0, t0 , . . . , tn , l1 , . . . , ln such that: t

0 1 1 n n t0 = t, G −→ −→ −→ · · · −→ −→ and

tn ∈ σ(R), and {ti , ti+1 } ∈ / C for all 0 ≤ i < n}. ▶ Definition 45 (Inference rules for checking well-formedness of swarm protocol compositions). We denote by W F (G1 || · · · || Gn ) and DCC(G1 || · · · || Gn ) the sets of subscriptions with respect to which G1 || · · · || Gn is, respectively, well-formed, and determinate and causalconsistent. We think of the task of proving that G1 || · · · || Gn is σ-well-formed as the same as showing that σ ∈ W F (G1 || · · · || Gn ). To check this, we use the judgment ⊢ σ ∈ WF(G1 ||G2 ) defined by the following inference rules:

composable({G1 , . . . , Gn }) conc({G1 , . . . , Gn }), subterms(G1 || · · · || Gn ), ∅ ⊢ σ ∈ DCC(G1 || · · · || Gn ) [Init]

⊢ σ ∈ WF(G1 || · · · || Gn )

G∈V ′

′

t′

′

∃t , l ∈ G. ∃G ⊑ G. G − → G ∧ t ∈ l ∧ G′ −→ ∧∀R′ ∈ roles(t′ , G′ , σ, C). t′ ∈ σ(R′ ) [Loop]

C, S, V ⊢ σ ∈ DCC(G)

i∈I R i ⟨ti ⟩.Gi

ti ∈ σ(Ri ) R⟨t⟩

∧ ∀R′ ∈ {R | Gi −−→ ∧{ti , t} ∈ / C}. ti ∈ σ(R′ ) ′ ∀i ∈ I. ∧ bw(ti , G, C) ̸= ∅ ⇒ ∀R ∈ roles(ti , G, σ, C). bw(ti , G, C) ∪ {ti } ⊆ σ(R′ ) ∧ jf(ti , G, C, S) ̸= ∅ ⇒ ∀R′ ∈ roles(ti , G, σ, C). jf(ti , G, C, S) ∪ {ti } ⊆ σ(R′ ) ∧ C, S, V ∪ {G} ⊢ σ ∈ DCC(Gi ) [Term]

C, S, V ⊢ σ ∈ DCC(G)

Non-branch-tracking Swarm

The swarm semantics from [41] (Def. 46 below) are similar to the semantics of Def. 27, but does not involve branch-tracking. These semantics ensures that a swarm realising a swarm protocol G that is well-formed w.r.t. a subscription σ according to the well-formedness definition from [41] is eventually faithful to G and σ. ▶ Definition 46 (Non-Branch-Tracking Swarm Semantics (from [41])). Given a mapping m, let m[a 7→ b] denote the mapping identical to m except m[a 7→ b](a) = b. We write t!

(M, l ) −→ (M, l · e) when machine M emits an event e of type t from state δ(M, l ), thus reaching state δ(M, l · e). The behaviour of a swarm is defined by the smallest relation closed under the following rules: t!

(Mi , l i ) −→ (Mi , l i · e)

S(i) = (Mi , l i ) ′

<l i ⊆<l ′

(S, l · l ) −→ (S[i 7→ (Mi , l i · e)], l · e · l )

S(i) = (Mi , l i ) [Local]

<l i ⊂<l ′ ⊆<l

(S, l ) −→ (S[i 7→ (Mi , l ′ )], l )

[Prop]

F. Furbach, L. Clorius, R. Kuhn, H. Melgratti, A. Scalas, and E. Tuosto

Well-formedness as defined in Def. 12, however, necessitates branch-tracking to ensure eventual fidelity. Using well-formedness as defined in Def. 12 together with the swarm semantics in Def. 46, leads to swarm behaviours where machines can enter conflicting states, from where they cannot recover consistency. This is shown in the following example. ▶ Example 47 (Incompatibilty between well-formedness in Def. 12 and swarm semantics in [41]). Consider Warehouse in Fig. 1. Let E denote the set of all event types in Warehouse and let σ = {T 7→ E, FL 7→ E \ {partOK}, D 7→ E \ {pos}}. The projections are given in Fig. 11. By Def. 12, Warehouse is σ-well-formed. Consider swarm S W with: S W = {iT1 7→ (MT , ϵ),

iT2 7→ (MT , ϵ), iFL 7→ (MFL , ϵ), iD 7→ (MD , ϵ)} σ where MT = Warehouse ↓T , MFL = Warehouse ↓σFL , and MD = Warehouse ↓σD . Observe that the machines with IDs iT1 and iT2 both enact role T (transport). Since all machines are obtained by projecting Warehouse onto its roles using σ, the swarm S W realises the protocol Warehouse w.r.t. σ (as defined in [41]). A possible execution of S W by Def. 46 (from [41]) is: partReq!

(S W , ϵ) −−−−−→ (S 1 , partReq 1 ) τ −→ (S 2 , partReq 1 ) pos!

−−→ (S 3 , partReq 1 · pos 2 ) τ −→ (S 4 , partReq 1 · pos 2 ) τ −→ (S 5 , partReq 1 · pos 2 )

partOK!

−−−−→ (S 6 , partReq 1 · pos 2 · partOK 3 )

partReq!

S 1 = S W [iT1 7→ (MT , partReq 1 )] S 2 = S 1 [iFL1 7→ (MFL , partReq 1 )] S 3 = S 2 [iFL 7→ (MFL , partReq 1 · pos 2 )] S 4 = S 3 [iT1 7→ (MT , partReq 1 · pos 2 )] S 5 = S 4 [iT2 7→ (MT , partReq 1 · pos 2 )] S 6 = S 5 [iT1 7→ (MT , partReq 1 · pos 2 · partOK 3 )]

−−−−−→ (S 7 , partReq 1 · pos 2 · partOK 3 · partReq 4 )

S 7 = S 6 [iT1 7→ (MT , partReq 1 · pos 2 · partOK 3 · partReq 4 )]

−−−−→ (S 8 , partReq 1 · pos 2 · partOK 3 · partReq 4 · partOK 5 ) τ −→ (S 9 , partReq 1 · pos 2 · partOK 3 · partReq 4 · partOK 5 )

S 8 = S 7 [iT2 7→ (MT , partReq 1 · pos 2 · partOK 5 )] S 9 = S 8 [iD 7→ (MD , partReq 1 · pos 2 · partOK 3 · partReq 4 · partOK 5 )]

partOK!

closingTime!

−−−−−−−−→ (S 10 , l ) τ ∗ −→ (S 11 , l )

S 10 = S 9 [iD 7→ (MD , l )] S 11 = S 10 [iT1 7→ (MT , l ), iT2 7→ (MT , l ), iFL 7→ (MFL , l )]

where the global log l = partReq 1 · pos 2 · partOK 3 · partReq 4 · partOK 5 · closingTime 6 has propagated to every machine. (Recall that by Def. 46, τ -transitions denote log propagation.) Observe that in state S 5 , the machine with ID iT1 emits an event partOK 3 as a response to partReq 1 ; however, the event does not immediately propagate to machine iT2 , which (in state S 7 ) responds to partReq 1 with another event partOK 5 . As the log l propagates to iT2 (in state S 11 ), the machine sees that its event partOK 5 is invalidated by the earlier partOK 3 . However, the machine iD (for the door) reaches a different conclusion: based on its local log in state S 9 , it interprets the event partOK 5 as a response to partReq 4 , when it was in fact emitted as a response to partReq 1 . Consequently, the machines in S do not reach a consensus on which events are valid and conform to an execution of Warehouse — despite having been projected from Warehouse for σ. Specifically, in the final swarm state S 11 reached after the propagation of the log l, the two machines MT (for the transport) with IDs iT1 and iT2 agree on the projection of the same state of the swarm protocol Warehouse — whereas MD with ID iD is in a completely different state: δ(MT , l ) = (FL⟨pos⟩.T⟨partOK⟩.Warehouse) ↓σT

and

δ(MD , l ) = 0

The machines MT expect the forklift to emit an event of type pos, while MD believes the door has closed and the protocol has ended. The swarm cannot recover from this conflict.12 ⋄

To avoid the issue in Example 47 with the swarm semantics Def. 46 (from [41]), we should also subscribe role D in σ to events of type pos. The additional subscriptions needed by Def. 46 would increase with swarm composition, leading to inefficient swarms: we measure these additional subscriptions in § 6.1.

Record · ID 31239 · SHA-256 86e595e6b6d44a7c
Conceptio Open Knowledge Archive — every document is proof-bundled with source, license, and retrieval metadata.