Skip to content

[Thesis MS] More useful stats output by privPrecCompare#1431

Merged
michael-schwarz merged 2 commits intomichael-schwarz-dissertationfrom
prec_compare_buckets
Apr 24, 2024
Merged

[Thesis MS] More useful stats output by privPrecCompare#1431
michael-schwarz merged 2 commits intomichael-schwarz-dissertationfrom
prec_compare_buckets

Conversation

@michael-schwarz
Copy link
Copy Markdown
Member

Creates list of buckets and boils down comparisons to per-bucket comparisons.

@michael-schwarz michael-schwarz merged commit ba4272d into michael-schwarz-dissertation Apr 24, 2024
@michael-schwarz michael-schwarz deleted the prec_compare_buckets branch April 24, 2024 08:29
@sim642
Copy link
Copy Markdown
Member

sim642 commented Apr 25, 2024

Can you explain in what way has the output changed over time and why the buckets are needed? I don't recall privPrecCompare being changed.

@michael-schwarz
Copy link
Copy Markdown
Member Author

The output has not changed over time. However, I am now considering many different configurations, and the pairwise output gets tedious:

protection equal to mine-W    (equal: 427, more precise: 0, less precise: 0, incomparable: 0, total: 427)
protection equal to lock    (equal: 427, more precise: 0, less precise: 0, incomparable: 0, total: 427)
protection equal to write    (equal: 427, more precise: 0, less precise: 0, incomparable: 0, total: 427)
protection equal to write+lock    (equal: 427, more precise: 0, less precise: 0, incomparable: 0, total: 427)
protection less precise than protection-interval    (equal: 51, more precise: 0, less precise: 376, incomparable: 0, total: 427)
protection less precise than mine-W-interval    (equal: 51, more precise: 0, less precise: 376, incomparable: 0, total: 427)
protection less precise than lock-interval    (equal: 51, more precise: 0, less precise: 376, incomparable: 0, total: 427)
protection less precise than write-interval    (equal: 51, more precise: 0, less precise: 376, incomparable: 0, total: 427)
protection less precise than write+lock-interval    (equal: 51, more precise: 0, less precise: 376, incomparable: 0, total: 427)
protection equal to protection-tid    (equal: 427, more precise: 0, less precise: 0, incomparable: 0, total: 427)
protection equal to lock-tid    (equal: 427, more precise: 0, less precise: 0, incomparable: 0, total: 427)
protection equal to write-tid    (equal: 427, more precise: 0, less precise: 0, incomparable: 0, total: 427)
protection equal to write+lock-tid    (equal: 427, more precise: 0, less precise: 0, incomparable: 0, total: 427)
protection less precise than protection-tid-interval    (equal: 51, more precise: 0, less precise: 376, incomparable: 0, total: 427)
protection less precise than lock-tid-interval    (equal: 51, more precise: 0, less precise: 376, incomparable: 0, total: 427)
protection less precise than write-tid-interval    (equal: 51, more precise: 0, less precise: 376, incomparable: 0, total: 427)
protection less precise than write+lock-tid-interval    (equal: 51, more precise: 0, less precise: 376, incomparable: 0, total: 427)
...

I have 18 configurations and thus 288 more pairwise comparisons like this (where many have equal precision).

With this PR, we still create the detailed output, but then at the end create buckets of approaches that have the same precision and then output one comparison per bucket.

For example, this output here (all approaches equally precise, TIDs do not matter, intervals pay off) is much easier to intuitively grasp than the 306 pairwise comparisons.

Bucket 0:
  protection-tid
  write
  write+lock-tid
  write+lock
  write-tid
  protection
  mine-W
  lock
  lock-tid
Bucket 1:
  write-interval
  lock-tid-interval
  write-tid-interval
  protection-interval
  mine-W-interval
  protection-tid-interval
  lock-interval
  write+lock-interval
  write+lock-tid-interval
Comparison between bucket 0 and 1: lock less precise than write+lock-tid-interval    (equal: 51, more precise: 0, less precise: 376, incomparable: 0, total: 427)

I merged this only into my dissertation branch for now, but wanted to have a PR we can refer to do decide if we want to merge this also into master.

@sim642
Copy link
Copy Markdown
Member

sim642 commented Apr 25, 2024

This looks more human-readable indeed. It might be worth considering to port it into Goblint (possibly with slight generalization for all of our compare business).

@sim642 sim642 added this to the v2.4.0 milestone Jul 24, 2024
@michael-schwarz michael-schwarz changed the title More useful stats output by privPrecCompare [Thesis MS] More useful stats output by privPrecCompare Dec 17, 2024
@michael-schwarz michael-schwarz removed this from the v2.4.0 milestone Dec 17, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants