Opis: Reliable Distributed Systems in OCaml

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.

Citation

Pierre-Évariste Dagand, Dejan Kostić, and Viktor Kuncak. Opis: Reliable distributed systems in OCaml. In ACM SIGPLAN TLDI, 2009.

BibTex Entry

@inproceedings{DagandETAL09Opis,
  author = {Pierre-\'Evariste Dagand and Dejan Kosti\'c and Viktor Kuncak},
  title = {Opis: Reliable Distributed Systems in {OCaml}},
  booktitle = {ACM SIGPLAN TLDI},
  abstract = {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.
},
  year = 2009
}