Detect unreleased Behavior Annex shared-data locks 馃 - #3246
Merged
Merged
Conversation
Exercise shared-data lock lifetimes through embedded AADL Behavior Annex models, including branches, unordered action sets, loops, wildcard operations, inherited and grouped accesses, and transition joins and cycles. Require precise diagnostics on complete-state entry with a possible held lock while accepting balanced and unreachable paths. Established violations are errors; findings that can be false positives because of runtime assumptions must be informational, including correlated conditions within and across transitions. The pre-fix regression demonstrates missing diagnostics without unrelated AADL validation failures.
Track required data-access locks through sequences, unordered action sets, branches, loops, and the behavior-state graph. Preserve inherited and nested feature-group access paths and expand wildcard operations over the visible required resources. Report complete-state entry with a held resource. Use errors for paths established without runtime assumptions and info messages for potential false positives from conservative branch or loop analysis. Reuse static Boolean evaluation to exclude impossible paths, document the analysis boundary, and add characterization baselines for the regression models. Validation: nine focused regression tests, 199 BA tests, and the clean root reactor with 1,660 tests passed. Fixes #3189
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
2 participants
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.
Fixes #3189
The Behavior Annex validator previously accepted paths that entered a complete state with shared data still locked. Add resource-lifetime analysis across sequences, unordered action sets, branches, loops, transition joins and cycles, and wildcard operations. Preserve distinct access paths through inherited, nested, and inverted feature groups.
Established violations produce errors. Findings that depend on conservative assumptions about runtime conditions produce info messages, so potential false positives do not invalidate balanced models.
Issue3189Testand its external AADL model project cover balanced and unreleased paths, grouped resources, unreachable code, and diagnostic severity for correlated conditions. The regression commit precedes the production fix.Validation
Targets
master; no dependencies on unmerged PRs. Runtime-value correlations and instance-level aliases between accesses remain outside this declarative analysis; its conservative runtime findings are informational.