Change search
ReferencesLink to record
Permanent link

Direct link
Opis: Reliable Distributed Systems in OCaml
EPFL.ORCID iD: 0000-0002-1256-1070
2009 (English)In: Proceedings of TLDI, Association for Computing Machinery (ACM), 2009, -78 p.Conference paper (Refereed)
Abstract [en]

Concurrency and distribution pose algorithmic and implementation challenges in developing reliable distributed systems, making the field an excellent testbed for evaluating programming language and verification paradigms. Several specialized domain-specific languages and extensions of memory-unsafe languages were proposed to aid distributed system development. We present an alternative to these approaches, showing that modern, higher-order, strongly typed, memory safe languages provide an excellent vehicle for developing and debugging distributed systems. We present Opis, a functional-reactive approach for developing distributed systems in Objective Caml. An Opis protocol description consists of a reactive function (called event function) describing the behavior of a distributed system node. The event functions in Opis are built from pure functions as building blocks, composed using the Arrow combinators. Such architecture aids reasoning about event functions both informally and using interactive theorem provers. For example, it facilitates simple termination arguments. Given a protocol description, a developer can use higher-order library functions of Opis to 1) deploy the distributed system, 2) run the distributed system in a network simulator with full-replay capabilities, 3) apply explicit-state model checking to the distributed system, detecting undesirable behaviors, and 4) do performance analysis on the system. We describe the design and implementation of Opis, and present our experience in using Opis to develop peer-to-peer overlay protocols, including the Chord distributed hash table and the Cyclon random gossip protocol. We found that using Opis results in high programmer productivity and leads to easily composable protocol descriptions. Opis tools were effective in helping identify and eliminate correctness and performance problems during distributed system development.

Place, publisher, year, edition, pages
Association for Computing Machinery (ACM), 2009. -78 p.
Keyword [en]
Reliability; Verification; Arrows; Distributed Systems; Functional Programming; Model-checking
National Category
Computer Science
URN: urn:nbn:se:kth:diva-147090OAI: diva2:727651
TLDI'09,Savannah, GA, USA,January 24, 2009

Qc 20140704

Available from: 2014-06-23 Created: 2014-06-23 Last updated: 2014-07-04Bibliographically approved

Open Access in DiVA

fulltext(1154 kB)47 downloads
File information
File name FULLTEXT01.pdfFile size 1154 kBChecksum SHA-512
Type fulltextMimetype application/pdf

Other links

ACM Digital Library

Search in DiVA

By author/editor
Kostic, Dejan
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 47 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Total: 24 hits
ReferencesLink to record
Permanent link

Direct link