Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
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, Published 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
Identifiers
URN: urn:nbn:se:kth:diva-147090OAI: oai:DiVA.org:kth-147090DiVA: diva2:727651
Conference
TLDI'09,Savannah, GA, USA,January 24, 2009
Note

Qc 20140704

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

Open Access in DiVA

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

Other links

ACM Digital Library

Authority records BETA

Kostic, Dejan

Search in DiVA

By author/editor
Kostic, Dejan
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 66 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

urn-nbn

Altmetric score

urn-nbn
Total: 38 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf