Repository files navigation

Verdi Runtime is an OCaml library providing the functionality necessary to run verified distributed systems developed in theCoq basedVerdi framework on real hardware. In particular, it provides several shims that handle the lower-level details of network communication.

• OCaml 4.02.3 (or later)
• OCamlbuild
• ocamlfind
• topkg
• cheerios-runtime
• base64 (3.0.0 or later)
• yojson (1.7.0 or later)

The easiest way to install the library (and its dependencies) is viaopam:

opam pin add cheerios-runtime -n -y -k git https://github.com/uwplse/cheerios.gitopam pin add verdi-runtime -k git https://github.com/DistributedComponents/verdi-runtime.git

If you don't use opam, consult theopam file for build instructions.

• Shim.ml: shim for extracted systems verified against a network semantics withunordered message passing and node reboots, implemented using UDP and state checkpointing
• UnorderedShim.ml: shim for extracted systems verified against a network semantics withunordered message passingwithout node reboots, implemented using UDP
• OrderedShim.ml: shim for extracted systems verified against a network semantics withordered message passing, implemented using TCP
• Daemon.ml: fair task-processing event loop based on the Unixselect system call, used inOrderedShim.ml andUnorderedShim.ml
• Opts.ml: basic Verdi cluster command line argument processing based on OCaml'sArg module
• Util.ml: miscellaneous functions, e.g., timestamps and conversion betweenchar list andstring

In order to run Verdi systems, the proper shim from Verdi Runtime must be linked to the OCaml event handler code extracted by Coq. Examples of this use can be found in Verdi-based verification projects:

• Verdi Raft
• Verdi LockServ