Skip to content

Group racing accesses into disjoint components#551

Merged
sim642 merged 5 commits intomasterfrom
group-accesses
Jan 21, 2022
Merged

Group racing accesses into disjoint components#551
sim642 merged 5 commits intomasterfrom
group-accesses

Conversation

@sim642
Copy link
Copy Markdown
Member

@sim642 sim642 commented Jan 20, 2022

Accesses of a single location are grouped into disjoint components, i.e. connected components in the graph of accesses with may_race edges).
This doesn't strictly improve precision, because all the same accesses are still printed, but it improves the precision and usability of the output by making it clearer, which accesses cannot race with which.
It makes sense to expose this information because the pairwise race checking internally knows (only previously only implicitly).

Example

In the added test tests/regression/10-synch/05-two_unique_two_lock.c.

Before

All accesses are printed under one warning.

[Warning][Race] Memory location myglobal@05-two_unique_two_lock.c:5:5-5:13 (race with conf. 110):
  write with [lock:{A}, thread * mhp:(([f1@tests/regression/10-synch/05-two_unique_two_lock.c:31:3-31:37, main], {}), ...)] (conf. 110)  (exp: & myglobal) (tests/regression/10-synch/05-two_unique_two_lock.c:11:3-11:13)
  write with [lock:{B}, thread * mhp:(([f1@tests/regression/10-synch/05-two_unique_two_lock.c:31:3-31:37, main], {}), ...)] (conf. 110)  (exp: & myglobal) (tests/regression/10-synch/05-two_unique_two_lock.c:14:3-14:13)
  write with [lock:{A}, thread * mhp:(([f2@tests/regression/10-synch/05-two_unique_two_lock.c:32:3-32:37, main], {}), ...)] (conf. 110)  (exp: & myglobal) (tests/regression/10-synch/05-two_unique_two_lock.c:21:3-21:13)
  write with [lock:{B}, thread * mhp:(([f2@tests/regression/10-synch/05-two_unique_two_lock.c:32:3-32:37, main], {}), ...)] (conf. 110)  (exp: & myglobal) (tests/regression/10-synch/05-two_unique_two_lock.c:24:3-24:13)

After

Accesses are printed under two different warnings for the same location such that the two racing components have no races between each other, only internally:

[Warning][Race] Memory location myglobal@05-two_unique_two_lock.c:5:5-5:13 (race with conf. 110):
  write with [lock:{B}, thread * mhp:(([f1@tests/regression/10-synch/05-two_unique_two_lock.c:31:3-31:37, main], {}), ...)] (conf. 110)  (exp: & myglobal) (tests/regression/10-synch/05-two_unique_two_lock.c:14:3-14:13)
  write with [lock:{A}, thread * mhp:(([f2@tests/regression/10-synch/05-two_unique_two_lock.c:32:3-32:37, main], {}), ...)] (conf. 110)  (exp: & myglobal) (tests/regression/10-synch/05-two_unique_two_lock.c:21:3-21:13)

[Warning][Race] Memory location myglobal@05-two_unique_two_lock.c:5:5-5:13 (race with conf. 110):
  write with [lock:{A}, thread * mhp:(([f1@tests/regression/10-synch/05-two_unique_two_lock.c:31:3-31:37, main], {}), ...)] (conf. 110)  (exp: & myglobal) (tests/regression/10-synch/05-two_unique_two_lock.c:11:3-11:13)
  write with [lock:{B}, thread * mhp:(([f2@tests/regression/10-synch/05-two_unique_two_lock.c:32:3-32:37, main], {}), ...)] (conf. 110)  (exp: & myglobal) (tests/regression/10-synch/05-two_unique_two_lock.c:24:3-24:13)

@sim642 sim642 merged commit dca6188 into master Jan 21, 2022
@sim642 sim642 deleted the group-accesses branch January 21, 2022 15:39
@sim642 sim642 mentioned this pull request Jan 27, 2022
Closed
@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

No one assigned

Labels

precision usability

Projects

None yet

Milestone

v2.0.0

Development

Successfully merging this pull request may close these issues.

2 participants

@sim642 @michael-schwarz