Opis: reliable distributed systems in OCaml

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.

REFERENCES

• 1: J. Armstrong. Making reliable distributed systems in the presence of software errors. PhD thesis, The Royal Institute of Technology, Stockholm, 2003.
• 2: G. Berry. The Foundations of Esterel. MIT Press, 2000.
• 3: Yves Bertot , Pierre Casteran, Interactive Theorem Proving and Program Development, SpringerVerlag, 2004
• 4: Edoardo Biagioni, A structured TCP in standard ML., ACM SIGCOMM Computer Communication Review, v.24 n.4, p.36-45, Oct. 1994
• 5: Brendan Burns , Kevin Grimaldi , Alexander Kostadinov , Emery D. Berger , Mark D. Corner, Flux: a language for programming high-performance servers, Proceedings of the annual conference on USENIX '06 Annual Technical Conference, p.13-13, May 30-June 03, 2006, Boston, MA
• 6: Magnus Carlsson , Thomas Hallgren, FUDGETS: a graphical user interface in a lazy functional language, Proceedings of the conference on Functional programming languages and computer architecture, p.321-330, June 09-11, 1993, Copenhagen, Denmark [doi>10.1145/165180.165228]
• 7: Hyunseok Chang , Ramesh Govindan , Sugih Jamin , Scott J. Shenker , Walter Willinger, Towards capturing representative AS-level Internet topologies, ACM SIGMETRICS Performance Evaluation Review, v.30 n.1, June 2002
• 8: Antony Courtney , Henrik Nilsson , John Peterson, The Yampa arcade, Proceedings of the 2003 ACM SIGPLAN workshop on Haskell, p.7-18, August 28-28, 2003, Uppsala, Sweden [doi>10.1145/871895.871897]
• 9: Ryan Cunningham , Eddie Kohler, Making events less slippery with eel, Proceedings of the 10th conference on Hot Topics in Operating Systems, p.3-3, June 12-15, 2005, Santa Fe, NM
• 10: Conal Elliott , Paul Hudak, Functional reactive animation, Proceedings of the second ACM SIGPLAN international conference on Functional programming, p.263-273, June 09-11, 1997, Amsterdam, The Netherlands
• 11: Cormac Flanagan , Patrice Godefroid, Dynamic partial-order reduction for model checking software, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.110-121, January 12-14, 2005, Long Beach, California, USA
• 12: Thierry Gautier , Paul Le Guernic , Löic Besnard, SIGNAL: A declarative language for synchronous programming of real-time systems, Proc. of a conference on Functional programming languages and computer architecture, p.257-277, October 1987, Portland, Oregon, United States
• 13: Patrice Godefroid , Pierre Wolper, A partial approach to model checking, Papers presented at the IEEE symposium on Logic in computer science, p.305-326, May 1994, Amsterdam, The Netherlands
• 14: G. Hager and J. Peterson. Frob: A transformational approach to the design of robot software. In ISRR, 1999.
• 15: N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud. The synchronous data-flow programming language LUSTRE. Proceedings of the IEEE, 79(9), 1991.
• 16: Mark Hayden, Distributed communication in ML, Journal of Functional Programming, v.10 n.1, p.91-120, January 2000 [doi>10.1017/S0956796899003275]
• 17: Jason Hickey , Nancy A. Lynch , Robbert van Renesse, Specifications and Proofs for Ensemble Layers, Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, p.119-133, March 22-28, 1999
• 18: Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, v.23 n.5, p.279-295, May 1997 [doi>10.1109/32.588521]
• 19: P. Hudak, A. Courtney, H. Nilsson, and J. Peterson. Arrows, robots, and functional reactive programming. In Advanced Functional Programming, volume 2638 of LNCS, 2002.
• 20: John Hughes, Generalising monads to arrows, Science of Computer Programming, v.37 n.1-3, p.67-111, May 2000 [doi>10.1016/S0167-6423(99)00023-4]
• 21: Galen C. Hunt , James R. Larus, Singularity: rethinking the software stack, ACM SIGOPS Operating Systems Review, v.41 n.2, p.37-49, April 2007 [doi>10.1145/1243418.1243424]
• 22: Charles Edwin Killian , James W. Anderson , Ryan Braud , Ranjit Jhala , Amin M. Vahdat, Mace: language support for building distributed systems, Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation, June 10-13, 2007, San Diego, California, USA
• 23: Jon Kleinberg, The small-world phenomenon: an algorithm perspective, Proceedings of the thirty-second annual ACM symposium on Theory of computing, p.163-170, May 21-23, 2000, Portland, Oregon, United States [doi>10.1145/335305.335325]
• 24: Christoph Kreitz , Mark Hayden , Jason Hickey, A Proof Environment for the Development of Group Communication Systems, Proceedings of the 15th International Conference on Automated Deduction: Automated Deduction, p.317-332, July 05-10, 1998
• 25: Xavier Leroy, A modular module system, Journal of Functional Programming, v.10 n.3, p.269-303, May 2000 [doi>10.1017/S0956796800003683]
• 26: Xavier Leroy, Formal certification of a compiler back-end or: programming a compiler with a proof assistant, Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.42-54, January 11-13, 2006, Charleston, South Carolina, USA
• 27: Peng Li , Steve Zdancewic, Combining events and threads for scalable network services implementation and evaluation of monadic, application-level concurrency primitives, ACM SIGPLAN Notices, v.42 n.6, June 2007
• 28: Shiding Lin , Aimin Pan , Zheng Zhang , Rui Guo , Zhenyu Guo, WiDS: an integrated toolkit for distributed system development, Proceedings of the 10th conference on Hot Topics in Operating Systems, p.17-17, June 12-15, 2005, Santa Fe, NM
• 29: Hai Liu , Paul Hudak, Plugging a Space Leak with an Arrow, Electronic Notes in Theoretical Computer Science (ENTCS), 193, p.29-45, November, 2007 [doi>10.1016/j.entcs.2007.10.006]
• 30: Xiaoming Liu , Christoph Kreitz , Robbert van Renesse , Jason Hickey , Mark Hayden , Kenneth Birman , Robert Constable, Building reliable, high-performance communication systems from components, Proceedings of the seventeenth ACM symposium on Operating systems principles, p.80-92, December 12-15, 1999, Charleston, South Carolina, United States
• 31: Boon Thau Loo , Tyson Condie , Joseph M. Hellerstein , Petros Maniatis , Timothy Roscoe , Ion Stoica, Implementing declarative overlays, ACM SIGOPS Operating Systems Review, v.39 n.5, December 2005
• 32: Anil Madhavapeddy , Alex Ho , Tim Deegan , David Scott , Ripduman Sohan, Melange: creating a "functional" internet, ACM SIGOPS Operating Systems Review, v.41 n.3, June 2007
• 33: R. Milner, A Calculus of Communicating Systems, Springer-Verlag New York, Inc., Secaucus, NJ, 1982
• 34: Isabelle/HOL: a proof assistant for higher-order logic, Springer-Verlag, London, 2002
• 35: Ross Paterson, A new notation for arrows, Proceedings of the sixth ACM SIGPLAN international conference on Functional programming, September 03-05, 2001, Florence, Italy
• 36: R. Paterson. The Fun of Programming. Palgrave, 2003.
• 37: J. H. Reppy. Higher-Order Concurrency. Technical Report TR92-1852, Cornell Univ, Ithaca, NY, 1992.
• 38: Adolfo Rodriguez , Charles Killian , Sooraj Bhat , Dejan Kostić , Amin Vahdat, MACEDON: methodology for automatically creating, evaluating, and designing overlay networks, Proceedings of the 1st conference on Symposium on Networked Systems Design and Implementation, p.20-20, March 29-31, 2004, San Francisco, California
• 39: Peter Sewell , James J. Leifer , Keith Wansbrough , Francesco Zappa Nardelli , Mair Allen-Williams , Pierre Habouzit , Viktor Vafeiadis, Acute: high-level programming language design for distributed computation, Proceedings of the tenth ACM SIGPLAN international conference on Functional programming, September 26-28, 2005, Tallinn, Estonia
• 40: Ion Stoica , Robert Morris , David Karger , M. Frans Kaashoek , Hari Balakrishnan, Chord: A scalable peer-to-peer lookup service for internet applications, ACM SIGCOMM Computer Communication Review, v.31 n.4, p.149-160, October 2001
• 41: S. Voulgaris, D. Gavidia, and M. Steen. Cyclon: Inexpensive membership management for unstructured p2p overlays. Journal of Network and Systems Management, 13, 2005.
• 42: S. Voulgaris and M. van Steen. Epidemic-style management of semantic overlays for content-based searching. In EuroPar, 2005.
• 43: MLDonkey, the p2p client for Linux/Unix/Windows. http://mldonkey.sourceforge.net/.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications
          Subjects: Concurrent, distributed, and parallel languages

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

General Terms:
Design, Reliability, Verification

Keywords:
arrows, distributed systems, functional programming, model checking