From cf0e2494de18b91eeb51a757c9f7c8ae71c34dd8 Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Fri, 5 May 2017 23:09:28 -0500 Subject: [PATCH] more requirements --- README.md | 24 +++++++++++++++++++++++- 1 file changed, 23 insertions(+), 1 deletion(-) 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 --------------------------------