render summary table in docker, start on artifact instructions

verus-lang · Aug 19, 2024 · 895fb37 · 895fb37
1 parent 16844ce
commit 895fb37
Show file tree

Hide file tree

Showing 8 changed files with 172 additions and 5 deletions.
diff --git a/macro-stats/run.sh b/macro-stats/run.sh
@@ -22,3 +22,8 @@ docker run --platform=linux/amd64 --rm -it -v .:/root/eval -v ./repos/ironsync/b
 print_top_header "summarizing"
 
 docker run --platform=linux/amd64 --rm -it -v .:/root/eval -w /root/eval ghcr.io/utaal/ubuntu-essentials-rust-1.76.0 /bin/bash util/entry-summarize.sh
+
+print_top_header "rendering table"
+
+docker run --platform=linux/amd64 --rm -it -v .:/root/eval -w /root/eval kjarosh/latex:2024.2-small /bin/bash util/entry-render-table.sh
+
diff --git a/macro-stats/summarize.sh b/macro-stats/summarize.sh
@@ -18,4 +18,4 @@ VERUS_ENCODING_TAR=$2
 print_header "summarizing"
 (cd summarize;
     cargo build --release;
-    ./target/release/summarize ../$RESULTS_DIR ../$VERUS_ENCODING_TAR)
+    ./target/release/summarize ../$RESULTS_DIR)
diff --git a/macro-stats/util/entry-render-table.sh b/macro-stats/util/entry-render-table.sh
@@ -0,0 +1,9 @@
+tlmgr update --self 
+tlmgr install multirow
+
+(cd summarize/render; \
+    pdflatex macro-table.tex; \
+    pdflatex macro-table.tex; \
+    pdflatex macro-table.tex)
+
+mv summarize/render/macro-table.pdf results/.
diff --git a/macro-stats/util/entry-summarize.sh b/macro-stats/util/entry-summarize.sh
@@ -1,8 +1,4 @@
 
-# apt-get update && \
-#     apt-get install -y curl git build-essential wget python3 && \
-#     curl --proto '=https' --tlsv1.2 --retry 10 --retry-connrefused -fsSL "https://sh.rustup.rs" | sh -s -- --default-toolchain none -y
-
 source "$HOME/.cargo/env"
 
 bash summarize.sh results
diff --git a/setup/cloudlab-1.sh b/setup/cloudlab-1.sh
@@ -0,0 +1,26 @@
+# Add Docker's official GPG key:
+apt-get update
+
+apt-get install ca-certificates curl
+install -m 0755 -d /etc/apt/keyrings
+curl -fsSL https://download.docker.com/linux/ubuntu/gpg -o /etc/apt/keyrings/docker.asc
+chmod a+r /etc/apt/keyrings/docker.asc
+
+apt-get update
+echo \
+  "deb [arch=$(dpkg --print-architecture) signed-by=/etc/apt/keyrings/docker.asc] https://download.docker.com/linux/ubuntu \
+  $(. /etc/os-release && echo "$VERSION_CODENAME") stable" | \
+  tee /etc/apt/sources.list.d/docker.list > /dev/null
+apt-get update
+
+# Install docker
+apt-get install -y docker-ce docker-ce-cli containerd.io docker-buildx-plugin docker-compose-plugin
+
+# Add user to docker group
+usermod -aG docker $USER
+
+# Logout / login
+
+# Disable Hyperthreading
+bash -c "echo off > /sys/devices/system/cpu/smt/control"
+
diff --git a/site/_layouts/md.html b/site/_layouts/md.html
@@ -0,0 +1,28 @@
+<!DOCTYPE html>
+<html>
+ <head>
+    <title>Verus: A Practical Foundation for Systems Verification (Artifact)</title>
+    <meta charset="utf-8" />
+    <link href="https://fonts.googleapis.com/css?family=Open+Sans:400,400i,600" rel="stylesheet" />
+    <link rel="stylesheet" type="text/css" href="css/base.css" />
+    <link rel="stylesheet" type="text/css" href="css/index.css" />
+  </head> 
+
+  <body>
+
+    <div class="page-content">
+      <div class="wrapper">
+        <div class="hero">
+          <div class="main relative card header">
+            <h1>{{ page.title }}</h1>
+          </div>
+          <div class="main relative card header md">
+            {{ content }}
+          </div>
+        </div>
+      </div>
+    </div>
+
+  </body>
+
+</html>
diff --git a/site/css/index.css b/site/css/index.css
@@ -142,3 +142,28 @@ span.comment {
 .paper-title {
   font-weight: bold;
 }
+
+div.md h1 {
+  margin-top: 10px;
+}
+div.md h1:first-child {
+  margin-top: 0px;
+}
+div.md h2 {
+  margin-top: 8px;
+}
+div.md h2:first-child {
+  margin-top: 0px;
+}
+div.md h3 {
+  margin-top: 6px;
+  padding-bottom: 4px;
+}
+div.md h3:first-child {
+  margin-top: 0px;
+}
+div.md div.highlight {
+  margin-top: 10px;
+  margin-bottom: 10px;
+  margin-left: 10px;
+}
diff --git a/site/guide.md b/site/guide.md
@@ -0,0 +1,78 @@
+---
+layout: md
+title: "Verus: A Practical Foundation for Systems Verification<br/>Artifact Guide"
+---
+
+# Overview and technical requirements
+
+There are three sets of experiments with different technical requirements.
+
+### Set 1: verification statistics for macrobenchmarks and millibenchmarks, page table performance, mimalloc performance comparison, persistent memory log performance (emulated) — Figures 6, 7, 8, 11, 12, 13.
+
+Set 1 requires Linux x86_64 (Ubuntu 22.04) with at least 8 physical cores on one CPU, although more cores may reduce scheduling noise (we recommend at least 10). Set 1 requires the Docker runtime (Docker-CE). We recommend CloudLab d6515, or if they are in short supply, CloudLab c220g2.
+
+### Set 2: IronKV performance comparison — Figure 9.
+
+Set 2 requires a Windows x86_64 machine with .NET 5 or newer (we tested .NET 8.0), rust 1.76.0, and python 3 (we will provide installation instructions). A reasonably recent laptop or desktop should be sufficient.
+
+### Set 3: node replication performance comparison — Figure 10.
+
+Set 3 used a Linux Intel-based x86_64 4-CPU NUMA system with 24 cores per CPU. However, a smaller Linux Intel-based x86_64 NUMA system with at least 2 CPUs should reproduce a similar performance pattern. We recommend CloudLab r650.
+
+# Experimental Sets
+
+## Set 1
+
+### Claims
+
+**TODO.**
+
+### Instructions
+
+Start a Linux x86_64 machine, with at least 8 physical cores on one CPU, and Ubuntu 22.04. **We recommend CloudLab d6515.**
+
+If you run on CloudLab, you can follow the instructions that follow. If you start a different machine or VM, the only requirement
+to follow the same instructions is that `/mydata` is a directory on a mount with at least 50GB of free space.
+Note that the commands and scripts in the following will manipulate the permissions of `/mydata`. The machine-level setup installs
+Docker-CE and gives permission to the current user to connect to the container daemon. Other container runtimes compatible with the docker CLI should work too.
+
+**Step 1. Clone artifact repository, set up container environment.**
+
+Clone the repository
+
+```sh
+sudo chown $USER /mydata
+cd /mydata
+git clone -b main --single-branch https://github.com/verus-lang/paper-sosp24-artifact.git verus-sosp24-artifact
+```
+
+and run the script `setup/cloudlab-1.sh`
+
+
+```sh
+cd verus-sosp24-artifact
+sudo bash setup/cloudlab-1.sh
+```
+
+Log out and log in again to ensure the current user is part of the `docker` group.
+
+**Step 2. Run the verification statistics (Figure 8).**
+
+**TODO** describe hand-tuned numbers and hard-coded baselines.
+
+The automation scripts to produce the statistics in Figure 8 are in `macro-stats`.
+The scripts make no changes to the system outside of the repository, other than spawning
+containers.  `run.sh` will run all the necessary experiments.
+
+```sh
+cd macro-stats
+bash run.sh
+```
+
+This will produce output in the `results/` directory (`macro-stats/results`).
+`results.json` are machine-readable results, which are also rendered as a pdf with the
+same structure as the figure in the paper, `results/macro-table.pdf`.
+
+
+
+