|
| |
Opis: Reliable Distributed Systems in OCaml
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 used 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.
Source code and documentation is
available
here.
Publications
- Opis: Reliable Distributed Systems in OCaml, Pierre-Evariste
Dagand, Dejan Kostic, and Viktor Kuncak, EPFL
Technical report, July 2008.
- Opis: Reliable Distributed Systems in OCaml, Pierre-Evariste
Dagand, Dejan Kostic, and Viktor Kuncak, Proceedings of TLDI, January 2009.
Faculty
Students
|
