-
Reasoning about Choreographic Programs
Authors:
Luís Cruz-Filipe,
Eva Graversen,
Fabrizio Montesi,
Marco Peressotti
Abstract:
Choreographic programming is a paradigm where a concurrent or distributed system is developed in a top-down fashion. Programs, called choreographies, detail the desired interactions between processes, and can be compiled to distributed implementations based on message passing. Choreographic languages usually guarantee deadlock-freedom and provide an operational correspondence between choreographie…
▽ More
Choreographic programming is a paradigm where a concurrent or distributed system is developed in a top-down fashion. Programs, called choreographies, detail the desired interactions between processes, and can be compiled to distributed implementations based on message passing. Choreographic languages usually guarantee deadlock-freedom and provide an operational correspondence between choreographies and their compiled implementations, but until now little work has been done on verifying other properties.
This paper presents a Hoare-style logic for reasoning about the behaviour of choreographies, and illustrate its usage in representative examples. We show that this logic is sound and complete, and discuss decidability of its judgements. Using existing results from choreographic programming, we show that any functional correctness property proven for a choreography also holds for its compiled implementation.
△ Less
Submitted 27 April, 2023;
originally announced April 2023.
-
Alice or Bob?: Process Polymorphism in Choreographies
Authors:
Eva Graversen,
Andrew K. Hirsch,
Fabrizio Montesi
Abstract:
We present PolyChor$λ$, a language for higher-order functional \emph{choreographic programming} -- an emerging paradigm by which programmers write the desired cooperative behaviour of a system of communicating processes and then compile it into distributed implementations for each process, a translation called \emph{endpoint projection}. Unlike its predecessor, Chor$λ$, PolyChor$λ$ has both type a…
▽ More
We present PolyChor$λ$, a language for higher-order functional \emph{choreographic programming} -- an emerging paradigm by which programmers write the desired cooperative behaviour of a system of communicating processes and then compile it into distributed implementations for each process, a translation called \emph{endpoint projection}. Unlike its predecessor, Chor$λ$, PolyChor$λ$ has both type and \emph{process} polymorphism inspired by System F$_ω$. That is, PolyChor$λ$ is the first (higher-order) functional choreographic language which gives programmers the ability to write generic choreographies and determine the participants at runtime. This novel combination of features also allows PolyChor$λ$ processes to communicate \emph{distributed values}, leading to a new and intuitive way to write delegation. While some of the functional features of PolyChor$λ$ give it a weaker correspondence between the semantics of choreographies and their endpoint-projected concurrent systems than some other choreographic languages, we still get the hallmark end result of choreographic programming: projected programs are deadlock-free by design.
△ Less
Submitted 8 March, 2023;
originally announced March 2023.
-
Functional Choreographic Programming
Authors:
Luís Cruz-Filipe,
Eva Graversen,
Lovro Lugović,
Fabrizio Montesi,
Marco Peressotti
Abstract:
Choreographic programming is an emerging programming paradigm for concurrent and distributed systems, whereby developers write the communications that should be enacted and then a distributed implementation is automatically obtained by means of a compiler. Theories of choreographic programming typically come with strong theoretical guarantees about the compilation process, most notably: the genera…
▽ More
Choreographic programming is an emerging programming paradigm for concurrent and distributed systems, whereby developers write the communications that should be enacted and then a distributed implementation is automatically obtained by means of a compiler. Theories of choreographic programming typically come with strong theoretical guarantees about the compilation process, most notably: the generated implementations operationally correspond to their source choreographies and are deadlock-free.
Currently, the most advanced incarnation of the paradigm is Choral, an object-oriented choreographic programming language that targets Java. Choral deviated significantly from known theories of choreographies, and introduced the possibility of expressing higher-order choreographies (choreographies parameterised over choreographies) that are fully distributed. As a consequence, it is unclear if the usual guarantees of choreographies can still hold in the more general setting of higher-order ones.
We introduce Chorλ, the first functional choreographic programming language: it introduces a new formulation of the standard communication primitive found in choreographies as a function, and it is based upon the λ-calculus. Chorλ is the first theory that explains the core ideas of higher-order choreographic programming (as in Choral). Bridging the gap between practice and theory requires develo** a new evaluation strategy and ty** discipline for λ terms that accounts for the distributed nature of computation in choreographies. We illustrate the expressivity of Chorλ with a series of examples, which include reconstructions of the key examples from the original presentation of Choral. Our theory supports the expected properties of choreographic programming and bridges the gap between the communities of functional and choreographic programming.
△ Less
Submitted 17 August, 2022; v1 submitted 5 November, 2021;
originally announced November 2021.
-
Event structures for the reversible early internal Pi-calculus
Authors:
Eva Graversen,
Iain Phillips,
Nobuko Yoshida
Abstract:
The pi-calculus is a widely used process calculus, which models communications between processes and allows the passing of communication links. Various operational semantics of the pi-calculus have been proposed, which can be classified according to whether transitions are unlabelled (so-called reductions) or labelled. With labelled transitions, we can distinguish early and late semantics. The ear…
▽ More
The pi-calculus is a widely used process calculus, which models communications between processes and allows the passing of communication links. Various operational semantics of the pi-calculus have been proposed, which can be classified according to whether transitions are unlabelled (so-called reductions) or labelled. With labelled transitions, we can distinguish early and late semantics. The early version allows a process to receive names it already knows from the environment, while the late semantics and reduction semantics do not. All existing reversible versions of the pi-calculus use reduction or late semantics, despite the early semantics of the (forward-only) pi-calculus being more widely used than the late. We define piIH, the first reversible early pi-calculus, and give it a denotational semantics in terms of reversible bundle event structures. The new calculus is a reversible form of the internal pi-calculus, which is a subset of the pi-calculus where every link sent by an output is private, yielding greater symmetry between inputs and outputs.
△ Less
Submitted 10 April, 2020; v1 submitted 2 April, 2020;
originally announced April 2020.
-
Towards a Categorical Representation of Reversible Event Structures
Authors:
Eva Graversen,
Iain Phillips,
Nobuko Yoshida
Abstract:
We study categories for reversible computing, focussing on reversible forms of event structures. Event structures are a well-established model of true concurrency. There exist a number of forms of event structures, including prime event structures, asymmetric event structures, and general event structures. More recently, reversible forms of these types of event structures have been defined. We…
▽ More
We study categories for reversible computing, focussing on reversible forms of event structures. Event structures are a well-established model of true concurrency. There exist a number of forms of event structures, including prime event structures, asymmetric event structures, and general event structures. More recently, reversible forms of these types of event structures have been defined. We formulate corresponding categories and functors between them. We show that products and co-products exist in many cases. In most work on reversible computing, including reversible process calculi, a cause-respecting condition is posited, meaning that the cause of an event may not be reversed before the event itself. Since reversible event structures are not assumed to be cause-respecting in general, we also define cause-respecting subcategories of these event structures. Our longer-term aim is to formulate event structure semantics for reversible process calculi.
△ Less
Submitted 10 April, 2017;
originally announced April 2017.
