We describe the semantic properties of Orc, a new language for task orchestration. Task orchestration is a form of concurrent programming in which multiple services are invoked to achieve a goal – while managing time-outs, priorities, and failures of services and communication.  Unlike traditional concurrency models, orchestration introduces an asymmetric relationship between a program and the services that constitute its environment; an orchestration invokes and receives responses from the external services, which do not initiate communication.

We start with an operational semantics of Orc, which models the threads created during an execution. The semantics allows us to prove a number of laws for Orc programs, similar to those in Kleene algebra, using strong bisimulation. Some identities of Orc, however, are difficult to establish directly using bisimulation. We show a trace semantics which is derived from the operational semantics. Equality of trace sets defines equality on programs, in that programs with identical trace sets are interchangeable in all contexts. We also show that Orc combinators are monotonic and continuous with respect to trace set inclusion, which allows us to get a least fixed point characterization of recursive programs.

Principles of Programming Seminars