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.

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

Extract MHP analysis, simplify printing in race output #595

Merged
merged 5 commits into from
Feb 16, 2022

Conversation

sim642
Copy link
Member

@sim642 sim642 commented Feb 15, 2022

Closes #571. Closes #552.

Changes

  1. Extracts the MHP component of accesses to be provided by a separately activated mhp analysis, as suggested by Configuration of access collecting precision and performance #571 (comment). That analysis does nothing on its own, but just provides the more precise MHP component to accesses using data queried from other analyses.
  2. The mhp analysis now needs to be explicitly enabled, it's not activated by default, because it's not clear whether its worth doing on most benchmarks where there are other bigger sources of imprecision. It's now easy to experiment either way and if useful for a benchmark, add a conf file. The few tests for MHP races now explicitly activate it.
  3. History thread ID prefixes are now "unreversed", so previous [t1, main] is shown as [main, t1]. The reversed order is an internal optimization which could be misleading compared to the relational traces paper.
  4. History thread ID sets are omitted when empty, so previous ([t1, main], {}) is shown as [main, t1].
  5. If created or must_joined components of MHP are empty, they are omitted for clarity.

@sim642 sim642 added usability precision performance Analysis time, memory usage labels Feb 15, 2022
@michael-schwarz
Copy link
Member

It makes sense to have it configurable... What strikes me as odd though is that in the default setting we now compute the expensive thread ids, only to then not really use them.

This seems strange, so I'd suggest we enable this by default.

@sim642
Copy link
Member Author

sim642 commented Feb 15, 2022

That's true... I guess my point is even a bit broader and orthogonal then because history thread IDs aren't used by default analyses and privatizations either. So maybe all the bigger benchmarking should start with the cheaper old thread IDs.

I suppose I could just add mhp to default analyses then still.

Copy link
Member

@michael-schwarz michael-schwarz left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think the changes where we add the mhp analysis to regression tests can be reverted, as it is now part of the defaults, right?

@sim642
Copy link
Member Author

sim642 commented Feb 16, 2022

I think the changes where we add the mhp analysis to regression tests can be reverted, as it is now part of the defaults, right?

Could be, but the test suite is more robust this way when the feature under test is made explicit. Otherwise changes in the defaults could cause tests to fail, just because there's an implicit assumption about what the defaults are, not that disabling mhp is an unsoundness problem or something.

@michael-schwarz
Copy link
Member

Could be, but the test suite is more robust this way when the feature under test is made explicit. Otherwise changes in the defaults could cause tests to fail, just because there's an implicit assumption about what the defaults are, not that disabling mhp is an unsoundness problem or something.

That's to some extent a departure from what we've been doing for other tests, but I guess it makes sense here.

@michael-schwarz michael-schwarz merged commit a0bb640 into master Feb 16, 2022
@michael-schwarz michael-schwarz deleted the mhp-analysis branch February 16, 2022 09:25
@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
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 added a commit to sim642/opam-repository that referenced this pull request Aug 18, 2022
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
Labels
performance Analysis time, memory usage precision usability
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Configuration of access collecting precision and performance User-friendly output of thread IDs and MHP
2 participants