Experiment formal verification scheduling results 01 - kmosoti/FabricO11y GitHub Wiki
Bounded verification scheduling results 01
Two local experiments compared identical seven-check inventories under bounded Rust orchestration. They do not qualify a deployment or complete alpha acceptance, which the owner paused. The underlying delivery/query/rate Python oracles remain independent and unchanged. This is not a full-CI or GPU speed comparison.
Workload and boundary
The selected registered fast IDs were delivery-oracle, query-oracle, workload-rate-oracle, soak-decision-rule, telemetry-contract, telemetry-cli and ui-palette. Every original command ran once per measured mode/repetition, in isolated receipt and scratch directories. The Rust pool uses bounded workers, an atomic FIFO cursor and completion messages. Weighted dispatch sorts the same independent jobs by frozen prior measurements and canonical ID ties.
Host: Intel i7-10750H, six physical cores/twelve threads, approximately 31 GiB RAM. All jobs used the mounted FabricO11y DATA drive and original enforced resource launcher with an exclusive engineering lease. Commands used pinned Rust 1.99.0 and locked dependencies. No concurrent local heavy jobs ran.
The per-mode clock includes worker dispatch, child execution and receipt validation. Registry/source preparation and dispatch-order construction precede that clock. Compilation is separately recorded. These are warm/reused-cache host observations, not cold-start whole-tool timings. Individual check durations are wall time, not CPU time; per-mode CPU and total memory were not measured.
FIFO experiment
Source: beb00f653bf39542a8ec89d98ec383f9f8e1c58d.
Command through python3 tools/resource_group.py --:
cargo run --release --locked -p xtask --example verification_concurrency -- /run/media/kmosoti/data/FabricO11y/results/verification-concurrency-01/native-paired-01
Actual exit 0, whole stop confirmed at 2026-10-18 02:20:06.360727 UTC. One warmup per mode and seven alternating pairs gave median serial 4185 ms and two-worker FIFO 2908 ms. Median per-pair reduction was 30.2638%; ratio-of-medians reduction was 30.5137%. These are different summaries of the same paired data.
The integrator independently rehashed 116 receipts/logs: 114 successful original commands and two actual injected exit-7 failures. Normalized command/source/ profile/result inventories matched. Observed worker peaks were one and two. Four copied-evidence defects were rejected. Whole command cost was 62.903 s and 237.1 MiB reported peak, including 5.17 s compilation; this is not per-mode cost.
Raw summary: results/verification-concurrency-01/native-paired-01/summary.json,
SHA-256 3aa8cb54a5ac0828cf326e1c65fef3142880e3b523c37f1cdfc59134c8f594bb.
Measured bottleneck and prospective follow-up
The serial medians were telemetry-cli 2241 ms, workload-rate-oracle 887, query-oracle 322, delivery-oracle 310, telemetry-contract 142, soak-decision-rule 87 and ui-palette 42. The longest job started late in FIFO. The follow-up protocol was committed before its implementation or measurement. For these frozen additive weights, exhaustive enumeration of all 128 assignments confirms the two-worker model minimum 2241 ms: run telemetry-cli alone and the other six on the other worker. This arithmetic excludes real launch, admission, contention and receipt overhead; it is not a measured universal lower bound.
Weighted experiment
Source: 8881e2e543d2268dfb7b0107ed2e7e591e145262. Actual commands through the original launcher exited 0 and stopped:
cargo test --locked -p xtask --example verification_concurrency
cargo clippy --locked -p xtask --example verification_concurrency -- -D warnings
cargo fmt --all --check
cargo run --release --locked -p xtask --example verification_concurrency -- /run/media/kmosoti/data/FabricO11y/results/verification-concurrency-01/native-triples-01
Three tests exercised all 5040 ID permutations, exact/positive weights and tie ordering, independent two-way partition enumeration, and overflow/size refusal. One warmup per mode and seven deterministically rotated triples then measured:
| Mode | Median measured execution wall time |
|---|---|
| Serial | 4207 ms |
| Two-worker FIFO | 2925 ms |
| Two-worker weighted | 2319 ms |
Median per-triple reduction versus FIFO was 20.4452%; ratio-of-medians reduction was 20.7179%. The reported paired reduction versus serial was 44.7825%. Use the raw pairs rather than treating these summaries as identical statistics.
All measured semantic inventories matched. The integrator independently rehashed 174 receipts/logs, including three actual injected exit-7 failures. Twelve copied-evidence controls were rejected, four for each mode. Observed worker peaks remained one/two/two. Final actual whole stop: 2026-10-18 02:38:00.447973 UTC.
Raw summary: results/verification-concurrency-01/native-triples-01/summary.json,
SHA-256 8d81aacea9de7da9fbb518b8e0c6b6d45941be2b152d382187e662c061777b03.
Archived executable SHA-256:
5ee93d37ec08e2a3c3e0e086a3959a7c5a9a69448031998db9941cc30e31019f.
Failures, decision and limits
The first weighted formatting attempt at source
15b84a2938d83ed22b5743414bad90f75ca3b72d exited 1 on an incomplete local
binding. No tests or weighted measurements ran on that source. Its diagnostic
and source remain preserved. The one-line correction and fresh formatting
attempt preceded the final clean 8881 experiment; no failed result was relabeled.
The weighted rule exceeds the registered 5% measured improvement threshold on this finite workload while retaining all checks and negative controls. It is a candidate for bounded lightweight verification scheduling. Production adoption and required CI evidence remain separate; this report is not their completion. The separate two-runner CI pilot compares a much larger critical path and must retain its own complete same-head baseline, cache/setup facts and failed runs.
The RTX 3060 Laptop GPU was available but not used. No current registered check was converted to GPU execution and no GPU speedup is claimed. A real two-hour soak still requires its full elapsed exposure. The pure model and successful finite tests do not establish arbitrary-program correctness or certification.
Reproduction and evidence joins
The literal environment-prefixed launcher commands, full reservation and compiler hashes are in the DATA plans below. Both drivers retained default 16 GiB memory high, 20 GiB maximum, zero swap and 1800-second deadline, with a fresh whole-DATA 95 GB census and 2 GiB reservation before each run.
- FIFO plan:
results/verification-concurrency-01/paired-plan-01.json; original wrapper:results/verification-concurrency-01/native-paired-01.json. - Weighted checks and triple plan:
results/verification-weighted-controls-01/plan-01.json; all four stopped wrappers:results/verification-weighted-controls-01/actual-results-01.json. - Independent evidence audit:
results/verification-weighted-controls-01/native-triples-actual-result-01.json. It records all 174 real receipt/log hashes and distinguishes the executed copied-control assertions from the integrator's artifact inspection. - Failed formatting source and successful correction:
results/verification-weighted-format-01/format-actual-result-{01,02}.json.
The weighted whole command reported 78.964 s and 125.1 MiB peak with zero swap,
including its 2.07-second release compilation. This does not measure separate
mode-specific memory use. Both experiment executables were copied to their
respective output artifacts/ directory and hashed before a later build could
replace the shared Cargo target.
The independently running hosted two-runner pilot is still pending at this report's publication; it supplies no hosted speedup or adoption result here. Its Rust collector performs bounded byte-preserving artifact collection; the unchanged Python validator owns stale/modified-evidence refusal and final completeness.
The public prototype history preserves the pinned FIFO protocol and weighted protocol. The prototype branch is an experiment artifact; it has no production adoption PR.
Full-profile finite integration, 18 October 2026
This later check belongs to clean implementation source 7fc4723, rather than the earlier prototype revisions. The same full 20-check fast registry ran once serially and once with the explicit two-worker light cohort. Each profile exited 0, followed by separate Rust and unchanged Python complete-receipt validation, each exiting 0 with confirmed whole-cgroup stop. The final positive validator stopped at 03:32:12.997122 UTC. All 20 IDs, literal command vectors, property IDs and contract fields match, and every output log hash was inspected.
The original serial receipts were copied into four fresh owned directories. Modified log, missing receipt, stale commit and running marker each produced actual exit 1 in both validators for the named defect. The real public cargo xtask mutants --light-workers 2 command exited 2 at its flag guard, before run_all. The last control stopped at 03:34:59.775300 UTC. Actual negative exits remain recorded as 1/2; all 80 canonical source files remained unchanged.
The following are individual receipt durations in milliseconds, not a controlled end-to-end speed comparison:
| Check | Serial ms | Two light workers ms |
|---|---|---|
| check | 11270 | 195 |
| clippy | 7629 | 245 |
| core-purity | 254 | 255 |
| counterexamples | 123 | 119 |
| delivery-oracle | 310 | 309 |
| fmt | 534 | 550 |
| fuzz-corpus | 11400 | 166 |
| kernel-properties | 23309 | 19724 |
| layers | 306 | 290 |
| network-simulation | 12701 | 2035 |
| package-contracts | 4018 | 3971 |
| qualification-runner | 4261 | 4172 |
| query-oracle | 330 | 324 |
| soak-decision-rule | 89 | 92 |
| telemetry-cli | 2276 | 2295 |
| telemetry-contract | 144 | 135 |
| test | 335800 | 278375 |
| ui-palette | 44 | 45 |
| wasm-check | 11762 | 127 |
| workload-rate-oracle | 881 | 913 |
Serial workspace tests alone took 335800 ms out of 427441 ms summed check time (78.56%). The seven light checks summed to 4074 ms, only 0.953% of that serial total. Their prototype improvement therefore does not imply a comparable full-profile improvement.
Outer elapsed time was 429.523 s serially and 312.973 s for the later opt-in run; cgroup memory peaks were 11261132800 and 413929472 bytes respectively. These differences are confounded by serial-first compilation, cache and runtime conditions and are not attributed to scheduling. This is one integration pair, without alternating order or end-to-end speedup statistics. Both retained zero swap, default 16/20 GiB high/max and the 1800-second limit, with whole-DATA admission plus a 10 GiB logical reservation covering the existing sparse-file test.
Exact DATA records: results/verification-dispatch-integration-01/{plan-01.json,actual-results-01.json,actual-control-plan-01.json,actual-control-results-01.json,actual-control-diagnostics-01.json,paired-duration-cost-model-01.json}. Terminal integration-terminal-01.json SHA256 49f9229c043c7a7dff39dac1490615ece686653377fab14695059c72cd4d6d0c; board readback. The caller adoption PR #80 has separate required hosted checks and is not reported merged here. Alpha acceptance remains owner-paused; this is engineering evidence, not qualification.