Skip to content

Optimize MCP by removing assoc usage#578

Merged
sim642 merged 20 commits intomasterfrom
mcp-no-assoc
Feb 1, 2022
Merged

Optimize MCP by removing assoc usage#578
sim642 merged 20 commits intomasterfrom
mcp-no-assoc

Conversation

@sim642
Copy link
Copy Markdown
Member

@sim642 sim642 commented Jan 28, 2022 •
edited
Loading

Changes

  1. Change presub and postsub from eagerly constructed assoc lists to lazy functions. This avoids the expensive (~5% of total runtime) filter_presubs, which constructed those lists for each transfer function, but they aren't even used by anything other than ARINC and OSEK. This slowdown was my original motivation for getting rid of these (Remove unmaintained features #460), but now that they aren't slowing down the usual analyses, they're not so much of a problem.
  2. Reimplement unop_fold and binop_fold of MCP's Printable and Lattice using fold_left2 and fold_left3 respectively, by folding the domain elements simultaneously with the list of activated analysis Specs. This avoids any assoc in those operations. To avoid nasty segfaults, there are assertions to check that the component IDs still match up.
  3. Reimplement MCP's combine and threadspawn by folding over both domain elements (and optional contexts) simultaneously.
  4. Replace MCPRegistry global assoc lists with Hashtbls for faster lookup where still needed.

TODO

  • Benchmark.
  • Figure out what Gobview needs the old MCP.analyses_table for, which was just a list of (analysis ID, analysis name) pairs.

sim642 added 15 commits January 27, 2022 16:43
@sim642
Optimize MCP binop_fold by avoiding assoc (issue #572)
08b580d
@sim642
Remove unnecessary length check from MCP binop_fold
5592fea
@sim642
Optimize presub and postsub by making them lazy functions (issue #572)
4257804
@sim642
Optimize MCP assoc_sub by not constructing dep list (issue #572)
499bab2
@sim642
Remove unnecessary argument from MCP assoc_sub
0ee4904
@sim642
Optimize MCP unop_fold by avoiding assoc_dom (issue #572)
5ae1a8d
@sim642
Fix MCPAccess.A
153b409
@sim642
Optimize MCP binop_fold by avoiding assoc_dom (issue #572)
15f6652
@sim642
Fix MCP context assert failure due to ctx_insens
2399262
@sim642
Extract MCPRegistry.find_spec_name
bef2062
@sim642
Replace MCPRegistry assoc lists with Hashtbl
a165e26
@sim642
Avoid assoc in MCP do_emits and threadspawn
a20723d
@sim642
Avoid assoc in MCP combine
c696758
@sim642
Rename MCPRegistry analyses_list -> activated
b9f95c2
@sim642
Use List.iter2 in MCP.init
e471906
@sim642 sim642 added cleanup Refactoring, clean-up performance Analysis time, memory usage labels Jan 28, 2022
@sim642 sim642 linked an issue Jan 28, 2022 that may be closed by this pull request
Optimize MCP assoc lists #572
Closed
@michael-schwarz michael-schwarz self-requested a review January 28, 2022 09:50
@michael-schwarz
Copy link
Copy Markdown
Member

michael-schwarz commented Jan 28, 2022

Figure out what Gobview needs the old MCP.analyses_table for, which was just a list of (analysis ID, analysis name) pairs.

Can you shed some light on that @keremc?

michael-schwarz
michael-schwarz reviewed Jan 28, 2022
View reviewed changes
michael-schwarz
michael-schwarz reviewed Jan 28, 2022
View reviewed changes
@sim642 sim642 mentioned this pull request Jan 28, 2022
Merged
1 task
@sim642
Copy link
Copy Markdown
Member Author

sim642 commented Jan 28, 2022

I'm still running sv-benchmarks, but here's ypbind_comb.c analysis times.

Before

TOTAL                           8.226 s
  parse                           0.055 s
  convert to CIL                  0.028 s
  analysis                        8.144 s
    global_inits                    0.002 s
    solving                         7.453 s
      S.Dom.equal                     0.027 s
      postsolver                      1.815 s
        access compare                  0.055 s
    warn_global                     0.669 s
      access                          0.668 s
        group_may_race                  0.613 s
          bfs                             0.613 s
            access compare                  0.330 s
            may_race                        0.109 s
        may_race                        0.001 s
        access compare                  0.004 s

After

TOTAL                           7.699 s
  parse                           0.054 s
  convert to CIL                  0.026 s
  analysis                        7.620 s
    global_inits                    0.002 s
    solving                         7.074 s
      S.Dom.equal                     0.026 s
      postsolver                      1.774 s
        access compare                  0.056 s
    warn_global                     0.521 s
      access                          0.520 s
        group_may_race                  0.459 s
          bfs                             0.458 s
            access compare                  0.234 s
            may_race                        0.078 s
        may_race                        0.001 s
        access compare                  0.004 s

@sim642
Copy link
Copy Markdown
Member Author

sim642 commented Jan 28, 2022

Here's the before vs after runtime on sv-benchmarks:
image
Full results table

That's a whopping ~19% improvement on average!

@sim642
Copy link
Copy Markdown
Member Author

sim642 commented Jan 31, 2022

I think I managed to make the Gobview adaptation. Function entry/return states and global states at least display correctly, statement nodes for some reason don't, but it's already that way on master: goblint/gobview#6.

@sim642 sim642 merged commit 86ba130 into master Feb 1, 2022
@sim642 sim642 deleted the mcp-no-assoc branch February 1, 2022 08:46
@keremc
Copy link
Copy Markdown
Contributor

keremc commented Feb 1, 2022

@michael-schwarz I don't know if this still holds, but I think the analysis ID used to be just an incremental ID and depended on the module initialization order. As a result, the ID was not stable across native and JS platforms, so I used MCP.analyses_table to reorder the analysis modules and reassign the IDs. At some point, the IDs ended up becoming stable across platforms somehow (maybe because of the -linkall flag), but I didn't remove the code for reordering.

@michael-schwarz
Copy link
Copy Markdown
Member

michael-schwarz commented Feb 1, 2022

Does goblint/gobview@3acd89c...d0d5b06#diff-22c5afd13651a2ae673bd24ed0234d0b09f51d2ede9fd99236875dbc8715fd73 sufficienlty address this issue then? At least at first glance, it seems like it. Or would we need more code for that?

@sim642
Copy link
Copy Markdown
Member Author

sim642 commented Feb 1, 2022

It's possible that #455 made that more consistent between native and JS builds. Anyway, my Gobview patch seemed to work as much as it could. And the reordering code is much shorter because there are fewer data structures to reorder.

@sim642 sim642 added this to the v2.0.0 milestone Aug 12, 2022
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 left review comments

Assignees

No one assigned

Labels

cleanup Refactoring, clean-up performance Analysis time, memory usage

Projects

None yet

Milestone

v2.0.0

Development

Successfully merging this pull request may close these issues.

Optimize MCP assoc lists

3 participants

@sim642 @michael-schwarz @keremc