On Asynchrony and Choreographies

Research output: Contribution to journalConference articleResearchpeer-review

86 Downloads (Pure)

Abstract

Choreographic Programming is a paradigm for the development of concurrent software, where deadlocks are prevented syntactically. However, choreography languages are typically synchronous, whereas many real-world systems have asynchronous communications. Previous attempts at enriching choreographies with asynchrony rely on ad-hoc constructions, whose adequacy is only argued
informally. In this work, we formalise the properties that an asynchronous semantics for choreographies should have: messages can be sent without the intended receiver being ready, and all sent messages are eventually received. We explore how out-of-order execution, used in choreographies for modelling concurrency, can be exploited to endow choreographies with an asynchronous semantics. Our approach satisfies the properties we identified. We show how our development yields a pleasant correspondence with FIFO-based asynchronous messaging, modelled in a process calculus, and discuss how it can be adopted in more complex choreography models.
Original languageEnglish
JournalElectronic Proceedings in Theoretical Computer Science
Volume261
Pages (from-to)76-90
ISSN2075-2180
DOIs
Publication statusPublished - 2017
Event10th Interaction and Concurrency Experience -
Duration: 22. Jun 201723. Jun 2017

Conference

Conference10th Interaction and Concurrency Experience
Period22/06/201723/06/2017

Fingerprint

Semantics
Communication

Cite this

@inproceedings{ff48fbb44a9641e98316643ba9ae487a,
title = "On Asynchrony and Choreographies",
abstract = "Choreographic Programming is a paradigm for the development of concurrent software, where deadlocks are prevented syntactically. However, choreography languages are typically synchronous, whereas many real-world systems have asynchronous communications. Previous attempts at enriching choreographies with asynchrony rely on ad-hoc constructions, whose adequacy is only arguedinformally. In this work, we formalise the properties that an asynchronous semantics for choreographies should have: messages can be sent without the intended receiver being ready, and all sent messages are eventually received. We explore how out-of-order execution, used in choreographies for modelling concurrency, can be exploited to endow choreographies with an asynchronous semantics. Our approach satisfies the properties we identified. We show how our development yields a pleasant correspondence with FIFO-based asynchronous messaging, modelled in a process calculus, and discuss how it can be adopted in more complex choreography models.",
author = "Lu{\'i}s Cruz-Filipe and Fabrizio Montesi",
year = "2017",
doi = "10.4204/EPTCS.261.8",
language = "English",
volume = "261",
pages = "76--90",
journal = "Electronic Proceedings in Theoretical Computer Science",
issn = "2075-2180",
publisher = "Open Publishing Association",

}

On Asynchrony and Choreographies. / Cruz-Filipe, Luís; Montesi, Fabrizio.

In: Electronic Proceedings in Theoretical Computer Science, Vol. 261, 2017, p. 76-90.

Research output: Contribution to journalConference articleResearchpeer-review

TY - GEN

T1 - On Asynchrony and Choreographies

AU - Cruz-Filipe, Luís

AU - Montesi, Fabrizio

PY - 2017

Y1 - 2017

N2 - Choreographic Programming is a paradigm for the development of concurrent software, where deadlocks are prevented syntactically. However, choreography languages are typically synchronous, whereas many real-world systems have asynchronous communications. Previous attempts at enriching choreographies with asynchrony rely on ad-hoc constructions, whose adequacy is only arguedinformally. In this work, we formalise the properties that an asynchronous semantics for choreographies should have: messages can be sent without the intended receiver being ready, and all sent messages are eventually received. We explore how out-of-order execution, used in choreographies for modelling concurrency, can be exploited to endow choreographies with an asynchronous semantics. Our approach satisfies the properties we identified. We show how our development yields a pleasant correspondence with FIFO-based asynchronous messaging, modelled in a process calculus, and discuss how it can be adopted in more complex choreography models.

AB - Choreographic Programming is a paradigm for the development of concurrent software, where deadlocks are prevented syntactically. However, choreography languages are typically synchronous, whereas many real-world systems have asynchronous communications. Previous attempts at enriching choreographies with asynchrony rely on ad-hoc constructions, whose adequacy is only arguedinformally. In this work, we formalise the properties that an asynchronous semantics for choreographies should have: messages can be sent without the intended receiver being ready, and all sent messages are eventually received. We explore how out-of-order execution, used in choreographies for modelling concurrency, can be exploited to endow choreographies with an asynchronous semantics. Our approach satisfies the properties we identified. We show how our development yields a pleasant correspondence with FIFO-based asynchronous messaging, modelled in a process calculus, and discuss how it can be adopted in more complex choreography models.

U2 - 10.4204/EPTCS.261.8

DO - 10.4204/EPTCS.261.8

M3 - Conference article

VL - 261

SP - 76

EP - 90

JO - Electronic Proceedings in Theoretical Computer Science

JF - Electronic Proceedings in Theoretical Computer Science

SN - 2075-2180

ER -