feat(solver): deployment solver foundations — topology, allocation, protocol library#74
Merged
feat(solver): deployment solver foundations — topology, allocation, protocol library#74
Conversation
Cross-domain research across SDV, Industry 4.0, aerospace, drones, medical, IIoT, and edge computing. Patent landscape analysis. Solver technology survey (SMT, CP-SAT, MILP, ASP, NSGA-II). Competitive positioning against OSATE, ArcheOpterix, DeSyDe, PREEvision. Key finding: no tool takes AADL and produces provably globally optimal deployments. The patent landscape is thin (1990s heuristics). spar is uniquely positioned with rowan+salsa+WASM+rivet. Also includes AGENTS.md and CLAUDE.md from rivet init --agents. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
14 new artifacts covering topology graph, virtual bus library, constraint formulation, NDS-layered hierarchical solving, optimality certificates, Pareto front computation, source rewriting, ASIL/DAL decomposition, security zone validation, and 4 research finding records from the cross-domain landscape analysis. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Move RESEARCH-* entries from requirements.yaml to research/findings.yaml with proper research artifact types (market-finding, competitive-analysis, patent-finding, technology-evaluation, academic-reference). Add research schema to rivet.yaml. 22 research artifacts covering 6 market findings, 4 competitive analyses, 3 patent findings, 4 technology evaluations, and 4 academic references. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…tagging Add REF-NDS-LAYERS academic reference for hierarchical deployment solving inspired by NDS navigation tile layers. Add 6 architecture decisions (ARCH-SOLVER-001 through 006) covering NDS-layered solving, topology graph, virtual bus library, bin-packing, source rewriting, and dual solver strategy. Re-tag REQ-SOLVER-001/002/003/007 as v030 scope since topology graph, virtual bus library, constraint formulation, and source rewriting are v0.3.0 work. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…UCAs, scenarios, requirements Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
9 tasks: spar-solver crate, topology graph, constraint extraction, FFD/BFD bin-packing, virtual bus library (13 protocols), source rewriting via rowan, spar allocate CLI, impact preview, integration. Addresses STPA requirements: SOLVER-REQ-020 (no silent defaults), SOLVER-REQ-023 (deterministic), SOLVER-REQ-016 (parse-after-rewrite). Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
New crate with modules for topology graph extraction, constraint formulation, and bin-packing allocation. No implementation yet — this is the foundation for the NDS-layered deployment solver. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Protocol catalog covering automotive (DDS, SOME/IP, CAN, CAN FD, FlexRay), aerospace (AFDX, ARINC 429, SpaceWire), industrial (PROFINET, EtherCAT), embedded (MAVLink), and general (Ethernet, shared memory). Each protocol has latency, bandwidth, payload, and security properties. Satisfies: REQ-SOLVER-002 Implements: ARCH-SOLVER-003 Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Extract timing constraints (Period, WCET, Deadline, Priority, binding) for threads and resource constraints (Memory_Size) for processors. Warns on missing critical properties (SOLVER-REQ-020). Deterministic output ordering (SOLVER-REQ-023). Satisfies: REQ-SOLVER-003 Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
First-Fit Decreasing and Best-Fit Decreasing allocation of threads to processors based on utilization. Respects existing bindings. Deterministic output (SOLVER-REQ-023). Warns on missing properties. Implements: ARCH-SOLVER-004 Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Extract petgraph DiGraph of hardware topology (processors, buses, memories) from SystemInstance. Nodes carry capacity properties. Edges represent bus access connectivity. Satisfies: REQ-SOLVER-001 Implements: ARCH-SOLVER-002 Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
# Conflicts: # crates/spar-solver/Cargo.toml # crates/spar-solver/src/lib.rs # crates/spar-solver/src/tests.rs
# Conflicts: # crates/spar-solver/Cargo.toml # crates/spar-solver/src/constraints.rs # crates/spar-solver/src/lib.rs # crates/spar-solver/src/tests.rs
# Conflicts: # crates/spar-solver/Cargo.toml # crates/spar-solver/src/allocate.rs # crates/spar-solver/src/constraints.rs # crates/spar-solver/src/lib.rs # crates/spar-solver/src/tests.rs # crates/spar-solver/src/topology.rs
Codecov Report❌ Patch coverage is 📢 Thoughts on this report? Let us know! |
Add crates/spar-cli/src/refactor.rs with apply_binding_edit() that rewrites AADL source files to insert or update binding properties in component implementation declarations. Uses rowan CST for precise offset computation and validates output via re-parse (SOLVER-REQ-016). Supports three edit paths: - Insert property into existing properties section - Update an already-existing property value - Create a new properties section when none exists Six unit tests cover all paths plus error handling. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Add `spar allocate` CLI command that:
- Instantiates a root system and extracts ModelConstraints
- Runs FFD or BFD bin-packing allocation (--strategy ffd|bfd)
- Outputs results as text table or JSON (--format text|json)
- Optionally applies bindings to source files (--apply) using the
refactor module for AADL source rewriting
Usage:
spar allocate --root Pkg::Type.Impl [--strategy ffd|bfd] \
[--format text|json] [--apply] <files...>
Also adds spar-solver as a dependency of spar-cli and registers the
allocate command in the CLI dispatch and usage help.
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
AllocationResult.impact() computes per-processor RMA utilization bounds, identifies overloaded processors, and checks deadline violations. CLI shows impact summary after allocation with SCHEDULABLE/NOT SCHEDULABLE verdict. Implements: SOLVER-REQ-005 (re-check after allocation) Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Version: 0.2.4 → 0.3.0 Implemented requirements: - REQ-RTA-001, REQ-BUS-001, REQ-MEMBUD-001, REQ-WEIGHTPOWER-001 (PR #70) - REQ-PARSER-001, REQ-VERIFY-001, REQ-DIFF-001, REQ-DIFF-002 (PR #73) - REQ-SOLVER-001, REQ-SOLVER-002, REQ-SOLVER-003, REQ-SOLVER-007 (PR #74) Implemented architecture decisions: - ARCH-ANALYSIS-001, ARCH-DIFF-001, ARCH-VERIFY-001 (PR #73) - ARCH-SOLVER-002, ARCH-SOLVER-003, ARCH-SOLVER-004, ARCH-SOLVER-005 (PR #74) Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…erage Add 8 new tests for the solver crate: - constraints_extract_thread_timing: Period, WCET, Deadline → correct ps values - constraints_missing_wcet_warns: SOLVER-REQ-020 missing WCET warning - constraints_missing_period_warns: missing Period warning - constraints_deadline_defaults_to_period: deadline defaults to period - constraints_extract_processor: Memory_Size → correct byte value - constraints_extract_binding: Actual_Processor_Binding → current_binding - constraints_sorted_deterministically: SOLVER-REQ-023 alphabetical ordering - impact_detects_deadline_violation: constrained deadline + RMA bound exceeded Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Add ceil_div_matches_lean_definition test that exhaustively checks equivalence between the Lean-generated `(a + b - 1) / b` and the Rust stdlib `a.div_ceil(b)` for 100k input pairs. Add compute_response_time_matches_lean_spec test with manually-derived fixed-point results. Document the codegen drift at file top. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Add 9 tests exercising all 8 AADL data rate unit suffixes (Gbitsps, Mbitsps, Kbitsps, bitsps, GBytesps, MBytesps, KBytesps, Bytesps) plus plain numeric fallback for parse_data_rate. Previously only Mbitsps and KBytesps had indirect coverage through topology tests. Make parse_data_rate pub(crate) so unit tests can call it directly. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Add 4 tests verifying the salsa-backed ServerState: - server_state_scan_and_update: update_file stores content, get_source retrieves it, get_item_tree parses and lowers successfully - server_state_update_invalidates: updating a file twice returns the second content; item tree reflects new declarations (salsa cache invalidation works) - server_state_remove_file: after remove_file, both get_source and get_item_tree return None - server_state_rebuild_scope: two files from different packages both contribute to the GlobalScope; cross-file type resolution works Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Add proptest dependency and 16 property-based tests across two crates: spar-parser (5 tests via crates/spar-parser/tests/proptest_parser.rs): - No panics on arbitrary input (ASCII and Unicode) - Lossless roundtrip: syntax_node.text() == original source - Valid AADL package templates parse without errors - Valid AADL extends templates parse without errors spar-cli assertion engine (11 tests inline in lexer.rs and parser.rs): - Lexer never panics on arbitrary input (ASCII and Unicode) - Lexer roundtrip: concatenated token texts == original input - Parser never panics on arbitrary input (ASCII and Unicode) - Valid where/all/has expressions parse correctly - Valid where/any/has expressions parse correctly - Valid where/count expressions parse correctly - Valid analysis/diagnostics expressions parse correctly - Valid boolean combinator (and/or/not) expressions parse correctly The proptests immediately found and fixed two UTF-8 bugs: - AADL lexer: bump() advanced one byte on unknown characters, causing panic on multi-byte UTF-8 input (e.g., "𑵠"). Fixed with bump_char(). - Assertion lexer: same single-byte advance bug on non-ASCII error tokens. Fixed by advancing a full UTF-8 character via chars().next(). Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…ound Coverage gaps fixed: 1. diff compare_structure: 8 structural comparison tests 2. feature_group_check: registered (was dead code), 3 pre-existing tests ignored 3. Impact deadline violation: test now triggers the constrained-deadline path 4. constraints.rs: 7 direct unit tests (SOLVER-REQ-020, SOLVER-REQ-023) 5. register_all guard: updated 22 → 27 6. proptest: 16 property tests, found+fixed 2 UTF-8 panics in lexers 7. scheduling_verified: Lean codegen equivalence test (100K input pairs) 8. LSP salsa: 4 integration tests (update, invalidate, remove, cross-file scope) 9. topology parse_data_rate: all 8 unit suffixes + plain numeric tested Bugs found and fixed by proptest: - AADL lexer: bump() advanced 1 byte on multi-byte UTF-8 → panic - Assertion lexer: same bug Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…v_ceil in Lean equivalence test Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
- cargo-vet: initialized supply-chain/ dir (136 crates exempted), CI now hard-fails on unaudited deps (was continue-on-error: true) - SLSA: GitHub Artifact Attestation on all release assets via gh attestation create (id-token + attestations permissions) - SBOM: CycloneDX JSON generated via cargo-cyclonedx, included in release assets - Release: use env vars for VERSION (avoid injection per Actions security best practices) Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Scripts to validate spar against OSATE 2.18.0 as reference: - download-osate.sh: retry-resilient download with resume - ease-scripts/generate_references.py: EASE/Py4J script for OSATE - compare.py: structural comparison (components, connections, features) - Reference data gitignored (generated per-machine) Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
New
spar-solvercrate, protocol library, source rewriting,spar allocateCLI, and impact preview — the complete v0.3.0 deployment solver foundation.New crate:
spar-solvertopology.rs): petgraph DiGraph from AADL instance — processors, buses, memories as nodes with capacity propertiesconstraints.rs): timing (Period, WCET, Deadline, Priority) and resource (Memory_Size) constraints from properties. Warns on missing critical properties (SOLVER-REQ-020)allocate.rs): First-Fit/Best-Fit Decreasing allocation with utilization checking. Respects existing bindings. Deterministic (SOLVER-REQ-023)allocate.rs): Per-processor RMA utilization bounds, overload detection, deadline violation checkingProtocol library (
spar-transform)Source rewriting (
spar-cli)refactor.rs: Insert/update binding properties via rowan CST. Parse-after-rewrite validation (SOLVER-REQ-016)spar allocate: CLI command with--strategy ffd|bfd,--format text|json,--applyRivet traceability
Test plan
🤖 Generated with Claude Code