diff --git a/README.md b/README.md index c8ce270..137bb42 100644 --- a/README.md +++ b/README.md @@ -14,13 +14,21 @@ Definitions and proofs: - [`Verdi`](https://github.com/uwplse/verdi) - [`StructTact`](https://github.com/uwplse/StructTact) -Executable code: +Executable program: - [`OCaml 4.02.3`](https://ocaml.org) (or later) - [`OCamlbuild`](https://github.com/ocaml/ocamlbuild) - [`ocamlfind`](http://projects.camlcity.org/projects/findlib.html) - [`verdi-runtime`](https://github.com/DistributedComponents/verdi-runtime) +Client to interface with program: + +- [`Python 2.7`](https://www.python.org/download/releases/2.7/) + +Testing of unverified code: + +- [`OUnit 2.0.0`](http://ounit.forge.ocamlcore.org) + Building -------- @@ -68,6 +76,9 @@ and port 9000 for inter-node communication, use the following: $ ./LockServMain.native -port 8000 -me Client-1 -node Server,192.168.0.1:9000 \ -node Client-0,192.168.0.2:9000 -node Client-1,192.168.0.3:9000 +Client Program for LockServ +--------------------------- + There is a simple client written in Python in the directory `extraction/lockserv/script` that can be used as follows: $ python -i client.py @@ -76,6 +87,17 @@ There is a simple client written in Python in the directory `extraction/lockserv 'Locked' >>> c.send_unlock() +Tests for Unverified Code +------------------------- + +Some example unit tests for unverified OCaml code are included in `extraction/lockserv/test`. To execute these tests, first install the OUnit library via OPAM: + +``` +opam install ounit +``` + +Then, go to `extraction/lockserv` and run `make test`. + LockServ with Sequence Numbering --------------------------------