diff --git a/.github/workflows/bench-nightly.yml b/.github/workflows/bench-nightly.yml new file mode 100644 index 0000000..f62bb24 --- /dev/null +++ b/.github/workflows/bench-nightly.yml @@ -0,0 +1,41 @@ +name: Bench Nightly + +# Runs criterion benchmarks nightly and archives the `target/criterion/` +# directory as a build artifact. No regression gate yet — the goal of +# this workflow is to collect a stable baseline across commits so we can +# build a data-driven ratchet later. +# +# Scheduled at 03:30 UTC, offset from other nightly jobs (e.g. fuzzing) +# so bench machines aren't contending for runner minutes. + +on: + schedule: + - cron: "30 3 * * *" + # Allow manual triggering from the GitHub UI for ad-hoc baselines. + workflow_dispatch: + +env: + CARGO_TERM_COLOR: always + +jobs: + solver-benchmarks: + name: Solver criterion nightly + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - uses: dtolnay/rust-toolchain@nightly + - uses: Swatinem/rust-cache@v2 + - name: Run solver benchmarks (save baseline) + # --save-baseline nightly stores this run under + # target/criterion/*/nightly so future runs can diff against it. + run: cargo bench --bench solver_benchmarks -p spar-solver -- --save-baseline nightly + - name: Run codegen benchmarks (save baseline) + run: cargo bench --bench codegen_benchmarks -p spar-codegen -- --save-baseline nightly + - name: Upload criterion output + if: always() + uses: actions/upload-artifact@v4 + with: + name: criterion-nightly + path: target/criterion/ + if-no-files-found: warn + retention-days: 30 diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 6fc9552..bb28b8c 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -55,6 +55,20 @@ jobs: path: target/nextest/ci/junit.xml if-no-files-found: ignore + # ── Bench compile smoke (fast regression gate) ────────────────────── + bench-smoke: + name: Bench compile smoke + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - uses: dtolnay/rust-toolchain@nightly + - uses: Swatinem/rust-cache@v2 + - name: Verify benches compile + # --no-run builds the bench binaries without executing them. This + # catches API drift in criterion harnesses on every PR with only + # the cost of a `cargo check`-like compile. + run: cargo bench --workspace --no-run + # ── Security audits ────────────────────────────────────────────────── audit: name: Security Audit (RustSec) diff --git a/Cargo.lock b/Cargo.lock index 4012961..9a7cfb0 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -17,6 +17,18 @@ version = "0.2.21" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "683d7910e743518b0e34f1186f92494becacb047c7b6bf616c96772180fef923" +[[package]] +name = "anes" +version = "0.1.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4b46cbb362ab8752921c97e041f5e366ee6297bd428a31275b9fcf1e380f7299" + +[[package]] +name = "anstyle" +version = "1.0.14" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "940b3a0ca603d1eade50a4846a2afffd5ef57a9feac2c0e2ec2e14f9ead76000" + [[package]] name = "anyhow" version = "1.0.102" @@ -38,7 +50,7 @@ dependencies = [ "bitflags 2.11.0", "cexpr", "clang-sys", - "itertools", + "itertools 0.13.0", "log", "prettyplease", "proc-macro2", @@ -92,12 +104,24 @@ version = "0.2.14" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "36f64beae40a84da1b4b26ff2761a5b895c12adc41dc25aaee1c4f2bbfe97a6e" +[[package]] +name = "bumpalo" +version = "3.20.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5d20789868f4b01b2f2caec9f5c4e0213b41e3e5702a50157d699ae31ced2fcb" + [[package]] name = "bytes" version = "1.11.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "1e748733b7cbc798e1434b6ac524f0c1ff2ab456fe201501e6497c8417a4fc33" +[[package]] +name = "cast" +version = "0.3.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "37b2a672a2cb129a2e41c10b1224bb368f9f37a2b16b612598138befd7b37eb5" + [[package]] name = "cc" version = "1.2.58" @@ -129,6 +153,33 @@ version = "0.2.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "613afe47fcd5fac7ccf1db93babcb082c5994d996f20b8b159f2ad1658eb5724" +[[package]] +name = "ciborium" +version = "0.2.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "42e69ffd6f0917f5c029256a24d0161db17cea3997d185db0d35926308770f0e" +dependencies = [ + "ciborium-io", + "ciborium-ll", + "serde", +] + +[[package]] +name = "ciborium-io" +version = "0.2.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "05afea1e0a06c9be33d539b876f1ce3692f4afea2cb41f740e7743225ed1c757" + +[[package]] +name = "ciborium-ll" +version = "0.2.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "57663b653d948a338bfb3eeba9bb2fd5fcfaecb9e199e87e1eda4d9e8b240fd9" +dependencies = [ + "ciborium-io", + "half", +] + [[package]] name = "clang-sys" version = "1.8.1" @@ -140,6 +191,31 @@ dependencies = [ "libloading", ] +[[package]] +name = "clap" +version = "4.6.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1ddb117e43bbf7dacf0a4190fef4d345b9bad68dfc649cb349e7d17d28428e51" +dependencies = [ + "clap_builder", +] + +[[package]] +name = "clap_builder" +version = "4.6.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "714a53001bf66416adb0e2ef5ac857140e7dc3a0c48fb28b2f10762fc4b5069f" +dependencies = [ + "anstyle", + "clap_lex", +] + +[[package]] +name = "clap_lex" +version = "1.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c8d4a3bb8b1e0c1050499d1815f5ab16d04f0959b233085fb31653fbfc9d98f9" + [[package]] name = "cmake" version = "0.1.58" @@ -155,6 +231,42 @@ version = "3.0.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "7704b5fdd17b18ae31c4c1da5a2e0305a2bf17b5249300a9ee9ed7b72114c636" +[[package]] +name = "criterion" +version = "0.5.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f2b12d017a929603d80db1831cd3a24082f8137ce19c69e6447f54f5fc8d692f" +dependencies = [ + "anes", + "cast", + "ciborium", + "clap", + "criterion-plot", + "is-terminal", + "itertools 0.10.5", + "num-traits", + "once_cell", + "oorandom", + "plotters", + "rayon", + "regex", + "serde", + "serde_derive", + "serde_json", + "tinytemplate", + "walkdir", +] + +[[package]] +name = "criterion-plot" +version = "0.5.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6b50826342786a51a89e2da3a28f1c32b06e387201bc2d19791f622c673706b1" +dependencies = [ + "cast", + "itertools 0.10.5", +] + [[package]] name = "crossbeam-channel" version = "0.5.15" @@ -198,6 +310,12 @@ version = "0.8.21" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "d0a5c400df2834b80a4c3327b3aad3a4c4cd4de0629063962b03235697506a28" +[[package]] +name = "crunchy" +version = "0.2.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "460fbee9c2c2f33933d720630a6a0bac33ba7053db5344fac858d4b8952d77d5" + [[package]] name = "dissimilar" version = "1.0.11" @@ -336,6 +454,17 @@ dependencies = [ "highs", ] +[[package]] +name = "half" +version = "2.7.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6ea2d84b969582b4b1864a92dc5d27cd2b77b622a8d79306834f1be5ba20d84b" +dependencies = [ + "cfg-if", + "crunchy", + "zerocopy", +] + [[package]] name = "hashbrown" version = "0.14.5" @@ -377,6 +506,12 @@ version = "0.5.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "2304e00983f87ffb38b55b444b5e3b60a884b5d30c0fca7d82fe33449bbe55ea" +[[package]] +name = "hermit-abi" +version = "0.5.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "fc0fef456e4baa96da950455cd02c081ca953b141298e41db3fc7e36b1da849c" + [[package]] name = "highs" version = "2.0.0" @@ -433,6 +568,26 @@ dependencies = [ "rustversion", ] +[[package]] +name = "is-terminal" +version = "0.4.17" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3640c1c38b8e4e43584d8df18be5fc6b0aa314ce6ebf51b53313d4306cca8e46" +dependencies = [ + "hermit-abi", + "libc", + "windows-sys", +] + +[[package]] +name = "itertools" +version = "0.10.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b0fd2260e829bddf4cb6ea802289de2f86d6a7a690192fbe91b3f46e0f2c8473" +dependencies = [ + "either", +] + [[package]] name = "itertools" version = "0.13.0" @@ -448,6 +603,16 @@ version = "1.0.18" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "8f42a60cbdf9a97f5d2305f08a87dc4e09308d1276d28c869c684d7777685682" +[[package]] +name = "js-sys" +version = "0.3.95" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2964e92d1d9dc3364cae4d718d93f227e3abb088e747d92e0395bfdedf1c12ca" +dependencies = [ + "once_cell", + "wasm-bindgen", +] + [[package]] name = "la-arena" version = "0.3.1" @@ -569,6 +734,12 @@ version = "1.21.4" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9f7c3e4beb33f85d45ae3e3a1792185706c8e16d043238c593331cc7cd313b50" +[[package]] +name = "oorandom" +version = "11.1.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d6790f58c7ff633d8771f42965289203411a5e5c68388703c06e14f24770b41e" + [[package]] name = "parking_lot" version = "0.12.5" @@ -618,6 +789,34 @@ version = "0.2.17" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "a89322df9ebe1c1578d689c92318e070967d1042b512afbe49518723f4e6d5cd" +[[package]] +name = "plotters" +version = "0.3.7" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5aeb6f403d7a4911efb1e33402027fc44f29b5bf6def3effcc22d7bb75f2b747" +dependencies = [ + "num-traits", + "plotters-backend", + "plotters-svg", + "wasm-bindgen", + "web-sys", +] + +[[package]] +name = "plotters-backend" +version = "0.3.7" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "df42e13c12958a16b3f7f4386b9ab1f3e7933914ecea48da7139435263a4172a" + +[[package]] +name = "plotters-svg" +version = "0.3.7" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "51bae2ac328883f7acdfea3d66a7c35751187f870bc81f94563733a154d7a670" +dependencies = [ + "plotters-backend", +] + [[package]] name = "portable-atomic" version = "1.13.1" @@ -892,6 +1091,15 @@ dependencies = [ "synstructure", ] +[[package]] +name = "same-file" +version = "1.0.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "93fc1dc3aaa9bfed95e02e6eadabb4baf7e3078b0bd1b4d7b6b0b68378900502" +dependencies = [ + "winapi-util", +] + [[package]] name = "scopeguard" version = "1.2.0" @@ -1049,6 +1257,7 @@ dependencies = [ name = "spar-codegen" version = "0.6.0" dependencies = [ + "criterion", "la-arena", "serde", "serde_json", @@ -1110,6 +1319,7 @@ dependencies = [ name = "spar-solver" version = "0.6.0" dependencies = [ + "criterion", "good_lp", "la-arena", "petgraph 0.7.1", @@ -1233,6 +1443,16 @@ version = "0.2.16" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "259cdf8ed4e4aca6f1e9d011e10bd53f524a2d0637d7b28450f6c64ac298c4c6" +[[package]] +name = "tinytemplate" +version = "1.2.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "be4d6b5f19ff7664e8c98d03e2139cb510db9b0a60b55f8e8709b689d939b6bc" +dependencies = [ + "serde", + "serde_json", +] + [[package]] name = "toml" version = "0.8.23" @@ -1320,6 +1540,16 @@ dependencies = [ "libc", ] +[[package]] +name = "walkdir" +version = "2.5.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "29790946404f91d9c5d06f9874efddea1dc06c5efe94541a7d6863108e3a5e4b" +dependencies = [ + "same-file", + "winapi-util", +] + [[package]] name = "wasip2" version = "1.0.2+wasi-0.2.9" @@ -1338,6 +1568,51 @@ dependencies = [ "wit-bindgen 0.51.0", ] +[[package]] +name = "wasm-bindgen" +version = "0.2.118" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0bf938a0bacb0469e83c1e148908bd7d5a6010354cf4fb73279b7447422e3a89" +dependencies = [ + "cfg-if", + "once_cell", + "rustversion", + "wasm-bindgen-macro", + "wasm-bindgen-shared", +] + +[[package]] +name = "wasm-bindgen-macro" +version = "0.2.118" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "eeff24f84126c0ec2db7a449f0c2ec963c6a49efe0698c4242929da037ca28ed" +dependencies = [ + "quote", + "wasm-bindgen-macro-support", +] + +[[package]] +name = "wasm-bindgen-macro-support" +version = "0.2.118" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9d08065faf983b2b80a79fd87d8254c409281cf7de75fc4b773019824196c904" +dependencies = [ + "bumpalo", + "proc-macro2", + "quote", + "syn", + "wasm-bindgen-shared", +] + +[[package]] +name = "wasm-bindgen-shared" +version = "0.2.118" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5fd04d9e306f1907bd13c6361b5c6bfc7b3b3c095ed3f8a9246390f8dbdee129" +dependencies = [ + "unicode-ident", +] + [[package]] name = "wasm-encoder" version = "0.244.0" @@ -1406,6 +1681,25 @@ dependencies = [ "semver", ] +[[package]] +name = "web-sys" +version = "0.3.95" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4f2dfbb17949fa2088e5d39408c48368947b86f7834484e87b73de55bc14d97d" +dependencies = [ + "js-sys", + "wasm-bindgen", +] + +[[package]] +name = "winapi-util" +version = "0.1.11" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c2a7b1c03c876122aa43f3020e6c3c3ee5c05081c9a00739faf7503aeba10d22" +dependencies = [ + "windows-sys", +] + [[package]] name = "windows-link" version = "0.2.1" diff --git a/Cargo.toml b/Cargo.toml index bd01a37..7635253 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -10,6 +10,7 @@ members = [ "crates/spar-analysis", "crates/spar-transform", "crates/spar-cli", + "crates/spar-codegen", "crates/spar-render", "crates/spar-solver", "crates/spar-sysml2", @@ -54,3 +55,4 @@ syn = { version = "2", features = ["full"] } proc-macro2 = "1" proptest = "1" good_lp = { version = "1", default-features = false, features = ["highs"] } +criterion = { version = "0.5", features = ["html_reports"] } diff --git a/artifacts/verification.yaml b/artifacts/verification.yaml index 903659b..0cea3ae 100644 --- a/artifacts/verification.yaml +++ b/artifacts/verification.yaml @@ -486,6 +486,114 @@ artifacts: - type: satisfies target: ARCH-R4 + # ── Performance Benchmarks (criterion) ────────────────────────────── + # + # Per ISO 26262-6 Table 10 row 1e ("performance test", HR at ASIL D): + # criterion benchmarks guard against silent runtime regressions in the + # scheduling solver and codegen emit path. CI runs `cargo bench --no-run` + # on every PR (bench-smoke job in .github/workflows/ci.yml). A nightly + # job (.github/workflows/bench-nightly.yml) runs the full bench and + # archives target/criterion/ as a build artifact for baseline tracking. + + - id: BENCH-SOLVER-SMALL + type: feature + title: Solver bench — 8-task workload + description: > + Criterion benchmark group `solver_small`: 8 periodic tasks, 2 + processors, utilisation ≤ 0.69 (below RM bound). Benches MILP, + FFD, BFD, and NSGA-II against the same input. Warmup 3s, + measurement 5s. + status: implemented + fields: + method: performance-test + steps: + - run: cargo bench --bench solver_benchmarks -p spar-solver -- solver_small + links: + - type: verifies + target: REQ-SOLVER-003 + - type: verifies + target: REQ-SOLVER-004 + + - id: BENCH-SOLVER-MEDIUM + type: feature + title: Solver bench — 64-task workload + description: > + Criterion benchmark group `solver_medium`: 64 periodic tasks + across 8 processors, representative avionics/automotive scale. + Exercises MILP, FFD, BFD, and NSGA-II. + status: implemented + fields: + method: performance-test + steps: + - run: cargo bench --bench solver_benchmarks -p spar-solver -- solver_medium + links: + - type: verifies + target: REQ-SOLVER-004 + - type: verifies + target: REQ-SOLVER-005 + - type: verifies + target: REQ-SOLVER-006 + + - id: BENCH-SOLVER-LARGE + type: feature + title: Solver bench — 256-task stress workload + description: > + Criterion benchmark group `solver_large`: 256 tasks across 32 + processors. `sample_size(10)` to bound wall-clock under MILP. + Intended as a regression canary for super-linear algorithmic + blowups. + status: implemented + fields: + method: performance-test + steps: + - run: cargo bench --bench solver_benchmarks -p spar-solver -- solver_large + links: + - type: verifies + target: REQ-SOLVER-004 + - type: verifies + target: REQ-SOLVER-005 + + - id: BENCH-SOLVER-WORST-CASE + type: feature + title: Solver bench — adversarial near-boundary workload + description: > + Criterion benchmark group `solver_worst_case`: 64 tasks near the + schedulability boundary (u ≈ 0.95) with prime periods forcing + many rate-monotonic priority-inversion checks. Emulates the + hardest inputs produced by the fuzz corpus. + status: implemented + fields: + method: performance-test + steps: + - run: cargo bench --bench solver_benchmarks -p spar-solver -- solver_worst_case + links: + - type: verifies + target: REQ-SOLVER-004 + - type: verifies + target: REQ-SOLVER-005 + - type: verifies + target: REQ-SOLVER-006 + + - id: BENCH-CODEGEN-EMIT + type: feature + title: Codegen bench — 64-thread emit pipeline + description: > + Criterion benchmark group `codegen_emit`: builds a synthetic + SystemInstance with 64 periodic threads and benches + `spar_codegen::generate()` end-to-end (Rust + WIT + config + + tests + proofs + docs + workspace) as well as the Rust-only + emit path. + status: implemented + fields: + method: performance-test + steps: + - run: cargo bench --bench codegen_benchmarks -p spar-codegen + links: + - type: verifies + target: REQ-CODEGEN-001 + - type: verifies + target: REQ-CODEGEN-RUST + # ── v0.3.0 Verification Records ───────────────────────────────────── - id: VAL-RTA-001 diff --git a/crates/spar-codegen/Cargo.toml b/crates/spar-codegen/Cargo.toml index 08489d3..5e155f3 100644 --- a/crates/spar-codegen/Cargo.toml +++ b/crates/spar-codegen/Cargo.toml @@ -18,3 +18,8 @@ toml.workspace = true spar-hir-def.workspace = true spar-base-db.workspace = true la-arena.workspace = true +criterion.workspace = true + +[[bench]] +name = "codegen_benchmarks" +harness = false diff --git a/crates/spar-codegen/benches/codegen_benchmarks.rs b/crates/spar-codegen/benches/codegen_benchmarks.rs new file mode 100644 index 0000000..939d764 --- /dev/null +++ b/crates/spar-codegen/benches/codegen_benchmarks.rs @@ -0,0 +1,148 @@ +//! Criterion benchmarks for the codegen emit path. +//! +//! Builds a synthetic AADL model with 64 periodic threads (the scheduling +//! "medium" workload) and benches the `generate()` emit-to-string pipeline. +//! This is the slow outer loop any build/CI run hits after the solver +//! has decided on bindings — we want to catch regressions in string +//! formatting, property lookup, and workspace generation. +//! +//! Tracks: REQ-CODEGEN-* (see artifacts/verification.yaml). + +use std::hint::black_box; +use std::time::Duration; + +use criterion::{Criterion, Throughput, criterion_group, criterion_main}; + +use spar_base_db::SourceFile; +use spar_codegen::{CodegenConfig, OutputFormat, VerifyMode, generate}; +use spar_hir_def::HirDefDatabase; +use spar_hir_def::file_item_tree; +use spar_hir_def::instance::SystemInstance; +use spar_hir_def::name::Name; +use spar_hir_def::resolver::GlobalScope; + +/// Render an AADL package string with `n_threads` periodic threads inside +/// a single process on a single processor. Threads have distinct names and +/// varied Period / Compute_Execution_Time so property lookup isn't cached +/// into a trivial constant. +fn synth_aadl(n_threads: usize) -> String { + // A small catalogue of periods to cycle through — covers the typical + // avionics/automotive range used in the solver benches. + const PERIODS_MS: &[u32] = &[1, 2, 5, 10, 20, 50, 100, 200]; + + let mut out = String::with_capacity(4096); + out.push_str( + "package BenchSystem\n\ + public\n\ + with Deployment_Properties;\n\ + with Timing_Properties;\n\n\ + data Msg\n\ + end Msg;\n\n\ + processor CPU\n\ + end CPU;\n\n", + ); + + // Emit N distinct thread types (one type per instance keeps the test + // representative of heterogeneous deployments). + for i in 0..n_threads { + let period = PERIODS_MS[i % PERIODS_MS.len()]; + let wcet_low = period.max(1) / 2; + let wcet_high = period.max(2).saturating_sub(1).max(wcet_low + 1); + out.push_str(&format!( + " thread Worker_{i:04}\n \ + properties\n \ + Timing_Properties::Period => {period} ms;\n \ + Timing_Properties::Deadline => {period} ms;\n \ + Timing_Properties::Compute_Execution_Time => {wcet_low} ms .. {wcet_high} ms;\n \ + Deployment_Properties::Dispatch_Protocol => Periodic;\n \ + end Worker_{i:04};\n\n \ + thread implementation Worker_{i:04}.impl\n \ + end Worker_{i:04}.impl;\n\n", + )); + } + + // One process that contains all threads. + out.push_str(" process Orchestrator\n end Orchestrator;\n\n"); + out.push_str(" process implementation Orchestrator.impl\n subcomponents\n"); + for i in 0..n_threads { + out.push_str(&format!(" w_{i:04}: thread Worker_{i:04}.impl;\n")); + } + out.push_str(" end Orchestrator.impl;\n\n"); + + // Top-level system. + out.push_str( + " system BenchRoot\n end BenchRoot;\n\n\ + system implementation BenchRoot.impl\n \ + subcomponents\n \ + cpu: processor CPU;\n \ + proc: process Orchestrator.impl;\n \ + end BenchRoot.impl;\n\n\ + end BenchSystem;\n", + ); + + out +} + +/// Build a `SystemInstance` from an AADL source string. +fn build_instance(aadl: &str) -> SystemInstance { + let db = HirDefDatabase::default(); + let sf = SourceFile::new(&db, "bench.aadl".to_string(), aadl.to_string()); + let tree = file_item_tree(&db, sf); + let scope = GlobalScope::from_trees(vec![tree]); + SystemInstance::instantiate( + &scope, + &Name::new("BenchSystem"), + &Name::new("BenchRoot"), + &Name::new("impl"), + ) +} + +fn bench_codegen_emit(c: &mut Criterion) { + let mut group = c.benchmark_group("codegen_emit"); + group + .warm_up_time(Duration::from_secs(3)) + .measurement_time(Duration::from_secs(5)); + + let n_threads = 64; + let aadl = synth_aadl(n_threads); + let instance = build_instance(&aadl); + let config = CodegenConfig { + root_name: "bench_root".into(), + output_dir: "output".into(), + format: OutputFormat::Both, + verify: Some(VerifyMode::All), + rivet: true, + dry_run: true, + }; + + group.throughput(Throughput::Elements(n_threads as u64)); + + // End-to-end emit: Rust + WIT + config + tests + proofs + docs + + // workspace, concatenated into in-memory strings. + group.bench_function("generate_full_64", |b| { + b.iter(|| { + let output = generate(black_box(&instance), black_box(&config)); + black_box(output); + }); + }); + + // Rust-only emit: isolates the schedule-emitting hot path (per-thread + // timing properties → Rust attributes) from WIT / Lean / Kani / docs. + let rust_only_config = CodegenConfig { + verify: None, + rivet: false, + format: OutputFormat::Rust, + ..config.clone() + }; + group.bench_function("generate_rust_only_64", |b| { + b.iter(|| { + let output = generate(black_box(&instance), black_box(&rust_only_config)); + black_box(output); + }); + }); + + group.finish(); +} + +criterion_group!(benches, bench_codegen_emit); +criterion_main!(benches); diff --git a/crates/spar-solver/Cargo.toml b/crates/spar-solver/Cargo.toml index 87f807b..5a04c22 100644 --- a/crates/spar-solver/Cargo.toml +++ b/crates/spar-solver/Cargo.toml @@ -14,3 +14,10 @@ la-arena.workspace = true rustc-hash = "2" serde.workspace = true good_lp.workspace = true + +[dev-dependencies] +criterion.workspace = true + +[[bench]] +name = "solver_benchmarks" +harness = false diff --git a/crates/spar-solver/benches/solver_benchmarks.rs b/crates/spar-solver/benches/solver_benchmarks.rs new file mode 100644 index 0000000..73fdd57 --- /dev/null +++ b/crates/spar-solver/benches/solver_benchmarks.rs @@ -0,0 +1,414 @@ +//! Criterion benchmarks for the scheduling/deployment solver. +//! +//! Covers the three public solver entrypoints exercised by the schedule +//! analysis flow: +//! +//! * [`spar_solver::milp::solve_milp`] — exact MILP allocator (HiGHS backend). +//! * [`spar_solver::nsga2::optimize`] — NSGA-II multi-objective Pareto front. +//! * [`spar_solver::allocate::Allocator::ffd`] / `bfd` — bin-packing heuristics. +//! +//! Workloads: +//! * `solver_small` — 8 periodic tasks, total utilisation ≤ 0.69 +//! (safely below the RM n*(2^(1/n)-1) bound for n=8 ≈ 0.724). +//! * `solver_medium` — 64 periodic tasks, same shape. +//! * `solver_large` — 256 periodic tasks, `sample_size(10)` to keep +//! wall-clock manageable under MILP. +//! * `solver_worst_case` — utilisation ≈ 0.95, many harmonic/near-harmonic +//! periods so that the MILP capacity constraints are tight and every +//! rate-monotonic priority-inversion boundary is exercised. +//! +//! Tracks: REQ-SOLVER-003, REQ-SOLVER-004, REQ-SOLVER-005, REQ-SOLVER-006. + +use std::hint::black_box; +use std::time::Duration; + +use criterion::{BenchmarkId, Criterion, Throughput, criterion_group, criterion_main}; + +use la_arena::Arena; +use spar_hir_def::instance::{ComponentInstance, ComponentInstanceIdx}; +use spar_hir_def::item_tree::ComponentCategory; +use spar_hir_def::name::Name; + +use spar_solver::allocate::Allocator; +use spar_solver::constraints::{ModelConstraints, ProcessorConstraint, ThreadConstraint}; +use spar_solver::milp::solve_milp; +use spar_solver::nsga2::{Nsga2Config, optimize as nsga2_optimize}; + +// --------------------------------------------------------------------------- +// Workload synthesis helpers +// --------------------------------------------------------------------------- + +/// Allocate a throwaway `ComponentInstanceIdx`. The solver only uses the +/// idx for downstream rewriting; for benchmarks the id just needs to be +/// syntactically valid. +fn dummy_idx() -> ComponentInstanceIdx { + let mut arena: Arena = Arena::new(); + arena.alloc(ComponentInstance { + name: Name::new("bench_dummy"), + category: ComponentCategory::Thread, + type_name: Name::new("BenchDummy"), + impl_name: None, + package: Name::new("Bench"), + parent: None, + children: Vec::new(), + features: Vec::new(), + connections: Vec::new(), + flows: Vec::new(), + modes: Vec::new(), + mode_transitions: Vec::new(), + array_index: None, + in_modes: Vec::new(), + }) +} + +fn make_thread(name: String, period_ps: u64, wcet_ps: u64) -> ThreadConstraint { + ThreadConstraint { + idx: dummy_idx(), + name, + period_ps, + wcet_ps, + deadline_ps: period_ps, + current_binding: None, + priority: None, + } +} + +fn make_processor(name: String) -> ProcessorConstraint { + ProcessorConstraint { + idx: dummy_idx(), + name, + memory_bytes: None, + } +} + +/// Synthesise a "realistic" periodic task set of `n_tasks` tasks distributed +/// across `n_procs` processors, with aggregate utilisation capped at +/// `target_util` per processor (so the resulting MILP is feasible). +/// +/// Periods are drawn from a small catalogue of typical avionics/automotive +/// rates (1 ms … 200 ms). WCETs are derived so that the sum of per-thread +/// utilisation stays under `target_util * n_procs`. +fn synth_periodic_taskset(n_tasks: usize, n_procs: usize, target_util: f64) -> ModelConstraints { + // Mix of common periods in picoseconds. These intentionally span a wide + // range so the RMA priority-inversion computation has non-trivial work. + const PERIODS_PS: &[u64] = &[ + 1_000_000_000, // 1 ms — high-rate control + 2_000_000_000, // 2 ms + 5_000_000_000, // 5 ms + 10_000_000_000, // 10 ms — typical control loop + 20_000_000_000, // 20 ms + 25_000_000_000, // 25 ms + 50_000_000_000, // 50 ms + 100_000_000_000, // 100 ms — sensor fusion + 200_000_000_000, // 200 ms — logging/telemetry + ]; + + // Target total utilisation across the fleet; divide equally so no + // single task is degenerate (≥ 1.0). + let total_util_budget = target_util * n_procs as f64; + let per_task_util = total_util_budget / n_tasks as f64; + + let threads: Vec = (0..n_tasks) + .map(|i| { + let period = PERIODS_PS[i % PERIODS_PS.len()]; + // WCET = utilisation * period, floored to an integer picosecond. + let wcet = (per_task_util * period as f64).max(1.0) as u64; + make_thread(format!("task_{i:04}"), period, wcet) + }) + .collect(); + + let processors: Vec = (0..n_procs) + .map(|j| make_processor(format!("cpu_{j:02}"))) + .collect(); + + ModelConstraints { + threads, + processors, + warnings: Vec::new(), + } +} + +/// Construct a deliberately adversarial task set near the schedulability +/// boundary. Properties: +/// +/// * Aggregate utilisation ≈ 0.95 × n_procs (just below the 1.0 capacity +/// bound, so bin-packing has very little slack and MILP must explore +/// many branches). +/// * Harmonic and near-harmonic period mix (1, 2, 5, 7, 11, 13 ms …) so +/// the rate-monotonic priority-inversion checks inside the schedulability +/// analysis fire on many pairs. +/// * Several "heavy" tasks (> 0.3 util each) forcing non-trivial packing. +/// +/// This is the style of input that fuzzing tends to produce in the +/// scheduling corpus — use it as a perf canary. +fn synth_worst_case(n_tasks: usize, n_procs: usize) -> ModelConstraints { + // Primes/near-primes in ms → picoseconds: maximise hyperperiod and + // guarantee non-harmonic interactions between tasks. + const ADVERSARIAL_PERIODS_PS: &[u64] = &[ + 1_000_000_000, + 2_000_000_000, + 5_000_000_000, + 7_000_000_000, + 11_000_000_000, + 13_000_000_000, + 17_000_000_000, + 23_000_000_000, + 29_000_000_000, + ]; + + let target_util = 0.95_f64; + let total_budget = target_util * n_procs as f64; + + // Split budget unevenly: 40% of tasks are "heavy" (each ~ 3× the + // average), the rest share what's left. This forces the solver off + // the trivial "spread evenly" path. + let n_heavy = (n_tasks as f64 * 0.4).round() as usize; + let n_light = n_tasks - n_heavy; + + let heavy_util_each = if n_heavy > 0 { + (total_budget * 0.7) / n_heavy as f64 + } else { + 0.0 + }; + let light_util_each = if n_light > 0 { + (total_budget * 0.3) / n_light as f64 + } else { + 0.0 + }; + + let mut threads = Vec::with_capacity(n_tasks); + + for i in 0..n_heavy { + let period = ADVERSARIAL_PERIODS_PS[i % ADVERSARIAL_PERIODS_PS.len()]; + // Clamp per-task util ≤ 0.95 so individual tasks remain feasible + // on a single processor (else the instance is trivially infeasible). + let util = heavy_util_each.min(0.95); + let wcet = (util * period as f64).max(1.0) as u64; + threads.push(make_thread(format!("heavy_{i:04}"), period, wcet)); + } + + for i in 0..n_light { + let period = ADVERSARIAL_PERIODS_PS[(i + 3) % ADVERSARIAL_PERIODS_PS.len()]; + let util = light_util_each.clamp(0.01, 0.95); + let wcet = (util * period as f64).max(1.0) as u64; + threads.push(make_thread(format!("light_{i:04}"), period, wcet)); + } + + let processors: Vec = (0..n_procs) + .map(|j| make_processor(format!("cpu_{j:02}"))) + .collect(); + + ModelConstraints { + threads, + processors, + warnings: Vec::new(), + } +} + +// --------------------------------------------------------------------------- +// Benchmark groups +// --------------------------------------------------------------------------- + +fn bench_solver_small(c: &mut Criterion) { + let mut group = c.benchmark_group("solver_small"); + group + .warm_up_time(Duration::from_secs(3)) + .measurement_time(Duration::from_secs(5)); + + // 8 tasks, 2 processors, u ≈ 0.69 per CPU (below RM bound 0.724). + let workload = synth_periodic_taskset(8, 2, 0.69); + group.throughput(Throughput::Elements(workload.threads.len() as u64)); + + group.bench_function(BenchmarkId::new("milp", 8), |b| { + b.iter(|| { + let result = solve_milp(black_box(&workload)).expect("feasible"); + black_box(result); + }); + }); + + group.bench_function(BenchmarkId::new("ffd", 8), |b| { + b.iter(|| { + let result = Allocator::ffd(black_box(&workload)); + black_box(result); + }); + }); + + group.bench_function(BenchmarkId::new("bfd", 8), |b| { + b.iter(|| { + let result = Allocator::bfd(black_box(&workload)); + black_box(result); + }); + }); + + // Small NSGA-II: tiny population to keep the small-bench fast. + let nsga_cfg = Nsga2Config { + population_size: 20, + generations: 20, + seed: 42, + ..Default::default() + }; + group.bench_function(BenchmarkId::new("nsga2", 8), |b| { + b.iter(|| { + let result = nsga2_optimize(black_box(&workload), black_box(&nsga_cfg)); + black_box(result); + }); + }); + + group.finish(); +} + +fn bench_solver_medium(c: &mut Criterion) { + let mut group = c.benchmark_group("solver_medium"); + group + .warm_up_time(Duration::from_secs(3)) + .measurement_time(Duration::from_secs(5)); + + // 64 tasks, 8 processors: representative avionics/automotive workload. + let workload = synth_periodic_taskset(64, 8, 0.69); + group.throughput(Throughput::Elements(workload.threads.len() as u64)); + + group.bench_function(BenchmarkId::new("milp", 64), |b| { + b.iter(|| { + let result = solve_milp(black_box(&workload)).expect("feasible"); + black_box(result); + }); + }); + + group.bench_function(BenchmarkId::new("ffd", 64), |b| { + b.iter(|| { + let result = Allocator::ffd(black_box(&workload)); + black_box(result); + }); + }); + + group.bench_function(BenchmarkId::new("bfd", 64), |b| { + b.iter(|| { + let result = Allocator::bfd(black_box(&workload)); + black_box(result); + }); + }); + + let nsga_cfg = Nsga2Config { + population_size: 40, + generations: 30, + seed: 42, + ..Default::default() + }; + group.bench_function(BenchmarkId::new("nsga2", 64), |b| { + b.iter(|| { + let result = nsga2_optimize(black_box(&workload), black_box(&nsga_cfg)); + black_box(result); + }); + }); + + group.finish(); +} + +fn bench_solver_large(c: &mut Criterion) { + let mut group = c.benchmark_group("solver_large"); + // Large MILP runs are expensive; keep sample_size small to bound wall-time. + group + .sample_size(10) + .warm_up_time(Duration::from_secs(3)) + .measurement_time(Duration::from_secs(5)); + + // 256 tasks, 32 processors: stress / regression detection. + let workload = synth_periodic_taskset(256, 32, 0.69); + group.throughput(Throughput::Elements(workload.threads.len() as u64)); + + group.bench_function(BenchmarkId::new("milp", 256), |b| { + b.iter(|| { + let result = solve_milp(black_box(&workload)).expect("feasible"); + black_box(result); + }); + }); + + group.bench_function(BenchmarkId::new("ffd", 256), |b| { + b.iter(|| { + let result = Allocator::ffd(black_box(&workload)); + black_box(result); + }); + }); + + group.bench_function(BenchmarkId::new("bfd", 256), |b| { + b.iter(|| { + let result = Allocator::bfd(black_box(&workload)); + black_box(result); + }); + }); + + let nsga_cfg = Nsga2Config { + population_size: 50, + generations: 20, + seed: 42, + ..Default::default() + }; + group.bench_function(BenchmarkId::new("nsga2", 256), |b| { + b.iter(|| { + let result = nsga2_optimize(black_box(&workload), black_box(&nsga_cfg)); + black_box(result); + }); + }); + + group.finish(); +} + +fn bench_solver_worst_case(c: &mut Criterion) { + let mut group = c.benchmark_group("solver_worst_case"); + // Worst-case instances are slow under MILP; keep sample_size small. + group + .sample_size(10) + .warm_up_time(Duration::from_secs(3)) + .measurement_time(Duration::from_secs(5)); + + // 64 tasks, 8 processors, u ≈ 0.95, prime periods → many RMA + // priority-inversion checks. + let workload = synth_worst_case(64, 8); + group.throughput(Throughput::Elements(workload.threads.len() as u64)); + + group.bench_function(BenchmarkId::new("milp", "worst_64"), |b| { + b.iter(|| { + // Worst-case inputs may be infeasible — treat the Result as data. + let result = solve_milp(black_box(&workload)); + let _ = black_box(result); + }); + }); + + group.bench_function(BenchmarkId::new("ffd", "worst_64"), |b| { + b.iter(|| { + let result = Allocator::ffd(black_box(&workload)); + black_box(result); + }); + }); + + group.bench_function(BenchmarkId::new("bfd", "worst_64"), |b| { + b.iter(|| { + let result = Allocator::bfd(black_box(&workload)); + black_box(result); + }); + }); + + let nsga_cfg = Nsga2Config { + population_size: 40, + generations: 30, + seed: 42, + ..Default::default() + }; + group.bench_function(BenchmarkId::new("nsga2", "worst_64"), |b| { + b.iter(|| { + let result = nsga2_optimize(black_box(&workload), black_box(&nsga_cfg)); + black_box(result); + }); + }); + + group.finish(); +} + +criterion_group!( + benches, + bench_solver_small, + bench_solver_medium, + bench_solver_large, + bench_solver_worst_case, +); +criterion_main!(benches); diff --git a/supply-chain/config.toml b/supply-chain/config.toml index 5c936e4..6f9a9a3 100644 --- a/supply-chain/config.toml +++ b/supply-chain/config.toml @@ -603,3 +603,128 @@ criteria = "safe-to-deploy" [[exemptions.zmij]] version = "1.0.21" criteria = "safe-to-deploy" + +# ── criterion bench dependencies (safe-to-run, dev-only via benches/) ── +[[exemptions.anes]] +version = "0.1.6" +criteria = "safe-to-run" + +[[exemptions.anstyle]] +version = "1.0.14" +criteria = "safe-to-run" + +[[exemptions.bumpalo]] +version = "3.20.2" +criteria = "safe-to-run" + +[[exemptions.cast]] +version = "0.3.0" +criteria = "safe-to-run" + +[[exemptions.ciborium]] +version = "0.2.2" +criteria = "safe-to-run" + +[[exemptions.ciborium-io]] +version = "0.2.2" +criteria = "safe-to-run" + +[[exemptions.ciborium-ll]] +version = "0.2.2" +criteria = "safe-to-run" + +[[exemptions.clap]] +version = "4.6.1" +criteria = "safe-to-run" + +[[exemptions.clap_builder]] +version = "4.6.0" +criteria = "safe-to-run" + +[[exemptions.clap_lex]] +version = "1.1.0" +criteria = "safe-to-run" + +[[exemptions.criterion]] +version = "0.5.1" +criteria = "safe-to-run" + +[[exemptions.criterion-plot]] +version = "0.5.0" +criteria = "safe-to-run" + +[[exemptions.crunchy]] +version = "0.2.4" +criteria = "safe-to-run" + +[[exemptions.half]] +version = "2.7.1" +criteria = "safe-to-run" + +[[exemptions.hermit-abi]] +version = "0.5.2" +criteria = "safe-to-run" + +[[exemptions.is-terminal]] +version = "0.4.17" +criteria = "safe-to-run" + +[[exemptions.itertools]] +version = "0.10.5" +criteria = "safe-to-run" + +[[exemptions.js-sys]] +version = "0.3.95" +criteria = "safe-to-run" + +[[exemptions.oorandom]] +version = "11.1.5" +criteria = "safe-to-run" + +[[exemptions.plotters]] +version = "0.3.7" +criteria = "safe-to-run" + +[[exemptions.plotters-backend]] +version = "0.3.7" +criteria = "safe-to-run" + +[[exemptions.plotters-svg]] +version = "0.3.7" +criteria = "safe-to-run" + +[[exemptions.same-file]] +version = "1.0.6" +criteria = "safe-to-run" + +[[exemptions.tinytemplate]] +version = "1.2.1" +criteria = "safe-to-run" + +[[exemptions.walkdir]] +version = "2.5.0" +criteria = "safe-to-run" + +[[exemptions.wasm-bindgen]] +version = "0.2.118" +criteria = "safe-to-run" + +[[exemptions.wasm-bindgen-macro]] +version = "0.2.118" +criteria = "safe-to-run" + +[[exemptions.wasm-bindgen-macro-support]] +version = "0.2.118" +criteria = "safe-to-run" + +[[exemptions.wasm-bindgen-shared]] +version = "0.2.118" +criteria = "safe-to-run" + +[[exemptions.web-sys]] +version = "0.3.95" +criteria = "safe-to-run" + +[[exemptions.winapi-util]] +version = "0.1.11" +criteria = "safe-to-run"