From 3a09216b137a847b296e2610db87cd669449143f Mon Sep 17 00:00:00 2001 From: Yishuai Li Date: Thu, 13 Feb 2020 15:58:15 -0500 Subject: [PATCH 1/2] generate.sh -> Makefile --- .gitignore | 1 + Makefile.meta | 13 ++ example/.gitignore | 6 + example/Makefile | 20 +++ example/meta.yml | 339 +++++++++++++++++++++++++++++++++++++++++++++ example/templates | 1 + generate.sh | 8 -- 7 files changed, 380 insertions(+), 8 deletions(-) create mode 100644 Makefile.meta create mode 100644 example/.gitignore create mode 100644 example/Makefile create mode 100644 example/meta.yml create mode 120000 example/templates delete mode 100755 generate.sh diff --git a/.gitignore b/.gitignore index b25c15b..93bfd12 100644 --- a/.gitignore +++ b/.gitignore @@ -1 +1,2 @@ *~ +.DS_Store diff --git a/Makefile.meta b/Makefile.meta new file mode 100644 index 0000000..818271f --- /dev/null +++ b/Makefile.meta @@ -0,0 +1,13 @@ +TEMPLATES ?= templates + +index.html: index.md + @echo "Generating $@..." + pandoc -s -o $@ $< + +%.opam: meta.yml $(TEMPLATES)/coq.opam.mustache + @echo "Generating $@..." + mustache $^ > $@ + +%: meta.yml $(TEMPLATES)/%.mustache + @echo "Generating $@..." + mustache $^ > $@ diff --git a/example/.gitignore b/example/.gitignore new file mode 100644 index 0000000..b14ea46 --- /dev/null +++ b/example/.gitignore @@ -0,0 +1,6 @@ +.travis.yml +README.md +coq-chapar-stores.opam +coq-chapar.opam +default.nix +index.html diff --git a/example/Makefile b/example/Makefile new file mode 100644 index 0000000..08dbaca --- /dev/null +++ b/example/Makefile @@ -0,0 +1,20 @@ +TEMPLATES ?= templates + +TARGETS= \ + .travis.yml \ + README.md \ + coq-chapar.opam \ + coq-chapar-stores.opam \ + default.nix \ + index.html + +all: $(TARGETS) + +clean: + $(RM) $(TARGETS) + +coq-chapar-stores.opam: meta.yml $(TEMPLATES)/extracted.opam.mustache + @echo "Generating $@..." + mustache $^ > $@ + +include $(TEMPLATES)/Makefile.meta diff --git a/example/meta.yml b/example/meta.yml new file mode 100644 index 0000000..62b9d36 --- /dev/null +++ b/example/meta.yml @@ -0,0 +1,339 @@ +--- +fullname: Chapar +shortname: chapar +organization: coq-community +community: true +travis: true +doi: 10.1145/2837614.2837622 + +synopsis: >- + A framework for verification of causal consistency for distributed key-value stores + and their clients in Coq + +description: |- + A framework for modular verification of causal consistency for replicated key-value + store implementations and their client programs in Coq. Includes proofs of the causal consistency + of two key-value store implementations and a simple automatic model checker for the correctness + of client programs. + +publications: +- pub_doi: 10.1145/2837614.2837622 + pub_url: http://adam.chlipala.net/papers/ChaparPOPL16/ + pub_title: 'Chapar: Certified Causally Consistent Distributed Key-value Stores' + +authors: +- name: Mohsen Lesani + initial: true +- name: Christian J. Bell + initial: true +- name: Adam Chlipala + initial: true + +maintainers: +- name: Karl Palmskog + nickname: palmskog + +opam-file-maintainer: palmskog@gmail.com + +opam-file-version: dev + +license: + fullname: MIT License + identifier: MIT + +supported_coq_versions: + text: 8.9 or later + opam: '{(>= "8.9" & < "8.12~") | (= "dev")}' + +tested_coq_nix_versions: +- version_or_url: https://github.com/coq/coq-on-cachix/tarball/master +- version_or_url: '8.11' +- version_or_url: '8.10' +- version_or_url: '8.9' + +tested_coq_opam_versions: +- version: dev + +namespace: Chapar + +extracted: + extracted_fullname: Chapar Key-value Stores + extracted_shortname: chapar-kv-stores + + extracted_synopsis: Three executable causally consistent distributed key-value stores + extracted_description: | + Three key-value stores, verified to be causally consistent in + the Coq proof assistant and extracted to executable code. + + extracted_make_target: stores + + extracted_supported_ocaml_versions: + text: 4.05.0 or later + opam: '{>= "4.05.0"}' + + extracted_tested_coq_opam_versions: + - version: dev + + extracted_dependencies: + - opam: + name: ocamlbuild + version: '{build}' + nix: ocamlbuild + description: >- + [OCamlbuild](https://github.com/ocaml/ocamlbuild) + - opam: + name: batteries + version: '{>= "2.8.0"}' + nix: batteries + description: >- + [Batteries Included](https://github.com/ocaml-batteries-team/batteries-included) 2.8.0 or later + +keywords: +- name: causal consistency +- name: key-value stores +- name: distributed algorithms +- name: program verification + +categories: +- name: Computer Science/Concurrent Systems and Protocols/Theory of concurrent systems + +documentation: | + ## Documentation + + ### Coq Framework + + The Coq definitions and proofs are located in the `coq` directory. The code location of the definitions and lemmas presented in the paper are listed below. + + #### Semantics and the Proof Technique + + - Section 2, Figure 3 (Program): `KVStore.v`, `Section ValSec` + - Section 2, Figure 4 (Key-value Store Algorithm Interface): `KVStore.v`, `Module Type AlgDef` + - Section 2, Figure 5 (Concrete Operational Semantics): `KVStore.v`, `Module ConcExec` + - Section 3, Figure 6 (Abstract Operational Semantics): `KVStore.v`, `Module AbsExec` + - Section 4, Figure 8 (Concrete Instrumented Operational Semantics): `KVStore.v`, `Module InstConcExec` + - Section 4, Figure 10 (Correctness Condition WellRec): `KVStore.v`, `Module Type CauseObl` + - Section 4, Figure 11 (Causal relation): `KVStore.v`, `Definition cause_step` and `Inductive cause` + - Section 4, Figure 12 (Sequential Operational Semantics): `KVStore.v`, `Module SeqExec` + - Section 4, Definition 2 (Causal Consistency) and Theorem 2 (Sufficiency of Well-reception): `KVStore.v`, `Theorem CausallyConsistent`. Note that `(CauseObl: CauseObl AlgDef)` is a parameter of the module `ExecToAbstExec`. + - Section 4, Lemma 1: `KVStore.v`, `Lemma FaultFreedom`. Note that `(CauseObl: CauseObl AlgDef)` is a parameter of the module `ExecToAbstExec`. + + #### Algorithms + + - Section 5, Figure 13 (Algorithm 1): `KVSAlg1.v`, `Module Type KVSAlg1` + - Section 5, Theorem 3: `KVSAlg1.v`, `Module KVSAlg1CauseObl (SyntaxArg: SyntaxPar) <: CauseObl KVSAlg1 SyntaxArg` + - Section 5, Corollary 1: `KVSAlg1.v`, `Lemma CausallyConsistent` + - Section 5, Lemma 2 (Clock Monotonicity): `KVSAlg1.v`, `Lemma cause_clock` + - Section 5, Lemma 3 (CauseCond): `KVSAlg1.v`, `Lemma cause_rec` + - Section 5, Figure 14 (Algorithm 2): `KVSAlg2.v`, `Module Type KVSAlg2` + - Section 5, Theorem 3: `KVSAlg1.v`, `Module KVSAlg2CauseObl (SyntaxArg: SyntaxPar) <: CauseObl KVSAlg2 SyntaxArg` + - Secton 5, Corollary 2: `KVSAlg2.v`, `Lemma CausallyConsistent` + - Secton 5, Lemma 4 (Update Dependency Transitivity): `KVSAlg2.v`, `Lemma cause_dep` + - Secton 5, Lemma 5: `KVSAlg2.v`, `Lemma cause_received_received` + - Secton 5, Lemma 6 (CauseCond): `KVSAlg2.v`, `Lemma cause_rec` + - Section 10, Figure 16 (Algorithm 3): `KVSAlg3.v`, `Module Type KVSAlg3` + - Section 10, Theorem 5: `KVSAlg3.v`, `Module KVSAlg3CauseObl (SyntaxArg: SyntaxPar) <: CauseObl KVSAlg3 SyntaxArg` + - Secton 5, Corollary 3: `KVSAlg3.v`, `Lemma CausallyConsistent` + - Section 5, Lemma 7 (Clock Monotonicity): `KVSAlg3.v`, `Lemma cause_clock` + - Section 5, Lemma 8 (Dep less than equal Rec): `KVSAlg3.v`, `Lemma dep_leq_rec` + - Section 5, Lemma 9 (CauseCond): `KVSAlg3.v`, `Lemma cause_rec` + + #### Clients + - Section 1, Program 1: `Clients.v`, `Definition prog_photo_upload` + - Section 1, Program 2: `Clients.v`, `Definition prog_lost_ring` + - Section 10, Program 3: `ListClient.v` + - Section 2, Theorem 1: `Clients.v`, `Lemma CauseConsistent_Prog1` + - Section 3, Definition 1 (Cause-content Program): `Definition CausallyContent` + - Section 6: `ReflectiveAbstractSemantics.v` + + ### Experiment Setup + + #### Directory structure + + - root (directory): The execution scripts described in the section Running Experiments below + + - `coq` (directory); the Coq verification framework: + * `Framework/KVStore.v`: The basic definitions, the semantics and accompanying lemma + * `Framework/ReflectiveAbstractSemantics.v`: The client verification definitions and lemmas + * `Algorithms/KVSAlg1.v`: The definition and proof of algorithm 1 in the paper + * `Algorithms/KVSAlg2.v`: The definition and proof of algorithm 2 in the paper + * `Algorithms/KVSAlg3.v`: The definition and proof of algorithm 3 in the appendix + * `Algorithms/Extract.v`: The Coq file that extracts the algorithms + * `Examples/Clients.v`: Verified client program + * `Examples/ListClient.v`: Verified client program + * `Lib` (directory): General purpose Coq libraries + + - `ml` (directory); the OCaml runtime to execute the algorithms: + * `algorithm.ml`: Key-value store algorithm shared interface + * `algorithm1.ml`, `algorithm2.ml`, `algorithm3.ml`: Wrappers for the extracted algorithms + * `benchgen.ml`: Benchmark generation and storing program + * `benchprog.ml`: Benchmark retrieval program + * `commonbench.ml`: Common definitions for benchmarks + * `common.ml`: Common definitions + * `configuration.ml`: Execution configuration definitions + * `readConfig.ml`: Configuration retrieval program + * `runtime.ml`: Execution runtime + * `launchStore1.ml`, `launchStore2.ml`, `launchStore3.ml`: Launchers for the extracted algorithms + * `util.ml`: General purpose OCaml functions + * `experiment.ml`: Small OCaml programming tests + + ### Running Experiments + + #### Overview + + We run with 4 nodes called the worker nodes and a node called the master node that keeps + track of the start and end of the runs. The scripts support running with both the current terminal + blocked or detached. In the former, the terminal should be active for the entire execution time. To + avoid this, we use another node called the launcher node. Repeating and collecting the results + of the runs is delegated to the launcher node. The terminal can be closed and the execution + results can be retrieved later from the launcher node. The four workers, the master and the + launcher can be different nodes. However, to simplify running, the scripts support assigning + one host to all of these roles. This is the default setting. + + The settings of the nodes can be edited in the file `Settings.txt`. The following should be + noted if other machines are used as the running nodes. + The host should have password-less ssh access to the launcher node. The launcher node + should have password-less ssh access to the other nodes. This can be done by copying + the public key of the accessing machine to the accessed machine by a command like: + ``` + cat ~/.ssh/id_dsa.pub | ssh -l remoteuser remote.example.com 'cat >> ~/.ssh/authorized_keys' + ``` + The port numbers 9100, 9101, 9102, and 9103 should be open on the worker nodes + 1, 2, 3 and 4 respectively. The port number 9099 should be open on the master node. + + #### A simple run + + To start the run: + ``` + ./batchrundetach + ``` + To check the status of the run: + ``` + ./printlauncherout + ``` + To get the results once the run is finished: + ``` + ./fetchresults + ``` + The result are stored in the file `RemoteAllResults.txt`. See `fetchresults` below for the format + of the results. + + #### Settings and scripts + + All of the following files are in the root directory: + + - `Settings.txt` + + * `KeyRange`: The range of keys in the generated benchmarks is from 0 to this number. For our experiments, it is set to 50. + * `RepeatCount`: The number of times that each experiment is repeated. For our experiments, it is set to 5. + * `LauncherNode`: The user name and the ip of the launcher node + * `MasterNode`: The user name and the ip of the master node + * `WorkerNodes`: The user name and the ip of the worker nodes + + - `batchrun`: + This is the place where the experiments are listed. Each call to the script `run` is an experiment. The arguments are: + + * argument 1: The number of nodes. This is 4 for our purpose. + * argument 2: The number of operations per server. This is 60000 in our experiments. + * argument 3: The percent of puts. This ranges from 10 to 90 in our experiments. + + This script can be called without using the launcher node. The current terminal is blocked. + See batchrundetach below for detached execution of the experiments. + + - `batchrundetach`: To execute using the launcher node. The current terminal is detached. + + - `printlauncherout`: To see the output of the launcher even while the experiments are being run + + - `printnodesout`: To see the output of the worker nodes + + - `fetchresults`: To get the results. The fetched files are: + + * `RemoteAllResults.txt`: The timing of the replicas + * `RemoteAllOutputs.txt`: The outputs of the replicas + * `RemoteLauncherOutput.txt`: The output of the launcher node + + The following example output is for the algorithm 2 with 4 worker nodes and 40000 operations per + node with 10 percent puts. It shows two runs. Under each run, the time spend by each of the + nodes is shown. We compute the maximum of these four numbers to compute the + total process time. + ``` + Algorithm: 2 + Server count: 4 + Operation count: 40000 + Put percent: 10 + Run: 1 + 1.000000 + 3.000000 + 1.000000 + 1.000000 + Run: 2 + 1.000000 + 1.000000 + 4.000000 + 1.000000 + ``` + + - `clearnodes`: To remove the output and result files and the running processes in all the nodes; this is used to start over + + #### The experiments in the paper + + The goal of our experimental result section was to show that our verification effort can + lead to executable code and also to compare the performance of the two algorithms. + As described in the paper, the experiments were done with four worker nodes cluster. + Each worker node had an Intel(R) Xeon(R) 2.27GHz CPU with 2GB of RAM and ran + Linux Ubuntu 14.04.2 with the kernel version 3.13.0-48-generic#80-Ubuntu. The nodes + were connected to a gigabit switch. + The keys were uniformly selected from 0 to 50 for the benchmarks. + Each experiment was repeated 5 times. (The reported numbers are the arithmetic mean of the five runs.) + Each node processed 60,000 requests. + The put ratio ranged from 10% to 90%. + + Here are the contents of the two configuration files, `Settings.txt` and `batchrun`: + Note: user and ip should be filled with specific values. + - `Settings.txt`: + ``` + KeyRange= + 50 + RepeatCount= + 5 + LauncherNode= + @ + MasterNode= + @ + WorkerNodes= + @ + @ + @ + @ + ``` + + - `batchrun`: + ``` + ./run 4 60000 10 + ./run 4 60000 20 + ./run 4 60000 30 + ./run 4 60000 40 + ./run 4 60000 50 + ./run 4 60000 60 + ./run 4 60000 70 + ./run 4 60000 80 + ./run 4 60000 90 + ``` + + #### Interpretation of results from the paper + + As expected, the throughput of both of the stores increases as the ratio of the get operation + increases. The second algorithm shows a higher throughput than the first algorithm. The + reason is twofold. Firstly, in the first algorithm, the clock function of a node keeps an + over-approximation of the dependencies of the node. This over-approximation incurs + extra dependencies on updates. On the other hand, the second algorithm does not require + any extra dependencies. Therefore, in the first algorithm compared to the second, + the updates can have longer waiting times, and the update queues tend to be longer. + Therefore, the traversal of the update queue is more time consuming in the first algorithm + than the second. Secondly, the update payload that is sent and received by the first + algorithm contains the function clock. OCaml cannot marshal functions. However, as + the clock function has the finite domain of the participating nodes, it can be serialized to + and deserialized from a list. Nonetheless, serialization and de-serialization on every + sent and received message adds performance cost. On the other hand, the payload + of the second algorithm consists of only data types that can be directly marshalled. + Therefore, the second algorithm has no extra marshalling cost. +--- diff --git a/example/templates b/example/templates new file mode 120000 index 0000000..a96aa0e --- /dev/null +++ b/example/templates @@ -0,0 +1 @@ +.. \ No newline at end of file diff --git a/generate.sh b/generate.sh deleted file mode 100755 index bf9b328..0000000 --- a/generate.sh +++ /dev/null @@ -1,8 +0,0 @@ -#!/usr/bin/env bash - -srcdir=$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null && pwd ) - -for f in "$srcdir"/{,.}*.mustache; do - echo "Generating $(basename "$f" .mustache)..." - mustache meta.yml "$f" > "$(basename "$f" .mustache)" -done From d806cbcc62640db3af7c66cc067ed675621d8717 Mon Sep 17 00:00:00 2001 From: Yishuai Li Date: Wed, 19 Feb 2020 17:10:46 -0500 Subject: [PATCH 2/2] update README --- README.md | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/README.md b/README.md index 7bb42b6..786e89f 100644 --- a/README.md +++ b/README.md @@ -45,13 +45,14 @@ Other projects using the templates in a similar way include You can generate the standard files from the templates, provided you have already written `meta.yml`, in the following way: -```shell -cd && cd .. -git clone https://github.com/coq-community/templates.git -cd - -../templates/generate.sh -git add -``` + +1. Clone https://github.com/coq-community/templates.git as subdirectory or submodule. +2. Include [`Makefile.meta`](Makefile.meta) in your `Makefile`. +3. (Optional) Add rules for extracted OPAM file. +4. Specify build targets. + +See [example](example) for more details. + Keeping generated files under version control is not ideal, but `README.md` has to exist, and generally this is a common practice when using build systems such as Autotools. To get a `mustache` tool in, e.g., NixOS, you can run `nix-env -i mustache-go`.