LockServ with SeqNum VST applied (#2)

System with applied SeqNum transformer and extraction-related files.

Makefile

@@ -21,26 +21,34 @@ default: Makefile.coq
 	+$(MAKE) -C extraction/lockserv
 
 LOCKSERV_MLFILES = extraction/lockserv/ocaml/LockServ.ml extraction/lockserv/ocaml/LockServ.mli
+LOCKSERV_SEQNUM_MLFILES = extraction/lockserv-seqnum/ocaml/LockServSeqNum.ml extraction/lockserv-seqnum/ocaml/LockServSeqNum.mli
 
 Makefile.coq: _CoqProject
 	coq_makefile -f _CoqProject -o Makefile.coq -no-install \
           -extra '$(LOCKSERV_MLFILES)' \
 	    'extraction/lockserv/coq/ExtractLockServ.v systems/LockServ.vo' \
 	    '$$(COQC) $$(COQDEBUG) $$(COQFLAGS) extraction/lockserv/coq/ExtractLockServ.v' \
+          -extra '$(LOCKSERV_SEQNUM_MLFILES)' \
+	    'extraction/lockserv-seqnum/coq/ExtractLockServSeqNum.v systems/LockServSeqNum.vo' \
+	    '$$(COQC) $$(COQDEBUG) $$(COQFLAGS) extraction/lockserv-seqnum/coq/ExtractLockServSeqNum.v' \
           -extra-phony 'distclean' 'clean' \
 	    'rm -f $$(join $$(dir $$(VFILES)),$$(addprefix .,$$(notdir $$(patsubst %.v,%.aux,$$(VFILES)))))'
 
-$(LOCKSERV_MLFILES): Makefile.coq
+$(LOCKSERV_MLFILES) $(LOCKSERV_SEQNUM_MLFILES): Makefile.coq
 	$(MAKE) -f Makefile.coq $@
 
 lockserv:
 	+$(MAKE) -C extraction/lockserv
 
+lockserv-seqnum:
+	+$(MAKE) -C extraction/lockserv-seqnum
+
 clean:
 	if [ -f Makefile.coq ]; then \
 	  $(MAKE) -f Makefile.coq distclean; fi
 	rm -f Makefile.coq
 	$(MAKE) -C extraction/lockserv clean
+	$(MAKE) -C extraction/lockserv-seqnum clean
 
 lint:
 	@echo "Possible use of hypothesis names:"
@@ -49,4 +57,4 @@ lint:
 distclean: clean
 	rm -f _CoqProject
 
-.PHONY: default clean lint $(LOCKSERV_MLFILES) lockserv
+.PHONY: default clean lint $(LOCKSERV_MLFILES) $(LOCKSERV_SEQNUM_MLFILES) lockserv lockserv-seqnum

README.md

@@ -3,7 +3,7 @@ Verdi LockServ
 
 [![Build Status](https://api.travis-ci.org/DistributedComponents/verdi-lockserv.svg?branch=master)](https://travis-ci.org/DistributedComponents/verdi-lockserv)
 
-An implementation of a lock server, verified in Coq using the Verdi framework.
+An implementation of a simple asynchronous lock server, verified in Coq using the Verdi framework to achieve mutual exclusion.
 
 Requirements
 ------------
@@ -36,7 +36,7 @@ Then, run `./configure` in the root directory.  This will check for the appropri
 
 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. 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.
+Finally, run `make` in the root directory. This will compile the lock server definitions, check the proofs of mutual exclusion, and finally build an OCaml program from the extracted code called called `LockServMain` in the `extraction/lockserv` directory.
 
 Running LockServ on a cluster
 -----------------------------
@@ -75,3 +75,10 @@ There is a simple client in the directory `extraction/lockserv/script` that can
     >>> c.send_lock()
     'Locked'
     >>> c.send_unlock()
+
+LockServ with Sequence Numbering
+--------------------------------
+
+As originally defined, the lock server does not tolerate duplicate messages, which means that `LockServMain` can potentially give unexpected results when the underlying UDP-based runtime system generates duplicates. However, the Verdi framework defines a sequence numbering verified system transformer that when applied allows systems to ignore duplicate messages, while still guaranteeing mutual exclusion.
+
+The directory `extraction/lockserv-seqnum` contains the files needed to produce an OCaml program called `LockServSeqNumMain` which uses the sequence numbering transformer. After running `./configure` in the root directory, simply run `make` in this directory to compile the program. `LockServSeqNumMain` has the same command-line option as `LockServMain`, and the python client can be used to interface with nodes in both kinds of clusters.

configure

@@ -4,7 +4,7 @@
 
 ## Configuration options for coqproject.sh
 DEPS=(Verdi StructTact)
-DIRS=(systems extraction/lockserv/coq)
+DIRS=(systems extraction/lockserv/coq extraction/lockserv-seqnum/coq)
 CANARIES=("Verdi.Verdi" "Build Verdi before building Verdi LockServ" "StructTact.StructTactics" "Build StructTact before building Verdi LockServ")
 Verdi_DIRS=(core lib systems extraction)
 source script/coqproject.sh

extraction/lockserv-seqnum/.gitignore

@@ -0,0 +1,4 @@
+ocaml/LockServSeqNum.ml
+ocaml/LockServSeqNum.mli
+_build
+LockServSeqNumMain.native

extraction/lockserv-seqnum/Makefile

@@ -0,0 +1,21 @@
+OCAMLBUILD = ocamlbuild -use-ocamlfind -tag thread -package verdi-runtime -I ocaml -cflag -g
+
+MLEXTRACTED = ocaml/LockServSeqNum.ml ocaml/LockServSeqNum.mli
+
+MLFILES = ocaml/LockServSeqNumArrangement.ml ocaml/LockServSeqNumSerialization.ml \
+ ocaml/LockServSeqNumMain.ml ocaml/LockServSeqNumOpts.ml
+
+default: LockServSeqNumMain.native
+
+$(MLEXTRACTED):
+	+$(MAKE) -C ../.. extraction/lockserv-seqnum/$@
+
+LockServSeqNumMain.native: $(MLEXTRACTED) $(MLFILES)
+	$(OCAMLBUILD) LockServSeqNumMain.native
+
+clean:
+	$(OCAMLBUILD) -clean
+
+.PHONY: default clean $(MLEXTRACTED)
+
+.NOTPARALLEL: $(MLEXTRACTED)

extraction/lockserv-seqnum/coq/ExtractLockServSeqNum.v

@@ -0,0 +1,12 @@
+Require Import Verdi.Verdi.
+
+Require Import LockServSeqNum.
+
+Require Import ExtrOcamlBasic.
+Require Import ExtrOcamlNatInt.
+
+Require Import Verdi.ExtrOcamlBasicExt.
+Require Import Verdi.ExtrOcamlList.
+Require Import Verdi.ExtrOcamlFin.
+
+Extraction "extraction/lockserv-seqnum/ocaml/LockServSeqNum.ml" seq transformed_base_params transformed_multi_params.

extraction/lockserv-seqnum/ocaml/LockServSeqNumArrangement.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 LockServSeqNumArrangement (P : Params) = struct
+  type name = LockServSeqNum.name0
+  type state = LockServSeqNum.seq_num_data
+  type input = LockServSeqNum.msg0
+  type output = LockServSeqNum.msg0
+  type msg = LockServSeqNum.seq_num_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 with Sequence Numbering"
+
+  let serializeName = LockServSeqNumSerialization.serializeName
+
+  let deserializeName = LockServSeqNumSerialization.deserializeName
+
+  let init = fun n ->
+    let open LockServSeqNum in
+    Obj.magic ((transformed_multi_params P.num_clients).init_handlers (Obj.magic n))
+
+  let handleIO = fun n i s ->
+    let open LockServSeqNum in
+    Obj.magic ((transformed_multi_params P.num_clients).input_handlers (Obj.magic n) (Obj.magic i) (Obj.magic s))
+
+  let handleNet = fun dst src m s ->
+    let open LockServSeqNum in
+    Obj.magic ((transformed_multi_params P.num_clients).net_handlers (Obj.magic dst) (Obj.magic src) (Obj.magic m) (Obj.magic s))
+
+  let deserializeMsg = LockServSeqNumSerialization.deserializeMsg
+
+  let serializeMsg = LockServSeqNumSerialization.serializeMsg
+
+  let deserializeInput = LockServSeqNumSerialization.deserializeInput
+
+  let serializeOutput = LockServSeqNumSerialization.serializeOutput
+
+  let debug = P.debug
+
+  let debugInput = fun _ inp ->
+    Printf.printf "[%s] got input %s" (Util.timestamp ()) (LockServSeqNumSerialization.debugSerializeInput inp);
+    print_newline ()
+
+  let debugRecv = fun _ (nm, msg) ->
+    Printf.printf "[%s] receiving message %s from %s" (Util.timestamp ()) (LockServSeqNumSerialization.debugSerializeMsg msg) (serializeName nm);
+    print_newline ()
+
+  let debugSend = fun _ (nm, msg) ->
+    Printf.printf "[%s] sending message %s to %s" (Util.timestamp ()) (LockServSeqNumSerialization.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-seqnum/ocaml/LockServSeqNumMain.ml

@@ -0,0 +1,34 @@
+open LockServSeqNumOpts
+open LockServSeqNumArrangement
+
+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 = LockServSeqNumArrangement (Pms) in
+  let module Shim = UnorderedShim.Shim (Arrangement) in
+  let open Shim in
+  main { cluster = !cluster
+       ; me = !me
+       ; port = !port
+       }

extraction/lockserv-seqnum/ocaml/LockServSeqNumOpts.ml

@@ -0,0 +1,53 @@
+open List
+open Printf
+open Str
+
+let cluster_default : (LockServSeqNum.name0 * (string * int)) list = []
+let me_default : LockServSeqNum.name0 = LockServSeqNum.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 LockServSeqNumSerialization.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 LockServSeqNumSerialization.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" (LockServSeqNumSerialization.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-seqnum/ocaml/LockServSeqNumSerialization.ml

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

extraction/lockserv-seqnum/script/run.sh

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

systems/LockServSeqNum.v

@@ -0,0 +1,30 @@
+Require Import Verdi.Verdi.
+
+Require Import LockServ.
+Require Verdi.SeqNum.
+Require Import Verdi.SeqNumCorrect.
+
+Section LockServSeqNum.
+  Variable num_Clients : nat.
+
+  Definition transformed_base_params :=
+    @SeqNum.base_params (LockServ_BaseParams num_Clients) (LockServ_MultiParams num_Clients).
+
+  Definition transformed_multi_params :=
+    @SeqNum.multi_params (LockServ_BaseParams num_Clients) (LockServ_MultiParams num_Clients).
+
+  Theorem transformed_correctness :
+    forall net tr,
+      step_dup_star (params := transformed_multi_params) step_async_init net tr ->
+      @mutual_exclusion num_Clients (nwState (revertNetwork net)).
+  Proof using.
+    intros.
+    pose proof @true_in_reachable_transform _ (LockServ_MultiParams num_Clients)
+         (fun net : network => mutual_exclusion (nwState net))
+         (@true_in_reachable_mutual_exclusion num_Clients).
+    unfold true_in_reachable in *.
+    apply H0.
+    unfold reachable.
+    eauto.
+  Qed.
+End LockServSeqNum.