From 1541b89fe50c0e3c0bc20f545b1838c8ff04c79a Mon Sep 17 00:00:00 2001 From: Tej Chajed Date: Thu, 24 Aug 2023 13:47:15 -0500 Subject: [PATCH] Add benchmarking infrastructure to run verification (#142) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- Cargo.lock | 356 ++++++++++++++++++++---------- Cargo.toml | 1 + benchmarking/Cargo.toml | 21 ++ benchmarking/src/bin/benchmark.rs | 69 ++++++ benchmarking/src/bin/time.rs | 15 ++ benchmarking/src/lib.rs | 16 ++ benchmarking/src/measurement.rs | 77 +++++++ benchmarking/src/run.rs | 153 +++++++++++++ benchmarking/src/time_bench.rs | 332 ++++++++++++++++++++++++++++ inference/src/quant.rs | 26 +-- temporal-verifier/Cargo.toml | 1 + 11 files changed, 939 insertions(+), 128 deletions(-) create mode 100644 benchmarking/Cargo.toml create mode 100644 benchmarking/src/bin/benchmark.rs create mode 100644 benchmarking/src/bin/time.rs create mode 100644 benchmarking/src/lib.rs create mode 100644 benchmarking/src/measurement.rs create mode 100644 benchmarking/src/run.rs create mode 100644 benchmarking/src/time_bench.rs diff --git a/Cargo.lock b/Cargo.lock index 7375530a..a58f2df8 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -4,9 +4,9 @@ version = 3 [[package]] name = "aho-corasick" -version = "1.0.2" +version = "1.0.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "43f6cb1bf222025340178f382c426f13757b2960e89779dfcb319c32542a5a41" +checksum = "6748e8def348ed4d14996fa801f4122cd763fff530258cdc03f64b25f89d3a5a" dependencies = [ "memchr", ] @@ -19,24 +19,23 @@ checksum = "4b46cbb362ab8752921c97e041f5e366ee6297bd428a31275b9fcf1e380f7299" [[package]] name = "anstream" -version = "0.3.2" +version = "0.5.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0ca84f3628370c59db74ee214b3263d58f9aadd9b4fe7e711fd87dc452b7f163" +checksum = "b1f58811cfac344940f1a400b6e6231ce35171f614f26439e80f8c1465c5cc0c" dependencies = [ "anstyle", "anstyle-parse", "anstyle-query", "anstyle-wincon", "colorchoice", - "is-terminal", "utf8parse", ] [[package]] name = "anstyle" -version = "1.0.1" +version = "1.0.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3a30da5c5f2d5e72842e00bcb57657162cdabef0931f40e2deb9b4140440cecd" +checksum = "15c4c2c83f81532e5845a733998b6971faca23490340a418e9b72a3ec9de12ea" [[package]] name = "anstyle-parse" @@ -58,9 +57,9 @@ dependencies = [ [[package]] name = "anstyle-wincon" -version = "1.0.1" +version = "2.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "180abfa45703aebe0093f79badacc01b8fd4ea2e35118747e5811127f926e188" +checksum = "58f54d10c6dfa51283a066ceab3ec1ab78d13fae00aa49243a45e4571fb79dfd" dependencies = [ "anstyle", "windows-sys 0.48.0", @@ -72,6 +71,22 @@ version = "1.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "d468802bab17cbc0cc575e9b053f41e72aa36bfa6b7f55e3529ffa43161b97fa" +[[package]] +name = "benchmarking" +version = "0.1.0" +dependencies = [ + "clap", + "exec", + "fork", + "humantime", + "nix", + "process-sync", + "serde", + "serde_json", + "tabled", + "walkdir", +] + [[package]] name = "biodivine-lib-bdd" version = "0.5.1" @@ -91,9 +106,9 @@ checksum = "bef38d45163c2f1dde094a7dfd33ccf595c92905c8f8f4fdc18d06fb1037718a" [[package]] name = "bitflags" -version = "2.3.3" +version = "2.4.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "630be753d4e58660abd17930c71b647fe46c27ea6b63cc59e1e3851406972e42" +checksum = "b4682ae6287fcf752ecaabbfcc7b6f9b72aa33933dc23a554d853aea8eea8635" [[package]] name = "bitmaps" @@ -132,6 +147,12 @@ version = "3.13.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "a3e2c3daef883ecc1b5d58c15adae93470a91d425f3532ba1695849656af3fc1" +[[package]] +name = "bytecount" +version = "0.6.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2c676a478f63e9fa2dd5368a42f28bba0d6c560b775f38583c8bbaa7fcd67c9c" + [[package]] name = "byteorder" version = "1.4.3" @@ -155,11 +176,12 @@ checksum = "37b2a672a2cb129a2e41c10b1224bb368f9f37a2b16b612598138befd7b37eb5" [[package]] name = "cc" -version = "1.0.79" +version = "1.0.83" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "50d30906286121d95be3d479533b458f87493b30a4b5f79a607db8f5d11aa91f" +checksum = "f1174fb0b6ec23863f8b971027804a42614e347eafb0a95bf0b12cdae21fc4d0" dependencies = [ "jobserver", + "libc", ] [[package]] @@ -197,9 +219,9 @@ dependencies = [ [[package]] name = "clap" -version = "4.3.11" +version = "4.4.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1640e5cc7fb47dbb8338fd471b105e7ed6c3cb2aeb00c2e067127ffd3764a05d" +checksum = "1d5f1946157a96594eb2d2c10eb7ad9a2b27518cb3000209dec700c35df9197d" dependencies = [ "clap_builder", "clap_derive", @@ -208,9 +230,9 @@ dependencies = [ [[package]] name = "clap_builder" -version = "4.3.11" +version = "4.4.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "98c59138d527eeaf9b53f35a77fcc1fad9d883116070c63d5de1c7dc7b00c72b" +checksum = "78116e32a042dd73c2901f0dc30790d20ff3447f3e3472fad359e8c3d282bcd6" dependencies = [ "anstream", "anstyle", @@ -220,21 +242,21 @@ dependencies = [ [[package]] name = "clap_derive" -version = "4.3.2" +version = "4.4.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b8cd2b2a819ad6eec39e8f1d6b53001af1e5469f8c177579cdaeb313115b825f" +checksum = "c9fd1a5729c4548118d7d70ff234a44868d00489a4b6597b0b020918a0e91a1a" dependencies = [ "heck", "proc-macro2", "quote", - "syn 2.0.23", + "syn 2.0.29", ] [[package]] name = "clap_lex" -version = "0.5.0" +version = "0.5.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2da6da31387c7e4ef160ffab6d5e7f00c42626fe39aea70a7b0f1773f7dd6c1b" +checksum = "cd7cc57abe963c6d3b9d8be5b06ba7c8957a930305ca90304f24ef040aa6f961" [[package]] name = "codespan-reporting" @@ -374,9 +396,9 @@ dependencies = [ [[package]] name = "either" -version = "1.8.1" +version = "1.9.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7fcaabb2fef8c910e7f4c7ce9f67a1283a1715879a7c230ca9d6d1ae31f16d91" +checksum = "a26ae43d7bcc3b814de94796a5e736d4029efb0ee900c12e2d54c993ad1a1e07" [[package]] name = "ena" @@ -408,15 +430,26 @@ dependencies = [ [[package]] name = "equivalent" -version = "1.0.0" +version = "1.0.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "88bffebc5d80432c9b140ee17875ff173a8ab62faad5b257da912bd2f6c1c0a1" +checksum = "5443807d6dff69373d433ab9ef5378ad8df50ca6298caf15de6e52e24aaf54d5" [[package]] name = "errno" -version = "0.3.1" +version = "0.2.8" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4bcfec3a70f97c962c307b2d2c56e358cf1d00b558d74262b5f929ee8cc7e73a" +checksum = "f639046355ee4f37944e44f60642c6f3a7efa3cf6b78c78a0d989a8ce6c396a1" +dependencies = [ + "errno-dragonfly", + "libc", + "winapi", +] + +[[package]] +name = "errno" +version = "0.3.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6b30f669a7961ef1631673d2766cc92f52d64f7ef354d4fe0ddfd30ed52f0f4f" dependencies = [ "errno-dragonfly", "libc", @@ -433,6 +466,16 @@ dependencies = [ "libc", ] +[[package]] +name = "exec" +version = "0.3.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "886b70328cba8871bfc025858e1de4be16b1d5088f2ba50b57816f4210672615" +dependencies = [ + "errno 0.2.8", + "libc", +] + [[package]] name = "eyre" version = "0.6.8" @@ -460,6 +503,21 @@ dependencies = [ "thiserror", ] +[[package]] +name = "fnv" +version = "1.0.7" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3f9eec918d3f24069decb9af1554cad7c880e2da24a9afd88aca000531ab82c1" + +[[package]] +name = "fork" +version = "0.1.22" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bf2ca97a59201425e7ee4d197c9c4fea282fe87a97d666a580bda889b95b8e88" +dependencies = [ + "libc", +] + [[package]] name = "fxhash" version = "0.2.1" @@ -589,9 +647,9 @@ dependencies = [ [[package]] name = "insta" -version = "1.30.0" +version = "1.31.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "28491f7753051e5704d4d0ae7860d45fae3238d7d235bc4289dcd45c48d3cec3" +checksum = "a0770b0a3d4c70567f0d58331f3088b0e4c4f56c9b8d764efe654b4a5d46de3a" dependencies = [ "console", "lazy_static", @@ -625,9 +683,9 @@ dependencies = [ [[package]] name = "itoa" -version = "1.0.8" +version = "1.0.9" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "62b02a5381cc465bd3041d84623d0fa3b66738b52b8e2fc3bab8ad63ab032f4a" +checksum = "af150ab688ff2122fcef229be89cb50dd66af9e01a4ff320cc137eecc9bacc38" [[package]] name = "jobserver" @@ -667,15 +725,15 @@ checksum = "0717cef1bc8b636c6e1c1bbdefc09e6322da8a9321966e8928ef80d20f7f770f" [[package]] name = "linux-raw-sys" -version = "0.4.3" +version = "0.4.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "09fc20d2ca12cb9f044c93e3bd6d32d523e6e2ec3db4f7b2939cd99026ecd3f0" +checksum = "57bcfdad1b858c2db7c38303a6d2ad4dfaf5eb53dfeb0910128b2c26d6158503" [[package]] name = "log" -version = "0.4.19" +version = "0.4.20" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b06a4cde4c0f271a446782e3eff8de789548ce57dbc8eca9292c27f4a42004b4" +checksum = "b5e6163cb8c49088c2c36f57875e58ccd8c87c7427f7fbd50ea6710b2f3f2e8f" [[package]] name = "memchr" @@ -706,9 +764,9 @@ dependencies = [ [[package]] name = "num-bigint" -version = "0.4.3" +version = "0.4.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f93ab6289c7b344a8a9f60f88d80aa20032336fe78da341afc91c8a2341fc75f" +checksum = "608e7659b5c3d7cba262d894801b9ec9d00de989e8a82bd4bef91d08da45cdc0" dependencies = [ "autocfg", "num-integer", @@ -727,9 +785,9 @@ dependencies = [ [[package]] name = "num-traits" -version = "0.2.15" +version = "0.2.16" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "578ede34cf02f8924ab9447f50c28075b4d3e5b269972345e7e0372b38c6cdcd" +checksum = "f30b0abd723be7e2ffca1272140fac1a2f084c77ec3e123c192b66af1ee9e6c2" dependencies = [ "autocfg", ] @@ -756,6 +814,17 @@ version = "11.1.3" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "0ab1bc2a289d34bd04a330323ac98a1b4bc82c9d9fcb1e66b63caa84da26b575" +[[package]] +name = "papergrid" +version = "0.10.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a2ccbe15f2b6db62f9a9871642746427e297b0ceb85f9a7f1ee5ff47d184d0c8" +dependencies = [ + "bytecount", + "fnv", + "unicode-width", +] + [[package]] name = "path-slash" version = "0.2.1" @@ -791,9 +860,9 @@ checksum = "9fa00462b37ead6d11a82c9d568b26682d78e0477dc02d1966c013af80969739" [[package]] name = "pest" -version = "2.7.0" +version = "2.7.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f73935e4d55e2abf7f130186537b19e7a4abc886a0252380b59248af473a3fc9" +checksum = "1acb4a4365a13f749a93f1a094a7805e5cfa0955373a9de860d962eaa3a5fe5a" dependencies = [ "thiserror", "ucd-trie", @@ -801,9 +870,9 @@ dependencies = [ [[package]] name = "pest_derive" -version = "2.7.0" +version = "2.7.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "aef623c9bbfa0eedf5a0efba11a5ee83209c326653ca31ff019bec3a95bfff2b" +checksum = "666d00490d4ac815001da55838c500eafb0320019bbaa44444137c48b443a853" dependencies = [ "pest", "pest_generator", @@ -811,22 +880,22 @@ dependencies = [ [[package]] name = "pest_generator" -version = "2.7.0" +version = "2.7.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b3e8cba4ec22bada7fc55ffe51e2deb6a0e0db2d0b7ab0b103acc80d2510c190" +checksum = "68ca01446f50dbda87c1786af8770d535423fa8a53aec03b8f4e3d7eb10e0929" dependencies = [ "pest", "pest_meta", "proc-macro2", "quote", - "syn 2.0.23", + "syn 2.0.29", ] [[package]] name = "pest_meta" -version = "2.7.0" +version = "2.7.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a01f71cb40bd8bb94232df14b946909e14660e33fc05db3e50ae2a82d7ea0ca0" +checksum = "56af0a30af74d0445c0bf6d9d051c979b516a1a5af790d251daee76005420a48" dependencies = [ "once_cell", "pest", @@ -877,20 +946,53 @@ dependencies = [ "log", ] +[[package]] +name = "proc-macro-error" +version = "1.0.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "da25490ff9892aab3fcf7c36f08cfb902dd3e71ca0f9f9517bea02a73a5ce38c" +dependencies = [ + "proc-macro-error-attr", + "proc-macro2", + "quote", + "syn 1.0.109", + "version_check", +] + +[[package]] +name = "proc-macro-error-attr" +version = "1.0.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a1be40180e52ecc98ad80b184934baf3d0d29f979574e439af5a55274b35f869" +dependencies = [ + "proc-macro2", + "quote", + "version_check", +] + [[package]] name = "proc-macro2" -version = "1.0.63" +version = "1.0.66" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7b368fba921b0dce7e60f5e04ec15e565b3303972b42bcfde1d0713b881959eb" +checksum = "18fb31db3f9bddb2ea821cde30a9f70117e3f119938b5ee630b7403aa6e2ead9" dependencies = [ "unicode-ident", ] +[[package]] +name = "process-sync" +version = "0.2.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8b44ec73273477e3a7845d45781a1fa7d4f3cdc7311edfd590f936ae69032d23" +dependencies = [ + "libc", +] + [[package]] name = "quote" -version = "1.0.29" +version = "1.0.33" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "573015e8ab27661678357f27dc26460738fd2b6c86e46f386fde94cb5d913105" +checksum = "5267fca4496028628a95160fc423a33e8b2e6af8a5302579e322e4b520293cae" dependencies = [ "proc-macro2", ] @@ -958,9 +1060,9 @@ dependencies = [ [[package]] name = "regex" -version = "1.9.0" +version = "1.9.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "89089e897c013b3deb627116ae56a6955a72b8bed395c9526af31c9fe528b484" +checksum = "81bc1d4caf89fac26a70747fe603c130093b53c773888797a6329091246d651a" dependencies = [ "aho-corasick", "memchr", @@ -970,9 +1072,9 @@ dependencies = [ [[package]] name = "regex-automata" -version = "0.3.0" +version = "0.3.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "fa250384981ea14565685dea16a9ccc4d1c541a13f82b9c168572264d1df8c56" +checksum = "fed1ceff11a1dddaee50c9dc8e4938bd106e9d89ae372f192311e7da498e3b69" dependencies = [ "aho-corasick", "memchr", @@ -981,18 +1083,18 @@ dependencies = [ [[package]] name = "regex-syntax" -version = "0.7.3" +version = "0.7.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2ab07dc67230e4a4718e70fd5c20055a4334b121f1f9db8fe63ef39ce9b8c846" +checksum = "e5ea92a5b6195c6ef2a0295ea818b312502c6fc94dde986c5553242e18fd4ce2" [[package]] name = "rustix" -version = "0.38.3" +version = "0.38.8" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ac5ffa1efe7548069688cd7028f32591853cd7b5b756d41bcffd2353e4fc75b4" +checksum = "19ed4fa021d81c8392ce04db050a3da9a60299050b7ae1cf482d862b54a7218f" dependencies = [ - "bitflags 2.3.3", - "errno", + "bitflags 2.4.0", + "errno 0.3.2", "libc", "linux-raw-sys", "windows-sys 0.48.0", @@ -1000,9 +1102,9 @@ dependencies = [ [[package]] name = "ryu" -version = "1.0.14" +version = "1.0.15" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "fe232bdf6be8c8de797b22184ee71118d63780ea42ac85b61d1baa6d3b782ae9" +checksum = "1ad4cc8da4ef723ed60bced201181d83791ad433213d8c24efffda1eec85d741" [[package]] name = "same-file" @@ -1015,35 +1117,35 @@ dependencies = [ [[package]] name = "scopeguard" -version = "1.1.0" +version = "1.2.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d29ab0c6d3fc0ee92fe66e2d99f700eab17a8d57d1c1d3b748380fb20baa78cd" +checksum = "94143f37725109f92c262ed2cf5e59bce7498c01bcc1502d7b9afe439a4e9f49" [[package]] name = "serde" -version = "1.0.166" +version = "1.0.186" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d01b7404f9d441d3ad40e6a636a7782c377d2abdbe4fa2440e2edcc2f4f10db8" +checksum = "9f5db24220c009de9bd45e69fb2938f4b6d2df856aa9304ce377b3180f83b7c1" dependencies = [ "serde_derive", ] [[package]] name = "serde_derive" -version = "1.0.166" +version = "1.0.186" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5dd83d6dde2b6b2d466e14d9d1acce8816dedee94f735eac6395808b3483c6d6" +checksum = "5ad697f7e0b65af4983a4ce8f56ed5b357e8d3c36651bf6a7e13639c17b8e670" dependencies = [ "proc-macro2", "quote", - "syn 2.0.23", + "syn 2.0.29", ] [[package]] name = "serde_json" -version = "1.0.100" +version = "1.0.105" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0f1e14e89be7aa4c4b78bdbdc9eb5bf8517829a600ae8eaa39a6e1d960b5185c" +checksum = "693151e1ac27563d6dbcec9dee9fbd5da8539b20fa14ad3752b2e6d363ace360" dependencies = [ "itoa", "ryu", @@ -1147,15 +1249,39 @@ dependencies = [ [[package]] name = "syn" -version = "2.0.23" +version = "2.0.29" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "59fb7d6d8281a51045d62b8eb3a7d1ce347b76f312af50cd3dc0af39c87c1737" +checksum = "c324c494eba9d92503e6f1ef2e6df781e78f6a7705a0202d9801b198807d518a" dependencies = [ "proc-macro2", "quote", "unicode-ident", ] +[[package]] +name = "tabled" +version = "0.13.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4d38d39c754ae037a9bc3ca1580a985db7371cd14f1229172d1db9093feb6739" +dependencies = [ + "papergrid", + "tabled_derive", + "unicode-width", +] + +[[package]] +name = "tabled_derive" +version = "0.6.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "99f688a08b54f4f02f0a3c382aefdb7884d3d69609f785bd253dc033243e3fe4" +dependencies = [ + "heck", + "proc-macro-error", + "proc-macro2", + "quote", + "syn 1.0.109", +] + [[package]] name = "temporal-verifier" version = "0.1.0" @@ -1203,22 +1329,22 @@ dependencies = [ [[package]] name = "thiserror" -version = "1.0.41" +version = "1.0.47" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c16a64ba9387ef3fdae4f9c1a7f07a0997fce91985c0336f1ddc1822b3b37802" +checksum = "97a802ec30afc17eee47b2855fc72e0c4cd62be9b4efe6591edde0ec5bd68d8f" dependencies = [ "thiserror-impl", ] [[package]] name = "thiserror-impl" -version = "1.0.41" +version = "1.0.47" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d14928354b01c4d6a4f0e549069adef399a284e7995c7ccca94e8a07a5346c59" +checksum = "6bb623b56e39ab7dcd4b1b98bb6c8f8d907ed255b18de254088016b27a8ee19b" dependencies = [ "proc-macro2", "quote", - "syn 2.0.23", + "syn 2.0.29", ] [[package]] @@ -1254,9 +1380,9 @@ dependencies = [ [[package]] name = "toml_edit" -version = "0.19.12" +version = "0.19.14" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c500344a19072298cd05a7224b3c0c629348b78692bf48466c5238656e315a78" +checksum = "f8123f27e969974a3dfba720fdb560be359f57b44302d280ba72e76a74480e8a" dependencies = [ "indexmap 2.0.0", "serde", @@ -1273,15 +1399,15 @@ checksum = "497961ef93d974e23eb6f433eb5fe1b7930b659f06d12dec6fc44a8f554c0bba" [[package]] name = "ucd-trie" -version = "0.1.5" +version = "0.1.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9e79c4d996edb816c91e4308506774452e55e95c3c9de07b6729e17e15a5ef81" +checksum = "ed646292ffc8188ef8ea4d1e0e0150fb15a5c2e12ad9b8fc191ae7a8a7f3c4b9" [[package]] name = "unicode-ident" -version = "1.0.10" +version = "1.0.11" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "22049a19f4a68748a168c0fc439f9516686aa045927ff767eca0a85101fb6e73" +checksum = "301abaae475aa91687eb82514b328ab47a211a533026cb25fc3e519b86adfc3c" [[package]] name = "unicode-width" @@ -1353,7 +1479,7 @@ dependencies = [ "once_cell", "proc-macro2", "quote", - "syn 2.0.23", + "syn 2.0.29", "wasm-bindgen-shared", ] @@ -1375,7 +1501,7 @@ checksum = "54681b18a46765f095758388f2d0cf16eb8d4169b639ab575a8f5693af210c7b" dependencies = [ "proc-macro2", "quote", - "syn 2.0.23", + "syn 2.0.29", "wasm-bindgen-backend", "wasm-bindgen-shared", ] @@ -1442,7 +1568,7 @@ version = "0.48.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "677d2418bec65e3338edb076e806bc1ec15693c5d0104683f2efe857f61056a9" dependencies = [ - "windows-targets 0.48.1", + "windows-targets 0.48.5", ] [[package]] @@ -1462,17 +1588,17 @@ dependencies = [ [[package]] name = "windows-targets" -version = "0.48.1" +version = "0.48.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "05d4b17490f70499f20b9e791dcf6a299785ce8af4d709018206dc5b4953e95f" +checksum = "9a2fa6e2155d7247be68c096456083145c183cbbbc2764150dda45a87197940c" dependencies = [ - "windows_aarch64_gnullvm 0.48.0", - "windows_aarch64_msvc 0.48.0", - "windows_i686_gnu 0.48.0", - "windows_i686_msvc 0.48.0", - "windows_x86_64_gnu 0.48.0", - "windows_x86_64_gnullvm 0.48.0", - "windows_x86_64_msvc 0.48.0", + "windows_aarch64_gnullvm 0.48.5", + "windows_aarch64_msvc 0.48.5", + "windows_i686_gnu 0.48.5", + "windows_i686_msvc 0.48.5", + "windows_x86_64_gnu 0.48.5", + "windows_x86_64_gnullvm 0.48.5", + "windows_x86_64_msvc 0.48.5", ] [[package]] @@ -1483,9 +1609,9 @@ checksum = "597a5118570b68bc08d8d59125332c54f1ba9d9adeedeef5b99b02ba2b0698f8" [[package]] name = "windows_aarch64_gnullvm" -version = "0.48.0" +version = "0.48.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "91ae572e1b79dba883e0d315474df7305d12f569b400fcf90581b06062f7e1bc" +checksum = "2b38e32f0abccf9987a4e3079dfb67dcd799fb61361e53e2882c3cbaf0d905d8" [[package]] name = "windows_aarch64_msvc" @@ -1495,9 +1621,9 @@ checksum = "e08e8864a60f06ef0d0ff4ba04124db8b0fb3be5776a5cd47641e942e58c4d43" [[package]] name = "windows_aarch64_msvc" -version = "0.48.0" +version = "0.48.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b2ef27e0d7bdfcfc7b868b317c1d32c641a6fe4629c171b8928c7b08d98d7cf3" +checksum = "dc35310971f3b2dbbf3f0690a219f40e2d9afcf64f9ab7cc1be722937c26b4bc" [[package]] name = "windows_i686_gnu" @@ -1507,9 +1633,9 @@ checksum = "c61d927d8da41da96a81f029489353e68739737d3beca43145c8afec9a31a84f" [[package]] name = "windows_i686_gnu" -version = "0.48.0" +version = "0.48.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "622a1962a7db830d6fd0a69683c80a18fda201879f0f447f065a3b7467daa241" +checksum = "a75915e7def60c94dcef72200b9a8e58e5091744960da64ec734a6c6e9b3743e" [[package]] name = "windows_i686_msvc" @@ -1519,9 +1645,9 @@ checksum = "44d840b6ec649f480a41c8d80f9c65108b92d89345dd94027bfe06ac444d1060" [[package]] name = "windows_i686_msvc" -version = "0.48.0" +version = "0.48.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4542c6e364ce21bf45d69fdd2a8e455fa38d316158cfd43b3ac1c5b1b19f8e00" +checksum = "8f55c233f70c4b27f66c523580f78f1004e8b5a8b659e05a4eb49d4166cca406" [[package]] name = "windows_x86_64_gnu" @@ -1531,9 +1657,9 @@ checksum = "8de912b8b8feb55c064867cf047dda097f92d51efad5b491dfb98f6bbb70cb36" [[package]] name = "windows_x86_64_gnu" -version = "0.48.0" +version = "0.48.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ca2b8a661f7628cbd23440e50b05d705db3686f894fc9580820623656af974b1" +checksum = "53d40abd2583d23e4718fddf1ebec84dbff8381c07cae67ff7768bbf19c6718e" [[package]] name = "windows_x86_64_gnullvm" @@ -1543,9 +1669,9 @@ checksum = "26d41b46a36d453748aedef1486d5c7a85db22e56aff34643984ea85514e94a3" [[package]] name = "windows_x86_64_gnullvm" -version = "0.48.0" +version = "0.48.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7896dbc1f41e08872e9d5e8f8baa8fdd2677f29468c4e156210174edc7f7b953" +checksum = "0b7b52767868a23d5bab768e390dc5f5c55825b6d30b86c844ff2dc7414044cc" [[package]] name = "windows_x86_64_msvc" @@ -1555,15 +1681,15 @@ checksum = "9aec5da331524158c6d1a4ac0ab1541149c0b9505fde06423b02f5ef0106b9f0" [[package]] name = "windows_x86_64_msvc" -version = "0.48.0" +version = "0.48.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1a515f5799fe4961cb532f983ce2b23082366b898e52ffbce459c86f67c8378a" +checksum = "ed94fce61571a4006852b7389a063ab983c02eb1bb37b47f8272ce92d06d9538" [[package]] name = "winnow" -version = "0.4.9" +version = "0.5.15" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "81a2094c43cc94775293eaa0e499fbc30048a6d824ac82c0351a8c0bf9112529" +checksum = "7c2e3184b9c4e92ad5167ca73039d0c42476302ab603e2fec4487511f38ccefc" dependencies = [ "memchr", ] diff --git a/Cargo.toml b/Cargo.toml index a11bc1a3..ab9e4342 100644 --- 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 new file mode 100644 index 00000000..ff3d422a --- /dev/null +++ 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 new file mode 100644 index 00000000..9d1f1e95 --- /dev/null +++ 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 { + 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 new file mode 100644 index 00000000..4d946187 --- /dev/null +++ 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 { + let app = Time::parse(); + app.exec() +} diff --git a/benchmarking/src/lib.rs b/benchmarking/src/lib.rs new file mode 100644 index 00000000..b38f34af --- /dev/null +++ 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 new file mode 100644 index 00000000..d30c9ceb --- /dev/null +++ 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> { + let v = serde_json::from_str(s)?; + Ok(v) + } +} diff --git a/benchmarking/src/run.rs b/benchmarking/src/run.rs new file mode 100644 index 00000000..6bd164e3 --- /dev/null +++ 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, + 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, + args: Vec, + 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 { + [ + "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 { + 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) { + 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 { + 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() +} diff --git a/benchmarking/src/time_bench.rs b/benchmarking/src/time_bench.rs new file mode 100644 index 00000000..613a4517 --- /dev/null +++ b/benchmarking/src/time_bench.rs @@ -0,0 +1,332 @@ +// Copyright 2022-2023 VMware, Inc. +// SPDX-License-Identifier: BSD-2-Clause + +//! Tools for running a benchmark and gathering performance statistics like +//! runtime, CPU time, and memory usage. Also allows killing the benchmark with +//! a timeout. + +use std::{ + ffi::{OsStr, OsString}, + io, + os::fd::AsRawFd, + path::{Path, PathBuf}, + process::{Command, ExitCode, Stdio}, + sync::{Arc, Mutex}, + thread, + time::{Duration, Instant}, +}; + +use fork::Fork; +use nix::{ + errno::Errno, + fcntl::{self, OFlag}, + sys::{ + resource::{getrusage, Usage, UsageWho}, + signal::{killpg, Signal}, + stat::Mode, + time::TimeVal, + wait::{waitpid, WaitStatus}, + }, + unistd::{dup2, getpgid, setsid, Pid}, +}; +use process_sync::{SharedCondvar, SharedMutex}; + +use crate::measurement::RunMeasurement; + +/// The `time` utility runs a benchmark, optionally kills it after a timeout, +/// and gathers resource usage statistics. +/// +/// It is implemented as a separate binary to enable appropriate process +/// isolation (in particular to run `getrusage` and get statistics for a single +/// benchmark). It is more commonly used programmatically, with the library that +/// wraps the binary in a nice Rust interface. +#[derive(clap::Parser, Debug)] +pub struct Time { + /// Kill process after this much time + #[arg(long, short)] + pub time_limit: Option, + /// Output in JSON rather than a human-readable format + #[arg(long)] + pub json: bool, + /// Program to run + pub prog: OsString, + /// Arguments to pass + pub args: Vec, +} + +/// Get the temporal-verifier root path. +/// TODO: Only works when using a binary compiled locally. Will need to fix when +/// distributing a precompiled binary. +#[allow(non_snake_case)] +pub fn REPO_ROOT_PATH() -> &'static Path { + Path::new(env!("CARGO_MANIFEST_DIR")) + .parent() + .expect("could not get parent directory of benchmarking package") +} + +fn time_bin() -> PathBuf { + let target = REPO_ROOT_PATH().join("target"); + let release = target.join("release/time"); + if release.exists() { + return release; + } + let debug = target.join("debug/time"); + if debug.exists() { + return debug; + } + panic!("time binary not available - try cargo build --bin time") +} + +/// Run cargo and print a warning if it fails +fn run_cargo(args: I) +where + I: IntoIterator, + S: AsRef, +{ + let args = args + .into_iter() + .map(|s| s.as_ref().to_owned()) + .collect::>(); + let status = Command::new("cargo") + .arg("--quiet") + .args(&args) + .stdin(Stdio::null()) + .stdout(Stdio::null()) + .stderr(Stdio::inherit()) + .current_dir(REPO_ROOT_PATH()) + .status(); + match status { + Ok(status) => { + if !status.success() { + eprintln!( + "cargo {} failed", + args.join(OsStr::new(" ")).to_string_lossy() + ); + } + } + Err(err) => { + eprintln!("could not run cargo: {err}"); + } + } +} + +/// Build the `time` binary, which is an implicit dependency of benchmarks. +pub fn compile_time_bin() { + run_cargo(["build", "--release", "--bin", "time"]); +} + +/// Compile the `temporal-verifier` binary, which is run by the benchmarks. +pub fn compile_flyvy_bin() { + run_cargo(["build", "--release", "--bin", "temporal-verifier"]); +} + +#[derive(Debug, Clone)] +struct RawRunMeasurement { + real_time: Duration, + usage: Usage, + self_usage: Usage, + timed_out: bool, + status: Option, +} + +fn time_val_to_duration(time: TimeVal) -> Duration { + Duration::from_secs(time.tv_sec() as u64) + Duration::from_micros(time.tv_usec() as u64) +} + +impl RawRunMeasurement { + fn max_rss_bytes(&self) -> i64 { + if cfg!(target_os = "macos") { + // macOS reports maxrss in bytes + self.usage.max_rss() + } else { + // on Linux maxrss is in KB + self.usage.max_rss() * 1024 + } + } + + fn into_measurement(self) -> RunMeasurement { + RunMeasurement { + real_time: self.real_time, + user_time: time_val_to_duration(self.usage.user_time()), + sys_time: time_val_to_duration(self.usage.system_time()), + self_user_time: time_val_to_duration(self.self_usage.user_time()), + max_mem_bytes: self.max_rss_bytes() as usize, + timed_out: self.timed_out, + success: self.status == Some(0), + } + } +} + +impl Time { + fn get_child_measurements(&self, child: i32) -> Result { + let child = Pid::from_raw(child); + let start = Instant::now(); + let timeout = Arc::new(Mutex::new(false)); + if let Some(limit) = &self.time_limit { + let limit: Duration = (*limit).into(); + let pgid = getpgid(Some(child)).expect("could not get child pgid"); + let timeout = timeout.clone(); + thread::spawn(move || { + thread::sleep(limit); + // hold a lock on the timeout flag until we determine whether a + // timeout really occurred or not + let mut timeout = timeout.lock().unwrap(); + let r = killpg(pgid, Signal::SIGTERM); + if let Err(err) = r { + // this happens when the child no longer exists + if err == Errno::EPERM { + // exit without setting timeout flag + return; + } + eprintln!("could not send SIGTERM: {err}"); + } + // now set the timeout flag because the timer really did expire + *timeout = true; + drop(timeout); + thread::sleep(Duration::from_secs(1)); + eprintln!("sending SIGKILL"); + _ = killpg(pgid, Signal::SIGKILL); + }); + } + + let wstatus = waitpid(Some(child), None)?; + let status = match wstatus { + WaitStatus::Exited(_, status) => Some(status), + _ => None, + }; + let real_time = start.elapsed(); + let timed_out = *timeout.lock().unwrap(); + let usage = getrusage(UsageWho::RUSAGE_CHILDREN)?; + let self_usage = getrusage(UsageWho::RUSAGE_SELF)?; + let measurement = RawRunMeasurement { + real_time, + usage, + self_usage, + timed_out, + status, + }; + Ok(measurement) + } + + /// Run `time` with the arguments in `self`. This uses `fork` and `exec` + /// directly and is thus only intended for running from the `time` binary, + /// not from user code. + pub fn exec(&self) -> Result { + let (mut lock, mut cvar) = (SharedMutex::new().unwrap(), SharedCondvar::new().unwrap()); + match fork::fork() { + Ok(Fork::Parent(child)) => { + cvar.wait(&mut lock).unwrap(); + let measurements = self.get_child_measurements(child)?; + let parsed = measurements.clone().into_measurement(); + if self.json { + println!("{}", parsed.to_json()); + } else { + parsed.print(); + } + // timed_out is true if and only if the timeout thread triggers + // (even if this happens after the child exits) + if measurements.timed_out { + // to match behavior of `timeout(1)` + return Ok(ExitCode::from(124u8)); + } + if let Some(code) = measurements.status { + return Ok(ExitCode::from(code as u8)); + } + Ok(ExitCode::SUCCESS) + } + Ok(Fork::Child) => { + _ = setsid(); + cvar.notify_one().unwrap(); + let null = fcntl::open("/dev/null", OFlag::O_WRONLY, Mode::empty()) + .expect("could not get /dev/null"); + dup2(null, io::stdout().as_raw_fd()).expect("could not replace stdout with null"); + let err = exec::Command::new(&self.prog).args(&self.args).exec(); + eprintln!("exec failed: {err}"); + // mimic `timeout(1)` (although it distinguishes the command + // being found vs not found) + Ok(ExitCode::from(126)) + } + Err(err) => { + eprintln!("fork failed: {err}"); + // mimic `timeout(1)` + Ok(ExitCode::from(125)) + } + } + } + + /// Create a new timing config for library use. + #[allow(clippy::new_without_default)] + pub fn new>(prog: S) -> Self { + Self { + time_limit: None, + json: true, + prog: prog.as_ref().to_owned(), + args: vec![], + } + } + + /// Set the time limit of `self`. + pub fn timeout(&mut self, limit: Duration) -> &mut Self { + self.time_limit = Some(limit.into()); + self + } + + /// Append an argument to `self`. + pub fn arg>(&mut self, arg: S) -> &mut Self { + self.args.push(arg.as_ref().to_owned()); + self + } + + /// Append multiple arguments to `self`. + pub fn args(&mut self, args: I) -> &mut Self + where + I: IntoIterator, + S: AsRef, + { + self.args + .extend(args.into_iter().map(|s| s.as_ref().to_owned())); + self + } + + /// Get the command line to be run for debugging purposes (for example, to + /// run manually). + pub fn cmdline(&self) -> String { + let mut cmdline: Vec = vec![self.prog.to_string_lossy().to_string()]; + for arg in &self.args { + let arg = arg.to_string_lossy(); + if arg.contains([' ', '"']) { + cmdline.push(format!("\"{}\"", arg.replace('"', "\\\""))); + } else { + cmdline.push(arg.to_string()) + } + } + cmdline.join(" ") + } + + /// Run a compiled `time` binary using the arguments in `self`. + /// + /// This must use the binary rather than running `exec()` directly in order + /// to isolate resource usage measurement. + pub fn run(&self) -> Result { + let mut cmd = Command::new(time_bin()); + if let Some(limit) = &self.time_limit { + cmd.arg("--time-limit"); + cmd.arg(format!("{}s", limit.as_secs_f64())); + } + if self.json { + cmd.arg("--json"); + } + cmd.arg("--"); + cmd.arg(&self.prog); + cmd.args(&self.args); + let output = cmd.output()?; + let output = std::str::from_utf8(&output.stdout).expect("non utf-8 output"); + match RunMeasurement::from_json(output) { + Ok(r) => Ok(r), + Err(err) => { + eprintln!("{output}"); + panic!("could not parse JSON from time: {err}") + } + } + } +} diff --git a/inference/src/quant.rs b/inference/src/quant.rs index 967fc244..c4834970 100644 --- a/inference/src/quant.rs +++ b/inference/src/quant.rs @@ -386,37 +386,37 @@ impl Debug for QuantifierPrefix { impl PartialOrd for QuantifierPrefix { fn partial_cmp(&self, other: &Self) -> Option { + Some(self.cmp(other)) + } +} + +impl Ord for QuantifierPrefix { + fn cmp(&self, other: &Self) -> Ordering { assert_eq!(self.len(), other.len()); assert_eq!(self.sorts, other.sorts); for i in 0..self.len() { match (self.names[i].is_empty(), other.names[i].is_empty()) { (true, true) => continue, - (true, false) => return Some(Ordering::Greater), - (false, true) => return Some(Ordering::Less), + (true, false) => return Ordering::Greater, + (false, true) => return Ordering::Less, (false, false) => (), } match (self.quantifiers[i], other.quantifiers[i]) { - (Quantifier::Forall, Quantifier::Exists) => return Some(Ordering::Less), - (Quantifier::Exists, Quantifier::Forall) => return Some(Ordering::Greater), + (Quantifier::Forall, Quantifier::Exists) => return Ordering::Less, + (Quantifier::Exists, Quantifier::Forall) => return Ordering::Greater, _ => (), } match self.names[i].len().cmp(&other.names[i].len()) { - Ordering::Greater => return Some(Ordering::Less), - Ordering::Less => return Some(Ordering::Greater), + Ordering::Greater => return Ordering::Less, + Ordering::Less => return Ordering::Greater, _ => (), } } - Some(Ordering::Equal) - } -} - -impl Ord for QuantifierPrefix { - fn cmp(&self, other: &Self) -> Ordering { - self.partial_cmp(other).unwrap() + Ordering::Equal } } diff --git a/temporal-verifier/Cargo.toml b/temporal-verifier/Cargo.toml index 7a8d7153..25c1cd2a 100644 --- a/temporal-verifier/Cargo.toml +++ b/temporal-verifier/Cargo.toml @@ -2,6 +2,7 @@ name = "temporal-verifier" version.workspace = true edition.workspace = true +default-run = "temporal-verifier" [dependencies] bounded = { path = "../bounded" }