Unordered shim arrangement (#1)

Executable LockServ with python client

Makefile

@@ -18,6 +18,7 @@ endif
 
 default: Makefile.coq
 	$(MAKE) -f Makefile.coq
+	+$(MAKE) -C extraction/lockserv
 
 LOCKSERV_MLFILES = extraction/lockserv/ocaml/LockServ.ml extraction/lockserv/ocaml/LockServ.mli
 

README.md

@@ -28,12 +28,50 @@ The recommended way to install the OCaml and Coq dependencies of Verdi LockServ
 
 ```
 opam repo add coq-released https://coq.inria.fr/opam/released
-opam repo add distributedcomponents http://opam.distributedcomponents.net
-opam install verdi StructTact verdi-runtime
+opam repo add distributedcomponents-dev http://opam-dev.distributedcomponents.net
+opam install verdi StructTact verdi-runtime ocamlbuild
 ```
 
 Then, run `./configure` in the root directory.  This will check for the appropriate version of Coq and ensure all necessary dependencies can be located.
 
 By default, the script assumes that `Verdi` and `StructTact` are installed in Coq's `user-contrib` directory, but this can be overridden by setting the `Verdi_PATH` and `StructTact_PATH` environment variables.
 
-Finally, run `make` in the root directory.
+Finally, run `make` in the root directory. This will compile the lock server definitions, check the proofs, and finally build an OCaml program from the extracted code called called `LockServMain` in the `extraction/lockserv` directory.
+
+Running LockServ on a cluster
+-----------------------------
+
+`LockServMain` accepts the following command-line options:
+
+```
+-me NAME             name for this node
+-port PORT           port for inputs
+-node NAME,IP:PORT   node in the cluster
+-debug               run in debug mode
+```
+
+Possible node names are `Server`, `Client-0`, `Client-1`, etc.
+
+For example, to run `LockServMain` on a cluster with IP addresses
+`192.168.0.1`, `192.168.0.2`, `192.168.0.3`, input port 8000,
+and port 9000 for inter-node communication, use the following:
+
+    # on 192.168.0.1
+    $ ./LockServMain.native -port 8000 -me Server -node Server,192.168.0.1:9000 \
+                    -node Client-0,192.168.0.2:9000 -node Client-1,192.168.0.3:9000
+
+    # on 192.168.0.2
+    $ ./LockServMain.native -port 8000 -me Client-0 -node Server,192.168.0.1:9000 \
+                    -node Client-0,192.168.0.2:9000 -node Client-1,192.168.0.3:9000
+
+    # on 192.168.0.3
+    $ ./LockServMain.native -port 8000 -me Client-1 -node Server,192.168.0.1:9000 \
+                    -node Client-0,192.168.0.2:9000 -node Client-2,192.168.0.3:9000
+
+There is a simple client in the directory `extraction/lockserv/script` that can be used as follows:
+
+    python -i client.py
+    >>> c=Client('192.168.0.2', 8000)
+    >>> c.send_lock()
+    'Locked'
+    >>> c.send_unlock()

extraction/lockserv/.gitignore

@@ -2,3 +2,4 @@ ocaml/LockServ.ml
 ocaml/LockServ.mli
 _build
 LockServMain.native
+LockServTest.native

extraction/lockserv/Makefile

@@ -3,9 +3,11 @@ OCAMLBUILD_TEST = $(OCAMLBUILD) -package oUnit -I test
 
 MLEXTRACTED = ocaml/LockServ.ml ocaml/LockServ.mli
 
-MLFILES = 
+MLFILES = ocaml/LockServArrangement.ml ocaml/LockServSerialization.ml \
+ ocaml/LockServMain.ml ocaml/LockServOpts.ml
 
-MLFILES_TEST = 
+MLFILES_TEST = test/LockServTest.ml test/OptsTest.ml \
+ test/SerializationTest.ml test/TestCommon.ml
 
 default: LockServMain.native
 
@@ -15,9 +17,16 @@ $(MLEXTRACTED):
 LockServMain.native: $(MLEXTRACTED) $(MLFILES)
 	$(OCAMLBUILD) LockServMain.native
 
+LockServTest.native: $(MLEXTRACTED) $(MLFILES) $(MLFILES_TEST)
+	$(OCAMLBUILD_TEST) LockServTest.native
+
+test: LockServTest.native
+	./LockServTest.native
+
 clean:
 	$(OCAMLBUILD) -clean
 
-.PHONY: default clean $(MLEXTRACTED)
+.PHONY: default clean test $(MLEXTRACTED)
 
+.NOTPARALLEL: LockServMain.native LockServTest.native
 .NOTPARALLEL: $(MLEXTRACTED)

extraction/lockserv/ocaml/LockServArrangement.ml

@@ -0,0 +1,68 @@
+module type IntValue = sig
+  val v : int
+end
+
+module type Params = sig
+  val debug : bool
+  val num_clients : int
+end
+
+module LockServArrangement (P : Params) = struct
+  type name = LockServ.name
+  type state = LockServ.data0
+  type input = LockServ.msg
+  type output = LockServ.msg
+  type msg = LockServ.msg
+  type client_id = int
+  type res = (output list * state) * ((name * msg) list)
+  type task_handler = name -> state -> res
+  type timeout_setter = name -> state -> float
+
+  let systemName = "Lock Server"
+
+  let serializeName = LockServSerialization.serializeName
+
+  let deserializeName = LockServSerialization.deserializeName
+
+  let init = fun n ->
+    let open LockServ in
+    Obj.magic ((lockServ_MultiParams P.num_clients).init_handlers (Obj.magic n))
+
+  let handleIO = fun n i s ->
+    let open LockServ in
+    Obj.magic ((lockServ_MultiParams P.num_clients).input_handlers (Obj.magic n) (Obj.magic i) (Obj.magic s))
+
+  let handleNet = fun dst src m s ->
+    let open LockServ in
+    Obj.magic ((lockServ_MultiParams P.num_clients).net_handlers (Obj.magic dst) (Obj.magic src) (Obj.magic m) (Obj.magic s))
+
+  let deserializeMsg = LockServSerialization.deserializeMsg
+
+  let serializeMsg = LockServSerialization.serializeMsg
+
+  let deserializeInput = LockServSerialization.deserializeInput
+
+  let serializeOutput = LockServSerialization.serializeOutput
+
+  let debug = P.debug
+
+  let debugInput = fun _ inp ->
+    Printf.printf "[%s] got input %s" (Util.timestamp ()) (LockServSerialization.debugSerializeInput inp);
+    print_newline ()
+
+  let debugRecv = fun _ (nm, msg) ->
+    Printf.printf "[%s] receiving message %s from %s" (Util.timestamp ()) (LockServSerialization.debugSerializeMsg msg) (serializeName nm);
+    print_newline ()
+
+  let debugSend = fun _ (nm, msg) ->
+    Printf.printf "[%s] sending message %s to %s" (Util.timestamp ()) (LockServSerialization.debugSerializeMsg msg) (serializeName nm);
+    print_newline ()
+
+  let createClientId () =
+    let upper_bound = 1073741823 in
+    Random.int upper_bound
+
+  let serializeClientId = string_of_int
+
+  let timeoutTasks = []
+end

extraction/lockserv/ocaml/LockServMain.ml

@@ -0,0 +1,34 @@
+open LockServOpts
+open LockServArrangement
+
+let () =
+  let () =
+    try
+      parse Sys.argv
+    with
+    | Arg.Help msg ->
+      Printf.printf "%s: %s" Sys.argv.(0) msg;
+      exit 2
+    | Arg.Bad msg ->
+      Printf.eprintf "%s" msg;
+      exit 2
+  in
+  let () =
+    try
+      validate ()
+    with Arg.Bad msg ->
+      Printf.eprintf "%s: %s." Sys.argv.(0) msg;
+      prerr_newline ();
+      exit 2
+  in
+  let module Pms = struct
+    let debug = !debug
+    let num_clients = List.length !cluster - 1
+  end in
+  let module Arrangement = LockServArrangement (Pms) in
+  let module Shim = UnorderedShim.Shim (Arrangement) in
+  let open Shim in
+  main { cluster = !cluster
+       ; me = !me
+       ; port = !port
+       }

extraction/lockserv/ocaml/LockServOpts.ml

@@ -0,0 +1,53 @@
+open List
+open Printf
+open Str
+
+let cluster_default : (LockServ.name * (string * int)) list = []
+let me_default : LockServ.name = LockServ.Server
+let port_default : int = 8351
+let debug_default : bool = true
+
+let cluster = ref cluster_default
+let me = ref me_default
+let port = ref port_default
+let debug = ref debug_default
+
+let node_spec arg nodes_ref doc =
+  let parse opt =
+    (* name,ip:port *)
+    if string_match (regexp "\\([^,]+\\),\\(.+\\):\\([0-9]+\\)") opt 0 then
+      match LockServSerialization.deserializeName (matched_group 1 opt) with
+      | Some nm -> (nm, (matched_group 2 opt, int_of_string (matched_group 3 opt)))
+      | None -> raise (Arg.Bad (sprintf "wrong argument: '%s'; option '%s' expects a proper name" arg opt))
+    else
+      raise (Arg.Bad (sprintf "wrong argument: '%s'; option '%s' expects an entry in the form 'name,host:port'" arg opt))
+  in (arg, Arg.String (fun opt -> nodes_ref := !nodes_ref @ [parse opt]), doc)
+
+let parse inp =
+  let opts =
+    [ node_spec "-node" cluster "{name,host:port} one node in the cluster"
+    ; ("-me", Arg.String (fun opt -> 
+      match LockServSerialization.deserializeName opt with 
+      | Some nm -> me := nm
+      | None -> raise (Arg.Bad (sprintf "wrong argument: '-me' expects a proper name"))), "{name} name for this node")
+    ; ("-port", Arg.Set_int port, "{port} port for client commands")
+    ; ("-debug", Arg.Set debug, "run in debug mode")
+    ] in
+   Arg.parse_argv ?current:(Some (ref 0)) inp
+    opts
+    (fun x -> raise (Arg.Bad (sprintf "%s does not take position arguments" inp.(0))))
+    "Try -help for help or one of the following."
+
+let rec assoc_unique = function
+  | [] -> true
+  | (k, _) :: l -> if mem_assoc k l then false else assoc_unique l
+
+let validate () =
+  if length !cluster = 0 then
+    raise (Arg.Bad "Please specify at least one -node");
+  if not (mem_assoc !me !cluster) then
+    raise (Arg.Bad (sprintf "%s is not a member of this cluster" (LockServSerialization.serializeName !me)));
+  if not (assoc_unique !cluster) then
+    raise (Arg.Bad "Please remove duplicate -node name entries");
+  if !port = snd (List.assoc !me !cluster) then
+    raise (Arg.Bad "Can't use same port for client commands and messages")

extraction/lockserv/ocaml/LockServSerialization.ml

@@ -0,0 +1,35 @@
+let serializeName : LockServ.name -> string = function
+  | LockServ.Server -> "Server"
+  | LockServ.Client i -> Printf.sprintf "Client-%d" i
+
+let deserializeName (s : string) : LockServ.name option =
+  match s with
+  | "Server" -> Some LockServ.Server
+  | _ -> 
+    try Scanf.sscanf s "Client-%d" (fun x -> Some (LockServ.Client (Obj.magic x)))
+    with _ -> None
+
+let deserializeMsg : string -> LockServ.msg = fun s ->
+  Marshal.from_string s 0
+
+let serializeMsg : LockServ.msg -> string = fun m ->
+  Marshal.to_string m []
+
+let deserializeInput inp c : LockServ.msg option =
+  match inp with
+  | "Unlock" -> Some LockServ.Unlock
+  | "Lock" -> Some (LockServ.Lock c)
+  | "Locked" -> Some (LockServ.Locked c)
+  | _ -> None
+
+let serializeOutput : LockServ.msg -> int * string = function
+  | LockServ.Lock _ -> (0, "Lock") (* never happens *)
+  | LockServ.Unlock -> (0, "Unlock") (* never happens *)
+  | LockServ.Locked c -> (c, "Locked")
+
+let debugSerializeInput : LockServ.msg -> string = function
+  | LockServ.Lock c -> Printf.sprintf "Lock %d" c
+  | LockServ.Unlock -> "Unlock"
+  | LockServ.Locked c -> Printf.sprintf "Locked %d" c
+
+let debugSerializeMsg = debugSerializeInput

extraction/lockserv/script/client.py

@@ -0,0 +1,55 @@
+import socket
+import re
+from struct import pack, unpack
+
+class SendError(Exception):
+    pass
+
+class ReceiveError(Exception):
+    pass
+
+class Client(object):
+    re_locked = re.compile(r'Locked')
+
+    def __init__(self, host, port, sock=None):
+        if not sock:
+            self.sock = socket.socket(socket.AF_INET, socket.SOCK_STREAM)
+            self.sock.connect((host, port))
+        else:
+            self.sock = sock
+
+    def send_msg(self, msg):
+        n = self.sock.send(pack("<I", len(msg)))
+        if n < 4:
+            raise SendError
+        else:
+            self.sock.send(msg)
+
+    def recv_msg(self, re):
+        len_bytes = self.sock.recv(4)
+        if len_bytes == '':
+            raise ReceiveError
+        else:
+            len = unpack("<I", len_bytes)[0]
+            data = self.sock.recv(len)
+            if data == '':
+                raise ReceiveError
+            else:
+                return self.parse_response(data, re)
+
+    def send_lock(self):
+        self.send_msg('Lock')
+        return self.recv_msg(self.re_locked)
+
+    def send_unlock(self):
+        self.send_msg('Unlock')
+
+    def parse_response(self, data, re):
+        try:
+            if re.match(data):
+                return 'Locked'
+            else:
+                return None
+        except Exception as e:
+            print "Parse error, data=%s" % data
+            raise e

extraction/lockserv/script/run.sh

@@ -0,0 +1,2 @@
+#!/usr/bin/env bash
+./LockServMain.native -me $1 -port $2 -node Server,localhost:9000 -node Client-0,localhost:9001 -node Client-1,localhost:9002

extraction/lockserv/test/LockServTest.ml

@@ -0,0 +1,10 @@
+open OUnit2
+
+let () =
+  run_test_tt_main 
+    ~exit
+    ("Lock Serv" >:::
+	[
+          SerializationTest.tests;
+	  OptsTest.tests
+	])