[Caml-list] [ANN] Opis, reliable distributed systems in OCaml

Pierre-Evariste Dagand

2008-08-18 22:59:35 UTC

Hi list,

After having delayed this announce for months, I think that Opis is
now mature enough to be publicly released. The literate code and a
technical report are available here:

http://perso.eleves.bretagne.ens-cachan.fr/~dagand/opis/

---------------------------
What Opis is about ?
---------------------------

Opis is a toolkit for large-scale distributed system programming. It
aims at easing the development of complex and reliable distributed
systems by:
- embedding a domain-specific language (EDSL) in OCaml: hence
offering a reactive, dataflow-oriented programming style while not
reinventing the wheel (type-checker, efficient code generation, ...))
- assisting the developer with powerful, integrated tools: network
simulator, debugger, model-checker and performance profiler
- working with purely-functional constructs: therefore lowering the
barrier to certify critical parts of the distributed system in a
theorem prover

----------------------
Technical details:
----------------------

The EDSL is based on the Arrow abstraction
[http://www.haskell.org/arrows/]. First, the developer defines some
pure functions, then abstracts them in the Arrow world and finally
wires them together using the Arrow combinators. The resulting
function is termed an "event function": it receives input events from
the network, the timer or the user interfaces and reacts with output
events.

Then, these output events are interpreted by the "launcher" subsystem.
For instance, the event function might ask to "Send( ip_x , TCP , data
)". Thus, the Network Launcher opens a TCP connection to "ip_x",
marshals "data" to a string and finally sends it.

Internally, the Arrow combinators build a Mealy automaton out of the
user-defined pure functions. Interestingly, Mealy automata has been
introduced and used by Lamport for decades to describe distributed
systems [http://en.wikipedia.org/wiki/State_machine_replication].

Hence, there already exists some encouraging, successful formalization
of Mealy-based systems [http://coq.inria.fr/contribs/fairisle.html].
We are currently experimenting with Coq to completely develop the
event functions in Coq (and to prove non trivial properties about the
behavior of the resulting distributed system).

Beyond an EDSL, Opis also provides some useful tools to speed-up the
development and deployment of event functions. Hence, given an event
function and without any modification, we can:

- deploy it on a real network
- simulate a network executing the event function, to test the
behavior of the system "in the large"
- debug a network of nodes running the event function, to inspect
the system "in the small", with forward and backward execution steps,
state inspection, ...
- model-check the distributed system against safety properties,
featuring a dynamic partial-order reduction mode that avoids the usual
combinatorial explosion in most systems
- performance-debug the pure functions, by measuring their
processing time and inferring their (algorithmic) complexity

Finally, by using OCaml and staying in the purely-functional world, we
benefit from:

- OCaml excellent performances (both on the computational side and
on the networking side) as well as its thoroughly tested type-checker
- the "code export" capability of theorem provers (Isabelle, Coq,
..): we have been able to certify critical code in Isabelle, export
the corresponding code and integrates it smoothly in an existing
system
- the usual benefit of functional programming: easier (informal)
reasoning and testing

--------------------------
Acknowledgements
--------------------------

I would like to thanks Zheng Li, Oleg Kiselyov and Jacques Garrigue
for their help on this list to design an efficient Arrow instance.

At this point of this long mail, I think I must also thank the reader
that have bravely read up to here ;-)

Regards,
--
Pierre-Evariste DAGAND
http://perso.eleves.bretagne.ens-cachan.fr/~dagand/

_______________________________________________
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs