add case studies page

verus-lang · Aug 15, 2024 · bb7be20 · bb7be20
1 parent 7a533dc
commit bb7be20
Show file tree

Hide file tree

Showing 15 changed files with 436 additions and 0 deletions.
diff --git a/.github/workflows/pages.yml b/.github/workflows/pages.yml
@@ -0,0 +1,48 @@
+name: pages
+
+on:
+  push:
+    branches:
+      - 'main'
+
+  workflow_dispatch:
+
+permissions:
+  contents: read
+  pages: write
+  id-token: write
+
+concurrency:
+  group: "pages"
+  cancel-in-progress: true
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    steps:
+      - name: checkout
+        uses: actions/checkout@v3
+
+      - name: set-up dir structure
+        run: |
+          mkdir ./_site
+
+      - name: add site
+        uses: actions/jekyll-build-pages@v1
+        with:
+          source: site
+          destination: ./_site
+
+      - name: upload artifact
+        uses: actions/upload-pages-artifact@v1
+
+  deploy:
+    environment:
+      name: github-pages
+      url: ${{ steps.deployment.outputs.page_url }}
+    runs-on: ubuntu-latest
+    needs: ['build']
+    steps:
+      - name: deploy to github pages
+        id: deployment
+        uses: actions/deploy-pages@v1
diff --git a/site/.gitignore b/site/.gitignore
@@ -0,0 +1,3 @@
+/_site/
+/vendor/
+/.jekyll-cache/
diff --git a/site/Gemfile b/site/Gemfile
@@ -0,0 +1,6 @@
+source "https://rubygems.org"
+gem 'jekyll'
+gem 'kramdown'
+gem 'rouge'
+gem 'jekyll-feed'
+gem 'webrick'
diff --git a/site/Gemfile.lock b/site/Gemfile.lock
@@ -0,0 +1,83 @@
+GEM
+  remote: https://rubygems.org/
+  specs:
+    addressable (2.8.7)
+      public_suffix (>= 2.0.2, < 7.0)
+    bigdecimal (3.1.8)
+    colorator (1.1.0)
+    concurrent-ruby (1.3.4)
+    em-websocket (0.5.3)
+      eventmachine (>= 0.12.9)
+      http_parser.rb (~> 0)
+    eventmachine (1.2.7)
+    ffi (1.17.0-x86_64-linux-musl)
+    forwardable-extended (2.6.0)
+    google-protobuf (4.27.3-x86_64-linux)
+      bigdecimal
+      rake (>= 13)
+    http_parser.rb (0.8.0)
+    i18n (1.14.5)
+      concurrent-ruby (~> 1.0)
+    jekyll (4.3.3)
+      addressable (~> 2.4)
+      colorator (~> 1.0)
+      em-websocket (~> 0.5)
+      i18n (~> 1.0)
+      jekyll-sass-converter (>= 2.0, < 4.0)
+      jekyll-watch (~> 2.0)
+      kramdown (~> 2.3, >= 2.3.1)
+      kramdown-parser-gfm (~> 1.0)
+      liquid (~> 4.0)
+      mercenary (>= 0.3.6, < 0.5)
+      pathutil (~> 0.9)
+      rouge (>= 3.0, < 5.0)
+      safe_yaml (~> 1.0)
+      terminal-table (>= 1.8, < 4.0)
+      webrick (~> 1.7)
+    jekyll-feed (0.17.0)
+      jekyll (>= 3.7, < 5.0)
+    jekyll-sass-converter (3.0.0)
+      sass-embedded (~> 1.54)
+    jekyll-watch (2.2.1)
+      listen (~> 3.0)
+    kramdown (2.4.0)
+      rexml
+    kramdown-parser-gfm (1.1.0)
+      kramdown (~> 2.0)
+    liquid (4.0.4)
+    listen (3.9.0)
+      rb-fsevent (~> 0.10, >= 0.10.3)
+      rb-inotify (~> 0.9, >= 0.9.10)
+    mercenary (0.4.0)
+    pathutil (0.16.2)
+      forwardable-extended (~> 2.6)
+    public_suffix (6.0.1)
+    rake (13.2.1)
+    rb-fsevent (0.11.2)
+    rb-inotify (0.11.1)
+      ffi (~> 1.0)
+    rexml (3.3.5)
+      strscan
+    rouge (4.3.0)
+    safe_yaml (1.0.5)
+    sass-embedded (1.77.8)
+      google-protobuf (~> 4.26)
+      rake (>= 13)
+    strscan (3.1.0)
+    terminal-table (3.0.2)
+      unicode-display_width (>= 1.1.1, < 3)
+    unicode-display_width (2.5.0)
+    webrick (1.8.1)
+
+PLATFORMS
+  x86_64-linux-musl
+
+DEPENDENCIES
+  jekyll
+  jekyll-feed
+  kramdown
+  rouge
+  webrick
+
+BUNDLED WITH
+   2.3.25
diff --git a/site/_config.yml b/site/_config.yml
@@ -0,0 +1,14 @@
+title: "Verus: A Practical Foundation for Systems Verification (Artifact)"
+lsi: false
+safe: true
+source: .
+incremental: false
+highlighter: rouge
+collections:
+  - projects
+gist:
+  noscript: false
+kramdown:
+  math_engine: mathjax
+  syntax_highlighter: rouge
+exclude: [Makefile]
diff --git a/site/_layouts/default.html b/site/_layouts/default.html
@@ -0,0 +1,21 @@
+<!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">
+        {{ content }}
+      </div>
+    </div>
+
+  </body>
+
+</html>
diff --git a/site/_projects/ironfleet-kv.md b/site/_projects/ironfleet-kv.md
@@ -0,0 +1,8 @@
+---
+title: "A Distributed Key-Value Store"
+date: 2024-05-01
+type: project
+code: https://github.com/verus-lang/verified-ironkv
+---
+
+A port of the IronKV system from [IronFleet](https://github.com/microsoft/Ironclad/tree/main/ironfleet) to Verus.  IronKV uses distribution for improved throughput by moving "hot" keys to dedicated machines.
diff --git a/site/_projects/mimalloc.md b/site/_projects/mimalloc.md
@@ -0,0 +1,7 @@
+---
+title: "A Concurrent Memory Allocator"
+date: 2024-05-01
+type: project
+code: https://github.com/verus-lang/verified-memory-allocator
+---
+A memory allocator based on [mimalloc](https://github.com/microsoft/mimalloc).
diff --git a/site/_projects/nr.md b/site/_projects/nr.md
@@ -0,0 +1,7 @@
+---
+title: "A Node Replication (NR) Library"
+date: 2024-05-01
+type: project
+code: https://github.com/verus-lang/verified-node-replication
+---
+Creates a linearizable NUMA-aware concurrent data structure from a black-box sequential one
diff --git a/site/_projects/persistent-storage.md b/site/_projects/persistent-storage.md
@@ -0,0 +1,7 @@
+---
+title: "An Append-only Log on Persistent Memory"
+date: 2024-05-01
+type: project
+code: https://github.com/microsoft/verified-storage.git
+---
+The implementation handles crash consistency, ensuring that even if the process or machine crashes, it acts like an append-only log across the crashes. It also handles bit corruption, detecting if metadata read from persistent memory is corrupted.
diff --git a/site/_projects/verified-pagetable.md b/site/_projects/verified-pagetable.md
@@ -0,0 +1,8 @@
+---
+title: "An OS Page Table Management Implementation and OS Model"
+date: 2024-08-15
+type: project
+code: https://github.com/utaal/verified-nrkernel
+---
+
+A verified implementation of an OS' page table management code, and proofs that it behaves according to a userspace process' expectations when combined with a model of the hardware's memory management (memory translation) subsystem.
diff --git a/site/case-studies.md b/site/case-studies.md
@@ -0,0 +1,24 @@
+---
+layout: default
+---
+
+<div class="hero">
+    <div class="main relative card header">
+        <h1>Verus: A Practical Foundation for Systems Verification<br/>Case Studies</h1><a name="projects"/>
+    </div>
+    <div class="main relative card header">
+        <ul class="publication">
+
+        {% assign projects = site.projects | where: "type", "project" %}
+        {% for project in projects %}
+            <li>
+                <div>
+                  <a href="{{ project.code }}" class="paper-title">{{ project.title }}</a>
+                </div>
+                {{ project.content }}
+            </li>
+        {% endfor %}
+
+        </ul>
+    </div>
+</div>
diff --git a/site/css/base.css b/site/css/base.css
@@ -0,0 +1,49 @@
+* { margin: 0; padding: 0;}
+
+body, html { height:100%; }
+body {
+  padding-top: 20px;
+  font-family: 'Open Sans', sans-serif;
+  font-size: 11pt;
+}
+a {
+  text-decoration: none;
+}
+a:hover {
+  text-decoration: underline;
+}
+
+div.main {
+  display: block;
+  background-color: white;
+  padding: 30px 10px 30px 10px;
+  color: #222;
+  border-bottom: 1px solid #999;
+}
+div.posts {
+  display: block;
+  flex-grow: 1;
+  margin-left: 30px;
+  margin-right: 30px;
+  max-width: 500px;
+}
+div.posts .excerpt {
+  text-align: justify;
+}
+div.main:first-child {
+  margin-top: 20px;
+  border-top: 1px solid #999;
+}
+div.main:last-child {
+  margin-bottom: 40px;
+}
+div.main.highlight {
+  background-color: #d0d0ff;
+}
+
+div.base_header {
+  display: flex;
+  justify-content: space-between;
+  padding-left: 40px;
+  padding-right: 40px;
+}