Paper Info
Title
A Theory of Available-by-Design Communicating Systems.
Abstract
Choreographic programming is a programming-language design approach that drives error-safe protocol development in distributed systems. Starting from a global specification (choreography) one can generate distributed implementations. The advantages of this top-down approach lie in the correctness-by-design principle, where implementations (endpoints) generated from a choreography behave according to the strict control flow described in the choreography, and do not deadlock. Motivated by challenging scenarios in Cyber-Physical Systems (CPS), we study how choreographic programming can cater for dynamic infrastructures where not all endpoints are always available. We introduce the Global Quality Calculus ($GC_q$), a variant of choreographic programming for the description of communication systems where some of the components involved in a communication might fail. GCq features novel operators for multiparty, partial and collective communications. This paper studies the nature of failure-aware communication: First, we introduce $GC_q$ syntax, semantics and examples of its use. The interplay between failures and collective communications in a choreography can lead to choreographies that cannot progress due to absence of resources. In our second contribution, we provide a type system that ensures that choreographies can be realized despite changing availability conditions. A specification in $GC_q$ guides the implementation of distributed endpoints when paired with global (session) types. Our third contribution provides an endpoint-projection based methodology for the generation of failure-aware distributed processes. We show the correctness of the projection, and that well-typed choreographies with availability considerations enjoy progress.
Year
Venue
Field
2016
arXiv: Programming Languages
Programming language,Computer science,Control flow,Deadlock,Correctness,Communications system,Theoretical computer science,Choreography,Implementation,Operator (computer programming),Semantics,Distributed computing
DocType
Volume
Citations 
Journal
abs/1611.05651
0
PageRank 
References 
Authors
0.34
0
3
Name
Order
Citations
PageRank
Hugo A. López102.03
flemming nielson21769172.05
Hanne Riis Nielson31719153.77