From 0289bb813f9057da897c01a20aae6ff9d2da34f5 Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Mon, 27 Feb 2017 16:03:53 -0600 Subject: [PATCH] Unordered shim arrangement (#1) Executable LockServ with python client --- Makefile | 1 + README.md | 44 ++- extraction/lockserv/.gitignore | 1 + extraction/lockserv/Makefile | 15 +- .../lockserv/ocaml/LockServArrangement.ml | 68 ++++ extraction/lockserv/ocaml/LockServMain.ml | 34 ++ extraction/lockserv/ocaml/LockServOpts.ml | 53 +++ .../lockserv/ocaml/LockServSerialization.ml | 35 ++ extraction/lockserv/ocaml/Serialization.ml | 16 - extraction/lockserv/script/client.py | 55 ++++ extraction/lockserv/script/run.sh | 2 + extraction/lockserv/test/LockServTest.ml | 10 + extraction/lockserv/test/OptsTest.ml | 53 +++ extraction/lockserv/test/SerializationTest.ml | 32 ++ extraction/lockserv/test/TestCommon.ml | 3 + systems/LockServ.v | 309 ++++++++++++------ 16 files changed, 606 insertions(+), 125 deletions(-) create mode 100644 extraction/lockserv/ocaml/LockServArrangement.ml create mode 100644 extraction/lockserv/ocaml/LockServMain.ml create mode 100644 extraction/lockserv/ocaml/LockServOpts.ml create mode 100644 extraction/lockserv/ocaml/LockServSerialization.ml delete mode 100644 extraction/lockserv/ocaml/Serialization.ml create mode 100644 extraction/lockserv/script/client.py create mode 100755 extraction/lockserv/script/run.sh create mode 100644 extraction/lockserv/test/LockServTest.ml create mode 100644 extraction/lockserv/test/OptsTest.ml create mode 100644 extraction/lockserv/test/SerializationTest.ml create mode 100644 extraction/lockserv/test/TestCommon.ml diff --git a/Makefile b/Makefile index abf7831..5deb3ea 100644 --- a/Makefile +++ b/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 diff --git a/README.md b/README.md index c9b150f..d235197 100644 --- a/README.md +++ b/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() diff --git a/extraction/lockserv/.gitignore b/extraction/lockserv/.gitignore index f04faf5..e7b3591 100644 --- a/extraction/lockserv/.gitignore +++ b/extraction/lockserv/.gitignore @@ -2,3 +2,4 @@ ocaml/LockServ.ml ocaml/LockServ.mli _build LockServMain.native +LockServTest.native diff --git a/extraction/lockserv/Makefile b/extraction/lockserv/Makefile index 0ac7088..2ec1b2b 100644 --- a/extraction/lockserv/Makefile +++ b/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) diff --git a/extraction/lockserv/ocaml/LockServArrangement.ml b/extraction/lockserv/ocaml/LockServArrangement.ml new file mode 100644 index 0000000..6ebd79d --- /dev/null +++ b/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 diff --git a/extraction/lockserv/ocaml/LockServMain.ml b/extraction/lockserv/ocaml/LockServMain.ml new file mode 100644 index 0000000..85515ec --- /dev/null +++ b/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 + } diff --git a/extraction/lockserv/ocaml/LockServOpts.ml b/extraction/lockserv/ocaml/LockServOpts.ml new file mode 100644 index 0000000..d2a1216 --- /dev/null +++ b/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") diff --git a/extraction/lockserv/ocaml/LockServSerialization.ml b/extraction/lockserv/ocaml/LockServSerialization.ml new file mode 100644 index 0000000..c0993e0 --- /dev/null +++ b/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 diff --git a/extraction/lockserv/ocaml/Serialization.ml b/extraction/lockserv/ocaml/Serialization.ml deleted file mode 100644 index 30f2844..0000000 --- a/extraction/lockserv/ocaml/Serialization.ml +++ /dev/null @@ -1,16 +0,0 @@ -open LockServ - -let serializeName : name -> string = function - | Server -> "Server" - | Client i -> Printf.sprintf "Client-%d" i - -let deserializeName : string -> name option = function - | "Server" -> Some Server - | try Scanf.sscanf s "Client-%d" (fun x -> Some (Client (Obj.magic x))) - with _ -> None - -let deserializeMsg : string -> msg = fun s -> - Marshal.from_string s 0 - -let serializeMsg : msg -> string = fun m -> - Marshal.to_string m [] diff --git a/extraction/lockserv/script/client.py b/extraction/lockserv/script/client.py new file mode 100644 index 0000000..42e4eed --- /dev/null +++ b/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("::: + [ + SerializationTest.tests; + OptsTest.tests + ]) diff --git a/extraction/lockserv/test/OptsTest.ml b/extraction/lockserv/test/OptsTest.ml new file mode 100644 index 0000000..3dafc65 --- /dev/null +++ b/extraction/lockserv/test/OptsTest.ml @@ -0,0 +1,53 @@ +open OUnit2 +open ListLabels +open TestCommon + +let tear_down () test_ctxt = + LockServOpts.cluster := LockServOpts.cluster_default; + LockServOpts.me := LockServOpts.me_default; + LockServOpts.port := LockServOpts.port_default; + LockServOpts.debug := LockServOpts.debug_default + +let test_parse_correct_line test_ctxt = + LockServOpts.parse (arr_of_string "./LockServMain.native -me Server -port 8000 -node Server,localhost:9000 -node Client-0,localhost:9001 -node Client-1,localhost:9002"); + assert_equal LockServ.Server !LockServOpts.me; + assert_equal 8000 !LockServOpts.port; + assert_equal [(LockServ.Server, ("localhost", 9000)); (LockServ.Client 0, ("localhost", 9001)); (LockServ.Client 1, ("localhost", 9002))] !LockServOpts.cluster; + assert_equal true !LockServOpts.debug + +let test_validate_correct_line test_ctxt = + LockServOpts.parse (arr_of_string "./LockServMain.native -me Server -port 8000 -node Server,localhost:9000 -node Client-0,localhost:9001 -node Client-1,localhost:9002"); + assert_equal () (LockServOpts.validate ()) + +let test_validate_empty_cluster test_ctxt = + LockServOpts.parse (arr_of_string "./LockServMain.native -me Server -port 8000"); + assert_raises (Arg.Bad "Please specify at least one -node") LockServOpts.validate + +let test_validate_me_not_cluster_member test_ctxt = + LockServOpts.parse (arr_of_string "./LockServMain.native -me Server -port 8000 -node Client-0,localhost:9001 -node Client-1,localhost:9002"); + assert_raises (Arg.Bad "Server is not a member of this cluster") LockServOpts.validate + +let test_validate_duplicate_node_entry test_ctxt = + LockServOpts.parse (arr_of_string "./LockServMain.native -me Server -port 8000 -node Server,localhost:9000 -node Server,localhost:9001"); + assert_raises (Arg.Bad "Please remove duplicate -node name entries") LockServOpts.validate + +let test_validate_same_client_msg_port test_ctxt = + LockServOpts.parse (arr_of_string "./LockServMain.native -me Server -port 8000 -node Server,localhost:8000 -node Client-0,localhost:9001"); + assert_raises (Arg.Bad "Can't use same port for client commands and messages") LockServOpts.validate + +let test_list = + ["parse correct line", test_parse_correct_line; + "validate correct line", test_validate_correct_line; + "validate empty cluster", test_validate_empty_cluster; + "validate me not member of cluster", test_validate_me_not_cluster_member; + "validate duplicate node entry", test_validate_duplicate_node_entry; + "validate same client/msg port", test_validate_same_client_msg_port; + ] + +let tests = + "Opts" >::: + (map test_list ~f:(fun (name, test_fn) -> + name >:: (fun test_ctxt -> + bracket ignore tear_down test_ctxt; + test_fn test_ctxt) + )) diff --git a/extraction/lockserv/test/SerializationTest.ml b/extraction/lockserv/test/SerializationTest.ml new file mode 100644 index 0000000..f1ef762 --- /dev/null +++ b/extraction/lockserv/test/SerializationTest.ml @@ -0,0 +1,32 @@ +open OUnit2 +open ListLabels + +let tear_down () test_ctxt = () + +let test_deserialize_server_name test_ctxt = + assert_equal (Some LockServ.Server) (LockServSerialization.deserializeName "Server") + +let test_deserialize_client_name test_ctxt = + assert_equal (Some (LockServ.Client 5)) (LockServSerialization.deserializeName "Client-5") + +let test_serialize_server_name test_ctxt = + assert_equal "Server" (LockServSerialization.serializeName LockServ.Server) + +let test_serialize_client_name test_ctxt = + assert_equal "Client-0" (LockServSerialization.serializeName (LockServ.Client 0)) + +let test_list = + [ + "deserialize server name", test_deserialize_server_name; + "deserialize client name", test_deserialize_client_name; + "serialize server name", test_serialize_server_name; + "serialize client name", test_serialize_client_name; + ] + +let tests = + "Serialization" >::: + (map test_list ~f:(fun (name, test_fn) -> + name >:: (fun test_ctxt -> + bracket ignore tear_down test_ctxt; + test_fn test_ctxt) + )) diff --git a/extraction/lockserv/test/TestCommon.ml b/extraction/lockserv/test/TestCommon.ml new file mode 100644 index 0000000..cadef13 --- /dev/null +++ b/extraction/lockserv/test/TestCommon.ml @@ -0,0 +1,3 @@ +let arr_of_string s = + let listl = (Str.split (Str.regexp " ") s) in + (Array.of_list listl) diff --git a/systems/LockServ.v b/systems/LockServ.v index bfa7db1..0029c0b 100644 --- a/systems/LockServ.v +++ b/systems/LockServ.v @@ -24,21 +24,19 @@ Section LockServ. decide equality. apply fin_eq_dec. Qed. - - Inductive Msg := - | Lock : Msg + | Lock : nat -> Msg | Unlock : Msg - | Locked : Msg. + | Locked : nat -> Msg. Definition Msg_eq_dec : forall a b : Msg, {a = b} + {a <> b}. - decide equality. + decide equality; auto using Nat.eq_dec. Qed. Definition Input := Msg. Definition Output := Msg. - Record Data := mkData { queue : list Client_index ; held : bool }. + Record Data := mkData { queue : list (Client_index * nat) ; held : bool }. Definition init_data (n : Name) : Data := mkData [] false. @@ -46,13 +44,13 @@ Section LockServ. Definition ClientNetHandler (i : Client_index) (m : Msg) : Handler Data := match m with - | Locked => (put (mkData [] true)) >> write_output Locked + | Locked id => (put (mkData [] true)) >> write_output (Locked id) | _ => nop end. Definition ClientIOHandler (i : Client_index) (m : Msg) : Handler Data := match m with - | Lock => send (Server, Lock) + | Lock id => send (Server, Lock id) | Unlock => data <- get ;; when (held data) (put (mkData [] false) >> send (Server, Unlock)) | _ => nop @@ -62,14 +60,14 @@ Section LockServ. st <- get ;; let q := queue st in match m with - | Lock => + | Lock id => match src with | Server => nop | Client c => - when (null q) (send (src, Locked)) >> put (mkData (q++[c]) (held st)) + when (null q) (send (src, Locked id)) >> put (mkData (q ++ [(c, id)]) (held st)) end | Unlock => match q with - | _ :: x :: xs => put (mkData (x :: xs) (held st)) >> send (Client x, Locked) + | _ :: (c, id) :: xs => put (mkData ((c, id) :: xs) (held st)) >> send (Client c, Locked id) | _ => put (mkData [] (held st)) end | _ => nop @@ -97,8 +95,6 @@ Section LockServ. ClientIOHandler, ServerIOHandler in *). - - Definition Nodes := Server :: list_Clients. Theorem In_n_Nodes : @@ -126,8 +122,6 @@ Section LockServ. + apply all_fin_NoDup. Qed. - - Global Instance LockServ_BaseParams : BaseParams := { data := Data ; @@ -167,8 +161,8 @@ Section LockServ. Definition locks_correct (sigma : name -> data) : Prop := forall n, held (sigma (Client n)) = true -> - exists t, - queue (sigma Server) = n :: t. + exists id t, + queue (sigma Server) = (n, id) :: t. (* We first show that this actually implies mutual exclusion. *) Lemma locks_correct_implies_mutex : @@ -186,7 +180,7 @@ Section LockServ. Definition valid_unlock q h c p := pSrc p = Client c /\ - (exists t, q = c :: t) /\ + (exists (id : nat) t, q = (c, id) :: t) /\ h = false. Definition locks_correct_unlock (sigma : name -> data) (p : packet) : Prop := @@ -195,23 +189,22 @@ Section LockServ. Definition valid_locked q h c p := pDst p = Client c /\ - (exists t, q = c :: t) /\ + (exists (id : nat) t, q = (c, id) :: t) /\ h = false. Definition locks_correct_locked (sigma : name -> data) (p : packet) : Prop := - pBody p = Locked -> + forall id, pBody p = Locked id -> exists c, valid_locked (queue (sigma Server)) (held (sigma (Client c))) c p. - Definition LockServ_network_invariant (sigma : name -> data) (p : packet) : Prop := locks_correct_unlock sigma p /\ locks_correct_locked sigma p. Definition LockServ_network_network_invariant (p q : packet) : Prop := (pBody p = Unlock -> pBody q = Unlock -> False) /\ - (pBody p = Locked -> pBody q = Unlock -> False) /\ - (pBody p = Unlock -> pBody q = Locked -> False) /\ - (pBody p = Locked -> pBody q = Locked -> False). + (forall id, pBody p = Locked id -> pBody q = Unlock -> False) /\ + (forall id, pBody p = Unlock -> pBody q = Locked id -> False) /\ + (forall id id', pBody p = Locked id -> pBody q = Locked id' -> False). Lemma nwnw_sym : forall p q, @@ -219,7 +212,7 @@ Section LockServ. LockServ_network_network_invariant q p. Proof using. unfold LockServ_network_network_invariant. - intuition. + intuition eauto. Qed. Lemma locks_correct_init : @@ -232,7 +225,7 @@ Section LockServ. forall h i st u out st' ms, InputHandler h i st = (u, out, st', ms) -> (exists c, h = Client c /\ - ((i = Lock /\ out = [] /\ st' = st /\ ms = [(Server, Lock)]) \/ + ((exists id, i = Lock id /\ out = [] /\ st' = st /\ ms = [(Server, Lock id)]) \/ (i = Unlock /\ out = [] /\ held st' = false /\ ((held st = true /\ ms = [(Server, Unlock)]) \/ (st' = st /\ ms = []))))) \/ @@ -242,7 +235,7 @@ Section LockServ. intros. repeat break_match; repeat tuple_inversion; subst; simpl in *; subst; simpl in *. - - left. eexists. intuition. + - left. eexists. intuition eauto. - left. eexists. intuition. - left. eexists. intuition. - auto. @@ -279,8 +272,17 @@ Section LockServ. locks_correct sigma -> locks_correct (update name_eq_dec sigma h st'). Proof using. - set_up_input_handlers; - auto using locks_correct_update_false. + set_up_input_handlers; break_exists; repeat break_and; + eauto using locks_correct_update_false. + subst. + unfold locks_correct in *. + intuition. + find_rewrite_lem update_nop_ext. + pose proof (H0 n H). + break_exists. + exists x1, x2. + rewrite update_nop_ext. + assumption. Qed. Lemma ClientNetHandler_cases : @@ -288,11 +290,11 @@ Section LockServ. ClientNetHandler c m st = (u, out, st', ms) -> ms = [] /\ ((st' = st /\ out = [] ) \/ - (m = Locked /\ out = [Locked] /\ held st' = true)). + (exists id, m = Locked id /\ out = [Locked id] /\ held st' = true)). Proof using. handler_unfold. intros. - repeat break_match; repeat tuple_inversion; subst; auto. + repeat break_match; repeat tuple_inversion; subst; intuition eauto. Qed. Lemma ServerNetHandler_cases : @@ -300,23 +302,23 @@ Section LockServ. ServerNetHandler src m st = (u, out, st', ms) -> out = [] /\ ((exists c, src = Client c /\ - (m = Lock /\ - queue st' = queue st ++ [c] /\ - ((queue st = [] /\ ms = [(Client c, Locked)]) \/ - (queue st <> [] /\ ms = [])))) \/ + (exists id, m = Lock id /\ queue st' = queue st ++ [(c, id)] /\ + ((exists id, queue st = [] /\ ms = [(Client c, Locked id)]) \/ + (queue st <> [] /\ ms = [])))) \/ ((m = Unlock /\ queue st' = tail (queue st) /\ ((queue st' = [] /\ ms = []) \/ - (exists next t, queue st' = next :: t /\ ms = [(Client next, Locked)])))) \/ + (exists c' id t, queue st' = (c', id) :: t /\ ms = [(Client c', Locked id)])))) \/ ms = [] /\ st' = st). Proof using. handler_unfold. intros. repeat break_match; repeat tuple_inversion; subst. - find_apply_lem_hyp null_sound. find_rewrite. simpl. - intuition. left. eexists. intuition. + intuition. left. eexists. intuition. eexists. intuition. + left. eexists. intuition. - simpl. find_apply_lem_hyp null_false_neq_nil. - intuition. left. eexists. intuition. + intuition. left. eexists. intuition. eexists. intuition. - simpl. auto. - simpl. destruct st; simpl in *; subst; auto. - simpl in *. intuition. @@ -324,11 +326,11 @@ Section LockServ. - simpl. intuition. Qed. - Definition at_head_of_queue sigma c := (exists t, queue (sigma Server) = c :: t). + Definition at_head_of_queue sigma c := (exists id t, queue (sigma Server) = (c, id) :: t). Lemma at_head_of_queue_intro : - forall sigma c t, - queue (sigma Server) = c :: t -> + forall sigma c id t, + queue (sigma Server) = (c, id) :: t -> at_head_of_queue sigma c. Proof using. unfold at_head_of_queue. @@ -348,15 +350,16 @@ Section LockServ. Qed. Lemma locks_correct_locked_at_head : - forall sigma p c, + forall sigma p c id, pDst p = Client c -> - pBody p = Locked -> + pBody p = Locked id -> locks_correct_locked sigma p -> at_head_of_queue sigma c. Proof using. unfold locks_correct_locked. firstorder. - repeat find_rewrite. find_inversion. + repeat find_rewrite. pose proof (H1 id). concludes. break_exists. unfold valid_locked in *. break_and. break_exists. + find_rewrite. find_injection. eauto using at_head_of_queue_intro. Qed. @@ -468,7 +471,7 @@ Section LockServ. locks_correct_locked sigma p -> locks_correct (update name_eq_dec sigma (pDst p) st'). Proof using. - set_up_net_handlers; + set_up_net_handlers; break_exists; break_and; eauto using locks_correct_update_true, locks_correct_locked_at_head, all_clients_false_locks_correct_server_update, empty_queue_all_clients_false, @@ -477,8 +480,8 @@ Section LockServ. Qed. Lemma locks_correct_unlock_sent_lock : - forall sigma p, - pBody p = Lock -> + forall sigma p id, + pBody p = Lock id -> locks_correct_unlock sigma p. Proof using. unfold locks_correct_unlock. @@ -486,8 +489,8 @@ Section LockServ. Qed. Lemma locks_correct_unlock_sent_locked : - forall sigma p, - pBody p = Locked -> + forall sigma p id, + pBody p = Locked id -> locks_correct_unlock sigma p. Proof using. unfold locks_correct_unlock. @@ -501,31 +504,39 @@ Section LockServ. locks_correct_unlock sigma p -> locks_correct_unlock (update name_eq_dec sigma h st') p. Proof using. - set_up_input_handlers. + set_up_input_handlers; break_exists; break_and; subst; try rewrite update_nop_ext; auto. destruct (pBody p) eqn:?. - - auto using locks_correct_unlock_sent_lock. + - eauto using locks_correct_unlock_sent_lock. - now erewrite unlock_in_flight_all_clients_false in * by eauto. - - auto using locks_correct_unlock_sent_locked. + - eauto using locks_correct_unlock_sent_locked. Qed. Lemma locked_in_flight_all_clients_false : - forall sigma p, - pBody p = Locked -> + forall sigma p id, + pBody p = Locked id -> locks_correct_locked sigma p -> locks_correct sigma -> (forall c, held (sigma (Client c)) = false). Proof using. intros. destruct (held (sigma (Client c))) eqn:?; auto. - firstorder. find_copy_apply_lem_hyp locks_correct_true_at_head_of_queue; auto. unfold at_head_of_queue in *. break_exists. + unfold locks_correct_locked in *. + pose proof (H0 id). + concludes. + break_exists. + unfold valid_locked in H3. + break_and. + break_exists. + find_rewrite. + find_injection. congruence. Qed. Lemma locks_correct_locked_sent_lock : - forall sigma p, - pBody p = Lock -> + forall sigma p id, + pBody p = Lock id -> locks_correct_locked sigma p. Proof using. unfold locks_correct_locked. @@ -548,10 +559,10 @@ Section LockServ. locks_correct_locked sigma p -> locks_correct_locked (update name_eq_dec sigma h st') p. Proof using. - set_up_input_handlers. + set_up_input_handlers; break_exists; break_and; subst; try rewrite update_nop_ext; auto. destruct (pBody p) eqn:?. - - auto using locks_correct_locked_sent_lock. - - auto using locks_correct_locked_sent_unlock. + - eauto using locks_correct_locked_sent_lock. + - eauto using locks_correct_locked_sent_unlock. - now erewrite locked_in_flight_all_clients_false in * by eauto. Qed. @@ -576,12 +587,23 @@ Section LockServ. pSrc p = h -> locks_correct_unlock (update name_eq_dec sigma h st') p. Proof using. - set_up_input_handlers; + set_up_input_handlers; break_exists; break_and; subst; try rewrite update_nop_ext; - auto using locks_correct_unlock_sent_lock, + eauto using locks_correct_unlock_sent_lock, locks_correct_unlock_true_to_false, locks_correct_true_at_head_of_queue. - Qed. + unfold locks_correct_unlock. + intro. + exists x. + unfold valid_unlock. + split; auto. + simpl in *. + break_or_hyp; intuition. + - find_injection. + congruence. + - find_injection. + congruence. + Qed. Lemma locks_correct_locked_input_handlers_new : forall h i sigma u st' out ms p, @@ -589,30 +611,42 @@ Section LockServ. In (pDst p, pBody p) ms -> locks_correct_locked (update name_eq_dec sigma h st') p. Proof using. - set_up_input_handlers; - auto using locks_correct_locked_sent_lock, locks_correct_locked_sent_unlock. + set_up_input_handlers; break_exists; break_and; subst; try rewrite update_nop_ext; auto. + - simpl in *. + intuition. + find_injection. + congruence. + - eauto using locks_correct_locked_sent_lock, locks_correct_locked_sent_unlock. Qed. Lemma nwnw_locked_lock : - forall p q, + forall p q id, LockServ_network_network_invariant p q -> - pBody p = Locked -> - pBody q = Lock. + pBody p = Locked id -> + exists id', pBody q = Lock id'. Proof using. unfold LockServ_network_network_invariant. intros. destruct (pBody q); intuition; try discriminate. + - exists n; auto. + - pose proof (H _ H0). + intuition. + - pose proof (H4 _ n H0). + congruence. Qed. Lemma nwnw_unlock_lock : forall p q, LockServ_network_network_invariant p q -> pBody p = Unlock -> - pBody q = Lock. + exists id, pBody q = Lock id. Proof using. unfold LockServ_network_network_invariant. intros. destruct (pBody q); intuition; try discriminate. + - exists n; auto. + - pose proof (H2 n H0). + congruence. Qed. Lemma locks_correct_unlock_at_head : @@ -666,10 +700,30 @@ Section LockServ. LockServ_network_network_invariant p q -> locks_correct_unlock (update name_eq_dec sigma (pDst p) st') q. Proof using. - set_up_net_handlers; - eauto using locks_correct_unlock_sent_lock, nwnw_locked_lock, + set_up_net_handlers; break_exists; break_and; subst; eauto using locks_correct_unlock_sent_lock, nwnw_locked_lock, locks_correct_unlock_at_head_preserved, snoc_at_head_of_queue_preserved, nwnw_unlock_lock, nil_at_head_of_queue_preserved. + - unfold locks_correct_unlock in *. + intros. + concludes. + break_exists. + pose proof (nwnw_locked_lock H2 H). + break_exists. + congruence. + - unfold locks_correct_unlock in *. + intros. + concludes. + break_exists. + pose proof (nwnw_unlock_lock H2 H). + break_exists. + congruence. + - unfold locks_correct_unlock in *. + intros. + concludes. + break_exists. + pose proof (nwnw_unlock_lock H2 H). + break_exists. + congruence. Qed. Lemma locks_correct_locked_at_head_preserved : @@ -680,6 +734,9 @@ Section LockServ. Proof using. unfold locks_correct_locked, valid_locked. intuition. + pose proof (H id H1). + break_exists. + break_and. break_exists. exists x. intuition. @@ -695,10 +752,31 @@ Section LockServ. LockServ_network_network_invariant p q -> locks_correct_locked (update name_eq_dec sigma (pDst p) st') q. Proof using. - set_up_net_handlers; + set_up_net_handlers; break_exists; break_and; subst; eauto using locks_correct_locked_sent_lock, nwnw_locked_lock, locks_correct_locked_at_head_preserved, snoc_at_head_of_queue_preserved, nwnw_unlock_lock, nil_at_head_of_queue_preserved. + - unfold locks_correct_locked in *. + intros. + pose proof (H1 _ H3). + break_exists. + pose proof (nwnw_locked_lock H2 H). + break_exists. + congruence. + - unfold locks_correct_locked in *. + intros. + pose proof (H1 id H3). + break_exists. + pose proof (nwnw_unlock_lock H2 H). + break_exists. + congruence. + - unfold locks_correct_locked in *. + intros. + pose proof (H1 id H3). + break_exists. + pose proof (nwnw_unlock_lock H2 H). + break_exists. + congruence. Qed. Lemma locks_correct_unlock_net_handlers_new : @@ -708,22 +786,21 @@ Section LockServ. In (pDst q, pBody q) ms -> locks_correct_unlock (update name_eq_dec sigma (pDst p) st') q. Proof using. - set_up_net_handlers; - auto using locks_correct_unlock_sent_locked. + set_up_net_handlers; break_exists; break_and; subst; intuition; break_exists; break_and; subst; simpl in *; intuition; try find_injection; try congruence. Qed. Lemma locks_correct_locked_intro : - forall sigma p c t st', + forall sigma p c id t st', pDst p = Client c -> held (sigma (Client c)) = false -> - queue st' = c :: t -> + queue st' = (c, id) :: t -> locks_correct_locked (update name_eq_dec sigma Server st') p. Proof using. unfold locks_correct_locked, valid_locked. intros. exists c. intuition. - - exists t. now rewrite_update. + - exists id, t. now rewrite_update. - now rewrite_update. Qed. @@ -735,15 +812,24 @@ Section LockServ. In (pDst q, pBody q) ms -> locks_correct_locked (update name_eq_dec sigma (pDst p) st') q. Proof using. - set_up_net_handlers; - eauto using locks_correct_locked_intro, - empty_queue_all_clients_false, - unlock_in_flight_all_clients_false. + set_up_net_handlers; break_exists; break_and; intuition; break_exists; break_and; subst; simpl in *; intuition; try find_injection; try congruence. + - eapply locks_correct_locked_intro; eauto. + eauto using locks_correct_locked_intro, + empty_queue_all_clients_false, + unlock_in_flight_all_clients_false. + rewrite H3. + rewrite H5. + simpl. + eauto. + - eapply locks_correct_locked_intro; eauto. + eauto using locks_correct_locked_intro, + empty_queue_all_clients_false, + unlock_in_flight_all_clients_false. Qed. Lemma nwnw_lock : - forall p p', - pBody p = Lock -> + forall p p' id, + pBody p = Lock id -> LockServ_network_network_invariant p p'. Proof using. unfold LockServ_network_network_invariant. @@ -761,9 +847,13 @@ Section LockServ. Proof using. unfold LockServ_network_invariant. set_up_input_handlers. - - auto using nwnw_sym, nwnw_lock. + - break_exists; break_and; subst. + simpl in *. + intuition. + find_injection. + eauto using nwnw_sym, nwnw_lock. - destruct (pBody p) eqn:?. - + auto using nwnw_lock. + + eauto using nwnw_lock. + now erewrite unlock_in_flight_all_clients_false in * by eauto. + now erewrite locked_in_flight_all_clients_false in * by eauto. Qed. @@ -774,21 +864,25 @@ Section LockServ. distinct_pairs_and LockServ_network_network_invariant (map (fun m => mkPacket h (fst m) (snd m)) ms). Proof using. - set_up_input_handlers. + set_up_input_handlers; break_exists; break_and; subst; simpl; split; intuition. Qed. Lemma nw_empty_queue_lock : forall sigma p, LockServ_network_invariant sigma p -> queue (sigma Server) = [] -> - pBody p = Lock. + exists i, pBody p = Lock i. Proof using. unfold LockServ_network_invariant, locks_correct_unlock, locks_correct_locked, valid_unlock, valid_locked. intuition. destruct (pBody p) eqn:?; intuition; break_exists; intuition; break_exists; - congruence. + try congruence. + - exists n; auto. + - pose proof (H2 n (eq_refl _)). + break_exists; break_and; break_exists. + congruence. Qed. Lemma LockServ_nwnw_net_handlers_old_new : @@ -801,9 +895,18 @@ Section LockServ. In (pDst p', pBody p') ms -> LockServ_network_network_invariant p' q. Proof using. - set_up_net_handlers; - eauto using nwnw_sym, nwnw_lock, nw_empty_queue_lock, nwnw_unlock_lock. - Qed. + set_up_net_handlers; break_exists; break_and; subst; intuition; break_exists; break_and; subst; simpl in *; intuition; try find_injection. + - pose proof (nw_empty_queue_lock H2 H7). + break_exists. + pose proof (nwnw_lock _ p' H9). + apply nwnw_sym. + assumption. + - pose proof (nwnw_unlock_lock H3 H). + break_exists. + pose proof (nwnw_lock _ p' H4). + apply nwnw_sym. + assumption. + Qed. Lemma LockServ_nwnw_net_handlers_new_new : forall p sigma u st' out ms, @@ -813,7 +916,7 @@ Section LockServ. distinct_pairs_and LockServ_network_network_invariant (map (fun m => mkPacket (pDst p) (fst m) (snd m)) ms). Proof using. - set_up_net_handlers. + set_up_net_handlers; break_exists; break_and; intuition; break_exists; break_and; subst; simpl; intuition. Qed. Instance LockServ_Decompositition : Decomposition _ LockServ_MultiParams. @@ -868,7 +971,7 @@ Section LockServ. else last_holder' holder tr end - | (Client n, inr [Locked]) :: tr => last_holder' (Some n) tr + | (Client n, inr [Locked id]) :: tr => last_holder' (Some n) tr | (n, _) :: tr => last_holder' holder tr end. @@ -882,7 +985,7 @@ Section LockServ. | _ => trace_mutual_exclusion' holder tr' end | (n, (inl _)) :: tr' => trace_mutual_exclusion' holder tr' - | (Client n, (inr [Locked])) :: tr' => match holder with + | (Client n, (inr [Locked id])) :: tr' => match holder with | None => trace_mutual_exclusion' (Some n) tr' | Some _ => False end @@ -957,14 +1060,14 @@ Section LockServ. Qed. Lemma trace_mutex'_locked_extend : - forall tr h n, + forall tr h n id, trace_mutual_exclusion' h tr -> last_holder' h tr = None -> - trace_mutual_exclusion' h (tr ++ [(Client n, inr [Locked])]). + trace_mutual_exclusion' h (tr ++ [(Client n, inr [Locked id])]). Proof using. induction tr; intros; simpl in *. - - subst. auto. - - simpl in *. repeat break_match; subst; intuition. + - subst; auto. + - simpl in *; repeat break_match; subst; intuition. Qed. Lemma reachable_intro : @@ -1010,8 +1113,8 @@ Section LockServ. Qed. Lemma last_holder'_locked_some_eq : - forall tr h c n, - last_holder' h (tr ++ [(Client c, inr [Locked])]) = Some n -> + forall tr h c n id, + last_holder' h (tr ++ [(Client c, inr [Locked id])]) = Some n -> c = n. Proof using. induction tr; intros; simpl in *; repeat break_match; subst; eauto. @@ -1032,8 +1135,8 @@ Section LockServ. Qed. Lemma last_holder'_locked_extend : - forall tr h n, - last_holder' h (tr ++ [(Client n, inr [Locked])]) = Some n. + forall tr h n id, + last_holder' h (tr ++ [(Client n, inr [Locked id])]) = Some n. Proof using. induction tr; intros; simpl in *; repeat break_match; auto. Qed. @@ -1155,7 +1258,7 @@ Section LockServ. end. find_apply_hyp_hyp. apply last_holder'_no_out_extend. auto. - - intuition; subst. + - intuition; subst; break_exists; break_and; subst. + apply trace_mutex'_locked_extend. auto. destruct (last_holder' None tr) eqn:?; auto. find_apply_hyp_hyp.