[T2] Engineering Distributed Systems via Protocols and Commitments
Many applications in domains such as finance, health, and e-commerce are conceptually decentralized in that they involve multiple autonomous parties. Protocol specification for such decentralized settings represents an exciting and growing area of research in the programming language community (PL). Witness the surge in interest around session types and related formalisms.
This tutorial dwells upon the theoretical foundations of multiparty protocols. We motivate information causality and information integrity as fundamental aspects of protocol specifications. Causality characterizes the knowledge needed to send a communication; integrity characterizes the consistency of communications. We show how causality and integrity yield elegant characterization of progress and safety of protocols. We present a declarative language, BSPL, that is based upon these ideas.
A fundamental challenge in protocol specification is supporting flexible concurrent enactments over a shared- nothing asynchronous infrastructure. We compare BSPL with PL approaches. Our analysis shows that the PL approaches demand more from the infrastructure (e.g., FIFO channels) but yet are unable to specify elementary real-world scenarios. BSPL would benefit from the theoretical treatments developed in the PL approaches.
Ultimately, what is of important to the parties are the social meanings of information communicated in protocol enactments. Social meanings include business contracts, which too are of interest to the PL community and which have applications for distributed ledger settings. We present the theoretical foundations for commitments (elemental business contracts) and a declarative language, Cupid, for specifying them. We show how commitments may be computed in a decentralized manner over BSPL protocols. We compare Cupid+BSPL with approaches developed in PL.
Both BSPL and Cupid stem from research done in the multiagent systems community (MAS). Despite a broad overlap of concerns, PL and MAS have largely worked in isolation from each other. This tutorial presents an opportunity for the cross fertilization of ideas.