Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Generalize pairwise race detection #529

Merged
merged 23 commits into from
Jan 20, 2022
Merged

Generalize pairwise race detection #529

merged 23 commits into from
Jan 20, 2022

Conversation

sim642
Copy link
Member

@sim642 sim642 commented Jan 12, 2022 •
edited
Loading

Closes #526.
This PR is currently opened on top of #518.

After hours of thinking I managed to find a way to find a way to do this in a satisfactory way. The trick was to use the combined access (A) module directly from the activated analyses, instead of accessing it through the outermost Spec. Achieving this required splitting parts of MCP into other modules (MCPRegistry and MCPAccess) to avoid circular dependencies.
One last circular dependency is broken by having the access analysis query PartAccess (which is now only answered by MCP, which uses the access functions of activated analyses) return the result as Obj.t. The only reason for that is to avoid mentioning MCPAccess in Queries (which is required by MCP again).

TODO

  • Comment some parts.
  • Clean up code.
  • Make race output readable (by omitting useless units from analyses that don't supply access information).

@sim642 sim642 added cleanup Refactoring, clean-up feature type-safety Type-safety improvements labels Jan 12, 2022
@sim642 sim642 self-assigned this Jan 12, 2022
@sim642 sim642 linked an issue Jan 13, 2022 that may be closed by this pull request
Replace labeled string based access partitioning with a richer type-safe one #526
Closed
@sim642 sim642 added the pr-dependency Depends or builds on another PR, which should be merged before label Jan 16, 2022
@michael-schwarz michael-schwarz self-requested a review January 17, 2022 10:09
Base automatically changed from use_tids_for_races to master January 18, 2022 13:08
@sim642 sim642 removed the pr-dependency Depends or builds on another PR, which should be merged before label Jan 18, 2022
@sim642 @michael-schwarz
Simplify MCPAccess.A.may_race
f2b1e5f 
Co-authored-by: Michael Schwarz <michael.schwarz93@gmail.com>
@sim642
Copy link
Member Author

sim642 commented Jan 20, 2022

@michael-schwarz Do you think it's ready to merge now?

@michael-schwarz michael-schwarz merged commit 27973d2 into master Jan 20, 2022
@michael-schwarz michael-schwarz deleted the part-access-refactor branch January 20, 2022 08:34
@sim642 sim642 added this to the v2.0.0 milestone Aug 12, 2022
sim642 added a commit to sim642/opam-repository that referenced this pull request Aug 18, 2022
@sim642
[new release] goblint (2.0.0)
6efdfdf 
CHANGES:

Goblint "lean" release after a lot of cleanup.

* Remove unmaintained analyses: OSEK, ARINC, shapes, containment, deadlocksByRaces (goblint/analyzer#460, goblint/analyzer#736, goblint/analyzer#812, goblint/analyzer#474).
* Add interactive analysis (goblint/analyzer#391).
* Add server mode (goblint/analyzer#522).
* Add Compilation Database support (goblint/analyzer#406, goblint/analyzer#448).
* Add floating point domain, unrolled array domain and improved struct domains (goblint/analyzer#734, goblint/analyzer#761, goblint/analyzer#577, goblint/analyzer#419).
* Add static loop unrolling and heap variable unrolling (goblint/analyzer#563, goblint/analyzer#722).
* Improve race detection with may-happen-in-parallel analysis (goblint/analyzer#529, goblint/analyzer#518, goblint/analyzer#595).
* Reimplement lockset and deadlock analyses (goblint/analyzer#659, goblint/analyzer#662, goblint/analyzer#650, goblint/analyzer#655).
* Add pthread extraction to Promela (goblint/analyzer#220).
* Add location spans to output (goblint/analyzer#428, goblint/analyzer#449).
* Improve race reporting (goblint/analyzer#550, goblint/analyzer#551).
* Improve dead code reporting (goblint/analyzer#94, goblint/analyzer#353, goblint/analyzer#785).
* Refactor warnings (goblint/analyzer#55, goblint/analyzer#783).
* Add JSON schema for configuration (goblint/analyzer#476, goblint/analyzer#499).
* Refactor option names (goblint/analyzer#28, goblint/analyzer#192, goblint/analyzer#516, goblint/analyzer#675).
* Add bash completion (goblint/analyzer#669).
* Add OCaml 4.13 and 4.14 support, remove OCaml 4.09 support (goblint/analyzer#503, goblint/analyzer#672).
@sim642 sim642 mentioned this pull request Aug 18, 2022
Merged
sim642 added a commit to sim642/opam-repository that referenced this pull request Aug 18, 2022
@sim642
[new release] goblint (2.0.0)
1c281d5 
CHANGES:

Goblint "lean" release after a lot of cleanup.

* Remove unmaintained analyses: OSEK, ARINC, shapes, containment, deadlocksByRaces (goblint/analyzer#460, goblint/analyzer#736, goblint/analyzer#812, goblint/analyzer#474).
* Add interactive analysis (goblint/analyzer#391).
* Add server mode (goblint/analyzer#522).
* Add Compilation Database support (goblint/analyzer#406, goblint/analyzer#448).
* Add floating point domain, unrolled array domain and improved struct domains (goblint/analyzer#734, goblint/analyzer#761, goblint/analyzer#577, goblint/analyzer#419).
* Add static loop unrolling and heap variable unrolling (goblint/analyzer#563, goblint/analyzer#722).
* Improve race detection with may-happen-in-parallel analysis (goblint/analyzer#529, goblint/analyzer#518, goblint/analyzer#595).
* Reimplement lockset and deadlock analyses (goblint/analyzer#659, goblint/analyzer#662, goblint/analyzer#650, goblint/analyzer#655).
* Add pthread extraction to Promela (goblint/analyzer#220).
* Add location spans to output (goblint/analyzer#428, goblint/analyzer#449).
* Improve race reporting (goblint/analyzer#550, goblint/analyzer#551).
* Improve dead code reporting (goblint/analyzer#94, goblint/analyzer#353, goblint/analyzer#785).
* Refactor warnings (goblint/analyzer#55, goblint/analyzer#783).
* Add JSON schema for configuration (goblint/analyzer#476, goblint/analyzer#499).
* Refactor option names (goblint/analyzer#28, goblint/analyzer#192, goblint/analyzer#516, goblint/analyzer#675).
* Add bash completion (goblint/analyzer#669).
* Add OCaml 4.13 and 4.14 support, remove OCaml 4.09 support (goblint/analyzer#503, goblint/analyzer#672).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@michael-schwarz michael-schwarz michael-schwarz approved these changes

Assignees

@sim642 sim642

Labels
cleanup Refactoring, clean-up feature type-safety Type-safety improvements
Projects
None yet
Milestone
v2.0.0
Development

Successfully merging this pull request may close these issues.

Replace labeled string based access partitioning with a richer type-safe one
2 participants
@sim642 @michael-schwarz