Opis

Reliable Distributed Systems in OCaml

Abstract

The importance of distributed systems is growing as computing devices become ubiquitous and bandwidth becomes plentiful. 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.

Recently, several specialized domain-specific languages and extensions of memory-unsafe languages have been proposed to aid distributed system development. In this paper we propose an alternative to these approaches, arguing 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. In Opis, a 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. This facilitates reasoning about event functions both informally and using interactive provers. For example, this approach leads to 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 and detect any 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 have found that using Opis results in high programmer productivity and leads to concise and easily composable protocol descriptions. Moreover, Opis tools were effective in helping identify and eliminate correctness and performance problems during distributed system development.

Dependencies:

To develop your distributed systems with Opis, you need:

OCaml
The OCaml language
OMake
A modern Make

Download

Literate code:
http://perso.eleves.bretagne.ens-cachan.fr/~dagand/opis/opis.pdf
Source code:
http://perso.eleves.bretagne.ens-cachan.fr/~dagand/opis/opis.tar.gz
Technical report:
Opis: Reliable Distributed Systems in OCaml
Presentation slides:
http://perso.eleves.bretagne.ens-cachan.fr/~dagand/opis/opis_presentation.pdf
TLDI'09 slides:
http://perso.eleves.bretagne.ens-cachan.fr/~dagand/opis/opis_tldi_presentation.pdf

Contact

Pierre-Evariste Dagand

Dejan Kostic

Viktor Kuncak

License

Copyright (C) 2008-2009 Pierre-Evariste DAGAND

Opis is free software: you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation, either version 3 of the License, or (at your option) any later version.

Opis is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details.