Awesome
Verdi Runtime
Verdi Runtime is an OCaml library providing the functionality necessary to run verified distributed systems developed in the Coq based Verdi framework on real hardware. In particular, it provides several shims that handle the lower-level details of network communication.
Requirements
OCaml 4.02.3
(or later)OCamlbuild
ocamlfind
topkg
cheerios-runtime
base64
(3.0.0 or later)yojson
(1.7.0 or later)
Installation
The easiest way to install the library (and its dependencies) is via opam:
opam pin add cheerios-runtime -n -y -k git https://github.com/uwplse/cheerios.git
opam pin add verdi-runtime -k git https://github.com/DistributedComponents/verdi-runtime.git
If you don't use opam, consult the opam file for build instructions.
Files
Shim.ml
: shim for extracted systems verified against a network semantics with unordered message passing and node reboots, implemented using UDP and state checkpointingUnorderedShim.ml
: shim for extracted systems verified against a network semantics with unordered message passing without node reboots, implemented using UDPOrderedShim.ml
: shim for extracted systems verified against a network semantics with ordered message passing, implemented using TCPDaemon.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
moduleUtil.ml
: miscellaneous functions, e.g., timestamps and conversion betweenchar list
andstring
Usage
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: