add more milli results

milli/.gitignore

@@ -2,3 +2,4 @@
 /results/
 /linked-list/creusot-sessions/**/*.bak
 /linked-list/errors/creusot*/**/*.bak
+/venv3/

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

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

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
+

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.