Add benchmarking infrastructure to run verification (#142)

The user-visible part of this is a library that allows running `temporal-verifier` with a timeout and gathering some runtime resource usage statistics as well as exit status, and a function to produce a nice table of all the results. I've used this in the simplest possible way to generate the results of running `temporal-verifier verify` over all the benchmarks, with the results shown below. This is the core infrastructure needed for #118. The remaining work (hopefully small) is to add configurations to do something similar for running qalpha and the bounded model checkers. These will be a bit more work since those have more parameters to configure. The infrastructure to monitor a benchmark is highly Unix-specific so it works on macOS and Linux and will not work on Windows (but it should work on WSL). To produce this table run `cargo run -r --bin benchmark -- verify --time-limit 30s`. ```txt ╭─────────┬──────────────────────────────────────────┬─────────┬────────┬──────────┬──────────┬────────┬─────────────╮ │ command │ file │ outcome │ time s │ cpu util │ solver % │ mem │ params │ ├─────────┼──────────────────────────────────────────┼─────────┼────────┼──────────┼──────────┼────────┼─────────────┤ │ verify │ consensus.fly │ fail │ 0.1 │ 2.5× │ 99% │ 24MB │ --solver=z3 │ │ verify │ consensus_epr.fly │ │ 0.1 │ 2.4× │ 99% │ 24MB │ --solver=z3 │ │ verify │ consensus_forall.fly │ │ 0.1 │ 2.6× │ 99% │ 23MB │ --solver=z3 │ │ verify │ fast_paxos_epr.fly │ │ 24.1 │ 1.4× │ 100% │ 172MB │ --solver=z3 │ │ verify │ fol/block_cache_system_frozen_async.fly │ timeout │ 30.0 │ 1.3× │ 100% │ 1817MB │ --solver=z3 │ │ verify │ fol/bosco_3t_safety.fly │ timeout │ 30.0 │ 0.7× │ 100% │ 313MB │ --solver=z3 │ │ verify │ fol/cache.fly │ │ 0.4 │ 6.5× │ 100% │ 25MB │ --solver=z3 │ │ verify │ fol/client_server_ae.fly │ fail │ 0.0 │ 1.3× │ 98% │ 23MB │ --solver=z3 │ │ verify │ fol/client_server_db_ae.fly │ │ 0.0 │ 2.0× │ 99% │ 21MB │ --solver=z3 │ │ verify │ fol/consensus_epr.fly │ │ 0.1 │ 2.6× │ 99% │ 24MB │ --solver=z3 │ │ verify │ fol/consensus_forall.fly │ │ 0.1 │ 2.8× │ 99% │ 23MB │ --solver=z3 │ │ verify │ fol/consensus_wo_decide.fly │ │ 0.1 │ 2.3× │ 99% │ 23MB │ --solver=z3 │ │ verify │ fol/fast_paxos_epr.fly │ │ 24.2 │ 1.5× │ 100% │ 175MB │ --solver=z3 │ │ verify │ fol/fast_paxos_forall.fly │ timeout │ 30.0 │ 0.9× │ 100% │ 195MB │ --solver=z3 │ │ verify │ fol/fast_paxos_forall_choosable.fly │ timeout │ 30.0 │ 0.0× │ 100% │ 35MB │ --solver=z3 │ │ verify │ fol/firewall.fly │ │ 0.0 │ 1.0× │ 97% │ 21MB │ --solver=z3 │ │ verify │ fol/flexible_paxos_epr.fly │ │ 0.2 │ 2.5× │ 100% │ 25MB │ --solver=z3 │ │ verify │ fol/flexible_paxos_forall.fly │ │ 0.4 │ 1.9× │ 100% │ 32MB │ --solver=z3 │ │ verify │ fol/flexible_paxos_forall_choosable.fly │ │ 2.9 │ 1.1× │ 100% │ 56MB │ --solver=z3 │ │ verify │ fol/hybrid_reliable_broadcast_cisa.fly │ │ 0.4 │ 4.2× │ 100% │ 31MB │ --solver=z3 │ │ verify │ fol/learning_switch.fly │ │ 0.1 │ 2.1× │ 99% │ 21MB │ --solver=z3 │ │ verify │ fol/lockserv.fly │ │ 0.1 │ 3.1× │ 99% │ 22MB │ --solver=z3 │ │ verify │ fol/multi_paxos_epr.fly │ timeout │ 30.0 │ 0.0× │ 100% │ 26MB │ --solver=z3 │ │ verify │ fol/paxos_epr.fly │ │ 1.0 │ 1.4× │ 100% │ 39MB │ --solver=z3 │ │ verify │ fol/paxos_forall.fly │ │ 0.2 │ 3.3× │ 100% │ 28MB │ --solver=z3 │ │ verify │ fol/paxos_forall_choosable.fly │ timeout │ 30.0 │ 0.0× │ 100% │ 28MB │ --solver=z3 │ │ verify │ fol/raft.fly │ fail │ 0.0 │ 0.4× │ 88% │ 1MB │ --solver=z3 │ │ verify │ fol/ring_id.fly │ │ 0.1 │ 1.9× │ 99% │ 23MB │ --solver=z3 │ │ verify │ fol/ring_id_not_dead.fly │ │ 0.5 │ 1.5× │ 100% │ 33MB │ --solver=z3 │ │ verify │ fol/sharded_kv.fly │ │ 0.1 │ 1.9× │ 99% │ 23MB │ --solver=z3 │ │ verify │ fol/sharded_kv_no_lost_keys.fly │ │ 0.1 │ 1.8× │ 99% │ 24MB │ --solver=z3 │ │ verify │ fol/stoppable_paxos_epr.fly │ timeout │ 30.0 │ 0.2× │ 100% │ 94MB │ --solver=z3 │ │ verify │ fol/stoppable_paxos_forall.fly │ timeout │ 30.0 │ 0.3× │ 100% │ 90MB │ --solver=z3 │ │ verify │ fol/stoppable_paxos_forall_choosable.fly │ timeout │ 30.0 │ 0.1× │ 100% │ 46MB │ --solver=z3 │ │ verify │ fol/ticket.fly │ │ 0.1 │ 4.4× │ 100% │ 23MB │ --solver=z3 │ │ verify │ fol/toy_consensus_epr.fly │ │ 0.1 │ 1.9× │ 99% │ 23MB │ --solver=z3 │ │ verify │ fol/toy_consensus_forall.fly │ │ 0.0 │ 1.8× │ 98% │ 22MB │ --solver=z3 │ │ verify │ fol/vertical_paxos_epr.fly │ │ 3.1 │ 1.2× │ 100% │ 68MB │ --solver=z3 │ │ verify │ fol/vertical_paxos_forall.fly │ │ 0.3 │ 3.7× │ 100% │ 27MB │ --solver=z3 │ │ verify │ fol/vertical_paxos_forall_choosable.fly │ │ 1.2 │ 1.7× │ 100% │ 49MB │ --solver=z3 │ │ verify │ lockserver.fly │ │ 0.0 │ 3.2× │ 99% │ 22MB │ --solver=z3 │ │ verify │ paxos_epr.fly │ │ 0.9 │ 1.2× │ 100% │ 37MB │ --solver=z3 │ │ verify │ pingpong.fly │ │ 0.0 │ 0.5× │ 92% │ 19MB │ --solver=z3 │ ╰─────────┴──────────────────────────────────────────┴─────────┴────────┴──────────┴──────────┴────────┴─────────────╯ total: 43 ok: 31 timeout: 9 fail: 3 ``` To produce this table run `cargo run --bin benchmark -- verify --time-limit 30s --solver cvc5`. ```txt ╭─────────┬──────────────────────────────────────────┬─────────┬────────┬──────────┬──────────┬──────┬───────────────╮ │ command │ file │ outcome │ time s │ cpu util │ solver % │ mem │ params │ ├─────────┼──────────────────────────────────────────┼─────────┼────────┼──────────┼──────────┼──────┼───────────────┤ │ verify │ consensus.fly │ fail │ 0.2 │ 2.2× │ 100% │ 20MB │ --solver=cvc5 │ │ verify │ consensus_epr.fly │ │ 1.1 │ 1.5× │ 100% │ 33MB │ --solver=cvc5 │ │ verify │ consensus_forall.fly │ │ 0.3 │ 1.9× │ 100% │ 25MB │ --solver=cvc5 │ │ verify │ fast_paxos_epr.fly │ timeout │ 30.0 │ 0.1× │ 100% │ 39MB │ --solver=cvc5 │ │ verify │ fol/block_cache_system_frozen_async.fly │ │ 7.3 │ 6.7× │ 100% │ 59MB │ --solver=cvc5 │ │ verify │ fol/bosco_3t_safety.fly │ timeout │ 30.0 │ 0.5× │ 100% │ 78MB │ --solver=cvc5 │ │ verify │ fol/cache.fly │ │ 1.6 │ 8.2× │ 100% │ 36MB │ --solver=cvc5 │ │ verify │ fol/client_server_ae.fly │ fail │ 0.0 │ 1.6× │ 98% │ 13MB │ --solver=cvc5 │ │ verify │ fol/client_server_db_ae.fly │ │ 0.1 │ 2.8× │ 100% │ 17MB │ --solver=cvc5 │ │ verify │ fol/consensus_epr.fly │ │ 1.0 │ 1.6× │ 100% │ 32MB │ --solver=cvc5 │ │ verify │ fol/consensus_forall.fly │ │ 0.3 │ 2.1× │ 100% │ 25MB │ --solver=cvc5 │ │ verify │ fol/consensus_wo_decide.fly │ │ 0.2 │ 1.8× │ 100% │ 25MB │ --solver=cvc5 │ │ verify │ fol/fast_paxos_epr.fly │ timeout │ 30.0 │ 0.1× │ 100% │ 43MB │ --solver=cvc5 │ │ verify │ fol/fast_paxos_forall.fly │ timeout │ 30.0 │ 0.1× │ 100% │ 45MB │ --solver=cvc5 │ │ verify │ fol/fast_paxos_forall_choosable.fly │ timeout │ 30.0 │ 0.5× │ 100% │ 63MB │ --solver=cvc5 │ │ verify │ fol/firewall.fly │ │ 0.2 │ 1.9× │ 100% │ 23MB │ --solver=cvc5 │ │ verify │ fol/flexible_paxos_epr.fly │ │ 22.8 │ 2.2× │ 100% │ 90MB │ --solver=cvc5 │ │ verify │ fol/flexible_paxos_forall.fly │ │ 2.4 │ 2.4× │ 100% │ 42MB │ --solver=cvc5 │ │ verify │ fol/flexible_paxos_forall_choosable.fly │ │ 3.8 │ 2.6× │ 100% │ 56MB │ --solver=cvc5 │ │ verify │ fol/hybrid_reliable_broadcast_cisa.fly │ │ 22.8 │ 3.3× │ 100% │ 74MB │ --solver=cvc5 │ │ verify │ fol/learning_switch.fly │ │ 1.0 │ 1.6× │ 100% │ 29MB │ --solver=cvc5 │ │ verify │ fol/lockserv.fly │ │ 0.1 │ 4.5× │ 100% │ 15MB │ --solver=cvc5 │ │ verify │ fol/multi_paxos_epr.fly │ │ 18.1 │ 2.9× │ 100% │ 91MB │ --solver=cvc5 │ │ verify │ fol/paxos_epr.fly │ timeout │ 30.0 │ 0.2× │ 100% │ 61MB │ --solver=cvc5 │ │ verify │ fol/paxos_forall.fly │ │ 2.4 │ 3.8× │ 100% │ 44MB │ --solver=cvc5 │ │ verify │ fol/paxos_forall_choosable.fly │ │ 3.6 │ 2.8× │ 100% │ 56MB │ --solver=cvc5 │ │ verify │ fol/raft.fly │ fail │ 0.0 │ 0.4× │ 89% │ 1MB │ --solver=cvc5 │ │ verify │ fol/ring_id.fly │ │ 0.4 │ 1.5× │ 100% │ 30MB │ --solver=cvc5 │ │ verify │ fol/ring_id_not_dead.fly │ │ 4.4 │ 2.5× │ 100% │ 45MB │ --solver=cvc5 │ │ verify │ fol/sharded_kv.fly │ │ 0.2 │ 2.8× │ 100% │ 18MB │ --solver=cvc5 │ │ verify │ fol/sharded_kv_no_lost_keys.fly │ │ 1.0 │ 1.4× │ 100% │ 35MB │ --solver=cvc5 │ │ verify │ fol/stoppable_paxos_epr.fly │ timeout │ 30.0 │ 0.1× │ 100% │ 36MB │ --solver=cvc5 │ │ verify │ fol/stoppable_paxos_forall.fly │ timeout │ 30.0 │ 2.1× │ 100% │ 81MB │ --solver=cvc5 │ │ verify │ fol/stoppable_paxos_forall_choosable.fly │ timeout │ 30.0 │ 0.6× │ 100% │ 85MB │ --solver=cvc5 │ │ verify │ fol/ticket.fly │ │ 0.3 │ 3.9× │ 100% │ 27MB │ --solver=cvc5 │ │ verify │ fol/toy_consensus_epr.fly │ │ 0.4 │ 2.1× │ 100% │ 34MB │ --solver=cvc5 │ │ verify │ fol/toy_consensus_forall.fly │ │ 0.1 │ 2.6× │ 99% │ 19MB │ --solver=cvc5 │ │ verify │ fol/vertical_paxos_epr.fly │ timeout │ 30.0 │ 0.1× │ 100% │ 50MB │ --solver=cvc5 │ │ verify │ fol/vertical_paxos_forall.fly │ timeout │ 30.0 │ 0.3× │ 100% │ 56MB │ --solver=cvc5 │ │ verify │ fol/vertical_paxos_forall_choosable.fly │ timeout │ 30.0 │ 1.0× │ 100% │ 72MB │ --solver=cvc5 │ │ verify │ lockserver.fly │ │ 0.1 │ 4.7× │ 100% │ 15MB │ --solver=cvc5 │ │ verify │ paxos_epr.fly │ timeout │ 30.0 │ 0.2× │ 100% │ 59MB │ --solver=cvc5 │ │ verify │ pingpong.fly │ │ 0.0 │ 0.6× │ 89% │ 7MB │ --solver=cvc5 │ ╰─────────┴──────────────────────────────────────────┴─────────┴────────┴──────────┴──────────┴──────┴───────────────╯ total: 43 ok: 27 timeout: 13 fail: 3 ``` --------- Signed-off-by: Tej Chajed <[email protected]>
flyvy-verifier · Aug 24, 2023 · 1541b89 · 1541b89
1 parent 96bbdb6
commit 1541b89
Show file tree

Hide file tree

Showing 11 changed files with 939 additions and 128 deletions.
diff --git a/Cargo.lock b/Cargo.lock
diff --git a/Cargo.toml b/Cargo.toml
@@ -7,6 +7,7 @@ members = [
 	"inference",
 	"verify",
 	"temporal-verifier",
+	"benchmarking",
 ]
 resolver = "2"
 

diff --git a/benchmarking/Cargo.toml b/benchmarking/Cargo.toml
@@ -0,0 +1,21 @@
+[package]
+name = "benchmarking"
+version.workspace = true
+edition.workspace = true
+
+[dependencies]
+clap = { version = "4.3.4", features = ["derive"] }
+humantime = "2.1.0"
+nix = { version = "0.26.2", default-features = false, features = [
+  "signal",
+  "process",
+  "resource",
+  "fs",
+] }
+fork = "0.1.22"
+exec = "0.3.1"
+process-sync = "0.2.2"
+serde = { version = "1.0.177", features = ["derive"] }
+serde_json = "1.0.104"
+walkdir = "2.3.3"
+tabled = "0.13.0"
diff --git a/benchmarking/src/bin/benchmark.rs b/benchmarking/src/bin/benchmark.rs
@@ -0,0 +1,69 @@
+// Copyright 2022-2023 VMware, Inc.
+// SPDX-License-Identifier: BSD-2-Clause
+
+//! Run all of the examples as benchmarks and report the results in a table.
+
+use std::time::Duration;
+
+use benchmarking::{
+    run::{get_examples, BenchmarkMeasurement},
+    time_bench::{compile_flyvy_bin, compile_time_bin, REPO_ROOT_PATH},
+};
+use clap::Parser;
+
+#[derive(clap::Subcommand, Clone, Debug, PartialEq, Eq)]
+enum Command {
+    Verify {
+        /// Time limit for verifying each file.
+        #[arg(long, default_value = "60s")]
+        time_limit: humantime::Duration,
+        /// Solver to use
+        #[arg(long, default_value = "z3")]
+        solver: String,
+    },
+}
+
+#[derive(clap::Parser, Debug)]
+struct App {
+    /// Command to run
+    #[command(subcommand)]
+    command: Command,
+}
+
+fn benchmark_verify(time_limit: Duration, solver: &str) -> Vec<BenchmarkMeasurement> {
+    get_examples()
+        .into_iter()
+        .map(|file| {
+            eprintln!(
+                "verify {}",
+                file.strip_prefix(REPO_ROOT_PATH()).unwrap().display()
+            );
+            BenchmarkMeasurement::run(
+                vec![String::from("verify")],
+                vec![format!("--solver={solver}")],
+                file,
+                time_limit,
+            )
+        })
+        .collect()
+}
+
+impl App {
+    fn exec(&self) {
+        // make sure `time` is available
+        compile_time_bin();
+        // make sure `temporal-verifier` is available
+        compile_flyvy_bin();
+        match &self.command {
+            Command::Verify { time_limit, solver } => {
+                let results = benchmark_verify((*time_limit).into(), solver);
+                BenchmarkMeasurement::print_table(results);
+            }
+        }
+    }
+}
+
+fn main() {
+    let app = App::parse();
+    app.exec();
+}
diff --git a/benchmarking/src/bin/time.rs b/benchmarking/src/bin/time.rs
@@ -0,0 +1,15 @@
+// Copyright 2022-2023 VMware, Inc.
+// SPDX-License-Identifier: BSD-2-Clause
+
+//! Implementation of the `time` binary. Everything interesting is in
+//! [`benchmarking::time_bench::Time`].
+
+use std::{io, process::ExitCode};
+
+use benchmarking::time_bench::Time;
+use clap::Parser;
+
+fn main() -> Result<ExitCode, io::Error> {
+    let app = Time::parse();
+    app.exec()
+}
diff --git a/benchmarking/src/lib.rs b/benchmarking/src/lib.rs
@@ -0,0 +1,16 @@
+// Copyright 2022-2023 VMware, Inc.
+// SPDX-License-Identifier: BSD-2-Clause
+
+//! Tools for benchmarking flyvy on the examples.
+
+#![deny(missing_docs)]
+// configure clippy
+#![deny(clippy::uninlined_format_args)]
+#![allow(clippy::comparison_to_empty)]
+// documentation-related lints (only checked when running rustdoc)
+#![allow(rustdoc::private_intra_doc_links)]
+#![deny(rustdoc::broken_intra_doc_links)]
+
+pub mod measurement;
+pub mod run;
+pub mod time_bench;
diff --git a/benchmarking/src/measurement.rs b/benchmarking/src/measurement.rs
@@ -0,0 +1,77 @@
+// Copyright 2022-2023 VMware, Inc.
+// SPDX-License-Identifier: BSD-2-Clause
+
+//! Statistics from a single benchmark run, mostly gathered through `getrusage`.
+
+use std::{error::Error, time::Duration};
+
+use serde::{Deserialize, Serialize};
+
+/// `RunMeasurement` holds the statistics captured from a single run. This includes
+/// resource usage through `getrusage` (the same system call that powers
+/// `time`), as well as basic info about whether the process exited with an
+/// error or not.
+#[derive(Debug, Clone, Serialize, Deserialize)]
+pub struct RunMeasurement {
+    /// Elapsed time of run.
+    pub real_time: Duration,
+    /// User time (including all child processes like solvers).
+    pub user_time: Duration,
+    /// System time (including all child processes like solvers).
+    pub sys_time: Duration,
+    /// User time (excluding child processes).
+    pub self_user_time: Duration,
+    /// Max memory usage (RSS) in bytes
+    pub max_mem_bytes: usize,
+    /// Whether the run was killed early due to a timeout.
+    pub timed_out: bool,
+    /// Whether the run was successful
+    pub success: bool,
+}
+
+impl RunMeasurement {
+    /// Maximum memory usage in MB.
+    pub fn max_mem_mb(&self) -> usize {
+        self.max_mem_bytes / 1024 / 1024
+    }
+
+    /// Time spent in subprocesses (eg, SMT solver).
+    pub fn subprocess_time(&self) -> Duration {
+        self.user_time.saturating_sub(self.self_user_time)
+    }
+
+    /// Percentage of time using CPU. This is simply the ratio of "CPU time" to
+    /// wall clock time, so it can exceed 1 for a multi-threaded program.
+    pub fn cpu_utilization(&self) -> f64 {
+        self.user_time.as_secs_f64() / self.real_time.as_secs_f64()
+    }
+
+    /// Percentage of user time in subprocesses. This should be at most 1.
+    pub fn subprocess_utilization(&self) -> f64 {
+        self.subprocess_time().as_secs_f64() / self.user_time.as_secs_f64()
+    }
+
+    /// Print a human-readable version of these results.
+    pub fn print(&self) {
+        println!(
+            "time: {:0.1}s{timed_out_msg}",
+            &self.real_time.as_secs_f64(),
+            timed_out_msg = if self.timed_out { " (timed out)" } else { "" }
+        );
+        println!("  user:   {:0.1}s", self.user_time.as_secs_f64());
+        println!("  solver: {:0.1}s", self.subprocess_time().as_secs_f64());
+        println!("  sys:    {:0.1}s", self.sys_time.as_secs_f64());
+        println!("max mem: {}MB", self.max_mem_mb());
+    }
+
+    /// Convert these results to a compact JSON representation.
+    pub fn to_json(&self) -> String {
+        serde_json::to_string(self).expect("could not serialize `RunResult`")
+    }
+
+    /// Parse results serialized as JSON.
+    pub fn from_json(s: &str) -> Result<Self, Box<dyn Error>> {
+        let v = serde_json::from_str(s)?;
+        Ok(v)
+    }
+}
diff --git a/benchmarking/src/run.rs b/benchmarking/src/run.rs
@@ -0,0 +1,153 @@
+// Copyright 2022-2023 VMware, Inc.
+// SPDX-License-Identifier: BSD-2-Clause
+
+//! Library for running and reporting benchmark measurements.
+
+use std::{collections::HashMap, ffi::OsStr, path::PathBuf, time::Duration};
+
+use crate::{
+    measurement::RunMeasurement,
+    time_bench::{Time, REPO_ROOT_PATH},
+};
+
+use tabled::settings::{
+    object::{Columns, Object, Rows},
+    width::MinWidth,
+    Alignment, Color, Modify, Style, Width,
+};
+use walkdir::WalkDir;
+
+/// A benchmark configuration and its resulting measurement.
+#[derive(Debug, Clone)]
+pub struct BenchmarkMeasurement {
+    command: Vec<String>,
+    params: String,
+    file: PathBuf,
+    measurement: RunMeasurement,
+}
+
+impl BenchmarkMeasurement {
+    /// Run flyvy on a single benchmark, isolated to its own process.
+    ///
+    /// command + args form the arguments to temporal-verifier. These are split
+    /// only for display purposes in the table; `command` is something like
+    /// `infer qalpha` while `args` has other configuration and quantifiers for
+    /// each sort, for example.
+    ///
+    /// file is added to the end of the argument list and also becomes a
+    /// separate column in the results.
+    ///
+    /// time_limit is a maximum time to wait for the benchmark before killing
+    /// it.
+    pub fn run(
+        command: Vec<String>,
+        args: Vec<String>,
+        file: PathBuf,
+        time_limit: Duration,
+    ) -> Self {
+        let mut timer = flyvy_timer();
+        timer.timeout(time_limit);
+        timer.args(&command);
+        timer.args(&args);
+        timer.arg(&file);
+        let measurement = timer.run().expect("error getting timing");
+        BenchmarkMeasurement {
+            command,
+            params: args.join(" "),
+            file,
+            measurement,
+        }
+    }
+
+    /// Header used for printing table. Make sure this stays in sync with [`Self::row`].
+    fn header() -> Vec<String> {
+        [
+            "command", "file", "outcome", "time s", "cpu util", "solver %", "mem", "params",
+        ]
+        .iter()
+        .map(|s| s.to_string())
+        .collect()
+    }
+
+    fn success(&self) -> &'static str {
+        if self.measurement.timed_out {
+            "timeout"
+        } else if self.measurement.success {
+            ""
+        } else {
+            "fail"
+        }
+    }
+
+    fn row(&self) -> Vec<String> {
+        let file_name = self
+            .file
+            .strip_prefix(REPO_ROOT_PATH().join("temporal-verifier/examples"))
+            .unwrap_or(self.file.strip_prefix(REPO_ROOT_PATH()).unwrap());
+        let measure = &self.measurement;
+        let real_time = measure.real_time.as_secs_f64();
+        vec![
+            format!("{}", self.command.join(" ")),
+            format!("{}", file_name.display()),
+            format!("{}", self.success()),
+            format!("{real_time:0.1}"),
+            format!("{:0.1}×", measure.cpu_utilization()),
+            format!("{:0.0}%", measure.subprocess_utilization() * 100.0),
+            format!("{}MB", measure.max_mem_mb()),
+            format!("{}", self.params),
+        ]
+    }
+
+    /// Print a nicely-formatting table from a list of results.
+    pub fn print_table(results: Vec<Self>) {
+        let mut success_counts = HashMap::<&str, usize>::new();
+        for r in &results {
+            let mut key = r.success();
+            if key == "" {
+                key = "ok";
+            }
+            *success_counts.entry(key).or_default() += 1;
+        }
+        let total = results.len();
+
+        let mut rows = vec![Self::header()];
+        rows.extend(results.iter().map(|r| r.row()));
+
+        let mut table = tabled::builder::Builder::from(rows).build();
+        let numerical_columns = Columns::new(3..=6);
+        table
+            .with(Style::rounded())
+            .with(Modify::new(Columns::single(2).not(Rows::first())).with(Color::FG_RED))
+            .with(Modify::new(numerical_columns).with(Alignment::right()))
+            .with(MinWidth::new(150))
+            .with(Width::truncate(300));
+        println!("{table}");
+        println!(
+            "total:    {total}
+ok:       {ok}
+timeout:  {timeout}
+fail:     {fail}",
+            ok = success_counts.get("ok").unwrap_or(&0),
+            timeout = success_counts.get("timeout").unwrap_or(&0),
+            fail = success_counts.get("fail").unwrap_or(&0)
+        );
+    }
+}
+
+/// Create an instance of Time that runs temporal-verifier
+fn flyvy_timer() -> Time {
+    Time::new(REPO_ROOT_PATH().join("target/release/temporal-verifier"))
+}
+
+/// Get all the .fly examples from `temporal-verifier/examples`.
+pub fn get_examples() -> Vec<PathBuf> {
+    let root = REPO_ROOT_PATH();
+    let examples_dir = root.join("temporal-verifier/examples");
+    WalkDir::new(examples_dir)
+        .sort_by_file_name()
+        .into_iter()
+        .filter_map(|e| e.ok())
+        .filter(|e| e.file_type().is_file() && e.path().extension() == Some(OsStr::new("fly")))
+        .map(|e| e.into_path())
+        .collect()
+}