Fast Verified SCCs for Probabilistic Model Checking

Browsing the Theories

You can view an html version of the theories. Here are some default starting points for browsing:

Skeleton Algorithm Abstract level and Gabow’s data structure

SCC Algorithm Abstract level and Gabow’s data structure

Bit-Packed Intervals

Modest MDP Data Structure

LLVM Code Generation

Main Correctness Theorem

Downloads

dist.tgz contains the Isabelle theories

modest.tgz contains our modified version of Modest (~1GiB)

Prerequisites

To compile the LLVM code: Working installation of LLVM version >= 10.0.0.
To re-check the proofs: Working installation of Isabelle/HOL with the Archive of Formal Proofs installed as as described on https://www.isa-afp.org/using.shtml. We require version = Isabelle-2022, which, at the time of writing, is the current version.
To replay the benchmarks: our modified version of Modest (modest.tgz)

Viewing the Theories

Warning: the .thy files in this arrtifact are best viewed with the Isabelle/HOL IDE. There is also a html version, that can be viewed in the browser. Look for html/index.html if you are viewing this file as README.md!

Verifying the Theories and Building the LLVM code

In the main directory, run

On Linux: Make sure that the isabelle command points to your installation of Isabelle 2022. If this is not the case, we recommend you do this first. Run:

isabelle build -D.

On Windows: You can start a cygwin terminal via $ISABELLE_HOME/Cygwin-Terminal.bat. You then have to navigate to the folder that this projects ROOT file is in. Note that the document path is expressed in the cygwin environment. If the path to the ROOT is located in “E:/example/mec-isabelle/ROOT” then you should enter “cd /cygdrive/e/example/mec-isabelle” into the terminal and run:

isabelle build -D.

This will check all proofs, and (re)generate the files Gabow_SCC/modest_gabow.{ll,h} that contain the executable code.

NOTE: The build process may fail on Windows. If this happens, you have to rerun the command.

Compiling into shared library for Modest

Copy ./isabelle_llvm/src/lib_isabelle_llvm.c into ./Gabow_SCC
cd ./Gabow_SCC
Windows: clang modest_gabow.ll lib_isabelle_llvm.c -shared -o GabowIsabelle.dll -O3
Linux: clang modest_gabow.ll lib_isabelle_llvm.c -shared -o GabowIsabelle.so -O3 -fPIC

In Windows/Linux, this generates GabowIsabelle.dll/.so in the current folder.

Replaying the Benchmarks

Place GabowIsabelle.dll/.so inside Modest_Windows/Modest_Linux inside the Modest folder
Open terminal in Modest_Windows/Modest_Linux
In Windows/Linux there is a file modest.exe/modest, make sure it is executable
Run
1. modest mobench Sccfull.mcsta.json for the scc algorithm runtimes (~5 hours)
2. modest mobench Sccfull.lp.mcsta.json for a full comparison of the runtimes (~10 hours)

Viewing the Plots

Open terminal in Modest_Windows/Modest_Linux
run

modest moplot scatter-scc1.json To generate Figure 4 (requires benchmark step 1)

modest moplot scatter-scc2.json to generate Figure 5 (requires benchmark step 1)

modest moplot scatter-scc-lp.json to generate Figure 6 (requires benchmark step 2)
The resulting files are called “scatter-scc-scctime.tex”,, “scatter-scc-totaltime.tex” and “scatter-scc-lp.tex”
Build using your favourite LaTex compiler

Inspecting the results

The given figures will closely represent the according figures in the paper.
We did some post-processing for the published version: We adapted the spacing of the text and removed the “ERR” column for clarity. The instances either do or do not time out on all implementations which does not give any meaningful insights.
Depending on the amount of memory, more instances may fail to produce results, we found that 32GB of RAM suffices to run these benchmarks.
As documented in the paper, 3 instances will fail no matter what (but only when running step 2 of the benchmarks). We kept them in the benchmarks for inspection.