Verdi framework runtime library
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
pkg
src
.gitignore
.merlin
.travis-ci.sh
.travis.yml
CHANGES.md
LICENSE.md
README.md
_tags
descr
opam

README.md

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

Installation

The easiest way to install the library (and its dependencies) is via OPAM.

opam repo add distributedcomponents-dev http://opam-dev.distributedcomponents.net
opam install verdi-runtime

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 checkpointing
  • UnorderedShim.ml: shim for extracted systems verified against a network semantics with unordered message passing without node reboots, implemented using UDP
  • OrderedShim.ml: shim for extracted systems verified against a network semantics with ordered message passing, implemented using TCP
  • Daemon.ml: fair task-processing event loop based on the Unix select system call, used in OrderedShim.ml and UnorderedShim.ml
  • Opts.ml: basic Verdi cluster command line argument processing based on OCaml's Arg module
  • Util.ml: miscellaneous functions, e.g., timestamps and conversion between char list and string

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.