From 9ec00297263aee4c84fd4faa0f6072d5a46edcc4 Mon Sep 17 00:00:00 2001 From: Andrea Lattuada Date: Mon, 2 Sep 2024 17:20:42 +0200 Subject: [PATCH] fix issues in Set 3: panic due to higher than expected thread count and missing default rust installation --- external-repository-versions.md | 2 +- site/guide.md | 26 +++++++++++++++----------- 2 files changed, 16 insertions(+), 12 deletions(-) diff --git a/external-repository-versions.md b/external-repository-versions.md index c8fe7cf..98f24ee 100644 --- a/external-repository-versions.md +++ b/external-repository-versions.md @@ -21,7 +21,7 @@ Commit: `6ee4b4fc8ac107f10d3ad420a2c42e26e3033ba7` A data structure replication library verified in Verus and scripts for comparison with a version written in Linear Dafny. -Commit: `341be41a31cfc5c7539f8b78a65f166a06251d02` +Commit: `0391d6c3fae1501766d6d833ba317323d8b55b06` ### Verified IronKV implementation: https://github.com/verus-lang/verified-ironkv diff --git a/site/guide.md b/site/guide.md index 5dd70fe..8ff7c9f 100644 --- a/site/guide.md +++ b/site/guide.md @@ -706,36 +706,40 @@ rm -rf libssl1.1_1.1.0g-2ubuntu4_amd64.deb ``` -Install Rust using rustup toolchain installer: +Install Rust using rustup toolchain installer (note that the last command starts with a `.`, +i.e. it sources the environment in the current shell): ```shell (curl --proto '=https' --tlsv1.2 --retry 10 --retry-connrefused -fsSL "https://sh.rustup.rs" \ - | sh -s -- --default-toolchain none -y) + | sh -s -- -y) # source the Rust environment . "$HOME/.cargo/env" ``` #### 2. Repository Setup -Clone the Verified Node Replication repository and checkout commit `341be41a31cfc5c7539f8b78a65f166a06251d02` +Clone the Verified Node Replication repository and checkout commit `0391d6c3fae1501766d6d833ba317323d8b55b06` as follows: ```shell cd /mydata git clone https://github.com/verus-lang/verified-node-replication.git cd verified-node-replication -git checkout 341be41a31cfc5c7539f8b78a65f166a06251d02 +git checkout 0391d6c3fae1501766d6d833ba317323d8b55b06 ``` -Initialize the submodules. This should initialize three submodules: - - `verus` - - `benchmarks/ironsync/ironsync-osdi2023` - - `benchmarks/lib/node-replication` +Initialize the submodules. ```shell # inside verified-node-replication repo git submodule update --init ``` + This should initialize three submodules: + - `verus` + - `benchmarks/ironsync/ironsync-osdi2023` + - `benchmarks/lib/node-replication` + + The repository should now be ready and we can build the binaries and run the benchmark. #### 3. Running the Benchmark @@ -769,13 +773,13 @@ Note, that the benchmarks will change the following CPU settings: Also note, that this will pull in the dependencies for building Linear Dafny automatically. - #### 4. Obtaining the Results -You can view the results of the benchmark by opening the automatically generated plots: +You can view the results of the benchmark by opening the automatically generated plots. +From the local machine, copy the results off the CloudLab instance. On Linux you can use something like the following: ```shell -open nr-results-throughput-vs-cores-numa-fill.pdf +scp '@.cloudlab.us:/mydata/verified-node-replication/benchmarks/nr-results-throughput-vs-cores-numa-fill.pdf' . ``` (There is also a PNG version)