design: Track E research — migration / design-space oracle (#150)#153
Merged
design: Track E research — migration / design-space oracle (#150)#153
Conversation
Survey + design-space exploration for issue #150: - Existing component-placement tooling (10-tool comparison table) - Multi-objective allocation literature - LLM + constraint-solver patterns - MCP tool design for verification oracles - AUTOSAR's contract layer mapped to spar hooks - spar's design space across 6 axes - Roadmap proposal for v0.8.0/0.9.0 No production code. Refines acceptance criteria for #150. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Codecov Report✅ All modified and coverable lines are covered by tests. 📢 Thoughts on this report? Let us know! |
This was referenced Apr 25, 2026
avrabe
added a commit
that referenced
this pull request
Apr 25, 2026
…I integration (#154) Closes the v0.7.0 Track A milestone: - COMPLIANCE.md "In progress / v0.7.0" expanded into a full narrative covering all four Track A commits (foundation #145, hierarchical RTA #147, Lean convergence #148, this close-out), the Track B variant- contract foundation (#144), v0.7.x infrastructure landings (#141-143, #151), and v0.8.0 planning anchors (Track D #149/#152, Track E #150/#153). - Updated header date to 2026-04-25 and crate count from "16 crates, 1200+ tests" to "17 crates, 1900+ tests" reflecting the test growth through Track A and the v0.7.x infrastructure additions. - New CLI integration test crates/spar-cli/tests/track_a_close_out.rs exercises the full parse → instance → analyze pipeline on a model using the Spar_Timing::ISR_* property surface plus a sporadic handler thread. The unit + fixture tests in spar-analysis cover the algorithm at the analysis-crate level; this test guards the property surface flowing through the CLI binary end-to-end. Out-of-scope items explicitly recorded: PIP/PCP blocking deferred to v0.7.1, multi-processor ISR migration deferred, cache-aware interference inflation deferred to v1.0+. Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
avrabe
added a commit
that referenced
this pull request
Apr 25, 2026
…lpers (Track E commit 1/8) Foundation for v0.8.0 Track E (frozen-platform / mobile-application split + hypothetical-rebinding oracle, #150). Spar_Migration::{Frozen, Mobile, Allowed_Targets, Pinned_Reason} provide the AADL vocabulary for declaring which items are platform (immutable for hypothetical rebinding) vs. which are application (eligible for movement). Per the research in PR #153 §6.1. Helper functions is_frozen() / is_mobile() expose the boolean state to downstream analyses without requiring a salsa query yet — the per-instance cache lands when the hypothetical-binding overlay needs it (Track E commit 2). Per §6.2's tradeoff analysis: minimal surface now, expand on demand. No CLI surface, no MCP, no solver extension in this commit — those are Track E commits 3-5. New requirements: REQ-MIGRATION-{001,002,003}. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
avrabe
added a commit
that referenced
this pull request
Apr 25, 2026
…lpers (Track E commit 1/8) (#156) Foundation for v0.8.0 Track E (frozen-platform / mobile-application split + hypothetical-rebinding oracle, #150). Spar_Migration::{Frozen, Mobile, Allowed_Targets, Pinned_Reason} provide the AADL vocabulary for declaring which items are platform (immutable for hypothetical rebinding) vs. which are application (eligible for movement). Per the research in PR #153 §6.1. Helper functions is_frozen() / is_mobile() expose the boolean state to downstream analyses without requiring a salsa query yet — the per-instance cache lands when the hypothetical-binding overlay needs it (Track E commit 2). Per §6.2's tradeoff analysis: minimal surface now, expand on demand. No CLI surface, no MCP, no solver extension in this commit — those are Track E commits 3-5. New requirements: REQ-MIGRATION-{001,002,003}. Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
avrabe
added a commit
that referenced
this pull request
Apr 25, 2026
* design: Track F — SysML v2 / KerML community engagement strategy Research-backed strategy doc for community engagement in the OMG SysML v2 / KerML ecosystem. Synthesizes two parallel research streams: (a) Audit of spar-sysml2: 7,167 LOC, zero TODOs/stubs, 59+ tests, 8 fully bidirectional concepts including the entire requirements roundtrip (satisfy/verify/refine/allocate/derive). Production-grade, not a stub. (b) Verified community landscape: KerML 1.0 + SysML v2 1.0 final adoption Jun 2025; OMG `Systems-Modeling/SysML-v2-AADL-Release` repo skeletal at 3 commits with named maintainers from Galois, CMU/SEI, Ellidiss; SMC free for OMG members; OMG fees re-confirmation needed (page auth-locked); Eclipse SysON via Obeo+CEA on 8-week cadence; Rust ecosystem positioning (syster-base by Microsoft is adjacent, not duplicate, since spar is the AADL side). Action plan: 30/60/90-day sequence anchored on the AADL-Release repo + named-maintainer outreach + Google Group + OMG issue tracker. Investment ladder with explicit Phase 1 ($2,150 Trial / $550 University) and Phase 2 ($3,000 Influencing Member) trigger criteria. Application text drafted for the sysml-v2-release Google Group (long + short versions). Risks + unknowns explicitly flagged including the auth-locked OMG fee page. No production code changes. Mirrors the Track D #152 / Track E #153 research-doc-first pattern. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs: amend Track F with deeper syster findings + cooperation policy Direct GitHub inspection of jade-codes/syster repos surfaced facts the initial research missed: - syster-base and syster-lsp have NO LICENSE files (only umbrella + syster-codegen + syster-cli are MIT). Default copyright is "all rights reserved" — code-level consumption is legally blocked until this is clarified. - Last commits Feb 14-24, 2026 (~2 months stale). Mostly repo-restructure + submodule shuffling, not feature work. Momentum cooled. - Architectural breadth is larger than initial Track F captured: full ecosystem (parser → codegen → CLI → Python wrapper → LSP → VS Code extensions → diagram core + UI). - syster-codegen (MIT) generates the parser from KEBNF grammar files. This is a real architectural asymmetry vs. spar-sysml2's hand-rolled parser — auto-conformance to future spec revisions for free. Not a v0.8.0 candidate; tracked as v0.9.0+ consideration. Refines §3 (Rust ecosystem) with license-status column flagging unlicensed subcrates. Adds §3.1 corrected picture, §3.2 refined positioning + cooperation policy, §3.3 KEBNF-codegen tracking note, §4.2 minimum-viable engagement criteria for syster (one license-clarification issue then stop until it's resolved). The cooperation policy reflects the user's stated preference: spar's SysML v2 work is a hobby track for an engineer whose day-job is already heavy on talking + doing. Cooperation must be a strategic asset, not a courtesy. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
avrabe
added a commit
that referenced
this pull request
Apr 26, 2026
Adds BindingOverlay — a HIR-level immutable map from component idx to hypothetical target processor idx — that lets any analysis run "as if" the binding were rebound without mutating the SystemInstance. The overlay validates against Spar_Migration::Frozen and Allowed_Targets from commit 1, returning structured FrozenViolation / AllowedTargetsViolation diagnostics. Empty overlay is the no-op identity (non-regression). This is the technical foundation for spar moves verify (commit 3) and spar moves enumerate (commit 4-5). No CLI surface, no solver wiring, no MCP in this commit. Per Track E research §6.4 (#153, merged). New requirement: REQ-MIGRATION-004. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
avrabe
added a commit
that referenced
this pull request
Apr 26, 2026
Adds BindingOverlay — a HIR-level immutable map from component idx to hypothetical target processor idx — that lets any analysis run "as if" the binding were rebound without mutating the SystemInstance. The overlay validates against Spar_Migration::Frozen and Allowed_Targets from commit 1, returning structured FrozenViolation / AllowedTargetsViolation diagnostics. Empty overlay is the no-op identity (non-regression). This is the technical foundation for spar moves verify (commit 3) and spar moves enumerate (commit 4-5). No CLI surface, no solver wiring, no MCP in this commit. Per Track E research §6.4 (#153, merged). New requirement: REQ-MIGRATION-004. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
avrabe
added a commit
that referenced
this pull request
Apr 26, 2026
Adds BindingOverlay — a HIR-level immutable map from component idx to hypothetical target processor idx — that lets any analysis run "as if" the binding were rebound without mutating the SystemInstance. The overlay validates against Spar_Migration::Frozen and Allowed_Targets from commit 1, returning structured FrozenViolation / AllowedTargetsViolation diagnostics. Empty overlay is the no-op identity (non-regression). This is the technical foundation for spar moves verify (commit 3) and spar moves enumerate (commit 4-5). No CLI surface, no solver wiring, no MCP in this commit. Per Track E research §6.4 (#153, merged). New requirement: REQ-MIGRATION-004. Co-authored-by: Claude Opus 4.7 (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
Research + design-space exploration document for issue #150 (Track E:
frozen-platform/mobile-application split + hypothetical-rebinding oracle).
Capella, AUTOSAR Classic + Adaptive, SCADE Architect, ROS 2, etc.) with
GOOD / MISSING analysis for spar.
including per-paper applicability scoring.
Sledgehammer, ConstraintLLM, LLM-as-architect).
Schema for
spar.verify_moveandspar.enumerate_moves.AADL and spar's hooks.
solver extension, MCP surface, rivet-variant integration.
(~8.5 weeks LLM/MCP).
Recommendations (TL;DR)
Spar_Migration::{Frozen, Mobile, Allowed_Targets, Pinned_Reason, Migration_Cost}.Allowed_Targets;reuse existing analysis passes — no MILP for v0.8.0.
spar moves verify+spar moves enumerate) ships in v0.8.0.MCP surface (LLM-facing) deliberately deferred to v0.9.0.
verify_move+enumerate_movesonly. The
applyverb is CLI-exclusive. The LLM never crosses into thecertified path.
EcucPostBuildVariantsanalogue.
Scope
literature.
Test plan
Closes part of: #150
Depends on: #144 (rivet variants v1)
🤖 Generated with Claude Code