update artifact site to prepare for camera ready, add landing page

verus-lang · Sep 21, 2024 · 3ece803 · 3ece803
1 parent 8b4a881
commit 3ece803
Show file tree

Hide file tree

Showing 5 changed files with 59 additions and 19 deletions.
diff --git a/.../assets/paper-20240821-212701-e33099e.pdf → ae/paper-20240821-212701-e33099e.pdf b/.../assets/paper-20240821-212701-e33099e.pdf → ae/paper-20240821-212701-e33099e.pdf
diff --git a/site/assets/paper-20240921-162720-b7db935.pdf b/site/assets/paper-20240921-162720-b7db935.pdf
diff --git a/site/css/index.css b/site/css/index.css
@@ -162,6 +162,22 @@ div.md div.highlight {
   margin-bottom: 10px;
   margin-left: 10px;
 }
+span.highlight-1 {
+  font-weight: bold;
+  background: linear-gradient(90deg, #260, #060, #070, #062);
+  -webkit-background-clip: text;
+  background-clip: text;
+  color: transparent;
+  display: inline;
+}
+span.highlight-2 {
+  font-weight: bold;
+  background: linear-gradient(90deg, #006, #226, #006);
+  -webkit-background-clip: text;
+  background-clip: text;
+  color: transparent;
+  display: inline;
+}
 div.md li {
   margin-left: 20px;
 }
diff --git a/site/guide.md b/site/guide.md
@@ -3,9 +3,11 @@ layout: md
 title: "Verus: A Practical Foundation for Systems Verification<br/>Artifact Guide"
 ---
 
-**This file is rendered at https://verus-lang.github.io/paper-sosp24-artifact/guide.html, we recommend reading it there.** This page's source is at [https://github.com/verus-lang/paper-sosp24-artifact/blob/main/site/guide.md](https://github.com/verus-lang/paper-sosp24-artifact/blob/main/site/guide.md).
+This file is rendered at https://verus-lang.github.io/paper-sosp24-artifact/guide.html, we recommend reading it there. This page's source is at [https://github.com/verus-lang/paper-sosp24-artifact/blob/main/site/guide.md](https://github.com/verus-lang/paper-sosp24-artifact/blob/main/site/guide.md).
 
-The paper draft is at [https://verus-lang.github.io/paper-sosp24-artifact/assets/paper-20240821-212701-e33099e.pdf](https://verus-lang.github.io/paper-sosp24-artifact/assets/paper-20240821-212701-e33099e.pdf). For artifact evaluators, a list of the changes from the accepted version is at [https://github.com/verus-lang/paper-sosp24-artifact/blob/main/ae/paper-draft-changes.md](https://github.com/verus-lang/paper-sosp24-artifact/blob/main/ae/paper-draft-changes.md).
+<div style="background-color: #eee; margin-top: 10px; margin-right: 0px;">
+{{ "The current paper draft (in shepherding) is at [assets/paper-20240921-162720-b7db935.pdf](assets/paper-20240921-162720-b7db935.pdf)." | markdownify }}
+</div>
 
 **This artifact references external repositories with open-source versions of Verus and the use cases presented. The artifact uses fixed commits (or "refspecs" / SHAs) which are also listed here: [https://github.com/verus-lang/paper-sosp24-artifact/blob/main/external-repository-versions.md](https://github.com/verus-lang/paper-sosp24-artifact/blob/main/external-repository-versions.md).**
 
@@ -55,18 +57,6 @@ implementation (except for eager directory reclamation, which the unverified imp
 
 **Claim E**. The initial version of the verified persistent memory log provided low throughput on small appends due to its extra copying; the latest version eliminates this overhead and achieves comparable throughput to the baseline, libpmemlog. (Figure 14)
 
-### Note: Millibenchmark programs -- Reusability
-
-The programs used for Millibenchmarks are in the `milli/` directory. Some are adapted from
-existing open source examples or projects, typically from one of the other verifiers' examples.
-
-If you would like to reuse these programs for further evaluation or to improve tooling, refer
-to the files in `linked-list` and `doubly-linked-list` with the name corresponding to the tool. These are the programs used for Figure 6a.
-
-Programs for the memory reasoning benchmark (Figure 6b) are generated with the `repeat*py` scripts, while programs for evaluating verification time of finding errors (Figure 7) are adapted from the linked list programs by removing necessary preconditions: these are in `linked-list/errors`.
-
-At the time of paper submission Creusot required interactive sessions in the Why3 prover environment. These have been stored in `creusot-*` directories in `linked-list`, `linked-list/errors`, and `doubly-linked-list`.
-
 ### Instructions
 
 Start a Linux x86_64 machine, with at least 8 physical cores on one CPU, and Ubuntu 22.04. **We recommend CloudLab d6515.**
@@ -383,7 +373,7 @@ python3 plot_verif_comparison.py results 8192
 
 (8192 is the total MiB appended to the log in each iteration of the experiment).
 This command will produce a PDF at `verified-storage/artifact_eval/experiment/results.pdf` with a
-graph resembling Figure 14.
+graph resembling Figure 14. 
 
 You can copy the pdf to the host with (enter `ubuntu` when prompted for a password).
 Close the ssh session with the VM and run this on the host, not inside the VM:

diff --git a/site/index.html b/site/index.html
@@ -14,10 +14,10 @@
       <div class="wrapper">
         <div class="hero">
           <div class="main relative card header">
-            This website and associated GitHub Repository <a href="https://github.com/verus-lang/paper-sosp24-artifact">https://github.com/verus-lang/paper-sosp24-artifact</a>
-            contain the artifact for the paper:
+            <span class="highlight-1">This website and associated GitHub Repository <a href="https://github.com/verus-lang/paper-sosp24-artifact">https://github.com/verus-lang/paper-sosp24-artifact</a>
+            contain the artifact for the paper:</span>
 
-            <h1>Verus: A Practical Foundation for Systems Verification</h1>
+            <h1 style="margin-top: 10px; margin-bottom: 10px;">Verus: A Practical Foundation for Systems Verification</h1>
 
             Andrea Lattuada (MPI-SWS),
             Travis Hance (Carnegie Mellon University),
@@ -33,10 +33,44 @@ <h1>Verus: A Practical Foundation for Systems Verification</h1>
             Jacob R. Lorch (Microsoft Research),
             Oded Padon (Weizmann Institute of Science),
             Bryan Parno (Carnegie Mellon University)
+
+
+            <div style="background-color: #eee; margin-top: 10px; margin-right: 0px;">
+              The current paper draft (in shepherding) is at
+              <a href="assets/paper-20240921-162720-b7db935.pdf">assets/paper-20240921-162720-b7db935.pdf</a>
+            </div>
 
           </div>
+          <div class="main relative card" style="font-weight: bold;">
+            <h3><a href="guide.html">Artifact Guide</a></h3>
+            The artifact <a href="guide.html">guide (guide.html)</a> contains instructions to reproduce the results in the paper.
+          </div>
+          <div class="main relative card" style="font-weight: bold;">
+            <h3><a href="case-studies.html">Case Studies</a></h3>
+            The case studies used in the paper are open-source and listed on the <a href="case-studies.html">case studies page (case-studies.html)</a>.
+          </div>
+          <div class="main relative card">
+            <h3>External Repositories</h3>
+            This artifact references external repositories with open-source versions of Verus and the use
+            cases presented. The artifact uses fixed commits (or "refspecs" / SHAs) which are also listed here:
+            <a href="https://github.com/verus-lang/paper-sosp24-artifact/blob/main/external-repository-versions.md">
+              https://github.com/verus-lang/paper-sosp24-artifact/blob/main/external-repository-versions.md</a>.
+          </div>
           <div class="main relative card">
-            The artifact <a href="guide.html">guide (/guide.html)</a> contains instructions to reproduce the results in the paper.
+            <h3>Reusability of Millibenchmark programs</h3>
+
+            <p>The programs used for Millibenchmarks are in the <code>milli/</code> directory. Some are adapted from
+            existing open source examples or projects, typically from one of the other verifiers' examples.</p>
+
+            <p>If you would like to reuse these programs for further evaluation or to improve tooling, refer
+            to the files in <code>linked-list</code> and <code>doubly-linked-list</code> with the name corresponding to the tool.<br/>These are the programs used for Figure 7a.</p>
+
+            <p>Programs for the memory reasoning benchmark (Figure 7b) are generated with the `repeat*py` scripts,
+            while programs for evaluating verification time of finding errors (Figure 8)
+            are adapted from the linked list programs by removing necessary preconditions: these are in <code>linked-list/errors</code>.</p>
+
+            At the time of paper submission Creusot required interactive sessions in the Why3 prover environment.
+            These have been stored in <code>creusot-*</code> directories in <code>linked-list</code>, <code>linked-list/errors</code>, and <code>doubly-linked-list</code>.
           </div>
         </div>
       </div>