Choral: Object-oriented Choreographic Programming

Background. Choreographies, broadly construed, are coordination plans for concurrent and distributed systems [W3C 2004; Object Management Group 2011]. Examples of choreographies include distributed authentication protocols [OpenID Foundation 2014; Sporny et al. 2011], cryptographic protocols [Diffie and Hellman 1976], and multiparty business processes [Object Management Group 2011; W3C 2004]. In software development, programmers use choreographies to agree on the interactions that communicating endpoints should enact to achieve a common goal; then, each endpoint can be programmed independently. The success of this development process hinges on achieving choreography compliance: when all endpoints are run together, they interact as defined by the choreographies agreed upon [Montesi 2023].

Achieving choreography compliance is hard, because of some usual suspects of concurrent and distributed programming: predicting how multiple programs will interact at runtime is challenging [O’Hearn 2018], and mainstream programming languages do not adequately support programmers in reasoning about coordination in their code [Lu et al. 2008; Leesatapornwongsa et al. 2016]. Additionally, choreographies are complex. At a minimum, choreographies define the expected communication flows among their roles (abstractions of endpoints, like “Alice,” “Bob,” “Buyer,” etc.) [Intl. Telecommunication Union 1996]. However, they often include computational details of arbitrary complexity, for example, pre- or post-processing of data (encryption, validation, anonymisation, etc.), state information, and decision procedures to choose among alternative behaviours. These computational details are essential parts of many protocols, ranging from security protocols to business processes. Figure 1 depicts the common situation where a programmer tries to ensure choreography compliance through their subjective interpretation of the choreography and the manual coding of endpoints.

In response to the challenge of choreography compliance, researchers investigated methods to relate choreographies to endpoint programs—many are reviewed in Ancona et al. [2016]; Hüttel et al. [2016]. Initially, these methods focused on simple choreographic languages without computation that were inspired by, e.g., communicating automata, process calculi, and session types [Qiu et al. 2007; Bravetti and Zavattaro 2007; Basu et al. 2012; Honda et al. 2016]. Some ideas developed for choreographies were later adopted in the paradigm of choreographic programming [Montesi 2013; Carbone and Montesi 2013], where choreographies are written in a Turing-complete programming language that allows for defining arbitrary computation at endpoints. Thanks to the capability of combining computation with coordination, choreographic programming languages can capture realistic protocols that include data manipulation and decision procedures, including encryption strategies (as in security protocols), retry strategies (as in transport protocols), and marshalling (as in application protocols). In choreographic programming, compliance is obtained by construction: given a choreography, a compiler automatically translates it to a set of compliant endpoint implementations. Choreographic programming has been shown to have promising potential in multiple contexts, including information flow [Lluch-Lafuente et al. 2015], distributed algorithms [Cruz-Filipe and Montesi 2016], cyber-physical systems [López et al. 2016; López and Heussen 2017], and self-adaptive systems [Dalla Preda et al. 2017].

The problem. Current approaches to choreographic programming come at a significant cost to modularity, and it remains unclear how the benefits of this paradigm can be applied to mainstream software development.

Typically, the endpoint code that implements a choreography comes in libraries that developers can use in their applications through an Application Programming Interface (API) [Murty 2008; Wilder 2012; Atzori et al. 2010]. For example, a library that implements a choreography for user authentication might provide a method \(\texttt {authenticate}\) that a web service can invoke to run (its part of) the protocol in collaboration with a connected client. The implementation of \(\texttt {authenticate}\) might involve a series of communications between the client and the web service. Potentially, a third-party identity provider might be involved as well, and messages might include passwords that should be hashed. Usually, and ideally, all these details are hidden from the API (the signature of the method) exposed to the developer of the web service. This abstraction allows the developer to minimise coupling between their implementation of the functionalities offered by the web service and the choreography used for authentication, bringing the expected benefit: the library implementing the choreography and the rest of the code of the web service can be updated independently and recombined, as long as the API provided by the former remains compatible with the one expected by the latter. This benefit is key to large-scale software development, and it is an initial assumption for modern development practices like microservices and DevOps [Dragoni et al. 2017].

Unfortunately, previous frameworks for choreographic programming do not support modular software development [Montesi 2013; Dalla Preda et al. 2017]. The code that these frameworks generate for each endpoint is a “black box” program without an API: it can be executed, but it is not designed to be composed by programmers within larger codebases. Thus, these frameworks fall short of providing the aforementioned benefit of modularity. Furthermore, the common scenario of programming an endpoint that participates in multiple choreographies is not supported, and neither is programming an endpoint where participating in a choreography is only part of what the endpoint does.

A major factor that makes modularity challenging is that current choreographic languages are based on behavioural models (process calculi, communicating automata, etc.), which makes translating choreographies into libraries based on mainstream abstractions (data, functions, objects, etc.) nontrivial. For the simpler setting of choreographic languages without computation, we know that choreographies can be translated to libraries that offer a “fluid” API. For instance, Scalas et al. [2017] produce object-oriented libraries whose APIs enforce the invocation of \(\texttt {send}\) and \(\texttt {receive}\) methods in the right order: If an endpoint should send, receive, and then send, then the developer will be forced to write something like \(\texttt {o.send(..).receive(..).send(..)}\) . However, this approach leaks the structure of the communication flow implemented by the library; thus, future versions of the library that adopt a different structure (e.g., an unnecessary communication might be removed, or some communications might be bunched together for efficiency) would require rewriting the application that uses the library. Furthermore, this approach does not let the choreography programmer decide how the generated API will look; thus, we cannot use this method to generate drop-in replacements for existing libraries.

In summary, we still have to discover how the principles of choreographic programming can be applied to mainstream programming. This article aims to fill this gap.

This article. We present Choral, a new choreographic programming language that supports modularity and is based on mainstream programming concepts (from object-oriented programming). To demonstrate applicability, Choral is compatible with Java, but our ideas apply to most statically typed, object-oriented languages.

The fulcrum of Choral is a new interpretation of choreographies that builds naturally on top of existing language abstractions: Choral is an object-oriented choreographic programming language, where choreographies are classes and their instances are objects. The starting point for this interpretation is a generalisation of the key idea found in Lambda 5 [Murphy VII et al. 2004], the model that inspired the research line on multitier programming [Neubauer and Thiemann 2005; Cooper et al. 2006; Serrano et al. 2006; Murphy VII et al. 2007; Weisenburger et al. 2020]. In Lambda 5, each data type is located at a (single) place, which enables reasoning on spatially distributed computation. Choral generalises these types from single to multiple locations, which allows us to express that an object is implemented choreographically: Choral objects have types of the form T@(A1, ..., An), where \(\texttt {T}\) is the usual interface of the object, and A1, ..., An are the roles that collaboratively implement the object.

As an example, consider the case of a multiparty choreography for distributed authentication, where a service authenticates a client via a third-party identity provider. We can define such a choreography as a Choral class with type DistAuth@(Client, Service, IP) (IP is short for identity provider). The class can implement methods that involve multiple roles. For example, it can offer a method \(\texttt {authenticate}\) with the following signature.

Invoking \(\texttt {authenticate}\) with some \(\texttt {Credentials}\) located at Client returns an authorisation token at Service ( \(\texttt {Optional}\) since authentication can fail), denoting the movement of data.

We leverage our object-oriented interpretation of choreographies to develop a methodology for choreography compliance that supports modularity and is compatible with mainstream programming. We depict this methodology in Figure 2. Given the code of a Choral class with some roles, a compiler produces a compliant-by-construction software library in pure Java for each role (“coordination code” in Figure 2): each library contains the local implementation of what its role should do to execute the choreography correctly. These libraries offer Java APIs derived from the source choreographies, which reveal only the details pertaining to the implemented role. When a software developer programs an endpoint that should engage in a choreography, they can just take the library compiled for the role that their endpoint needs to play and use the library through its Java API. Those APIs allow developers to modularly compose multiple libraries within their code (“local code” in Figure 2), thus gaining the ability to participate in multiple choreographies.

The Java code compiled from the method \(\texttt {authenticate}\) for the roles Client and Service has the following signatures, respectively.

The compiled signatures follow the principle that we have just mentioned—that is, for each role, only what pertains to that role is reported. This is why the signature compiled for Client has a parameter of type \(\texttt {Credentials}\) and return type \(\texttt {Unit}\) : in the source choreography, the parameter is located at Client whereas the return type is located at another role.¹ Following the same principle, the signature for Service has return type \(\texttt {Optional}< \texttt{AuthToken}>\) and no parameters.

Contributions. We outline our main contributions.

Language. We present Choral, the first choreographic programming language based on mainstream abstractions and interoperable with a mainstream language (Java). The key novelty of the Choral language is that data types are higher-kinded types parameterised on roles. We leverage this feature to bring the key aspects of choreographies to object-oriented programming (spatial distribution, interaction, and knowledge of choice). Choral is also the first truly higher-order choreographic language, where choreographies passed as arguments can carry state and invocations of higher-order choreographies require no centralised coordination [Demangeon and Honda 2012; Dalla Preda et al. 2017].

Integrating object-oriented principles with choreographies brings key benefits in the other direction too, in the sense that we gain a much richer choreographic language than the state-of-the-art. By using subtyping, we can define abstract APIs for choreographies that can be implemented in different ways and communication behaviours, bringing the usual substitution principle for objects to choreographies. Method overloading allows us to specialise computation based on the locations of arguments—which is a new dimension for overloading. Semantic parametricity enables the writing of reusable choreographies that treat uniformly parameters that implement a shared API. These features allow us to generalise choreographies from assuming a fixed communication primitive to user-definable communication methods, thus freeing Choral from commitments to any communication technology or middleware. Furthermore, we can define in Choral the first hierarchy of “channel types” for choreographies, which can be used to represent at the level of types the topological assumptions of a choreography. In general, users are free to define other ‘channel types’ to support more topologies.

We implement a type checker that, in addition to the expected checks for an object-oriented language, detects coding errors related to roles. For example, our checker can rule out computation at a role that erroneously accesses data at another role without proper communication. This makes distribution errors manifest to the programmer. Our typing also supports the reuse of all existing Java classes and interfaces in Choral, because every such type can be lifted to a Choral type located at a single role.

In Choral, choreographies are concrete software artefacts. This poses questions such as what code should go in these artefacts, what code should remain local, and how these two parts of software should interact through APIs. We elicit these questions and report on our experience in addressing them throughout the article, where they become relevant.

Compiler. We implement a compiler that translates Choral source into Java libraries that comply with the source choreography: the code generated for each role performs the actions prescribed by the choreography. With our compiler, the programmer of the choreography is in control of the generated APIs: the APIs for each role follow the same structure found in the choreography, but where all data types and parameters in method signatures that do not pertain to the role are omitted, as we exemplified previously for the \(\texttt {authenticate}\) method.

Testing. We present the first testing tool for choreographic programming. Since choreography implementations are spread over multiple components (one for each role), testing choreographies can be difficult, because it calls for integration testing. Our testing tool leverages Choral to write ‘choreographic tests’ that look like simple unit tests at the choreographic level, but are then compiled to integration tests that integrate the respective implementations of all roles.

Evaluation. We explore the expressivity of Choral with use cases of different kinds, covering security protocols, cyber-physical systems connected to the cloud, and parallel algorithms. For these use cases, we discuss relevant code excerpts and development techniques induced by Choral.

We then move from our examples to real-world comparisons.

First, we show how Choral can be used to transition existing Java programs to choreographies. We reimplement in Choral the Java implementation of Karatsuba’s algorithm for fast multiplication, which yields a parallel implementation. Furthermore, we reimplement a clone of Twitter developed by the Spring team. Implementing this system in Choral requires identifying roles, which makes the original monolithic application much more modular.

Second, we compare Choral to a popular framework for concurrent programming in Java based on actors (Akka). In particular, we identify the key differences in the development processes and resulting architectures induced by the two technologies. We find that Choral provides concrete benefits in avoiding subtle concurrency bugs.

Third, we carry out a quantitative evaluation of how Choral impacts software development and runtime performance. Thanks to its choreographic approach, Choral consistently leads to smaller codebases. Moreover, the impact of our compiler on the speed of the edit-compile cycle is negligible (milliseconds). Finally, we show that the runtime performance of the code generated by Choral is not worse (and often better) than that of alternative implementations in Java and Akka.

Outline. We overview Choral with simple examples in Section 2, and give more realistic use cases in Section 3. The syntax and implementation of Choral are discussed in Section 4, and testing in Section 5. We evaluate Choral in depth in Section 6. Related and future work are discussed in Section 7. We draw conclusions in Section 8.

We start with an overview of the key features of Choral. First, spatial distribution: the expression of computation that takes place at different roles (Section 2.1). Second, interaction: the coding of data exchanges between roles (Section 2.2). Third, knowledge of choice: the coordination of roles to choose between alternative behaviours (Section 2.3).

The Choral language is quite big. Its usefulness depends on the capability to produce software libraries whose APIs look like “idiomatic” Java APIs, so we chose to incorporate a substantial set of features, which would commonly be considered necessary to use and produce Java APIs: Choral supports classes, interfaces, generics, inheritance, and method overloading. APIs generated by Choral support lambda expressions, in the sense that Java programmers can pass lambda expressions as arguments to our APIs. (Just as in Java, Choral sees these arguments as objects.) Supporting the Java syntax for lambda expressions inside Choral programs is not necessary for our objective, since they can be encoded as objects, so we leave it to future work on ergonomics.

In the rest of this section, we explain the key aspects of Choral by assuming that the reader is familiar with Java. The reader can assume that language constructs that have the same syntax as Java behave as expected (modulo our additions, which we explain in the text).

We dedicate this section to illustrating how the features of Choral contribute to writing realistic choreographies. We start with a protocol for distributed authentication (Section 3.1), which we then reuse modularly in another use case from the healthcare sector that mixes cloud computing, edge computing, and Internet of Things (IoT) (Section 3.2). Finally, we show a use case on parallel computing, by showing a distributed implementation of merge sort (Section 3.3).

We discuss the main elements of the implementation of Choral. First, we show its syntax and comment on the main differences with Java’s. Then, we present the Choral type checker, including examples of the main errors related to roles that it detects and related error messages. Finally, we describe the key components of the Choral compiler.

Testing implementations of choreographies is challenging, since the distributed programs of all participants need to be integrated (integration testing). We introduce ChoralUnit, a testing tool that enables the writing of integration tests as simple unit tests for choreographic classes.

Writing tests. Following standard practice in object-oriented languages and inspired by JUnit, tests in ChoralUnit are defined as methods marked with a @Test annotation [Hamill 2004; Murphy VII et al. 2004]. For example, we can define the following unit test for the \(\texttt {VitalsStreaming}\) class from Section 3.2.

The test method \(\texttt {test1}\) checks that data is pseudonymised correctly by \(\texttt {VitalsStreaming}\) . Test methods must be annotated with @Test, be static, have no parameters, and return no values.

At lines 4 and 5, we create a channel between the Device and the Gatherer by invoking the \(\texttt {TestUtils .newLocalChannel}\) method, which is provided by ChoralUnit as a library to simplify the creation of channels for testing purposes. This method returns an in-memory channel, which both Device and Gatherer will find by looking it up in a shared map under the key "VST_channel 1". Thus, both roles must have the same key in their compiled code, which is guaranteed, here, by the fact that the expression "VST_channel 1"@[Device,Gatherer] is syntactic sugar for "VST_channel 1"@Device, "VST_channel 1"@Gatherer.

At lines 6 and 7, we create an instance of \(\texttt {VitalsStreaming}\) (the choreography we want to test). We use a \(\texttt {FakeSensor}\) object to simulate a sensor that sends some data containing sensitive information (omitted). We then invoke the \(\texttt {gather}\) method, passing an implementation of a consumer that checks whether the data received by the Gatherer has been pseudonymised correctly.

Given a class like \(\texttt {VitalsStreamingTest}\) , ChoralUnit compiles it by invoking our compiler with a special flag ( \(\texttt {-annotate}\) ). This flag makes the compiler annotate each generated Java class with an @Choreography annotation that contains the name of its source Choral class and the role that the Java class implements.

When the compilation is finished, we can invoke ChoralUnit to run the tests from the class \(\texttt {VitalsStreamingTest}\) . Once launched, the tool finds all the Java classes with an @Choreography annotation whose \(\texttt {name}\) value corresponds to \(\texttt {VitalsStreamingTest}\) . By construction, each discovered class has a method with the same name, corresponding to the namesake method from the source Choral test class ( \(\texttt {test1}\) , in our example). ChoralUnit exhaustively runs all the tests found in the test class. Namely, for each @Test-annotated method and for each class generated from the Choral source, ChoralUnit starts a thread that runs the local implementation of that method implemented by that class.

In our example, \(\texttt {VitalsStreamingTest}\) is compiled to a class for Device and another for Gatherer, each with a \(\texttt {test1}\) method. Thus, ChoralUnit starts two threads, one running \(\texttt {test1}\) of the first generated Java class and the other running \(\texttt {test1}\) of the second generated Java class.

Multiparty assertions. In the previous example, we have written an assertion (in \(\texttt {PseudoChecker}\) ) that checks a condition at a single role (Gatherer). Sometimes, it is useful to assert conditions that involve multiple roles. A typical example is testing the correct implementation of protocols that aim at making two parties agree on a symmetric cryptographic key, like the Diffie-Hellman protocol [Diffie and Hellman 1976]. In particular, after running the protocol, the two participants (say A and B) should have the same key. We can express this assertion as follows.

Above, method \(\texttt {assertEquals}\) of class \(\texttt {Assert2}\) uses the channel \(\texttt {chAB}\) to communicate the key at A ( \(\texttt {keyA}\) ) from A to B, and then checks locally at B that it is equal to the key at B ( \(\texttt {keyB}\) ). If the check fails, then an assertion error is raised at B.

Class \(\texttt {Assert2}\) can be user-defined, and likewise, developers can define classes that allow for assertions that involve more roles (e.g., \(\texttt {Assert3}\) , \(\texttt {Assert4}\) , etc.). In these implementations, the user can also freely code different protocols for communicating the data among the participants.

In Section 3, we explored how Choral can be used to program choreographies for a few realistic scenarios. In this section, we extend the evaluation of our approach in three different directions:

Overall, our results are encouraging. In addition to the advantage of choreography compliance, smaller codebases tend to host fewer bugs [Bessey et al. 2010], and Choral appears rather approachable when we consider the context of existing practices.

The code used in this evaluation is available in two public repositories. The first contains the material for the comparison with Java and Akka (both quantitative and qualitative) and for benchmarking the performance of the compiler.³ The second includes the original code and the Choral re-implementation of RetwisJ.⁴

Choral is a choreographic programming language, in that it makes the flow of interactions and their related computations manifest from a global viewpoint [Montesi 2013]. While Choral suffices already in tackling different kinds of use cases, as we have discussed in this article, the literature on choreographies is vast. Choral includes and generalises many features found in previous work on choreographies. There are other features that we have not considered in this work, along with open problems that we pointed out when appropriate in the previous sections. We discuss related work and other potential future developments of Choral in the rest of this section.

Previous implementations of choreographic programming. The idea of synthesising local participant specifications that comply with choreographies has been a hot research topic for more than 20 years, and work in this line of research is typically based on automata or process calculi abstractions [Alur et al. 2000; Qiu et al. 2007; Basu et al. 2012; Honda et al. 2016; Autili et al. 2018]. Previous implementations of choreographic programming consist of Chor [Carbone and Montesi 2013] and AIOCJ [Dalla Preda et al. 2017], which are based on process calculi and generate executable Jolie code. Compared to them, Choral solves the modularity problems mentioned in the Introduction, by revisiting choreographies under the light of mainstream abstractions. Another advantage is that the types of channels needed by a choreography are made explicit and can be user-defined [Qiu et al. 2007; Carbone et al. 2012; Carbone and Montesi 2013; Honda et al. 2016].

Other approaches to spatially distributed programming. The types that support our choreography-as-objects interpretation have been inspired by ideas found in modal logics for mobile ambients [Cardelli and Gordon 2000] and, later, in the line of work on multitier programming [Murphy VII et al. 2004; Neubauer and Thiemann 2005; Cooper et al. 2006; Serrano et al. 2006; Murphy VII et al. 2007; Liu et al. 2009; Weisenburger et al. 2018]. In the words of Murphy VII et al. [2004], these works represent other approaches to “spatially distributed computation.” For example, in the most recent incarnation of multitier programming (ScalaLoci, by Weisenburger et al. [2018]), a distributed application is essentially defined as a single program that composes different functions, each localised at a single participant. A function can then invoke special primitives to request remote computation by another participant, whose implementation must always be ready for such requests [Weisenburger et al. 2020]. Differently from choreographies, this makes the flow of communications implicit and dependent on an underlying middleware—indeed, multitier programming was not designed to address the problems of defining choreographies and addressing choreography compliance as an aim. Choral generalises data types localised at a single participant to data types localised at many participants (roles), which enables our novel development process for choreography-compliant libraries. Castro-Perez and Yoshida [2020] explored the parallelisation of a simple multitier first-order functional language, for which they can infer abstract (computation is not included) choreographies of the communication flows that these programs can enact; Choral could be a candidate implementation language for this kind of models. Fowler et al. [2019] explored the idea of incorporating simple choreographic languages (without computation) to ensure that multitier code between two participants enacts specific protocols.

Choral’s clear relation to the ideas found in logics for mobile ambients has already proven useful. In particular, Giallorenzo et al. [2021] use Choral to kickstart an investigation of the links and differences between choreographic and multitier programming, by taking Choral and ScalaLoci as representative languages. After identifying the core abstractions that differentiate the two approaches, the authors provide algorithms for translating Choral code into ScalaLoci code and vice versa. Going from a multitier program to a choreographic one requires synthesising one of the many possible protocols (a choreography) that implements the necessary communications to execute the multitier program (which does not specify this aspect). This connection paves the way for joint research and cross-fertilisation between the two communities [Giallorenzo et al. 2021].

Higher-order choreographies. Interpreting choreographies as objects enables, for the first time, higher-order composition of choreographies that carry state (the fields of the objects): stateful choreographies (objects) can be passed as arguments. Stateful choreographies have been investigated before without higher-order composition—see, for example, the works by Carbone et al. [2012]; Chen and Honda [2012]; Cruz-Filipe and Montesi [2020]. Demangeon and Honda [2012] studied how parameters that abstract choreographies can be expanded syntactically, but their choreographies cannot carry state and there must be a role that acts as an orchestrator to “enter” into a choreography (whereas in Choral, control is fully distributed). In the setting of multitier programming, Weisenburger and Salvaneschi [2019] introduced a module system to write multitier programs as compositions of submodules. Differently from Choral and the work by Demangeon and Honda [2012], their approach requires fixing roles statically, whereas in our case roles can be freely instantiated at runtime—for example, our merge sort example in Section 3.3 exploits this feature when roles are exchanged in recursive calls. Thus, our new data types might be interesting in the setting of multitier programming too.

Choral’s principles in other settings. The core idea in Choral’s design is to have data types at multiple locations (the roles of the choreography): \(\texttt {T@(A_1, ... A_n)}\) . This information is the compass that guided us in lifting the various aspects of Java to the choreographic level and in designing our notion of projection. We believe that this idea can be easily applied to other object-oriented languages—C#, Kotlin, Scala, and others—by extending their types in the same way and retracing our steps.

The applicability of this core idea goes even beyond object-oriented languages. Choral’s first technical report and release [Giallorenzo et al. 2020; Choral Development Team 2020] have already inspired the investigation of theories and implementations of functional choreographic programming languages [Cruz-Filipe et al. 2022;, 2023a; Hirsch and Garg 2022; Shen et al. 2023; Graversen et al. 2023]. These studies confirm the generality of our approach: just like extending Java types with roles yields an object-oriented choreographic programming language (Choral), doing the same to the \(\lambda\) -calculus supports the development of a theory of functional choreographic programming [Cruz-Filipe et al. 2022;, 2023a].

Safety and liveness. The theory of choreographic languages comes with strong safety and liveness properties, which stem from the high-level abstractions provided by choreographies and their projections to distributed code [Montesi 2023]. Under the same assumptions made (sometimes implicitly) in these proofs, Choral promises the traditional safety and liveness properties of choreographic programming languages. We discuss these properties and how they relate to Choral’s modularity and flexibility wrt communication middleware. Furthermore, in the end, we report useful references and outline future research for the formalisation of these promises.

Choreographic programming languages guarantee communication safety. That is, processes never try to interact by performing incompatible communication actions—if one action is “send,” then the other is a “receive,” and the type of the sent message is always (a subtype of) the one expected by the receiver [Montesi 2023; Carbone et al. 2012]. Proofs of this result rely on the assumption that communications is reliable (messages are never lost, duplicated, or corrupted) or at least that message exchange primitives adopt suitable best-effort and timeout strategies [Montesi and Peressotti 2017; Montesi 2023]. Furthermore, communication primitives should respect a locality principle: messages should be dispatched to their intended recipients—and vice versa, receiving from a role gives a message that was sent by that role [Montesi 2013; Giallorenzo et al. 2018]. In Choral, like in any previous implementation of choreographic languages, these assumptions form a contract for the implementation of channels. This contract must be manually enforced, or communication methods might be “wrong.” A trivial example is a channel for communicating integers that always returns the constant \(\texttt {1}\) at the receiver. In the future, it would be interesting to explore the formalisation of contracts for channel middleware and libraries and the development of verified implementations.

Another property of choreographic programming—and probably the most known—is deadlock-freedom by design: the code compiled from a choreography is deadlock-free, because it is not possible to write mismatched communications in choreographies [Carbone and Montesi 2013; Dalla Preda et al. 2017; Hirsch and Garg 2022; Montesi 2023; Jongmans and van den Bos 2022]. The relevant assumptions, here, are that foreign code (in our case, Java code) used within a choreography always terminates, and that communication never blocks the sender or receiver indefinitely. In the real world, these assumptions usually do not hold, so it is important to adopt timeout and supervision mechanisms to avoid divergence and deal with failures—as exemplified in Sections 2.5 and 3.2.

Under the same assumptions for deadlock-freedom, a choreography that is tail-recursive gives the stronger liveness property of starvation-freedom (or livelock-freedom): no role ever gets stuck, or “starves” [Montesi 2023]. (In deadlock-freedom, it is sufficient that some part of the system keeps running [Kobayashi 2000].) The same holds for Choral.

Last, choreographic programming languages typically guarantee race-freedom, provided that no role uses the same channel in parallel via internal threads [Honda et al. 2016; Carbone et al. 2012; Montesi 2023; Lanese et al. 2008]—unless the underlying middleware can disambiguate messages, but this is not often the case. Choral gives finer control over race freedom, thanks to its expressive (Channel) types (cf. Section 2.4). For example, given a bidirectional channel, we can pass it as a directed channel in one direction and as a directed channel in the other direction to two separate threads. The API of directed channels would then allow the two threads to use the channel, respectively, only for sending or for receiving, which is safe to do in parallel. This control over channel usage was found to be useful in the choreographic implementation of full-duplex asynchronous communication (a pattern where roles can freely interleave different requests and responses in both directions), as found in the IRC client-server protocol. Lugovic and Montesi [2023] present a detailed discussion of this pattern and an interoperable implementation of IRC in Choral.

Since channel implementations play a key role in the properties discussed above, these implementations should ideally be simple, well-tested, or even verified. Choral’s features allow for encapsulating more sophisticated interaction behaviour as choreographies. Lugovic and Montesi [2023] started this activity, offering a reusable Choral library for programming asynchronous reactive protocols.

While, in principle, composing choreographies in Choral preserves safety and liveness, one must pay attention to the interplay with local code. Most notably, local code is free to compose and intertwine multiple instances of the same or different choreographies, as we exemplified in Section 3.2. This flexibility makes it possible to write two local programs that instantiate two choreographies and try to communicate with each other in incompatible orders, share the same channel across different instances of the same choreography running in parallel, and so on. Doing so can create communication errors and make choreographies trivially timeout and fail. This problem can be tackled in several ways, which we leave to future work. Briefly, one option is to devise middleware for making local programs agree on which choreography they want to engage in at any time. One such middleware can avoid some incompatibilities, create dedicated channels, or, in general, throw a runtime exception in case of disagreements. Other potential solutions include devising static or runtime checks for how local code composes instances of choreographies. Options for these checks encompass constraints such as keeping the graph of connections among local programs acyclic; making (projections of) choreographies that run in parallel have dedicated channels; ensuring that call to different methods of different choreographic objects follow compatible orderings; and/or synthesising an overall choreography that describes the collective behaviour of how local programs combine their (sub)choreographies, thereby providing a witness of safety and liveness [Montesi and Yoshida 2013; Coppo et al. 2016; Voinea et al. 2020; Lange et al. 2015; Carbone and Montesi 2013; Honda et al. 2016; Jacobs et al. 2022; Cruz-Filipe et al. 2017]. Some of these methods could be applied via structured concurrency libraries backed by middleware.

“Bad” programming of code that interacts with projections of choreographies is not a new issue, as it was already present in previous implementations of choreographic languages [Scalas et al. 2017; Dalla Preda et al. 2017; Carbone and Montesi 2013; Montesi 2013]. In fact, this is a general issue when composing code from libraries that engage in communications, even if these are not generated from choreographies. At the very least, Choral already guarantees type safety: the APIs of choreography projections are always respected.

Formalising Choral’s ideas, implementation, and guarantees is an interesting area of research. As already mentioned, the principles of compiling terms and data types equipped with roles as in Choral have been studied in the simple setting of the \(\lambda\) -calculus [Cruz-Filipe et al. 2022;, 2023a; Graversen et al. 2023]. The proofs in these models are not machine-checked. Mechanisation could be achieved by building on the existing formalisations of the foundations of choreographic languages made with theorem provers [Cruz-Filipe et al. 2021b;, 2021a;, 2023; Castro-Perez et al. 2021; Pohjola et al. 2022; Hirsch and Garg 2022]. These efforts are still focused on choreographic programming languages that are far less expressive than Choral, which by contrast is a large programming language that inherits all the complexities of both choreographic and object orientation.

Selection inference. Choral requires the programmer to insert the necessary selections to achieve knowledge of choice (Section 2.3). Developing techniques for inferring these selections automatically is an ongoing research topic. Typically, these techniques either modify the source choreography to include extra selections or inject hidden communications in the generated endpoint code [Lanese et al. 2013; Jongmans et al. 2015; Basu and Bultan 2016; Dalla Preda et al. 2017; Cruz-Filipe and Montesi 2020]. However, there is no silver bullet.

Since both issues are still the object of active investigation, we decided that the first version of Choral should be a base that future work can use to explore their design spaces. A promising compromise could be a hybrid, assisted way. That is, the programmer should be able to write a choreography including some selections deemed important, but also potentially missing some necessary other selections; then, a tool should detect the missing selections and propose a solution. The programmer could thus decide whether to accept the proposal or improve it manually to achieve their requirements.

In general, we believe that there is a lot of potential in future research on how to optimise communications in Choral. New algorithms might leverage annotations of channels, static analysis, and profiling data. Some algorithms might choose simpler approaches at the expense of parallelism, whereas others might take a more decentralised approach to spreading knowledge of choice to favour parallelism or energy saving (in the Internet of Things, spreading battery consumption evenly or in a focused way might be an advantage depending on the scenario).

Expressivity. We discuss a few interesting directions for future work regarding the expressivity of Choral and its type system. In general, we believe that our choreographic interpretation of object-oriented programming (OOP) allows for importing established techniques from type theory to reason statically about roles in useful ways.

Choral can capture a variety of interaction patterns, like scatter-gather and producers-consumers with races. Nevertheless, there are cases where our types can be coarse. For instance, the following could be an interface of a channel where two receivers, B and C, race to consume a message.

The return type of method \(\texttt {com}\) above guarantees that both receivers will have a value of type \(\texttt {Optional}< \texttt{S}>\) located at them. However, depending on the behaviour that the programmer wishes to model, the interface above could be an over-approximation. For example, implementations that simply discard the message sent from A or that deliver the message to both B and C will satisfy the return type. Currently, we cannot express the type of a channel that forbids such implementations, e.g., a channel guaranteeing that exactly one between B and C will obtain the message. This means that, in such cases, we have to “pollute” the continuation of the choreography with local checks at both potential receivers.

A way to achieve a more specific type for races could be to extend Choral types with existential quantification over role parameters. For example, we could write

to express an instance of \(\texttt {S}\) located at some role D in the list [B,C] (i.e., S@D can be either S@B or S@C). With this type, we can write a more specific signature: method \(\texttt {com}\) returns a value of type S@B or of type S@C, but we cannot statically know which of the two types.

Although there is some work on the use of existential quantification in simple choreography languages [Jongmans and Yoshida 2020], its application and integration with a general-purpose language like Choral poses some challenges and design choices. For instance, should roles that lose the race in method \(\texttt {com}\) be blocked? If so, then is this specific to this method or the standard interpretation of every method with an existential return type? These and similar questions beg for a thorough investigation and go beyond Choral. In fact, a satisfactory and general handling of races in choreographic programming languages is still missing. In addition to the ideas just proposed, useful inspiration to address this aspect might come from nondeterministic choice in choreographies [Lanese et al. 2008; Montesi 2023] and choreographic languages for the verification of message-passing parallel programs [Vasconcelos et al. 2022].

Another limitation of the current type system is that the number of role parameters of a choreography is fixed. This limitation is common to many choreographic languages. [Deniélou and Yoshida 2011] developed a theory for parameterising choreographies over “collections of roles,” whose sizes are determined at runtime. All roles in the same collection must be treated uniformly (e.g., broadcast). We can import that feature to Choral by allowing for role parameters to be collections. For example, we could prefix a role parameter declaration with \(\texttt {*}\) , as in *Ds, to specify that it is a collection of roles. Then, we can write the type of a channel for broadcasting data from A to all roles in the collection Ds as follows.

The method \(\texttt {com}\) for this channel should take a value of type S@A and return a value of type S@D for every role D in the collection Ds. This would require investigating how Choral can be extended with types for distributed data collections, as well.

Error handling. Choral supports exception handling at a single role, which can then propagate errors to others via knowledge of choice. However, in our experience, it is more convenient to represent failures in return types, like we did in Section 3.1 by using \(\texttt {Optional}\) . The channel APIs that we showed in this article are implemented by performing automatic retries. These APIs also have equivalent versions that wrap results in \(\texttt {Result}\) objects—essentially sum types of the transmitted value type and an error type, as in Go and Rust. Choosing among these implementations is up to the choreography programmer, and programmers might also devise channel implementations with their strategies (e.g., exponential backoff with a bound on the number of retries). Our compiler can, in principle, be extended to synthesise coordination for distributed exceptions, theorised by Carbone et al. [2008].

Type and role inference. Choral’s intended audience consists of developers familiar with OOP and, more specifically, Java. For example, our syntax extends that of Java and our library of channels follows common OOP practices, like coding to interfaces [Gamma et al. 1995]. Our design choices rely heavily on generics to achieve reusability, similar to what is done in the standard Java Collections framework [Naftalin and Wadler 2006]. However, this comes at the cost of requiring that programmers have experience with generics and additional parameters in code.

Standard remedies to the verbosity of generics include shorthands like the diamond notation and type inference [Stadelmeier et al. 2022]. We plan to lift these features to Choral and expect that the standard solutions adopted for Java will be applicable in scenarios where roles are known, without major modifications. For example, with such facilities, we could rewrite method \(\texttt {consumeItems}\) from Section 2.3 by removing all generic instantiations in its body, as follows.

Similar to generics, role parameterisation adds crucial flexibility at the cost of added verbosity. It would therefore be interesting to explore inference mechanisms for role parameters, as well, in order the lighten the syntax of Choral even further. At a basic level, programmers would be able to omit roles when these can be unambiguously determined from the context, e.g., in assignments and some method invocations. The next snippets exemplify the potential gain in simplicity from the current situation (left) to one with this feature (right).

We conjecture that this feature can be achieved by machinery similar to that already used for inferring generic parameters, because role information is available from type declarations and the typing context without ambiguity.

At a more advanced level, we could allow programmers to delegate to the Choral compiler decisions on the placement of data and computation. Consider the snippet below.

Since \(\texttt {x}\) and \(\texttt {y}\) reside at different roles, the location of \(\texttt {z}\) is ambiguous. Even more, performing the addition at Line 2 requires communication, which the compiler would need to infer and inject by appropriately using channels available from the context. This faces similar challenges to the ones previously discussed for selection inference. We believe that exploring methods for the synthesis of communication strategies in choreographies is an interesting research line in general, with a scope that goes beyond that of Choral’s.

Other features from Java. There are other features provided by Java (or other object-oriented languages) that Choral could benefit from. We do not discuss them in detail, because we do not expect that lifting them to choreographies would pose significant challenges. For example, we believe that adding wildcard types ( \(\texttt {?}\) ) would be a natural adaptation of Java’s mechanism.

The patterns and libraries that support idiomatic Java programming, like streams (from the package \(\texttt {java .util .stream}\) ), are immediately available in Choral thanks to our lifting of Java types to Choral types with a single role. In some cases, it can be interesting to generalise these patterns to multiple roles. For example, a possible interpretation of a “choreographic stream” at two roles A and B could be that of a stream of elements distributed at these roles (Stream@(A, B)< T@(C, D)>). Methods for stream operations would then take choreographies at A and B as input. Whether these choreographies would perform communications between the two roles or not would be left to the implementor and is irrelevant to the implementation of the stream.

Asynchronous programming. The choreographies that we presented here use channel APIs as if they were blocking. This does not mean that an endpoint must dedicate a thread for participating in a choreography: future versions of Java will include fibers and the asynchronous execution of blocking APIs (reactor pattern) [OpenJDK 2020]. Choral is compatible with this direction. Should programmers want to program a choreography explicitly for asynchronous execution by using continuation-passing style, our channel APIs can be extended to take choreographic continuations as parameters.

Fluid APIs from choreographic specifications. As we mentioned and discussed in Section 1, previous work explored the automatic generation of fluid APIs that enforce the code to follow a choreographic specification [Scalas et al. 2017]. Such a choreographic language cannot include computation, so it cannot express any of our use cases, and its approach does not support modularity and API control, as we discussed more in detail in the Introduction. Thus, Choral brings two improvements. First, our APIs are more reusable: they change only if the source API is changed, not if the communication behaviour of a method is simply updated. Second, the APIs of our compiled Java code are more idiomatic: they are plain object APIs that look like the typical task-oriented APIs distributed by cloud vendors [Murty 2008; Wilder 2012], which makes Choral a candidate drop-in replacement for current development practices.

Choreography-based verification and testing. Choreographic languages that are less expressive than Choral (e.g., they cannot include computation) have been used also to verify that interactions among objects respect a protocol. This is obtained by statically checking method invocations, either by using typestates [Kouzapas et al. 2018] or model checking [Scalas et al. 2019]. As noted by Hirsch and Garg [2022], choreographic programming offers a simpler development method. Indeed, verification approaches require the programmer to design both a choreographic specification and then manually take care of writing a correct implementation of the projection of each role. On the contrary, choreographic programming (and hence Choral) generates the latter automatically. Additionally, since our approach is based on compilation instead of verification, we can provide a more expressive choreographic language and apply formal reasoning techniques at the level of choreographies as in, e.g., Jongmans and van den Bos [2022]; Cruz-Filipe et al. [2023b]. Because choreographies syntactically elicit interactions, carrying out verification at this level avoids the cost of reconstructing interactions from endpoint implementations, which usually leads to a combinatorial explosion of cases.

Choreographic languages without computation have been used also in a tool for testing abstract specifications of components given as labelled transition systems [Coto et al. 2021]. The purpose, there, is to test that the communication behaviour of a component (given as a labelled transition system) complies with a choreography. By contrast, our testing tool is the first aimed at testing the functional correctness of a choreography and its generated implementation. Choral’s capability of expressing internal computation is important to this end, since it allows us to write arbitrary checks on the distributed state of the system.

With the increased adoption of cloud computing, edge computing, the Internet of Things, and microservices, the need for libraries that implementors can use to participate correctly in choreographies is growing steadily [Murty 2008; Wilder 2012; Atzori et al. 2010; Dragoni et al. 2017]. Building on previous results on the theory of choreographies, choreographic programming came with the promise of aiding in the implementation of choreography-compliant concurrent and distributed software [Montesi 2015]. While the approach has been successfully applied in principle to different scenarios [Lluch-Lafuente et al. 2015; Cruz-Filipe and Montesi 2016; López et al. 2016; López and Heussen 2017; Dalla Preda et al. 2017], the link between choreographic programming and mainstream programming has remained unexplored until now (all implementations rely on the Jolie programming language [Montesi et al. 2014], which is based on the theory of Calculus of Communicating Systems [Milner 1980]). Among the most important consequences, none of the implementations of the paradigm so far properly supported modularity—generating reusable libraries and controlling their APIs.

In this article, we have taken a fundamental step in the pursuit of the choreographic programming agenda. We have also shown that choreographies can be modelled by extending mainstream abstractions (in our case, objects) and that this leads to a choreographic programming language that supports modularity and can integrate with existing Java code. Choral is sufficiently expressive to capture use cases of different kinds, discussed the design of our compiler, and performed a first evaluation, which points out that the approach is promising. It is thus a step toward equipping programmers with a tool that safely ferries them from the design of choreographies to compliant implementations at the press of the proverbial button.

In the future, Choral could also be a useful vector for the application of research on choreographies based on other paradigms (automata, processes, etc.): researchers could develop translations of their choreography models to Choral, and then leverage our compiler to obtain library implementations that can be used in mainstream software (in Java). Hopefully, this will lead to more implementations of choreography theories, allowing for their evaluation [Ancona et al. 2016].