From fe1559506cee92c8745d5d9cd57b1f26c2c305bd Mon Sep 17 00:00:00 2001
From: Andrea Lattuada <andrea@lattuada.me>
Date: Wed, 21 Aug 2024 21:11:04 +0200
Subject: [PATCH] add more milli results

---
 milli/.gitignore         |  1 +
 milli/plot/run.sh        |  8 ++++++++
 milli/plot/setup_venv.sh | 11 +++++++++++
 milli/run.sh             |  2 ++
 site/guide.md            | 19 ++++++++++++++++++-
 5 files changed, 40 insertions(+), 1 deletion(-)
 create mode 100644 milli/plot/run.sh
 create mode 100644 milli/plot/setup_venv.sh

diff --git a/milli/.gitignore b/milli/.gitignore
index 6bec74e..d446dba 100644
--- a/milli/.gitignore
+++ b/milli/.gitignore
@@ -2,3 +2,4 @@
 /results/
 /linked-list/creusot-sessions/**/*.bak
 /linked-list/errors/creusot*/**/*.bak
+/venv3/
diff --git a/milli/plot/run.sh b/milli/plot/run.sh
new file mode 100644
index 0000000..b6905eb
--- /dev/null
+++ b/milli/plot/run.sh
@@ -0,0 +1,8 @@
+bash plot/setup_venv.sh
+
+. ./venv3/bin/activate
+
+cd results
+
+python3 ../plot/linked_list_repeat.py
+python3 ../plot/doubly_linked_list_repeat.py
diff --git a/milli/plot/setup_venv.sh b/milli/plot/setup_venv.sh
new file mode 100644
index 0000000..40e8990
--- /dev/null
+++ b/milli/plot/setup_venv.sh
@@ -0,0 +1,11 @@
+apt-get install python3.10-venv -y
+
+if [ -d "venv3" ]; then
+  rm -R venv3
+fi
+
+python3 -m venv venv3
+
+. ./venv3/bin/activate
+
+pip install plotnine
diff --git a/milli/run.sh b/milli/run.sh
index 46b36e1..891f0ed 100644
--- a/milli/run.sh
+++ b/milli/run.sh
@@ -11,3 +11,5 @@ docker exec verus-sosp24-milli /bin/bash setup/verifiers.sh
 
 docker exec verus-sosp24-milli /bin/bash experiments.sh $1
 
+docker exec verus-sosp24-milli /bin/bash plot/run.sh
+
diff --git a/site/guide.md b/site/guide.md
index c4f0d22..5230962 100644
--- a/site/guide.md
+++ b/site/guide.md
@@ -137,7 +137,24 @@ When the experiments complete, stop and delete the container:
 docker rm -f verus-sosp24-milli
 ```
 
-**TODO.** Result plots.
+This will produce results in the `/mydata/verus-sosp24-artifact/milli/results` directory.
+
+First, inspect the verification times for the singly linked list and the doubly linked list as follows.
+Still in the `/mydata/verus-sosp24-artifact/milli` directory, run:
+
+```shell
+cat results/linked-list-oneshot.txt
+```
+
+to see the results which correspond to the "Single" column of Figure 6a.
+
+Then run:
+
+```shell
+cat results/doubly-linked-list-oneshot.txt
+```
+
+to see the results which correspond to the "Double" column of Figure 6a.
 
 **TODO.** Interpreting results.